X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FImmutableHeap.hs;fp=examples%2FImmutableHeap.hs;h=56ff12c2481806a09cfefad24c7c666c2f70fa6f;hp=0000000000000000000000000000000000000000;hb=caa7ad74b99b34abc5181553e66423da6bdfee26;hpb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4

diff --git a/examples/ImmutableHeap.hs b/examples/ImmutableHeap.hs
new file mode 100644
index 0000000..56ff12c
--- /dev/null
+++ b/examples/ImmutableHeap.hs
@@ -0,0 +1,23 @@
+{-# OPTIONS_GHC -XModalTypes -XScopedTypeVariables -ddump-types -XNoMonoPatBinds #-}
+module ImmutableHeap
+where
+import IsomorphismForCodeTypes
+import Prelude hiding ( id, (.) )
+
+
+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 
+                       in let x' = ~~alloc (1,x)
+                       in let y' = ~~alloc (2,y)
+                       in (x',y')
+                     ]>