blob: cb7625e507a776168a09791ecdd85ae1413ce57c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
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
|
