1 {-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
2 module Demo (demo, demo2) where
7 let delayed = ~~reg output
8 output = ~~xor input delayed
12 demo z = <[ \y -> ~~z ]>
14 demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
15 demo2 x y = <[ ~~x ~~y ]>
17 swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
18 swap f = <[ \x -> \y -> ~~f y x ]>
20 -- bad = <[ \f -> \x -> f x ]>
22 demo3 x y z q = <[ ~~q (~~x ~~y ~~z) ]>
26 class BitSerialHardwarePrimitives g where
29 <[ not ]> :: <[ (Wire,()) ~~> Wire ]>@g
30 <[ xor ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
31 <[ or ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
32 <[ and ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
33 <[ mux2 ]> :: <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
34 <[ maj3 ]> :: <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
35 <[ reg ]> :: <[ (Wire,()) ~~> Wire ]>@g
36 <[ zero ]> :: <[ () ~~> Wire ]>@g
37 <[ one ]> :: <[ () ~~> Wire ]>@g
39 loop :: [Bool] -> <[ () ~~> Wire ]>@g
40 <[ lfsr ]> :: Int -> [ <[ Wire ]>@g ]
41 <[ adder ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
42 fifo :: Int -> <[ (Wire,()) ~~> Wire ]>@g
44 <[ probe ]> :: Int -> <[ (Wire,()) ~~> Wire ]>@g
45 <[ oracle ]> :: Int -> <[ Wire ]>@g
47 xor3 :: forall g . BitSerialHardwarePrimitives g => <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
48 xor3 = <[ \x -> \y -> \z -> xor (xor x y) z ]>
53 let firstBitMarker = ~~(loop [ i/=0 | i <- [0..31] ])
54 carry_out = reg (mux2 firstBitMarker zero carry_in)
55 carry_in = maj3 carry_out in1 in2
56 in ~~xor3 carry_out in1 in2
62 let sel = ~~(loop [ i >= 32-n | i<-[0..31] ])
63 fifo1 = ~~(fifo (32-n)) input
64 fifo2 = ~~(fifo 32 ) fifo1
65 in mux2 sel fifo1 fifo2
72 let a = ~~(fifo 32) (mux2 load a_in input)
76 e = ~~(fifo 32) (mux2 load e_in d)
82 (~~(rotRight 13) a_in)
83 (~~(rotRight 22) a_in)
86 (~~(rotRight 11) e_in)
87 (~~(rotRight 25) e_in)
94 t2 = adder s0 (maj3 a b c)