KappaDemo.hs: add examples from hardware design paper

[coq-hetmet.git] / examples / KappaDemo.hs

diff --git a/examples/KappaDemo.hs b/examples/KappaDemo.hs
index f052012..a1831ef 100644 (file)
--- a/examples/KappaDemo.hs
+++ b/examples/KappaDemo.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types #-}
+{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
 module Demo (demo, demo2) where
 
 demo  z   = <{ \y -> ~~z }>
@@ -6,7 +6,83 @@ demo  z   = <{ \y -> ~~z }>
 demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
 demo2 x y = <{ ~~x ~~y }>
 
+swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
+swap f = <{ \x -> \y -> ~~f y x }>
+
+-- bad = <{ \f -> \x -> f x }>
+
 demo3 x y z q = <{ ~~q (~~x ~~y ~~z) }>
 
 
 
+class BitSerialHardwarePrimitives g where
+  type Wire
+
+  <[ not ]>    :: <[             (Wire,())    ~~> Wire ]>@g
+  <[ xor ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
+  <[ or  ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
+  <[ and ]>    :: <[       (Wire,(Wire,()))   ~~> Wire ]>@g
+  <[ mux2 ]>   :: <[ (Wire,(Wire,(Wire,())))  ~~> Wire ]>@g
+  <[ maj3 ]>   :: <[ (Wire,(Wire,(Wire,())))  ~~> Wire ]>@g
+  <[ reg ]>    :: <[             (Wire,())    ~~> Wire ]>@g
+  <[ zero ]>   :: <[             ()    ~~> Wire ]>@g
+  <[ one ]>    :: <[             ()    ~~> Wire ]>@g
+
+  loop   :: [Bool] -> <[ () ~~> Wire ]>@g
+  <[ lfsr ]>   :: Int ->  [ <[ Wire ]>@g ]
+  <[ adder ]>  :: <[  (Wire,(Wire,())) ~~> Wire ]>@g
+  fifo         :: Int -> <[  (Wire,()) ~~> Wire ]>@g
+
+  <[ probe ]>  :: Int -> <[ (Wire,())  ~~> Wire ]>@g
+  <[ oracle ]> :: Int -> <[                Wire ]>@g
+
+xor3 :: forall g . BitSerialHardwarePrimitives g => <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
+xor3 = <{ \x -> \y -> \z -> xor (xor x y) z }>
+
+adder =
+   <{ \in1 ->
+      \in2 ->
+      let firstBitMarker = ~~(loop [ i/=0 | i <- [0..31] ])
+          carry_out      = reg (mux2 firstBitMarker zero carry_in)
+          carry_in       = maj3 carry_out in1 in2
+      in  ~~xor3 carry_out in1 in2
+    }>
+
+
+rotRight n =
+  <{ \input ->
+     let sel   = ~~(loop [ i >= 32-n | i<-[0..31] ])
+         fifo1 = ~~(fifo (32-n)) input
+         fifo2 = ~~(fifo  32   ) fifo1
+     in  mux2 sel fifo1 fifo2
+   }>
+
+sha256round =
+  <{ \load ->
+     \input ->
+     \k_plus_w ->
+     let a    = ~~(fifo 32) (mux2 load a_in input)
+         b    = ~~(fifo 32) a
+         c    = ~~(fifo 32) b
+         d    = ~~(fifo 32) c
+         e    = ~~(fifo 32) (mux2 load e_in d)
+         f    = ~~(fifo 32) e
+         g    = ~~(fifo 32) f
+         h    = ~~(fifo 32) g
+         s0   = ~~xor3
+                    (~~(rotRight  2) a_in)
+                    (~~(rotRight 13) a_in)
+                    (~~(rotRight 22) a_in)
+         s1   = ~~xor3
+                    (~~(rotRight  6) e_in)
+                    (~~(rotRight 11) e_in)
+                    (~~(rotRight 25) e_in)
+         a_in = adder t1 t2
+         e_in = adder t1 d
+         t1   = adder
+                   (adder h s1)
+                   (adder (mux2 e g f)
+                          k_plus_w)
+         t2   = adder s0 (maj3 a b c)
+     in h
+   }>
\ No newline at end of file