Add u32 formats

Author: brendanzab

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

@@ -24,9 +24,8 @@ import Fathom.Data.Sing
 ||| bit temperamental and result in ambiguities when importing modules that
 ||| contain types of the same name as those defined in the current module.
 public export
-record CustomFormat where
-  constructor MkCustomFormat
-  Rep : Type
+record CustomFormatOf (Rep : Type) where
+  constructor MkCustomFormatOf
   decode : Decode (Rep, ByteStream) ByteStream
   encode : Encode Rep ByteStream
 
@@ -41,7 +40,7 @@ data FormatOf : (A : Type) -> Type where
   Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
   Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
   Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
-  Custom :  (f : CustomFormat) -> FormatOf f.Rep
+  Custom :  {0 A : Type} -> (f : CustomFormatOf A) -> FormatOf A
 
 
 namespace FormatOf
@@ -97,6 +96,51 @@ namespace FormatOf
   encode (Custom f) x = f.encode x
 
 
+  --------------------
+  -- CUSTOM FORMATS --
+  --------------------
+
+
+  public export
+  u8 : FormatOf Nat
+  u8 = Custom (MkCustomFormatOf
+    { decode = map cast decodeU8
+    , encode = encodeU8 . cast {to = Bits8}
+    })
+
+
+  public export
+  u16Le : FormatOf Nat
+  u16Le = Custom (MkCustomFormatOf
+    { decode = map cast (decodeU16 LE)
+    , encode = encodeU16 LE . cast {to = Bits16}
+    })
+
+
+  public export
+  u16Be : FormatOf Nat
+  u16Be = Custom (MkCustomFormatOf
+    { decode = map cast (decodeU16 BE)
+    , encode = encodeU16 BE . cast {to = Bits16}
+    })
+
+
+  public export
+  u32Le : FormatOf Nat
+  u32Le = Custom (MkCustomFormatOf
+    { decode = map cast (decodeU32 LE)
+    , encode = encodeU32 LE . cast {to = Bits32}
+    })
+
+
+  public export
+  u32Be : FormatOf Nat
+  u32Be = Custom (MkCustomFormatOf
+    { decode = map cast (decodeU32 BE)
+    , encode = encodeU32 BE . cast {to = Bits32}
+    })
+
+
 -------------------------
 -- FORMAT DESCRIPTIONS --
 -------------------------
@@ -224,35 +268,3 @@ namespace Format
   public export
   (>>=) : (f : Format) -> (Rep f -> Format) -> Format
   (>>=) = bind
-
-
---------------------
--- CUSTOM FORMATS --
---------------------
-
-
-public export
-u8 : FormatOf Nat
-u8 = Custom (MkCustomFormat
-  { Rep = Nat
-  , decode = map cast decodeU8
-  , encode = encodeU8 . cast {to = Bits8}
-  })
-
-
-public export
-u16Le : FormatOf Nat
-u16Le = Custom (MkCustomFormat
-  { Rep = Nat
-  , decode = map cast (decodeU16 LE)
-  , encode = encodeU16 LE . cast {to = Bits16}
-  })
-
-
-public export
-u16Be : FormatOf Nat
-u16Be = Custom (MkCustomFormat
-  { Rep = Nat
-  , decode = map cast (decodeU16 BE)
-  , encode = encodeU16 BE . cast {to = Bits16}
-  })

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

@@ -150,6 +150,24 @@ namespace Format
     })
 
 
+  public export
+  u32Le : Format
+  u32Le = Custom (MkCustomFormat
+    { Rep = Nat
+    , decode = map cast (decodeU32 LE)
+    , encode = encodeU32 LE . cast {to = Bits32}
+    })
+
+
+  public export
+  u32Be : Format
+  u32Be = Custom (MkCustomFormat
+    { Rep = Nat
+    , decode = map cast (decodeU32 BE)
+    , encode = encodeU32 BE . cast {to = Bits32}
+    })
+
+
 ---------------------------------
 -- INDEXED FORMAT DESCRIPTIONS --
 ---------------------------------

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

@@ -180,6 +180,24 @@ namespace Format
     }
 
 
+  public export
+  u32Le : Format
+  u32Le = MkFormat
+    { Rep = Nat
+    , decode = map cast (decodeU32 LE)
+    , encode = encodeU32 LE . cast {to = Bits32}
+    }
+
+
+  public export
+  u32Be : Format
+  u32Be = MkFormat
+    { Rep = Nat
+    , decode = map cast (decodeU32 BE)
+    , encode = encodeU32 BE . cast {to = Bits32}
+    }
+
+
 ---------------------------------
 -- INDEXED FORMAT DESCRIPTIONS --
 ---------------------------------