projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
1569640
)
syntax update in KappaDemo.hs
author
Adam Megacz
<megacz@cs.berkeley.edu>
Tue, 4 Oct 2011 18:28:26 +0000
(13:28 -0500)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Tue, 4 Oct 2011 18:28:26 +0000
(13:28 -0500)
examples/KappaDemo.hs
patch
|
blob
|
history
diff --git
a/examples/KappaDemo.hs
b/examples/KappaDemo.hs
index
a1831ef
..
43d29f4
100644
(file)
--- a/
examples/KappaDemo.hs
+++ b/
examples/KappaDemo.hs
@@
-1,17
+1,17
@@
{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
module Demo (demo, demo2) where
{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
module Demo (demo, demo2) where
-demo z = <{ \y -> ~~z }>
+demo z = <[ \y -> ~~z ]>
demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
-demo2 x y = <{ ~~x ~~y }>
+demo2 x y = <[ ~~x ~~y ]>
swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
-swap f = <{ \x -> \y -> ~~f y x }>
+swap f = <[ \x -> \y -> ~~f y x ]>
--- bad = <{ \f -> \x -> f x }>
+-- bad = <[ \f -> \x -> f x ]>
-demo3 x y z q = <{ ~~q (~~x ~~y ~~z) }>
+demo3 x y z q = <[ ~~q (~~x ~~y ~~z) ]>
@@
-37,28
+37,28
@@
class BitSerialHardwarePrimitives g where
<[ oracle ]> :: Int -> <[ Wire ]>@g
xor3 :: forall g . BitSerialHardwarePrimitives g => <[ (Wire,(Wire,(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 }>
+xor3 = <[ \x -> \y -> \z -> xor (xor x y) z ]>
adder =
adder =
- <{ \in1 ->
+ <[ \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
\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 =
rotRight n =
- <{ \input ->
+ <[ \input ->
let sel = ~~(loop [ i >= 32-n | i<-[0..31] ])
fifo1 = ~~(fifo (32-n)) input
fifo2 = ~~(fifo 32 ) fifo1
in mux2 sel fifo1 fifo2
let sel = ~~(loop [ i >= 32-n | i<-[0..31] ])
fifo1 = ~~(fifo (32-n)) input
fifo2 = ~~(fifo 32 ) fifo1
in mux2 sel fifo1 fifo2
- }>
+ ]>
sha256round =
sha256round =
- <{ \load ->
+ <[ \load ->
\input ->
\k_plus_w ->
let a = ~~(fifo 32) (mux2 load a_in input)
\input ->
\k_plus_w ->
let a = ~~(fifo 32) (mux2 load a_in input)
@@
-85,4
+85,4
@@
sha256round =
k_plus_w)
t2 = adder s0 (maj3 a b c)
in h
k_plus_w)
t2 = adder s0 (maj3 a b c)
in h
- }>
\ No newline at end of file
+ ]>
\ No newline at end of file