Try a different FormatOf representation

Author: brendanzab

experiments/idris/src/Fathom/Closed/IndexedInductive.idr

@@ -18,7 +18,7 @@ import Fathom.Data.Sing
 
 ||| Universe of format descriptions indexed by their machine representations
 public export
-data FormatOf : (0 Rep : Type) -> Type where
+data FormatOf : (0 A : Type) -> Type where
   End : FormatOf Unit
   Fail : FormatOf Void
   Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
@@ -42,8 +42,9 @@ public export
 -- ENCODER/DECODER PAIRS --
 ---------------------------
 
+
 export
-decode : {0 Rep : Type} -> (f : FormatOf Rep) -> Decode (Rep, Colist a) (Colist a)
+decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
 decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
@@ -65,7 +66,7 @@ decode (Bind f1 f2) buffer = do
 
 
 export
-encode : {0 Rep : Type} -> (f : FormatOf Rep) -> Encode Rep (Colist a)
+encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
 encode End () = Just []
 encode (Pure x) (MkSing _) = Just []
 encode (Skip f def) () = encode f def

experiments/idris/src/Fathom/Closed/InductiveRecursive.idr

@@ -27,7 +27,6 @@ import Data.Vect
 
 import Fathom.Base
 import Fathom.Data.Sing
-import Fathom.Data.Refine
 
 -- import Fathom.Open.Record
 
@@ -155,35 +154,32 @@ encode (Bind f1 f2) (x ** y) = do
 
 ||| A format description refined with a fixed representation
 public export
-FormatOf : (0 Rep : Type) -> Type
-FormatOf rep = Refine Format (\f => Rep f = rep)
-
-
-toFormatOf : (f : Format) -> FormatOf (Rep f)
-toFormatOf f = MkRefine f
+data FormatOf : (0 A : Type) -> Type where
+  MkFormatOf : (f : Format) -> FormatOf (Rep f)
 
 
 export
 either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = MkRefine f1
-either False _ f2 = MkRefine f2
+either True f1 _ = MkFormatOf f1
+either False _ f2 = MkFormatOf f2
 
 
-export
+public export
 orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure True f _ = f
-orPure False _ def = MkRefine (Pure def)
+orPure False _ def = MkFormatOf (Pure def)
 
 
-export
+public export
 orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure' True f _ = f
-orPure' False _ def = MkRefine (Pure def)
+orPure' False _ def = MkFormatOf (Pure def)
 
 
-foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
-foo cond f def = case orPure cond (toFormatOf f) def of
-  MkRefine f' {prf} =>
-    Bind f' (\x => case cond of
-      True => ?todo1
-      False => ?todo2)
+-- foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
+-- foo cond f def with (orPure cond (MkFormatOf f) def)
+--   foo True f def | MkFormatOf f' = ?help1
+--   foo False f def | MkFormatOf f' = ?help
+    -- Bind f' (\x => case cond of
+    --   True => ?todo1
+    --   False => ?todo2)

experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr

@@ -135,38 +135,38 @@ u8 = Custom (MkCustomFormat
 
 ||| A format description refined with a fixed representation
 public export
-FormatOf : (0 Rep : Type) -> Type
-FormatOf rep = Refine Format (\f => Rep f = rep)
+data FormatOf : (0 Rep : Type) -> Type where
+  MkFormatOf : (f : Format) -> FormatOf (Rep f)
 
 
 toFormatOf : (f : Format) -> FormatOf (Rep f)
-toFormatOf f = MkRefine f
+toFormatOf f = MkFormatOf f
 
 
 export
 either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = MkRefine f1
-either False _ f2 = MkRefine f2
+either True f1 _ = MkFormatOf f1
+either False _ f2 = MkFormatOf f2
 
 
 export
 orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure True f _ = f
-orPure False _ def = MkRefine (Pure def)
+orPure False _ def = MkFormatOf (Pure def)
 
 
 export
 orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
 orPure' True f _ = f
-orPure' False _ def = MkRefine (Pure def)
+orPure' False _ def = MkFormatOf (Pure def)
 
 
-foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
-foo cond f def = case orPure cond (toFormatOf f) def of
-  MkRefine f' {prf} =>
-    Bind f' (\x => case cond of
-      True => ?todo1
-      False => ?todo2)
+-- foo : (cond : Bool) -> (f : Format) -> Rep f -> Format
+-- foo cond f def = case orPure cond (MkFormatOf f) def of
+--   MkRefine f' {prf} =>
+--     Bind f' (\x => case cond of
+--       True => ?todo1
+--       False => ?todo2)
 
 
 -- Reproduction of difficulties in OpenType format

experiments/idris/src/Fathom/Open/Record.idr

@@ -15,7 +15,6 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
-import Fathom.Data.Refine
 import Fathom.Data.Sing
 
 
@@ -147,9 +146,5 @@ public export
 
 ||| A format description refined with a fixed representation
 public export
-FormatOf : (0 Rep : Type) -> Type
-FormatOf rep = Refine Format (\f => f.Rep = rep)
-
-
-toFormatOf : (f : Format) -> FormatOf f.Rep
-toFormatOf f = MkRefine f
+data FormatOf : (0 A : Type) -> Type where
+  MkFormatOf : (f : Format) -> FormatOf f.Rep