Experiment with bit and word definitions

Author: brendanzab

experiments/idris/fathom.ipkg

@@ -15,8 +15,10 @@ package fathom
 -- modules to install
 modules = Fathom
         , Fathom.Base
+        , Fathom.Data.Bit
         , Fathom.Data.Sing
         , Fathom.Data.Refine
+        , Fathom.Data.Word
         , Fathom.Closed.IndexedInductive
         , Fathom.Closed.InductiveRecursive
         , Fathom.Closed.InductiveRecursiveCustom

experiments/idris/src/Fathom/Data/Bit.idr

@@ -0,0 +1,71 @@
+||| Binary digits
+
+module Fathom.Data.Bit
+
+
+||| A binary digit
+public export
+data Bit : Type where
+  B0 : Bit
+  B1 : Bit
+
+
+public export
+Cast Bit Bool where
+  cast B0 = True
+  cast B1 = False
+
+public export
+Cast Bit Nat where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Int where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Integer where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Bits8 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Bits16 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Bits32 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Bits64 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Int8 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Int16 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Int32 where
+  cast B0 = 0
+  cast B1 = 1
+
+public export
+Cast Bit Int64 where
+  cast B0 = 0
+  cast B1 = 1

experiments/idris/src/Fathom/Data/Word.idr

@@ -0,0 +1,26 @@
+module Fathom.Data.Word
+
+
+import Data.Fin
+
+import Fathom.Data.Bit
+
+
+||| A binary word with a specified number of bits
+public export
+data Word : (0 size : Nat) -> Type where
+  Z : Word 0
+  S : Bit -> {0 n : Nat} -> Word n -> Word (S n)
+
+
+export
+Cast (Word size) Nat where
+  cast Z = 0
+  cast (S B0 w) = cast w * 2
+  cast (S B1 w) = S (cast w * 2)
+
+export
+Cast (Word size) Bits8 where
+  cast Z = 0
+  cast (S B0 w) = cast w * 2
+  cast (S B1 w) = (cast w * 2) + 1