projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
change ECKind to *=>*=>*
[coq-hetmet.git]
/
examples
/
ImmutableHeap.hs
diff --git
a/examples/ImmutableHeap.hs
b/examples/ImmutableHeap.hs
index
56ff12c
..
717f84b
100644
(file)
--- a/
examples/ImmutableHeap.hs
+++ b/
examples/ImmutableHeap.hs
@@
-4,16
+4,10
@@
where
import IsomorphismForCodeTypes
import Prelude hiding ( id, (.) )
import IsomorphismForCodeTypes
import Prelude hiding ( id, (.) )
-
class GuestLanguageHeap c where
alloc :: <[ (Integer,Integer) -> Integer ]>@c
lookup :: <[ Integer -> (Integer,Integer) ]>@c
class GuestLanguageHeap c where
alloc :: <[ (Integer,Integer) -> Integer ]>@c
lookup :: <[ Integer -> (Integer,Integer) ]>@c
---
--- Here's nice example of Sheard's observation that it's often easier
--- to write two-stage programs by applying "back" to some function rather than
--- writing the final result directly
---
onetwocycle = back onetwocycle'
where
onetwocycle' xy = <[ let (x,y) = ~~xy
onetwocycle = back onetwocycle'
where
onetwocycle' xy = <[ let (x,y) = ~~xy