]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/num.ml
Debugging information improved
[fireball-separation.git] / ocaml / num.ml
1 open Util
2 open Util.Vars
3 open Pure
4
5 (* debug options *)
6 let debug_display_arities = false;;
7
8 (************ Syntax ************************************)
9
10 (* Normal forms*)
11
12 (* Var n = n-th De Bruijn index, 0-based *)
13
14 (*type nf =
15   | Lam of nf
16   | Var of int
17   | i
18 and i =
19   | I of int * nf listx
20 ;;*)
21 type var = int * (* arity of variable*) int;;
22 type 'nf_nob i_var_ = [ `I of var * 'nf_nob Listx.listx | `Var of var ]
23 type 'nf_nob i_n_var_ = [ `N of int | 'nf_nob i_var_ ]
24 type ('nf_nob,'nf) i_num_var_ = [
25   | 'nf_nob i_n_var_
26   | `Match of ('nf_nob,'nf) i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf_nob list
27 ]
28 type 'nf nf_nob_ = [ `Lam of (* was_unpacked *) bool * 'nf | `Pacman | ('nf nf_nob_,'nf) i_num_var_ ]
29 type nf = [ nf nf_nob_ | `Bottom  ]
30 type nf_nob = nf nf_nob_
31 type i_var = nf_nob i_var_;;
32 type i_n_var = nf_nob i_n_var_;;
33 type i_num_var = (nf_nob,nf) i_num_var_;;
34
35 let hd_of_i_var =
36  function
37    `I ((v,_),_)
38  | `Var (v,_) -> v
39
40 let hd_of =
41  function
42    `I ((v,_),_)
43  | `Var(v,_) -> Some v
44  | `N _ -> None
45  | `Match _ -> assert false
46
47 let arity_of_hd =
48 function
49   `I ((_,a),_)
50 | `Var(_,a) -> a
51 | _ -> 0 (* FIXME? *)
52
53 let lift m (t : nf) =
54  let aux_var l (n, ar) = (if n < l then n else n+m), ar in
55  let rec aux_i_num_var l =
56   function
57     `I(v,args) -> `I(aux_var l v, Listx.map (aux_nob l) args)
58    | `Var v -> `Var(aux_var l v)
59    | `N _ as x -> x
60    | `Match(t,v,lift,bs,args) ->
61       `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux_nob l) args)
62  and aux_nob l =
63   function
64      #i_num_var as x -> (aux_i_num_var l x :> nf_nob)
65    | `Lam(b,nf) -> `Lam (b, aux (l+1) nf)
66    | `Pacman -> `Pacman
67  and aux l =
68   function
69      #nf_nob as x -> (aux_nob l x :> nf)
70    | `Bottom -> `Bottom
71  in
72   (aux 0 t : nf)
73 ;;
74
75 (* put t under n lambdas, lifting t accordingtly *)
76 let rec make_lams t =
77  function
78    0 -> t
79  | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)))
80  | _ -> assert false
81
82 let free_vars' =
83  let rec aux n = function
84     `N _ -> []
85   | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
86   | `I((x,ar),args) ->
87       (if x < n then [] else [(x-n,ar)]) @
88       List.concat (List.map (aux n) (Listx.to_list args :> nf list))
89   | `Lam(_,t) -> aux (n+1) t
90   | `Match(t,_,liftno,bs,args) ->
91       aux n (t :> nf) @
92       List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
93       List.concat (List.map (aux n) (args :> nf list))
94   | `Bottom | `Pacman -> []
95   in aux 0
96 ;;
97 let free_vars = (List.map fst) ++ free_vars';;
98
99 module ToScott =
100 struct
101
102 let rec scott_of_nf = function
103  | `N n -> Scott.mk_n n
104  | `Var(v,_) -> Pure.V v
105  | `Match(t,_,liftno,bs,args) ->
106  let bs = List.map (fun (n,t) -> n, scott_of_nf (lift liftno (t :> nf))) !bs in
107      let t = scott_of_nf (t :> nf) in
108      let m = Scott.mk_match t bs in
109      List.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) m (args :> nf list)
110  | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,scott_of_nf t)) (Pure.V v) (args :> nf Listx.listx)
111  | `Lam(_,t) -> Pure.L (scott_of_nf t)
112  | `Bottom -> Pure.B
113  | `Pacman -> let f x = Pure.A (x,x) in f (Pure.L (Pure.L (f (Pure.V 0))))
114 end
115
116
117 (************ Pretty-printing ************************************)
118
119 (* let rec string_of_term l  = fun _ -> "";; *)
120
121 let rec string_of_term =
122  let boundvar x = "v" ^ string_of_int x in
123  let varname lev l n =
124   if n < lev then boundvar (lev-n-1)
125    else if n < List.length l then List.nth l (n-lev)
126     else "`" ^ string_of_int (n-lev) in
127  let rec string_of_term_w_pars lev l  = function
128   | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
129   | `N n -> string_of_int n
130   | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
131   | `Lam(_,`Bottom) -> "BOMB"
132   | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
133   | `Match(t,(v,ar),bs_lift,bs,args) ->
134       (* assert (bs_lift = lev); *)
135      "(["^ varname lev l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
136      " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
137      String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
138   | `Bottom -> "BOT"
139   | `Pacman -> "PAC"
140  and string_of_term_no_pars_app lev l  = function
141   | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
142   | #nf as t -> string_of_term_w_pars lev l t
143  and string_of_term_no_pars_lam lev l  = function
144   | `Lam(_,`Bottom) -> "BOMB"
145   | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
146   | _ as t -> string_of_term_no_pars lev l t
147  and string_of_term_no_pars lev l = function
148   | `Lam _ as t -> string_of_term_no_pars_lam lev l t
149   | #nf as t -> string_of_term_no_pars_app lev l t
150  in string_of_term_no_pars 0
151 ;;
152
153 let print ?(l=[]) = string_of_term l;;
154 let string_of_nf t = string_of_term [] (t :> nf);;
155
156 (************ Hereditary substitutions ************************************)
157
158 let cast_to_i_var =
159  function
160     #i_var as y -> (y : i_var)
161   | t ->
162     prerr_endline (print (t :> nf));
163     assert false (* algorithm failed *)
164
165 let cast_to_i_n_var =
166  function
167     #i_n_var as y -> (y : i_n_var)
168   | t ->
169     prerr_endline (print (t :> nf));
170     assert false (* algorithm failed *)
171
172 let cast_to_i_num_var =
173  function
174     #i_num_var as y -> (y : i_num_var)
175   | t ->
176     prerr_endline (print (t :> nf));
177     assert false (* algorithm failed *)
178
179 let rec set_arity arity = function
180 (* FIXME because onlt variables should be in branches of matches, one day *)
181 | `Var(n,_) -> `Var(n,arity)
182 | `N _ | `Bottom | `Pacman as t -> t
183 | `Lam(false, t) -> `Lam(false, set_arity arity t)
184 | `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
185 | `I _ | `Lam _ -> assert false
186
187 let minus1 n = if n = min_int then n else n - 1;;
188
189 let rec mk_app (h : nf) (arg : nf) =
190  match arg with
191   | `Bottom -> `Bottom
192   | #nf_nob as arg ->
193     match h with
194      | `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
195      | `Var v -> `I(v, Listx.Nil arg)
196      | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
197      | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
198      | `Bottom | `Pacman as t -> t
199      | `N _ -> assert false (* Numbers cannot be applied *)
200 (*in let l = ["v0";"v1";"v2"] in
201 prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
202
203 and mk_appl h args =
204  (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
205  List.fold_left mk_app h args
206
207 and mk_appx h args = Listx.fold_left mk_app h args
208
209 and mk_match t (n,ar) bs_lift bs args =
210  (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
211  let m =
212   match t with
213     `N m as t ->
214       (try
215         let h = List.assoc m !bs in
216         let h = set_arity (minus1 ar) h in
217         let h = lift bs_lift h in
218          h
219        with Not_found ->
220         `Match (t,(n,ar),bs_lift,bs,[]))
221    (* We are assuming that the econding of matches is s.t.:
222       - match PAC.. --> PAC
223       - match BOT.. --> BOT *)
224    | `Bottom -> `Bottom
225    | `Pacman -> `Pacman
226    | `Lam _ -> assert false
227    | `I _ | `Var _ | `Match _ as t -> `Match(t,(n,ar),bs_lift,bs,[]) in
228  mk_appl m args
229
230 and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) =
231  let rec aux_propagate_arity ar = function
232  | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
233  | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
234     `Match(`I(v,args),(x,ar),liftno,bs,args')
235  | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
236  | _ as t -> t in
237  let rec aux_i_num_var l =
238   function
239      `I((n,ar),args) ->
240        if n = what + l then
241        let args = Listx.map (aux l) (args :> nf Listx.listx) in
242         mk_appx (lift l (aux_propagate_arity ar (with_what :> nf))) args
243        else
244         mk_appl (`Var ((if delift_by_one && n >= l then n-1 else n), ar)) (List.map (aux l) (Listx.to_list (args :> nf Listx.listx)))
245    | `Var(n,ar) ->
246        if n = what + l then
247         lift l (aux_propagate_arity ar (with_what :> nf))
248        else
249         `Var((if delift_by_one && n >= l then n-1 else n), ar)
250    | `N _ as x -> x
251    | `Match(t,v,bs_lift,bs,args) ->
252        let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
253        (* Warning! It now applies again the substitution in branches of matches.
254           But careful, it does it many times, for every occurrence of
255           the match. This is okay because what does not occur in with_what. *)
256        let l' = l - bs_lift  in
257        let with_what' = lift l' (with_what :> nf) in
258        (* The following line should be the identity when delift_by_one = true because we
259           are assuming the ts to not contain lambda-bound variables. *)
260        bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
261        let body = aux_i_num_var l t in
262        mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
263  and aux l(*lift*) =
264 (*function iii -> let res = match iii with*)
265   function
266    | #i_num_var as x -> aux_i_num_var l x
267    | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
268    | `Bottom -> `Bottom
269    | `Pacman -> `Pacman
270 (*in let ll = ["v0";"v1";"v2"] in
271 prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
272  in
273   aux 0 where
274 ;;
275
276 (************ Parsing ************************************)
277
278 (************** Algorithm(s) ************************)
279
280 let eta_compare x y =
281  (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
282  let clex aux1 aux2 (a1,a2) (b1,b2) =
283   let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
284  let rec lex aux l1 l2 =
285   match l1,l2 with
286  | [], [] -> 0
287  | [], _ -> -1
288  | _, [] -> 1
289  | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
290  let rec aux t1 t2 = match t1, t2 with
291   | `Var(n,_) , `Var(m,_) -> compare n m
292   | `I((n1,_), l1), `I((n2,_), l2) ->
293     clex compare (lex aux) (n1, (Listx.to_list l1 :> nf list)) (n2, (Listx.to_list l2 :> nf list))
294   | `Bottom, `Bottom
295   | `Pacman, `Pacman -> 0
296   | `Lam _, `N _ -> -1
297   | `N _, `Lam _ -> 1
298   | `Bottom, `Lam(_,t) -> -1
299   | `Lam(_,t), `Bottom ->  1
300   | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
301   | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
302   | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
303   | `N n1, `N n2 -> compare n1 n2
304   | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
305     let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
306     let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
307     clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, (args :> nf list))) ((u' :> nf), (bs', (args' :> nf list)))
308   | `Match _, _ -> -1
309   | _, `Match _ -> 1
310   | `N _, _ -> -1
311   | _, `N _ -> 1
312   | `I _, _ -> -1
313   | _, `I _ -> 1
314   | `Bottom, _ -> -1
315   | _, `Bottom -> 1
316   | `Pacman, _ -> -1
317   | _, `Pacman -> 1
318   in aux x y
319 ;;
320
321 let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
322
323 let rec eta_subterm sub t =
324  if eta_eq sub t then true else
325   match t with
326   | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
327   | `Bottom
328   | `Pacman  -> false
329   | `Match(u,ar,liftno,bs,args) ->
330      eta_subterm sub (u :> nf)
331      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
332      || List.exists (eta_subterm sub) (args :> nf list)
333   | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
334    | `Var(v',_) -> v = v'
335    | `I((v',_), args') -> v = v'
336     && Listx.length args' < Listx.length args
337     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args :> nf list)) (Listx.to_list args' :> nf list))
338    | _ -> false
339    )
340   | `N _ | `Var _ -> false
341 ;;
342
343 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
344
345 let max_arity_tms n =
346  let max a b = match a, b with
347   | None, None -> None
348   | None, Some x
349   | Some x, None -> Some x
350   | Some x, Some y -> Some (Pervasives.max x y) in
351  let aux_var l (m,a) = if n + l = m then Some a else None in
352  let rec aux l = function
353   | `Var v -> aux_var l v
354   | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms :> nf list))
355   | `Lam(_,t) -> aux (l+1) t
356   | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l (args :> nf list))) (aux_tms l (List.map snd !bs))
357   | `N _ | `Bottom | `Pacman -> None
358  and aux_tms l =
359   List.fold_left (fun acc t -> max acc (aux l t)) None in
360  fun tms -> aux_tms 0 (tms :> nf list)
361 ;;