Add field syntax for inductive-recursive reps

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)

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)

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

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