1 files changed, 78 insertions, 0 deletions
diff --git a/lib/Impure/ocaml/ImpLoopOracles.ml b/lib/Impure/ocaml/ImpLoopOracles.ml
new file mode 100644
index 00000000..cb7625e5
--- /dev/null
+++ b/lib/Impure/ocaml/ImpLoopOracles.ml
@@ -0,0 +1,78 @@
+open ImpPrelude
+open Datatypes
+
+(** GENERIC ITERATIVE LOOP **) 
+
+(* a simple version of loop *)
+let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let rec iter: 'a -> 'b
+      = fun a ->
+        match f a with
+        | Coq_inl a' -> iter a'
+        | Coq_inr b -> b
+    in
+    iter a0;;
+
+(* loop from while *)
+let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b
+  = fun (a0, f) ->
+    let s = ref (f a0) in
+    while (match !s with Coq_inl _ -> true | _ -> false) do
+      match !s with
+      | Coq_inl a -> s:=f a
+      | _ -> assert false
+    done;
+    match !s with
+    | Coq_inr b -> b
+    | _ -> assert false;;
+
+let loop = simple_loop
+
+
+(** GENERIC FIXPOINTS **)
+  
+let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let rec f x = recf f x in
+  f
+
+let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let memo = Hashtbl.create 10 in
+  let rec f x =
+    try
+      Hashtbl.find memo x
+    with
+      Not_found ->
+        let r = recf f x in
+        Hashtbl.replace memo x r;
+        r
+  in f
+
+let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b  =
+  let fix = ref (fun x -> failwith "init") in
+  fix := (fun x -> recf !fix x);
+  !fix;;
+  
+let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b =
+  let memo = ref None in
+  let rec f x =
+    match !memo with
+    | Some y -> y
+    | None ->
+       let r = recf f x in
+       memo := Some r;
+       r
+  in f
+
+let xrec_mode = ref MemoRec
+
+let xrec_set_option : recMode -> unit
+= fun m -> xrec_mode := m
+
+let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b )
+  = fun recf ->
+    match !xrec_mode with
+    | StdRec -> std_rec recf
+    | MemoRec -> memo_rec recf
+    | BareRec -> bare_rec recf
+    | BuggyRec -> buggy_rec recf