8 ; ps: i_n_var list (* the n-th inert must become n *)
9 ; sigma: (int * nf) list (* the computed substitution *)
10 ; deltas: (int * nf) list ref list (* collection of all branches *)
13 let print_problem {freshno; ps; deltas} =
14 let deltas = String.concat "\n" (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
15 let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
16 deltas ^ (if deltas = "" then "" else "\n") ^
17 String.concat "\n" (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps)
20 let make_fresh_var freshno =
23 let make_fresh_vars p m =
28 let freshno,vars = aux (n-1) in
29 let freshno,v = make_fresh_var freshno in
30 freshno,`Var (0,v)::vars
31 | _ -> assert false in
32 let freshno,vars = aux m in
33 {p with freshno}, vars
35 let simple_expand_match ps =
36 let rec aux level = function
37 | #i_num_var as t -> aux_i_num_var level t
38 | `Lam(b,t) -> `Lam(b, aux (level+1) t)
39 and aux_i_num_var level = function
40 | `Match(ar,u,bs_lift,bs,args) as torig ->
41 let u = aux_i_num_var level u in
42 bs := List.map (fun (n, x) -> n, aux 0 x) !bs;
46 let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *)
47 in let t = mk_match ar (`N i) bs_lift bs args in
51 | _ -> raise Not_found)
53 `Match(ar,cast_to_i_num_var u,bs_lift,bs,List.map (aux level) args))
54 | `I(ar,k,args) -> `I(ar,k,Listx.map (aux level) args)
55 | `N _ | `Var _ as t -> t
58 let rec super_simplify_ps ps it =
59 let it' = List.map (fun t -> cast_to_i_num_var (simple_expand_match ps t)) (it :> i_num_var list) in
60 if it <> it' then super_simplify_ps ps it' else it'
62 let super_simplify ({ps} as p) =
63 let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in
64 {p with ps=List.map cast_to_i_n_var ps}
66 let subst_in_problem x inst ({freshno; ps; sigma} as p) =
67 let len_ps = List.length ps in
68 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
69 prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
70 let rec aux ((freshno,acc_ps,acc_new_ps) as acc) =
74 (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
75 let t = subst false x inst (t :> nf) in
76 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
77 let freshno,new_t,acc_new_ps =
78 expand_match (freshno,acc_ps@`Var(-1,max_int/3)::todo_ps,acc_new_ps) t
80 aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
82 and expand_match ((freshno,acc_ps, acc_new_ps) as acc) t =
84 | `Match(ar,u',bs_lift,bs,args) ->
85 let freshno,u,acc_new_ps = expand_match acc (u' :> nf) in
90 let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in
91 let super_simplified_ps = super_simplify_ps ps ps in
92 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
93 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;
94 List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*)
95 match index_of_opt ~eq:eta_eq super_simplified_ps u with
96 Some i -> acc_new_ps, i
97 | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps
100 if List.exists (fun (j,_) -> i=j) !bs then
103 let freshno,v = make_fresh_var freshno in
104 bs := !bs @ [i, `Var (ar - 1,v)] ;
106 (*prerr_endlie ("t DA RIDURRE:" ^ print (`Match(`N i,arity,bs_lift,bs,args) :> nf) ^ " more_args=" ^ string_of_int more_args);*)
107 let t = mk_match ar (`N i) bs_lift bs args in
108 (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
109 expand_match (freshno,acc_ps,acc_new_ps) t
111 (* the cast will fail *)
112 (* freshno,(cast_to_i_n_var t),acc_new_ps *)
115 let x = simple_expand_match (acc_ps@acc_new_ps) x in
116 freshno,cast_to_i_num_var x,acc_new_ps in
117 let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in
118 let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in
119 (let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
120 prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst));
121 let p = {p with freshno; ps; sigma = sigma@[x,inst]} in
122 let p = super_simplify p in
123 prerr_endline (print_problem p); p
127 let rec dangerous arities showstoppers =
132 | `Match(_,t,liftno,bs,args) ->
133 (* CSC: XXX partial dependency on the encoding *)
135 `N _ -> List.iter (dangerous arities showstoppers) args
136 | `Match _ as t -> dangerous arities showstoppers t ; List.iter (dangerous arities showstoppers) args
137 | `Var (_,x) -> dangerous_inert arities showstoppers x args 2 (* 2 coming from Scott's encoding *)
138 | `I(_,x,args') -> dangerous_inert arities showstoppers x (Listx.to_list args' @ args) 2 (* 2 coming from Scott's encoding *)
140 | `I(_,k,args) -> dangerous_inert arities showstoppers k (Listx.to_list args) 0
142 and dangerous_inert arities showstoppers k args more_args =
143 List.iter (dangerous arities showstoppers) args ;
144 if List.mem k showstoppers then raise Dangerous else
146 let _,_,y = List.find (fun (v,_,_) -> v=k) arities in
147 let arity = match y with `Var _ -> 0 | `I(_,_,args) -> Listx.length args | _ -> assert false in
148 if List.length args + more_args > arity then raise Dangerous else ()
152 (* inefficient algorithm *)
153 let edible arities showstoppers ps =
154 let rec aux showstoppers =
157 | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers ->
158 (* se la testa di x e' uno show-stopper *)
159 let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in
160 (* aggiungi tutte le variabili libere di x *)
161 if List.length showstoppers <> List.length new_showstoppers then
162 aux new_showstoppers ps
167 None -> aux showstoppers xs
170 dangerous arities showstoppers (x : i_n_var :> nf) ;
174 aux (sort_uniq (h::showstoppers)) ps
178 let precompute_edible_data {ps} xs =
180 let y = List.find (fun y -> hd_of y = Some x) ps in
181 x, index_of ~eq:eta_eq y ps, y) xs
184 let critical_showstoppers p =
185 let p = super_simplify p in
186 let showstoppers_step =
187 List.concat (List.map (fun bs ->
188 let heads = List.map (fun (i,_) -> List.nth p.ps i) !bs in
189 let heads = List.sort compare (filter_map hd_of heads) in
190 snd (split_duplicates heads)
192 let showstoppers_step = sort_uniq showstoppers_step in
193 let showstoppers_eat =
194 let heads_and_arities =
195 List.sort (fun (k,_) (h,_) -> compare k h)
196 (filter_map (function `Var (_,k) -> Some (k,0) | `I(_,k,args) -> Some (k,Listx.length args) | _ -> None ) p.ps) in
197 let rec multiple_arities =
201 | (x,i)::(y,j)::tl when x = y && i <> j ->
202 x::multiple_arities tl
203 | _::tl -> multiple_arities tl in
204 multiple_arities heads_and_arities in
206 let showstoppers_eat = sort_uniq showstoppers_eat in
207 let showstoppers_eat = List.filter
208 (fun x -> not (List.mem x showstoppers_step))
210 List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ string_of_var v)) showstoppers_step;
211 List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ string_of_var v)) showstoppers_eat;
212 p, showstoppers_step, showstoppers_eat
216 let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
217 let showstoppers = showstoppers_step @ showstoppers_eat in
218 let heads = List.sort compare (filter_map hd_of ps) in
219 let arities = precompute_edible_data p (uniq heads) in
220 let showstoppers = edible arities showstoppers ps in
221 let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
223 List.fold_left (fun p (x,pos,(xx : i_n_var)) ->
224 let n = match xx with `I(_,_,args) -> Listx.length args | _ -> 0 in
226 let inst = make_lams v n in
227 (let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in
228 prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst));
229 (* CSC: XXX to avoid applied numbers in safe positions that
230 trigger assert failures subst_in_problem x inst p*)
231 { p with sigma = p.sigma @ [x,inst] }
236 let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in
245 match List.nth ps n with
250 let p = { p with ps } in
251 if l <> [] then prerr_endline (print_problem p);
252 if List.for_all (function `N _ -> true | _ -> false) ps then
257 let instantiate p x n =
258 let p,vars = make_fresh_vars p n in
259 let freshno,zero = make_fresh_var p.freshno in
260 let p = {p with freshno} in
261 let zero = Listx.Nil (`Var (0,zero)) in
262 let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in
264 let inst = `Lam(false,`Match(-1,`I(-1,0,Listx.map (lift 1) args),1,bs,[])) in
265 let p = {p with deltas=bs::p.deltas} in
266 subst_in_problem x inst p
269 let compute_special_k tms =
270 let rec aux k (t: nf) = Pervasives.max k (match t with
271 | `Lam(b,t) -> aux (k + if b then 1 else 0) t
272 | `I(_, n, tms) -> Listx.max (Listx.map (aux 0) tms)
273 | `Match(_, t, liftno, bs, args) ->
274 List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
277 ) in Listx.max (Listx.map (aux 0) tms)
280 let auto_instantiate (n,p) =
281 let ({ps} as p), showstoppers_step, showstoppers_eat = critical_showstoppers p in
283 match showstoppers_step, showstoppers_eat with
285 prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
287 let heads = List.sort compare (filter_map (fun t -> match t with `Var _ -> None | x -> hd_of x) ps) in
291 prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
294 prerr_endline ("INSTANTIATING " ^ string_of_var x);
296 (* Strategy that decreases the special_k to 0 first (round robin)
297 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
300 (match hd_of (List.find (fun t -> compute_special_k (Listx.Nil (t :> nf)) > 0) ps) with
303 prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
308 (* Instantiate in decreasing order of compute_special_k
309 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
312 (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) ps)))) with
315 prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
321 compute_special_k (Listx.from_list (p.ps :> nf list) )in
322 if special_k < n then
323 prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@");
324 let p = instantiate p x special_k in
327 let problem_measure {ps} =
328 (* let rec term_size_i_n_var =
332 (List.fold_right (fun (a,b) c -> 10 + ((a+1) * term_size b) + c) (List.mapi (fun x y -> (x,y)) (Listx.to_list nfs)) 0)
337 | #i_n_var as t -> term_size_i_n_var t
338 | `Match(t,lift,bs,args) -> 1 + (term_size (t :> nf)) + 1 + (List.fold_right ((+) ++ term_size) args 0)
339 | `Lam(b,t) -> (if b then 0 else 1) + term_size t
340 (* in List.fold_right ((+) ++ term_size_i_n_var) ps 0;; *)
344 let rec auto_eat (n,({ps} as p)) =
348 let p' = auto_instantiate (n,p) in
349 let m' = problem_measure (snd p') in
350 let delta = m' - problem_measure p in
352 then print_endline ("$$$$ MEASURE DID NOT DECREASE (after inst) delta=" ^ string_of_int delta));
353 let p'' = auto_eat p' in
354 (if m' <= problem_measure p''
355 then print_endline ("$$$$ MEASURE DID NOT DECREASE (after eat) $$$"));
360 prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@");
367 x y = y 0 a y = k k z = z 0 c y = k y u = u h1 h2 0 h2 a = h3
368 1 x a c 1 a 0 c 1 k c 1 c 0 1 k 1 k 1 k
369 2 x a y 2 a 0 y 2 k y 2 y 0 2 y 0 2 h2 0 2 h3
370 3 x b y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 y 3 b 0 (\u. u h1 h2 0) 3 b 0 (\u. u h1 (\w.h3) 0)
371 4 x b c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c 4 b 0 c
372 5 x (b e) 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0 5 b e 0
373 6 y y 6 y y 6 y y 6 y y 6 y y 6 h1 h1 h2 0 h2 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0
376 b u = u l1 l2 0 e _ _ _ _ = f l3 n = n j 0
379 3 l2 0 (\u. u h1 (\w. h3) 0) 3 l3 (\u. u h1 (\w. h3) 0) 3 j h1 (\w. h3) 0 0
380 4 l2 0 c 4 l3 c 4 c j 0
381 5 e l1 l2 0 0 5 f 5 f
382 6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0 6 h1 h1 (\w. h3) 0 (\w. h3) 0
387 x a (b (a c)) a 0 = 1 ? (b (a c)) 8
388 x a (b d') a 0 = 1 ? (b d') 7
389 x b (a c) b 0 = 1 ? (a c) 4
390 x b (a c') b 0 = 1 ? (a c') 5
398 b 4 = 8 (* b (a c) *)
403 (************** Tests ************************)
405 let optimize_numerals p =
406 let replace_in_sigma perm =
407 let rec aux = function
408 | `N n -> `N (List.nth perm n)
409 | `I _ | `Var _ -> assert false
410 | `Lam(v,t) -> `Lam(v, aux t)
411 | `Match(_,_,_,bs,_) as t -> (bs := List.map (fun (n,t) -> (List.nth perm n, t)) !bs); t
412 in List.map (fun (n,t) -> (n,aux t))
414 let deltas' = List.mapi (fun n d -> (n, List.map fst !d)) p.deltas in
415 let maxs = Array.to_list (Array.init (List.length deltas') (fun _ -> 0)) in
416 let max = Listx.max (Listx.from_list (
417 List.concat (List.map snd deltas')
419 let perm,_ = List.fold_left (fun (perm, maxs) (curr_n:int) ->
420 let containing = filter_map (fun (i, bs) -> if List.mem curr_n bs then Some i else None) deltas' in
421 (* (prerr_endline (string_of_int curr_n ^ " occurs in: " ^ (String.concat " " (List.map string_of_int containing)))); *)
422 let neww = Listx.max (Listx.from_list (List.mapi (fun n max -> if List.mem n containing then max else 0) maxs)) in
423 let maxs = List.mapi (fun i m -> if List.mem i containing then neww+1 else m) maxs in
425 ) ([],maxs) (Array.to_list (Array.init (max+1) (fun x -> x))) in
426 replace_in_sigma (List.rev perm) p.sigma
429 prerr_endline "########## main ##########";;
432 v ==> v := \a. a k1 .. kn \^m.0
433 + ==> v := \^k. numero for every v such that ...
434 * ==> tries v as long as possible and then +v as long as possible
437 let rec aux ({ps} as p) n l =
438 if List.for_all (function `N _ -> true | _ -> false) ps then begin
442 let _ = prerr_endline (print_problem p) in
446 | [] -> read_line (),[] in
455 | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *)
457 let x = var_of_string x in
458 aux (instantiate p x n) n l
459 | `Auto -> aux (auto p n) n l
463 let p_finale = aux p n cmds in
464 let freshno,sigma = p_finale.freshno, p_finale.sigma in
465 prerr_endline "------- <DONE> ------";
466 prerr_endline (print_problem p);
467 prerr_endline "---------------------";
468 let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
469 List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
471 prerr_endline "----------------------";
473 List.fold_left (fun ps (x,inst) ->
474 (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *)
475 (* In this non-recursive version, the intermediate states may containt Matchs *)
476 List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps)
477 (p.ps :> i_num_var list) sigma in
478 prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno});
479 List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ;
481 prerr_endline "---------<OPT>----------";
482 let sigma = optimize_numerals p_finale in (* optimize numerals *)
483 let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
484 List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
485 prerr_endline "---------<PURE>---------";
486 let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in
487 let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in
488 (*let ps_ok = List.fold_left (fun ps (x,inst) ->
489 List.map (Pure.subst false x inst) ps) ps sigma in*)
497 e,Pure.lift (-n-1) (let t = (snd (List.find (fun (i,_) -> i = n) sigma)) in prerr_endline (string_of_var n ^ " := " ^ Pure.print t); t),[]
499 Not_found -> [],Pure.V n,[])::e
503 prerr_endline "---------<PPP>---------";
505 "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]"
507 prerr_endline (print_e e);
508 List.iter (fun (t,t_ok) ->
509 prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok);
510 (*assert (Pure.unwind (e,t,[]) = t_ok)*)
511 ) (List.combine ps ps_ok);
513 prerr_endline "--------<REDUCE>---------";
514 List.iteri (fun i n ->
515 (*prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));*)
516 let t = Pure.mwhd (e,n,[]) in
517 prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t));
518 assert (t = Scott.mk_n i)
520 prerr_endline "-------- </DONE> --------"
523 (********************** problems *******************)
525 let zero = `Var (0,0);;
530 | `Var _ as i -> cast_to_i_n_var (mk_app i zero)
534 type t = problem * int * string list;;
536 let magic strings cmds =
537 let tms, _ = parse' strings in (* *)
538 let tms = sort_uniq ~compare:eta_compare tms in
539 let special_k = compute_special_k (Listx.from_list tms) in (* compute special K *)
540 let fv = sort_uniq (List.concat (List.map free_vars tms)) in (* free variables *)
541 let tms = List.map cast_to_i_n_var tms in (* cast nf list -> i_n_var list *)
542 let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *)
543 (*let _ = prerr_endline ("Free vars: " ^ String.concat ", " (List.map string_of_var fv)) in*)
544 let freshno = Listx.max (Listx.from_list fv) in
545 let dummy = `Var (-1,max_int / 2) in
546 let deltas = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
547 {freshno; ps; sigma=[] ; deltas}, special_k, cmds
550 let magic_conv ~div:_ ~conv:_ ~nums:_ _ = assert false;;