Forwar encode/decode functions via wrapper formats

Author: brendanzab

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

@@ -96,6 +96,16 @@ record Format where
   format : FormatOf Rep
 
 
+namespace Format
+
+  decode : (f : Format) -> Decode (Rep f, Colist a) (Colist a)
+  decode f = FormatOf.decode f.format
+
+
+  encode : (f : Format) -> Encode (Rep f) (Colist a)
+  encode f = FormatOf.encode f.format
+
+
 ------------------------------------
 -- FORMAT DESCRIPTION CONVERSIONS --
 ------------------------------------

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

@@ -62,7 +62,7 @@ namespace FormatOf
 
 
   export
-  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) (ByteStream)
+  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
   decode End [] = Just ((), [])
   decode End (_::_) = Nothing
   decode Fail _ = Nothing
@@ -85,7 +85,7 @@ namespace FormatOf
 
 
   export
-  encode : {0 A : Type} -> (f : FormatOf A) -> Encode A (ByteStream)
+  encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
   encode End () = Just []
   encode (Pure x) (MkSing _) = Just []
   encode (Skip f def) () = encode f def
@@ -112,6 +112,16 @@ record Format where
   format : FormatOf Rep
 
 
+namespace Format
+
+  decode : (f : Format) -> Decode (Rep f, ByteStream) ByteStream
+  decode f = FormatOf.decode f.format
+
+
+  encode : (f : Format) -> Encode (Rep f) ByteStream
+  encode f = FormatOf.encode f.format
+
+
 ------------------------------------
 -- FORMAT DESCRIPTION CONVERSIONS --
 ------------------------------------

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

@@ -124,6 +124,16 @@ data FormatOf : (A : Type) -> Type where
   MkFormatOf : (f : Format) -> FormatOf (Rep f)
 
 
+namespace FormatOf
+
+  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
+  decode  (MkFormatOf f) = Format.decode f
+
+
+  encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
+  encode  (MkFormatOf f) = Format.encode f
+
+
 ------------------------------------
 -- FORMAT DESCRIPTION CONVERSIONS --
 ------------------------------------

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

@@ -159,6 +159,16 @@ data FormatOf : (Rep : Type) -> Type where
   MkFormatOf : (f : Format) -> FormatOf (Rep f)
 
 
+namespace FormatOf
+
+  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
+  decode  (MkFormatOf f) = Format.decode f
+
+
+  encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
+  encode  (MkFormatOf f) = Format.encode f
+
+
 ------------------------------------
 -- FORMAT DESCRIPTION CONVERSIONS --
 ------------------------------------

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

@@ -182,6 +182,16 @@ data FormatOf : (A : Type) -> Type where
   MkFormatOf : (f : Format) -> FormatOf f.Rep
 
 
+namespace FormatOf
+
+  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
+  decode  (MkFormatOf f) = Format.decode f
+
+
+  encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
+  encode  (MkFormatOf f) = Format.encode f
+
+
 ------------------------------------
 -- FORMAT DESCRIPTION CONVERSIONS --
 ------------------------------------