-{-# 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 }>
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