From 8c0dc84883db818efb2565d6f83b7a8e3b066ca5 Mon Sep 17 00:00:00 2001 From: brendanzab Date: Fri, 9 Sep 2022 13:19:00 +1000 Subject: [PATCH] Add field syntax for inductive-recursive reps --- .../src/Fathom/Closed/InductiveRecursive.idr | 30 +++++++++++-------- .../Closed/InductiveRecursiveCustom.idr | 30 +++++++++++-------- experiments/idris/src/Playground.idr | 12 ++++---- .../OpenType/InductiveRecursive.idr | 2 +- 4 files changed, 43 insertions(+), 31 deletions(-) diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr index 61ab87165..742da2f20 100644 --- a/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr +++ b/experiments/idris/src/Fathom/Closed/InductiveRecursive.idr @@ -45,9 +45,9 @@ mutual End : Format Fail : Format Pure : {0 A : Type} -> A -> Format - Ignore : (f : Format) -> (def : Rep f) -> Format + Ignore : (f : Format) -> (def : f.Rep) -> Format Repeat : Nat -> Format -> Format - Bind : (f : Format) -> (Rep f -> Format) -> Format + Bind : (f : Format) -> (f.Rep -> Format) -> Format ||| The in-memory representation of format descriptions @@ -56,9 +56,15 @@ mutual Rep End = Unit Rep Fail = Void Rep (Ignore _ _) = Unit - Rep (Repeat len f) = Vect len (Rep f) + Rep (Repeat len f) = Vect len f.Rep Rep (Pure x) = Sing x - Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x)) + Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep) + + + ||| Field syntax for representations + public export + (.Rep) : Format -> Type + (.Rep) = Rep namespace Format @@ -70,7 +76,7 @@ namespace Format pure = Pure public export - (>>=) : (f : Format) -> (Rep f -> Format) -> Format + (>>=) : (f : Format) -> (f.Rep -> Format) -> Format (>>=) = Bind @@ -80,7 +86,7 @@ namespace Format export - decode : (f : Format) -> DecodePart (Rep f) (Colist a) + decode : (f : Format) -> DecodePart f.Rep (Colist a) decode End = \case [] => Just ((), []) (_::_) => Nothing @@ -99,7 +105,7 @@ namespace Format export - encode : (f : Format) -> Encode (Rep f) (Colist a) + encode : (f : Format) -> Encode f.Rep (Colist a) encode End () = pure [] encode (Pure x) (MkSing _) = pure [] encode (Ignore f def) () = encode f def @@ -118,7 +124,7 @@ namespace Format ||| A format description refined with a fixed representation public export data FormatOf : (A : Type) -> Type where - MkFormatOf : (f : Format) -> FormatOf (Rep f) + MkFormatOf : (f : Format) -> FormatOf f.Rep namespace FormatOf @@ -139,14 +145,14 @@ namespace FormatOf namespace Format public export - toFormatOf : (f : Format) -> FormatOf (Rep f) + toFormatOf : (f : Format) -> FormatOf f.Rep toFormatOf f = MkFormatOf f ||| Convert a format description into an indexed format description with an ||| equality proof that the representation is the same as the index. public export - toFormatOfEq : {0 A : Type} -> (Subset Format (\f => Rep f = A)) -> FormatOf A + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f @@ -160,7 +166,7 @@ namespace FormatOf ||| Convert an indexed format description to a existential format description, ||| along with a proof that the representation is the same as the index. public export - toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => Rep f = A)) + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) toFormatEq (MkFormatOf f) = Element f Refl @@ -175,7 +181,7 @@ toFormatOfIso = MkIso public export -toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => Rep f = a)))) (Exists FormatOf) +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) toFormatOfEqIso = MkIso { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) , from = \(Evidence _ f) => Evidence _ (toFormatEq f) diff --git a/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr index 7aee799b7..4e676a3bd 100644 --- a/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr +++ b/experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr @@ -39,9 +39,9 @@ mutual End : Format Fail : Format Pure : {0 A : Type} -> A -> Format - Ignore : (f : Format) -> (def : Rep f) -> Format + Ignore : (f : Format) -> (def : f.Rep) -> Format Repeat : Nat -> Format -> Format - Bind : (f : Format) -> (Rep f -> Format) -> Format + Bind : (f : Format) -> (f.Rep -> Format) -> Format Custom : (f : CustomFormat) -> Format @@ -51,12 +51,18 @@ mutual Rep End = Unit Rep Fail = Void Rep (Ignore _ _) = Unit - Rep (Repeat len f) = Vect len (Rep f) + Rep (Repeat len f) = Vect len f.Rep Rep (Pure x) = Sing x - Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x)) + Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep) Rep (Custom f) = f.Rep + ||| Field syntax for representations + public export + (.Rep) : Format -> Type + (.Rep) = Rep + + namespace Format -- Support for do notation @@ -66,7 +72,7 @@ namespace Format pure = Pure public export - (>>=) : (f : Format) -> (Rep f -> Format) -> Format + (>>=) : (f : Format) -> (f.Rep -> Format) -> Format (>>=) = Bind @@ -76,7 +82,7 @@ namespace Format export - decode : (f : Format) -> DecodePart (Rep f) ByteStream + decode : (f : Format) -> DecodePart f.Rep ByteStream decode End = \case [] => Just ((), []) (_::_) => Nothing @@ -96,7 +102,7 @@ namespace Format export - encode : (f : Format) -> Encode (Rep f) ByteStream + encode : (f : Format) -> Encode f.Rep ByteStream encode End () = pure [] encode (Pure x) (MkSing _) = pure [] encode (Ignore f def) () = encode f def @@ -148,7 +154,7 @@ namespace Format ||| A format description indexed with a fixed representation public export data FormatOf : (Rep : Type) -> Type where - MkFormatOf : (f : Format) -> FormatOf (Rep f) + MkFormatOf : (f : Format) -> FormatOf f.Rep namespace FormatOf @@ -169,14 +175,14 @@ namespace FormatOf namespace Format public export - toFormatOf : (f : Format) -> FormatOf (Rep f) + toFormatOf : (f : Format) -> FormatOf f.Rep toFormatOf f = MkFormatOf f ||| Convert a format description into an indexed format description with an ||| equality proof that the representation is the same as the index. public export - toFormatOfEq : {0 A : Type} -> (Subset Format (\f => Rep f = A)) -> FormatOf A + toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A toFormatOfEq (Element f prf) = rewrite sym prf in MkFormatOf f @@ -190,7 +196,7 @@ namespace FormatOf ||| Convert an indexed format description to a existential format description, ||| along with a proof that the representation is the same as the index. public export - toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => Rep f = A)) + toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A)) toFormatEq (MkFormatOf f) = Element f Refl @@ -205,7 +211,7 @@ toFormatOfIso = MkIso public export -toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => Rep f = a)))) (Exists FormatOf) +toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf) toFormatOfEqIso = MkIso { to = \(Evidence _ f) => Evidence _ (toFormatOfEq f) , from = \(Evidence _ f) => Evidence _ (toFormatEq f) diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr index eedee36f1..1f6dd96b1 100644 --- a/experiments/idris/src/Playground.idr +++ b/experiments/idris/src/Playground.idr @@ -18,7 +18,7 @@ import Fathom.Open.Record as Record public export format : IndRec.Format -> Record.Format format f = Record.MkFormat - { Rep = Rep f + { Rep = f.Rep , decode = decode f , encode = encode f } @@ -64,7 +64,7 @@ formatOf f = Record.MkFormat ||| Convert an inductive-recursive format description to an indexed format -indRecToIndexed : (f : IndRec.Format) -> Indexed.FormatOf (Rep f) +indRecToIndexed : (f : IndRec.Format) -> Indexed.FormatOf f.Rep indRecToIndexed End = Indexed.End indRecToIndexed Fail = Indexed.Fail indRecToIndexed (Pure x) = Indexed.Pure x @@ -76,7 +76,7 @@ indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToInd mutual ||| Convert an indexed format description to an inductive-recursive format - indexedToIndRecFormat : (f : Indexed.Format) -> (f' : IndRec.Format ** Rep f = Rep f') + indexedToIndRecFormat : (f : Indexed.Format) -> (f' : IndRec.Format ** f.Rep = f'.Rep) indexedToIndRecFormat (MkFormat () End) = (End ** Refl) indexedToIndRecFormat (MkFormat Void Fail) = (Fail ** Refl) indexedToIndRecFormat (MkFormat (Sing x) (Pure x)) = (Pure x ** Refl) @@ -150,8 +150,8 @@ mutual -- indexedToIndRec (Bind _ f2) | MkFormatOf f1 = -- let -- bindF1 = Bind f1 --- bodyF2 : x : Rep f1 -> FormatOf () --- bodyF2 = x : Rep f1 => +-- bodyF2 : x : f1.Rep -> FormatOf () +-- bodyF2 = x : f1.Rep => -- case sameRep (indexedToIndRec (f2 x)) of -- (f2' ** prf) => f2') -- in @@ -188,7 +188,7 @@ mutual -- in -- -- f1 : Format -- -- 0 A : Type --- -- f2 : (x : Rep f1) -> FormatOf (B x) +-- -- f2 : (x : f1.Rep) -> FormatOf (B x) -- -- ------------------------------ -- -- todo_indexedToIndRec : FormatOf (DPair (Rep f1) (\x => B x)) -- ?todo_indexedToIndRec diff --git a/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr b/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr index e12fd0f23..5593e77a6 100644 --- a/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr +++ b/experiments/idris/src/Playground/OpenType/InductiveRecursive.idr @@ -25,7 +25,7 @@ namespace Format Pure () - (.repeat) : Rep Format.flag -> Nat + (.repeat) : Format.flag.Rep -> Nat (.repeat) (0 ** repeat ** _) = repeat (.repeat) (S _ ** repeat ** _) = val repeat