Get OpenType examples to work for all approaches

brendanzab · brendanzab · commit b5b4439c38fe · 2022-09-01T19:15:43.000+10:00
diff --git a/experiments/idris/src/Fathom/Closed/IndexedInductive.idr b/experiments/idris/src/Fathom/Closed/IndexedInductive.idr
@@ -164,17 +164,3 @@ toFormatOfEqIso = MkIso
   , toFrom = \(Evidence _ _) => Refl
   , fromTo = \(Evidence _ ((MkFormat _ _) ** Refl)) => Refl
   }
-
-
------------------
--- EXPERIMENTS --
------------------
-
-
-either : (cond : Bool) -> FormatOf a -> FormatOf b -> FormatOf (if cond then a else b)
-either True f1 _ = f1
-either False _ f2 = f2
-
-orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
-orPure True f _ = f
-orPure False _ def = Pure def
diff --git a/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr
@@ -10,6 +10,7 @@ import Data.Vect
 
 import Fathom.Base
 import Fathom.Data.Iso
+import Fathom.Data.Sing
 
 
 ---------------------------------
@@ -35,7 +36,7 @@ public export
 data FormatOf : (A : Type) -> Type where
   End : FormatOf Unit
   Fail : FormatOf Void
-  Pure : {0 A : Type} -> (x : A) -> FormatOf A
+  Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
   Skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
   Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
   Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
@@ -45,7 +46,7 @@ data FormatOf : (A : Type) -> Type where
 -- Support for do notation
 
 public export
-pure : {0 A : Type} -> (x : A) -> FormatOf A
+pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
 pure = Pure
 
 public export
@@ -64,7 +65,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (x, buffer)
+  Just (MkSing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -84,7 +85,7 @@ decode (Custom f) buffer = f.decode buffer
 export
 encode : {0 A : Type} -> (f : FormatOf A) -> Encode A (ByteStream)
 encode End () = Just []
-encode (Pure x) _ = Just []
+encode (Pure x) (MkSing _) = Just []
 encode (Skip f def) () = encode f def
 encode (Repeat Z f) [] = Just []
 encode (Repeat (S len) f) (x :: xs) =
@@ -194,24 +195,22 @@ u16Be = Custom (MkCustomFormat
 -- EXPERIMENTS --
 -----------------
 
-
-either : (cond : Bool) -> FormatOf a -> FormatOf b -> FormatOf (if cond then a else b)
-either True f1 _ = f1
-either False _ f2 = f2
-
-orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf a
-orPure True f _ = f
-orPure False _ def = Pure def
-
-
 -- Reproduction of difficulties in OpenType format
 
 
 Flag : Type
-Flag = (flag : Nat ** repeat : Nat ** ())
+Flag =
+  (  id : Nat
+  ** repeat :
+    case id of
+      0 => Nat
+      S n => Sing {A = Nat} 0
+  ** Sing ()
+  )
 
 (.repeat) : Flag -> Nat
-(.repeat) (_ ** repeat ** _) = repeat
+(.repeat) (0 ** repeat ** _) = repeat
+(.repeat) (S _ ** repeat ** _) = val repeat
 
 
 -- def flag = {
@@ -226,12 +225,15 @@ flag = do
   flag <- u8
   repeat <- case flag of
     0 => u8
-    _ => Pure {A = Nat} 0
+    S _ => Pure {A = Nat} 0
   Pure ()
 
 
 SimpleGlyph : Type
-SimpleGlyph = (flag : Flag ** Nat)
+SimpleGlyph =
+  (  flag : Flag
+  ** Sing (flag.repeat + 1)
+  )
 
 
 -- def simple_glyph = fun (number_of_contours : U16) => {
diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr
@@ -49,15 +49,6 @@ mutual
     Repeat : Nat -> Format -> Format
     Bind : (f : Format) -> (Rep f -> Format) -> Format
 
-    -- Questionable format descriptions
-    -- OrPure : (cond : Bool) -> (f : Format) -> (def : Rep f) -> Format
-    -- OfSing : (f : Format) -> Sing (Rep f) -> Format
-    -- OfEq : (f : Format) -> (r : Type) -> {auto 0 prf : Rep f = r} -> Format
-
-    -- Broken stuff
-    -- Let : (f : Format) -> (Rep f -> Format) -> Format
-    -- Custom : (f : Record.Format) -> Format
-
 
   ||| The in-memory representation of format descriptions
   public export
@@ -69,15 +60,6 @@ mutual
   Rep (Pure x) = Sing x
   Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x))
 
-  -- Questionable format descriptions
-  -- Rep (OrPure _ f _) = Rep f
-  -- Rep (OfSing f r) = value r
-  -- Rep (OfEq f r) = r
-
-  -- Broken stuff
-  -- Rep (Let f1 f2) = Rep (f2 ?halp)
-  -- Rep (Custom f) = f.Rep
-
 
 -- Support for do notation
 
@@ -187,19 +169,3 @@ toFormatOfEqIso = MkIso
   , toFrom = \(Evidence _ (MkFormatOf _)) => Refl
   , fromTo = \(Evidence _ (f ** Refl)) => Refl
   }
-export
-either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = MkFormatOf f1
-either False _ f2 = MkFormatOf f2
-
-
-public export
-orPure : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
-orPure True f _ = f
-orPure False _ def = MkFormatOf (Pure def)
-
-
-public export
-orPure' : (cond : Bool) -> FormatOf a -> (def : a) -> FormatOf (if cond then a else Sing def)
-orPure' True f _ = f
-orPure' False _ def = MkFormatOf (Pure def)
diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr
@@ -12,6 +12,7 @@ import Data.Vect
 import Fathom.Base
 import Fathom.Data.Iso
 import Fathom.Data.Refine
+import Fathom.Data.Sing
 
 
 public export
@@ -43,7 +44,7 @@ mutual
   data Format : Type where
     End : Format
     Fail : Format
-    Pure : {A : Type} -> A -> Format
+    Pure : {0 A : Type} -> A -> Format
     Skip : (f : Format) -> (def : Rep f) -> Format
     Repeat : Nat -> Format -> Format
     Bind : (f : Format) -> (Rep f -> Format) -> Format
@@ -57,7 +58,7 @@ mutual
   Rep Fail = Void
   Rep (Skip _ _) = Unit
   Rep (Repeat len f) = Vect len (Rep f)
-  Rep (Pure x) = typeOf x
+  Rep (Pure x) = Sing x
   Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x))
   Rep (Custom f) = f.Rep
 
@@ -73,7 +74,7 @@ decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing
 decode (Pure x) buffer =
-  Just (x, buffer)
+  Just (MkSing x, buffer)
 decode (Skip f _) buffer = do
   (x, buffer') <- decode f buffer
   Just ((), buffer')
@@ -93,7 +94,7 @@ decode (Custom f) buffer = f.decode buffer
 export
 encode : (f : Format) -> Encode (Rep f) ByteStream
 encode End () = Just []
-encode (Pure x) _ = Just []
+encode (Pure x) (MkSing _) = Just []
 encode (Skip f def) () = encode f def
 encode (Repeat Z f) [] = Just []
 encode (Repeat (S len) f) (x :: xs) =
@@ -110,7 +111,7 @@ encode (Custom f) x = f.encode x
 -- Support for do notation
 
 public export
-pure : {A : Type} -> A -> Format
+pure : {0 A : Type} -> A -> Format
 pure = Pure
 
 public export
@@ -214,25 +215,6 @@ toFormatOfEqIso = MkIso
 -- EXPERIMENTS --
 -----------------
 
-
-export
-either : (cond : Bool) -> (f1 : Format) -> (f2 : Format) -> FormatOf (if cond then Rep f1 else Rep f2)
-either True f1 _ = MkFormatOf f1
-either False _ f2 = MkFormatOf f2
-
-
-export
-orPure : {A : Type} -> (cond : Bool) -> FormatOf A -> (def : A) -> FormatOf A
-orPure True f _ = f
-orPure False _ def = MkFormatOf (Pure def)
-
-
-export
-orPure' : {A : Type} -> (cond : Bool) -> FormatOf A -> (def : A) -> FormatOf A
-orPure' True f _ = f
-orPure' False _ def = MkFormatOf (Pure def)
-
-
 -- Reproduction of difficulties in OpenType format
 
 -- def flag = {
@@ -244,23 +226,24 @@ orPure' False _ def = MkFormatOf (Pure def)
 -- };
 flag : Format
 flag = do
-  flag <- u8
-  repeat <- case flag of
+  id <- u8
+  repeat <- case id of
     0 => u8
-    _ => Pure {A = Nat} 0
+    S n => Pure {A = Nat} 0
   Pure ()
 
+
 -- def simple_glyph = fun (number_of_contours : U16) => {
 --     ...
 --     let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
 --     ...
 -- };
 simple_glyph : Format
 simple_glyph = do
-  (flag ** repeat ** ()) <- flag
+  flag <- flag
   let
-    repeat' : Nat
-    repeat' = case flag of
-      0 => repeat
-      repeat => ?todo_repeat
-  Pure (repeat' + 1)
+    repeat : Nat
+    repeat = case flag of
+      (0 ** repeat ** MkSing ()) => repeat
+      (S n ** repeat ** MkSing ()) => repeat
+  Pure (repeat + 1)
diff --git a/experiments/idris/src/Fathom/Open/Record.idr b/experiments/idris/src/Fathom/Open/Record.idr
@@ -182,25 +182,65 @@ public export
 public export
 u8 : Format
 u8 = MkFormat
-  { Rep = Bits8
-  , decode = decodeU8
-  , encode = encodeU8
+  { Rep = Nat
+  , decode = map cast decodeU8
+  , encode = encodeU8 . cast {to = Bits8}
   }
 
 
 public export
 u16Le : Format
 u16Le = MkFormat
-  { Rep = Bits16
-  , decode = decodeU16 LE
-  , encode = encodeU16 LE
+  { Rep = Nat
+  , decode = map cast (decodeU16 LE)
+  , encode = encodeU16 LE . cast {to = Bits16}
   }
 
 
 public export
 u16Be : Format
 u16Be = MkFormat
-  { Rep = Bits16
-  , decode = decodeU16 BE
-  , encode = encodeU16 BE
+  { Rep = Nat
+  , decode = map cast (decodeU16 BE)
+  , encode = encodeU16 BE . cast {to = Bits16}
   }
+
+
+-----------------
+-- EXPERIMENTS --
+-----------------
+
+
+-- Reproduction of difficulties in OpenType format
+
+
+-- def flag = {
+--     flag <- u8,
+--     repeat <- match ((u8_and flag 8) != (0 : U8)) {
+--       true => u8,
+--       false => succeed U8 0,
+--     },
+-- };
+flag : Format
+flag = do
+  id <- u8
+  repeat <- case id of
+    0 => u8
+    S _ => pure {A = Nat} 0
+  pure ()
+
+
+(.repeat) : Record.flag.Rep -> Nat
+(.repeat) (0 ** repeat ** _) = repeat
+(.repeat) (S _ ** repeat ** _) = val repeat
+
+
+-- def simple_glyph = fun (number_of_contours : U16) => {
+--     ...
+--     let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
+--     ...
+-- };
+simple_glyph : Format
+simple_glyph = do
+  flag <- flag
+  pure (flag.repeat + 1)
diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr
@@ -101,3 +101,25 @@ mutual
   indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1)
     _ | MkFormatOf f1' =
       ?indexedToIndRecFormatOfBind
+
+
+-- Reproduction of difficulties in OpenType format, drawing parallels to
+-- Tarski-style universes.
+
+repeatWithId : Nat -> Type
+repeatWithId 0 = Nat
+repeatWithId (S _) = Sing {A = Nat} 0
+
+record Flag where
+  constructor MkFlag
+  id : Nat
+  repeat : case id of
+    0 => Nat
+    (S n) => Sing {A = Nat} 0
+
+record SimpleGlyph where
+  constructor MkSimpleGlyph
+  flag : Flag
+  flag_repeat : Sing {A = Nat} (case flag of
+    MkFlag 0 repeat => repeat
+    MkFlag (S n) repeat => val repeat)
