]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/pure.ml
Debugging information improved
[fireball-separation.git] / ocaml / pure.ml
1 open Util.Vars
2
3 module Pure =
4 struct
5
6 type t =
7   | V of int
8   | A of t * t
9   | L of t
10   | B
11
12 let rec print ?(l=[]) =
13  function
14     V n -> print_name l n
15   | A(t1,t2) -> "(" ^ print ~l t1 ^ " " ^ print ~l t2 ^ ")"
16   | L t ->
17      let name = string_of_var (List.length l) in
18      "λ" ^ name ^ "." ^ print ~l:(name::l) t
19   | B -> "B"
20
21 let lift m =
22  let rec aux l =
23   function
24    | V n -> V (if n < l then n else n+m)
25    | A (t1,t2) -> A (aux l t1, aux l t2)
26    | L t -> L (aux (l+1) t)
27    | B -> B
28  in
29   aux 0
30
31 (* Reference implementation.
32    Reduction machine used below
33 let subst delift_by_one what with_what =
34  let rec aux l =
35   function
36    | A(t1,t2) -> A(aux l t1, aux l t2)
37    | V n ->
38        if n = what + l then
39         lift l with_what
40        else
41         V (if delift_by_one && n >= l then n-1 else n)
42    | L t -> L (aux (l+1) t)
43  in
44   aux 0
45
46 let rec whd =
47  function
48   | A(t1, t2) ->
49      let t2 = whd t2 in
50      let t1 = whd t1 in
51       (match t1 with
52         | L f -> whd (subst true 0 t2 f)
53         | V _
54         | A _ -> A(t1,t2))
55   | V _
56   | L _ as t -> t
57 *)
58
59 let unwind ?(tbl = Hashtbl.create 317) m =
60  let rec unwind (e,t,s) =
61   let cache_unwind m =
62    try
63     Hashtbl.find tbl m
64    with
65     Not_found ->
66      let t = unwind m in
67       Hashtbl.add tbl m t ;
68       t in
69   let s = List.map cache_unwind s in
70   let rec aux l =
71    function
72     | A(t1,t2) -> A(aux l t1, aux l t2)
73     | V n as x when n < l -> x
74     | V n ->
75        (try
76          lift l (cache_unwind (List.nth e (n - l)))
77         with Failure _ -> V (n - l))
78     | L t -> L (aux (l+1) t)
79     | B -> B in
80   let t = aux 0 t in
81   List.fold_left (fun f a -> A(f,a)) t s
82 in
83  unwind m
84
85 let mwhd m =
86  let rec aux =
87   function
88    | (e,A(t1,t2),s) ->
89        let t2' = aux (e,t2,[]) in
90        let (_,t,_) = t2' in
91        if t = B
92         then t2'
93         else aux (e,t1,t2'::s)
94    | (e,L t,x::s) -> aux (x::e,t,s)
95    | (e,V n,s) as m ->
96       (try
97         let e,t,s' = List.nth e n in
98         aux (e,t,s'@s)
99        with Failure _ -> m)
100    | (e, B, _) -> (e, B, [])
101    | (_,L _,[]) as m -> m
102  in
103   unwind (aux m)
104
105 end
106
107 module Scott =
108 struct
109
110 open Pure
111
112 let rec mk_n n =
113  if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
114
115 let dummy = V (max_int / 2)
116
117 let mk_match t bs =
118  let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
119  let rec aux m t =
120   function
121      [] -> A (L dummy, t)
122    | (n,p)::tl as l ->
123       if n = m then
124        A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
125       else
126        A (A (t, dummy), L (aux (m+1) (V 0) l))
127  in
128   aux 0 t bs
129
130 end