Commits

Rob Simmons  committed ceaf71e

Add figure 3 to Minamide's example

  • Participants
  • Parent commits 33df908
  • Branches fast_linear

Comments (0)

Files changed (1)

File minamide.levy

             then force binsert' t2 y ([hole: tree] k (Br x t1 hole))
             else return k (Br x t1 t2) 
   in 
-    force binsert' t y ([hole: tree] hole) ;;
+    force binsert' t y ([hole: tree] hole) ;;
+
+val addone = thunk rec addone: tree -> F tree is
+  fun t: tree ->
+    match t with
+      | Lf -> return Lf
+      | Br x t1 t2 -> 
+          force addone t1 to t1' in
+          force addone t2 to t2' in
+          return Br (x+1) t1' t2' ;;
+
+# Woah. This one's crazy.
+
+val hfun_addone = thunk rec hfun_addone: tree -> F tree is
+  fun t: tree ->
+    match t with
+      | Lf -> return Lf
+      | Br x t1 t2 ->
+          let addone' be thunk rec addone': tree -> (tree -o tree) -> F tree is
+            fun t: tree -> 
+            fun k: tree -o tree ->
+              match t with
+                | Lf -> return k Lf
+                | Br x t1 t2 ->  
+                    force hfun_addone t1 to t1' in 
+                    force addone' t2 ([hole: tree] Br (x+1) t1' hole)
+          in
+             force hfun_addone t1 to t1' in
+             force addone' t2 ([hole: tree] Br (x+1) t1' hole) ;;