1 (* type var = (* unique name *) int * (int * term) option * (*level*) int *)
\r
4 | Tapp of term * term * bool
\r
8 let zero = Tvar 1010;;
\r
9 let dummy = Tvar 333;;
\r
12 (* mk_app & subst implementano la beta *)
\r
13 let rec mk_app t1 t2 = match t1 with
\r
14 | Tlam(v, t1') -> subst v t2 t1'
\r
15 | _ -> Tapp(t1, t2, false)
\r
17 let rec aux = function
\r
18 | Tapp(t1, t2, _) -> mk_app (aux t1) (aux t2)
\r
19 | Tvar v' as t -> if v = v' then tv else t
\r
20 | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t')
\r
24 (* PARSING AND PRINTING *)
\r
27 let rec minus1 = function
\r
28 | Tvar n -> Tvar (n-1)
\r
29 | Tapp(t1, t2, b) -> Tapp(minus1 t1, minus1 t2, b)
\r
30 | Tlam(n, t) -> Tlam(n-1, minus1 t)
\r
31 (* in let open Parser *)
\r
32 in let rec myterm_of_term = function
\r
33 | Parser.Var n -> Tvar n
\r
34 | Parser.App(t1, t2) -> (*Tapp(myterm_of_term t1, myterm_of_term t2) WARNING! BETA DOWN HERE! *)
\r
35 mk_app (myterm_of_term t1) (myterm_of_term t2)
\r
36 | Parser.Lam(t) -> minus1 (Tlam(0, myterm_of_term t))
\r
38 let (tms, free) = Parser.parse_many strs
\r
39 in List.map myterm_of_term tms
\r
43 (* PRETTY PRINTING *)
\r
46 let fancy_of_term t =
\r
47 let rec string_of_term =
\r
48 let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"] in
\r
49 let bound = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in
\r
50 let string_of_int' n = if n >= 0 then "free" ^ string_of_int n else "bound" ^ string_of_int n in
\r
51 let rec string_of_var t =
\r
52 if Tvar t = dummy then "_" else if Tvar t = zero then "ZZ" else match t with
\r
53 | n -> string_of_int' n
\r
54 and string_of_term_w_pars = function
\r
55 | Tvar v -> string_of_var v
\r
56 | Tapp(t1, t2, _) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"
\r
57 | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"
\r
58 and string_of_term_no_pars_app = function
\r
59 | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)
\r
60 | _ as t -> string_of_term_w_pars t
\r
61 and string_of_term_no_pars_lam = function
\r
62 | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)
\r
63 | _ as t -> string_of_term_no_pars t
\r
64 and string_of_term_no_pars = function
\r
65 | Tlam(_, _) as t -> string_of_term_no_pars_lam t
\r
66 | _ as t -> string_of_term_no_pars_app t
\r
67 in string_of_term_no_pars
\r
68 in let rec html_of_term =
\r
69 let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in
\r
70 let bound = ["x"; "y"; "z"; "w"; "q"] in
\r
71 let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in
\r
72 let rec string_of_var t =
\r
73 if Tvar t = dummy then "#" else if Tvar t = zero then "Z" else string_of_int' t
\r
74 and string_of_term_w_pars = function
\r
75 | Tvar v -> string_of_var v
\r
76 | Tapp(t1, t2,_) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"
\r
77 | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"
\r
78 and string_of_term_no_pars_app = function
\r
79 | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)
\r
80 | _ as t -> string_of_term_w_pars t
\r
81 and string_of_term_no_pars_lam = function
\r
82 | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)
\r
83 | _ as t -> string_of_term_no_pars t
\r
84 and string_of_term_no_pars = function
\r
85 | Tlam(_, _) as t -> string_of_term_no_pars_lam t
\r
86 | _ as t -> string_of_term_no_pars_app t
\r
87 in string_of_term_no_pars
\r
89 string_of_term t / "html_of_term t"
\r
92 let fancy_of_nf t: Console.fancyobj =
\r
93 let rec print ?(l=[]) =
\r
95 `Var n -> Util.Vars.print_name l n
\r
96 | `N n -> string_of_int n
\r
97 | `Match(t,bs_lift,bs,args) ->
\r
98 "([" ^ print ~l (t :> Num.nf) ^
\r
99 " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Num.lift bs_lift t)) !bs) ^ "] " ^
\r
100 String.concat " " (List.map (print ~l) args) ^ ")"
\r
101 | `I(n,args) -> "(" ^ Util.Vars.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
\r
103 let name = Util.Vars.string_of_var (List.length l) in
\r
104 "" ^ name ^ "." ^ print ~l:(name::l) (nf : Num.nf)
\r
106 (* in let rec print_html ?(l=[]) =
\r
108 `Var n -> Lambda3.print_name l n
\r
109 | `N n -> string_of_int n
\r
110 | `Match(t,bs_lift,bs,args) ->
\r
111 "(<b>match</b> " ^ print_html ~l (t :> Lambda3.nf) ^
\r
112 " <b>with</b> " ^ String.concat " <b>|</b> " (List.map (fun (n,t) -> string_of_int n ^ " <b>⇒</b> " ^ print_html ~l (Lambda3.lift bs_lift t)) !bs) ^ "..." (* Attenzion non sto stampando gli argomenti applicati! Perche' non ce ne sono mai *)
\r
113 | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")"
\r
115 let name = Lambda3.string_of_var (List.length l) in
\r
116 "λ" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf) *)
\r
121 let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);;
\r
125 let varcount = ref 11;;
\r
127 let freshvar () = (
\r
128 varcount := (!varcount + 1);
\r
132 let find_applicative =
\r
133 let rec aux = function
\r
134 | Tapp(t1, Tlam _, _) -> Some t1
\r
135 | Tapp(t1, t2, _) ->
\r
140 in let rec aux2 = function
\r
142 | x::xs -> (match aux x with
\r
144 | _ as result -> result
\r
149 let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)
\r
151 let rec hd = function | Tvar _ as x -> x | Tapp(t, _, _) -> hd t | _ -> assert false;;
\r
153 let rec set_applied =
\r
156 | Tlam _ -> assert false
\r
157 | Tapp(t1,t2,_) -> Tapp(set_applied t1, set_applied t2, true)
\r
160 let rec constant a n =
\r
161 if n = 0 then [] else a:: (constant a (n-1))
\r
164 let rec mk_dummies k t =
\r
165 set_applied (mk_apps t (constant dummy (k+1)))
\r
168 let rec make_lambda_zero k =
\r
169 if k = 0 then mk_dummies (k+1) zero else Tlam(0, make_lambda_zero (k-1))
\r
176 else (Tvar (freshvar ())) :: (aux (n-1))
\r
177 in aux n @ [make_lambda_zero (n+1)]
\r
181 let rec aux = function
\r
182 | Tapp(t1, t2, b) ->
\r
184 then (assert (not b); Tapp(aux t1, mk_apps' t2 vars, true))
\r
185 else Tapp(aux t1, aux t2, b)
\r
187 and mk_apps' t vars =
\r
189 then mk_dummies (List.length vars - 1) t
\r
190 else aux (mk_apps t vars)
\r
194 let round k (app_map, tms) =
\r
195 match find_applicative tms with
\r
196 | None -> raise Not_found
\r
198 let vars = mk_vars k in
\r
199 let f = apply a vars in
\r
200 let app_map = (a, vars) :: (List.map (fun (x,y) -> f x, y) app_map)
\r
201 in (app_map, List.map f tms)
\r
204 let ends_with t1 t2 = match t1 with
\r
205 | Tapp(_, t, _) -> t = t2
\r
209 let rec last_round k (app_map, forbidden, t) =
\r
210 let mk_apps' forbidden t vars =
\r
211 if List.mem t forbidden
\r
212 then mk_dummies (List.length vars - 1) t
\r
213 else mk_apps t vars
\r
214 (* in let rec already_applied = function
\r
215 | Tapp(_, t) -> t = zero || t = dummy || hd t = zero
\r
217 in if ends_with t dummy then (app_map, forbidden, t) else (match t with
\r
218 | Tapp(t1, t2, b) ->
\r
221 let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)
\r
222 in let app_map, forbidden, t2 = last_round k (app_map, forbidden, t2)
\r
223 in app_map, forbidden, Tapp(t1, t2, b)
\r
225 let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)
\r
226 in let app_map, forbidden, t2 =
\r
228 let vars = List.assoc t1 app_map
\r
229 in last_round k (app_map, forbidden, (mk_apps' forbidden t2 vars))
\r
231 let vars = mk_vars k in
\r
232 let app_map = (t1, vars) :: app_map in
\r
233 last_round k (app_map, (vars @ forbidden), (mk_apps' forbidden t2 vars))
\r
234 in app_map, forbidden, Tapp(t1, t2, true)
\r
235 | _ as t -> app_map, forbidden, t
\r
240 let rec aux x = try
\r
241 let y = f x in aux y
\r
242 with Not_found -> x
\r
246 (* lista di sottotermini applicativi *)
\r
247 let rec subterms = function
\r
248 | Tlam _ -> assert false
\r
249 | Tvar _ as v -> [v]
\r
250 | Tapp(t1, t2, b) -> Tapp(t1, t2, b) :: ((subterms t1) @ (subterms t2))
\r
253 (* filtra dai sottotermini le variabili *)
\r
254 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;
\r
256 let stupid_sort_uniq map l =
\r
257 let rec stupid_uniq = function
\r
259 | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)
\r
260 in let stupid_compare a b =
\r
261 let rec size = function
\r
262 | Tvar n as v -> if v = zero then 0 else (
\r
264 let t, _ = List.find (fun (_,vars) -> List.mem v vars) map
\r
266 with Not_found -> 1 + n)
\r
267 | Tapp(t1,t2,_) -> 1 + size t1 + size t2
\r
268 | Tlam _ -> assert false
\r
269 in compare (size a) (size b)
\r
270 in stupid_uniq (List.sort stupid_compare l)
\r
273 (* crea i match ricorsivamente.
\r
274 - k e' lo special-K
\r
275 - subs e' l'insieme dei sottotermini
\r
276 TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione
\r
278 let crea_match subs map forbidden (acc : (term * Num.nf) list) : term -> Num.nf =
\r
279 let req t = try List.assoc t acc with Not_found -> `Var 9999 in
\r
281 if t1 = dummy then `Var 99999 else
\r
282 (* let _ = print_term t1 in *)
\r
283 let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2,true)) subs) subs
\r
284 in if cont = [] then
\r
285 try `N (Util.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else
\r
287 if List.mem (hd t1) forbidden then `Lam (true,req (Tapp(t1, dummy, true)))
\r
289 let vars = List.assoc t1 map
\r
290 (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))
\r
291 in let _ = print_term (mk_apps dummy vars) *)
\r
292 in let vars = List.map req vars
\r
293 in let vars = List.map (Num.lift 1) vars (* forse lift non necessario *)
\r
294 in let vars = Listx.from_list vars
\r
295 in let body = `I(0, vars)
\r
296 in let branches = List.map (fun t2 -> (Util.index_of t2 subs, req (Tapp(t1, t2, true)))) cont
\r
297 in let bs = ref(branches)
\r
300 in `Lam (true, `Match(body, lift, bs, args))
\r
305 (* filtra dai sottotermini le variabili *)
\r
306 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;
\r
309 let rec aux n prev =
\r
310 if n = 0 then [zero]
\r
311 else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev
\r
315 let rec freevars = function
\r
316 | Tvar _ as v -> [v]
\r
317 | Tlam(v,t) -> List.filter (fun x-> x <> Tvar v) (freevars t)
\r
318 | Tapp(t1,t2,_) -> (freevars t1) @ (freevars t2)
\r
323 let is_scott_n t n =
\r
324 let open Lambda4 in let open Pure in
\r
325 let rec aux n = function
\r
326 | L (L (A (V 1, L (V 0)))) -> n = 0
\r
327 | L (L (A (V 0, t))) -> aux (n-1) t
\r
328 | _ -> assert false
\r
332 let open Lambda4 in let open Pure in
\r
333 let rec aux = function
\r
334 | L (L (A (V 1, L (V 0)))) -> 0
\r
335 | L (L (A (V 0, t))) -> 1 + aux t
\r
336 | _ -> assert false
\r
340 let compute_special_k tms =
\r
341 let rec aux k t = match t with
\r
343 | Tapp(t1,t2,_) -> Pervasives.max (aux 0 t1) (aux 0 t2)
\r
344 | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)
\r
345 in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms
\r
348 let magic strings =
\r
349 let rec map_helper_3 a b f =
\r
353 let a, b, d = f (a, b, c) in
\r
354 let a, b, ds = map_helper_3 a b f cs in
\r
356 in let _ = print_hline ()
\r
357 in let tms = parse strings
\r
358 in let k = compute_special_k tms
\r
359 in let zero' = make_lambda_zero (k+1)
\r
360 in let tms = List.map (fun x -> Tapp(x, zero', false)) tms
\r
361 in let fv = Util.sort_uniq (List.concat (List.map freevars tms))
\r
362 in let (map, tms') = fixpoint (round k) ([], tms)
\r
363 (* in let _ = print_string_endline "map1 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok1" *)
\r
364 in let _ = List.map print_term tms'
\r
366 in let map1 = List.map fst map
\r
367 in let map2 = List.map snd map
\r
368 in let map_new, forbidden, map1' = map_helper_3 [] [zero] (last_round k) map1
\r
370 in let map = map_new @ (List.combine map1' map2)
\r
371 (* in let _ = print_string_endline "map2 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok2" *)
\r
372 in let map, forbidden, tms' = map_helper_3 map forbidden (last_round k) tms'
\r
374 in let _ = List.map print_term tms'
\r
375 in let subs = List.concat (List.map subterms tms')
\r
376 in let subs = stupid_sort_uniq map subs
\r
377 (* metti gli zeri in testa, perche' vanno calcolati per primi *)
\r
378 in let zeros = mk_zeros k
\r
379 in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)
\r
381 (* in let _ = print_string_endline " subs"; List.iter print_term subs *)
\r
382 (* in let _ = print_string_endline "map "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok" *)
\r
384 in let f t acc = let res = crea_match subs map forbidden acc t in (t,res)::acc
\r
385 in let acc = List.fold_right f subs []
\r
387 in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc
\r
388 in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " ↦ ") ^^ fancy_of_nf y)) sigma
\r
390 in let _ = print_string_endline "controllo di purezza";
\r
391 (* in let open Num *)
\r
392 in let ps, _ = Num.parse' strings
\r
393 in let ps = List.map (fun x -> Num.mk_app x (`Var 1010)) ps
\r
394 in let ps = List.map (fun t -> Num.ToScott.t_of_nf (t :> Num.nf)) ps
\r
395 in let sigma = List.map (
\r
396 function (Tvar n , inst) -> n, Num.ToScott.t_of_nf inst | _ -> assert false
\r
399 List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma
\r
400 in let _ = List.iteri (fun i n ->
\r
401 print_string_endline ("X " ^ Pure.print (Pure.whd n));
\r
402 (* assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs)) *)
\r
403 is_scott (Pure.whd n); ()
\r
409 (* magic ["x (x x x)"; "x (y. y x)"; "x x (y. y y (x x y))"] ;; *)
\r
410 magic ["((x x) (x. x))";"x x"];;
\r
414 let alive (_, _, n) = n;;
\r
415 let rec setalive c = function
\r
416 | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v
\r
417 | Tapp(a,b) -> Tapp(setalive c a, setalive c b)
\r
418 | Tlam(n, t) -> Tlam(n, setalive c t)
\r
421 let mk_vars t lev =
\r
425 else Tvar(0, Some(n, t), lev) :: (aux (n-1))
\r
429 let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)
\r
432 let compute_special_k tms =
\r
433 let rec aux k t = match t with
\r
435 | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2)
\r
436 | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)
\r
437 in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms
\r
440 let compute_special_h tms =
\r
441 let rec eat_lam = function
\r
442 | Tlam(_,t) -> eat_lam t
\r
445 let rec aux t = match t with
\r
447 | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2)
\r
448 | Tlam(v,t) -> 1 + (aux (eat_lam t))
\r
449 in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms
\r
452 (* funzione di traduzione brutta & cattiva *)
\r
454 let rec aux = function
\r
455 | Tlam _ -> assert false
\r
460 let t1' = aux t1 in
\r
463 else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero])
\r
464 in Tapp(t1', aux t2')
\r
468 (* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *)
\r
469 let rec dummize = function
\r
470 | Tlam _ -> assert false
\r
471 | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c)
\r
474 if alive (hd t1) = 0
\r
475 then Tapp(dummize t1, dummy)
\r
476 else Tapp(dummize t1, dummize t2)
\r
479 (* lista di sottotermini applicativi *)
\r
480 let rec subterms = function
\r
481 | Tlam _ -> assert false
\r
482 | Tvar _ as v -> [v]
\r
483 | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2))
\r
486 (* filtra dai sottotermini le variabili *)
\r
487 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;
\r
490 let rec stupid_uniq = function
\r
492 | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)
\r
494 let stupid_compare a b =
\r
495 let rec size = function
\r
496 | Tvar(_,None,_) -> 0
\r
497 | Tvar(_,Some(_,t),_) -> 1 + size t
\r
498 | Tapp(t1,t2) -> 1 + size t1 + size t2
\r
499 | Tlam _ -> assert false
\r
500 in compare (size a) (size b)
\r
502 let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);;
\r
504 (* crea i match ricorsivamente.
\r
505 - k e' lo special-K
\r
506 - subs e' l'insieme dei sottotermini
\r
507 TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione
\r
509 let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf =
\r
510 let req t = try List.assoc t acc with Not_found -> `Var 9999 in
\r
512 if t1 = dummy then `Var 99999 else
\r
513 (* let _ = print_term t1 in *)
\r
514 let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs
\r
515 in if cont = [] then
\r
516 try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else
\r
517 let a = alive (hd t1) in
\r
518 if a = 0 then `Lam (req (Tapp(t1, dummy)))
\r
520 let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero]
\r
521 (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))
\r
522 in let _ = print_term (mk_apps dummy vars) *)
\r
523 in let vars = List.map req vars
\r
524 in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *)
\r
525 in let vars = Listx.from_list vars
\r
526 in let body = `I(0, vars)
\r
527 in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont
\r
528 in let bs = ref(branches)
\r
531 in `Lam (`Match(body, lift, bs, args))
\r
537 let rec aux n prev =
\r
538 if n = 0 then [zero]
\r
539 else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev
\r
543 let is_scott_n t n =
\r
544 let open Lambda3 in let open Pure in
\r
545 let rec aux n = function
\r
546 | L (L (A (V 1, L (V 0)))) -> n = 0
\r
547 | L (L (A (V 0, t))) -> aux (n-1) t
\r
548 | _ -> assert false
\r
553 let magic strings k h = (
\r
554 let tms = parse strings
\r
555 in let tms = List.map (fun x -> Tapp(x, zero)) tms
\r
556 in let tms' = List.map (setalive h) tms
\r
557 in let tms' = List.map (translate k) tms'
\r
558 in let tms' = List.map dummize tms'
\r
559 (* in let bullet = ">" / "•" *)
\r
560 (* in let progress s = print_endline (bullet ^^ fancy_of_string s) *)
\r
561 in let progress = print_h1
\r
562 in let _ = progress "traduzione completata"
\r
563 (* in let _ = List.map print_term tms' *)
\r
564 in let _ = progress "ordino i sottotermini"
\r
565 in let subs = List.concat (List.map subterms tms')
\r
566 in let subs = stupid_sort_uniq subs
\r
567 (* metti gli zeri in testa, perche' vanno calcolati per primi *)
\r
568 in let zeros = mk_zeros k
\r
569 in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)
\r
570 in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs))
\r
571 in let vars = vars subs
\r
572 (* in let _ = List.iter print_term subs *)
\r
573 (* in let _ = 0/0 *)
\r
574 in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars
\r
575 (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *)
\r
576 in let _ = progress "sto creando i match"
\r
577 (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *)
\r
578 in let f t acc = let res = crea_match k subs acc t in (t,res)::acc
\r
579 in let acc = List.fold_right f subs []
\r
580 in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc
\r
581 in let _ = progress "match creati"
\r
582 in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " ↦ ") ^^ fancy_of_nf y)) sigma
\r
584 in let _ = progress "controllo di purezza";
\r
585 in let open Lambda3
\r
586 in let ps, _ = Lambda3.parse' strings
\r
587 in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps
\r
588 in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps
\r
589 in let sigma = List.map (
\r
590 function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false
\r
593 List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma
\r
594 in let _ = List.iteri (fun i n ->
\r
595 (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *)
\r
596 (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *)
\r
597 assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps
\r
598 in let _ = progress "fatto." in ()
\r
601 let do_everything tms =
\r
602 let tms' = parse tms in
\r
603 let k = compute_special_k tms' in
\r
604 let h = compute_special_h tms' in
\r
605 (* let _ = print_string_endline (string_of_int h) in *)
\r
610 let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in
\r
612 (* let tms = ["x c" ; "b (x c d e)"; "b"] in *)
\r
614 (* let tms = ["x x x"] in *)
\r
615 let tms' = parse tms in
\r
616 let k = compute_special_k tms' in
\r
617 let h = compute_special_h tms' in
\r
618 (* let _ = print_string_endline (string_of_int h) in *)
\r
622 (* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option
\r
625 | Tapp' of term' * term' * (* active *) bool
\r
626 | Tlam' of int * term'
\r
629 let rec iter mustapply =
\r
631 | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b)
\r
632 | Tvar' _ as v -> v
\r
633 | Tapp'(t1, t2, b) -> if b &&
\r