X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=c376f01fe85a195e28f2a9fc0524febf97a70522;hb=87e0182247e9176ec3612eaf3c7f90b81f43b6f5;hp=62837b2fd9842ce177e507737d3b8ffd89a6ea4c;hpb=755d93e13cb4f05e987406d8702567ad7af09dd9;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 62837b2..c376f01 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -11,6 +11,11 @@ let bomb = ref(`Var(-1,-666));; For Scott's encoding, two. *) let num_more_args = 2;; +let _very_verbose = false;; + +let verbose s = + if _very_verbose then prerr_endline s +;; let convergent_dummy = `N ~-1; @@ -58,7 +63,7 @@ let string_of_measure (a,b) = "(fakevars="^string_of_int a^",sum_arities="^strin let problem_measure p = sum_arities p;; let string_of_measure = string_of_int;; -let print_problem label ({freshno; div; conv; ps; deltas} as p) = +let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - "); let nl = "\n" in @@ -79,7 +84,7 @@ let print_problem label ({freshno; div; conv; ps; deltas} as p) = let failwithProblem p reason = - print_endline (print_problem "FAIL" p); + print_endline (string_of_problem "FAIL" p); failwith reason ;; @@ -227,7 +232,7 @@ prerr_endline ("# INST: " ^ string_of_var x ^ " := " ^ print ~l inst)); ); let p = {p with sigma = sigma@[x,inst]} in let p = super_simplify p in - prerr_endline (print_problem "instantiate" p); + prerr_endline (string_of_problem "instantiate" p); p ;; @@ -450,7 +455,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let old_conv = p.conv in let p = { p with ps; conv } in if l <> [] || old_conv <> conv - then prerr_endline (print_problem "eat" p); + then prerr_endline (string_of_problem "eat" p); if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then `Finished p else @@ -526,7 +531,10 @@ let auto_instantiate (n,p) = prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x); x with - Not_found -> x in + Not_found -> + let arity_of_x = max_arity_tms x (all_terms p) in + assert (Util.option_get arity_of_x > 0); + x in (* Instantiate in decreasing order of compute_special_k 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s let x = @@ -652,107 +660,80 @@ let env_of_sigma freshno sigma should_explode = in aux 0 ;; -prerr_endline "########## main ##########";; - -(* Commands: - v ==> v := \a. a k1 .. kn \^m.0 - + ==> v := \^k. numero for every v such that ... - * ==> tries v as long as possible and then +v as long as possible -*) -let main problems = - let rec aux ({ps} as p) n l = - if List.for_all (function `N _ -> true | _ -> false) ps && p.div = None then begin - p - end else - let _ = prerr_endline (print_problem "main" p) in - let x,l = - match l with - | cmd::l -> cmd,l - | [] -> read_line (),[] in - let cmd = - if x = "+" then - `DoneWith - else if x = "*" then - `Auto - else - `Step x in - match cmd with - | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *) - | `Step x -> - let x = var_of_string x in - aux (instantiate p x n) n l - | `Auto -> aux (auto p n) n l - in - List.iter - (fun (p,n,cmds) -> - Console.print_hline(); - bomb := `Var (-1,-666); - let p_finale = aux p n cmds in - let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline ("------- ------\n "); - (* prerr_endline (print_problem "Original problem" p); *) - prerr_endline "---------------------"; - let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - prerr_endline (" BOMB == " ^ print ~l !bomb); - prerr_endline "---------------------"; - List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; +let solve p = + bomb := `Var(-1,-666); + if List.for_all (function `N _ -> true | _ -> false) p.ps && p.div = None + then (prerr_endline "Initial problem is already completed, nothing to do") + else ( + Console.print_hline(); + prerr_endline (string_of_problem "main" p); + let p_finale = auto p p.initialSpecialK in + let freshno,sigma = p_finale.freshno, p_finale.sigma in + prerr_endline ("------- ------ measure=. \n "); + (* prerr_endline (string_of_problem "Original problem" p); *) + (* prerr_endline "---------------------"; *) + let l = Array.to_list (Array.init (freshno + 1) string_of_var) in + (* prerr_endline "---------------------"; *) + List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; (* - prerr_endline "----------------------"; - let ps = - List.fold_left (fun ps (x,inst) -> - (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *) - (* In this non-recursive version, the intermediate states may containt Matchs *) - List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps) - (p.ps :> i_num_var list) sigma in - prerr_endline (print_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno}); - List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; + prerr_endline "----------------------"; + let ps = + List.fold_left (fun ps (x,inst) -> + (* CSC: XXXX Is the subst always sorted correctly? Otherwise, implement a recursive subst *) + (* In this non-recursive version, the intermediate states may containt Matchs *) + List.map (fun t -> let t = subst false x inst (t :> nf) in cast_to_i_num_var t) ps) + (p.ps :> i_num_var list) sigma in + prerr_endline (string_of_problem {p with ps= List.map (function t -> cast_to_i_n_var t) ps; freshno}); + List.iteri (fun i (n,more_args) -> assert (more_args = 0 && n = `N i)) ps ; *) - prerr_endline "-------------------"; - let sigma = optimize_numerals p_finale in (* optimize numerals *) - let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; - prerr_endline "------------------"; - let div = option_map (fun div -> ToScott.t_of_nf (div :> nf)) p.div in - let conv = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.conv in - let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) p.ps in - let sigma = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in - (*let ps_ok = List.fold_left (fun ps (x,inst) -> - List.map (Pure.subst false x inst) ps) ps sigma in*) - let e = env_of_sigma freshno sigma true in - let e' = env_of_sigma freshno sigma false in + prerr_endline "-------------------"; + let sigma = optimize_numerals p_finale in (* optimize numerals *) + let l = Array.to_list (Array.init (freshno + 1) string_of_var) in + List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma; + + prerr_endline "------------------"; + let t_of_nf t = ToScott.t_of_nf (t :> nf) in + let div = option_map t_of_nf p.div in + let conv = List.map t_of_nf p.conv in + let ps = List.map t_of_nf p.ps in + + let sigma' = List.map (fun (x,inst) -> x, ToScott.t_of_nf inst) sigma in + let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in (* - prerr_endline "------------------"; + prerr_endline "------------------"; let rec print_e e = - "[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]" +"[" ^ String.concat ";" (List.map (fun (e,t,[]) -> print_e e ^ ":" ^ Pure.print t) e) ^ "]" in - prerr_endline (print_e e); - List.iter (fun (t,t_ok) -> - prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok); - (*assert (Pure.unwind (e,t,[]) = t_ok)*) - ) (List.combine ps ps_ok); + prerr_endline (print_e e); + List.iter (fun (t,t_ok) -> + prerr_endline ("T0= " ^ Pure.print t ^ "\nTM= " ^ Pure.print (Pure.unwind (e,t,[])) ^ "\nOM= " ^ Pure.print t_ok); + (*assert (Pure.unwind (e,t,[]) = t_ok)*) + ) (List.combine ps ps_ok); *) - prerr_endline "-----------------"; - (function Some div -> - print_endline (Pure.print div); - let t = Pure.mwhd (e',div,[]) in - prerr_endline ("*:: " ^ (Pure.print t)); - prerr_endline (print !bomb); - assert (t = ToScott.t_of_nf (!bomb:>nf)) - | None -> ()) div; - List.iter (fun n -> - prerr_endline ("_::: " ^ (Pure.print n)); - let t = Pure.mwhd (e,n,[]) in - prerr_endline ("_:: " ^ (Pure.print t)) - ) conv ; - List.iteri (fun i n -> - prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n)); - let t = Pure.mwhd (e,n,[]) in - prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t)); - assert (t = Scott.mk_n i) - ) ps ; - prerr_endline "-------- --------" - ) problems + prerr_endline "-----------------"; + let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *) + (function Some div -> + print_endline (Pure.print div); + let t = Pure.mwhd (e',div,[]) in + prerr_endline ("*:: " ^ (Pure.print t)); + assert (t = pure_bomb) + | None -> ()) div; + List.iter (fun n -> + verbose ("_::: " ^ (Pure.print n)); + let t = Pure.mwhd (e',n,[]) in + verbose ("_:: " ^ (Pure.print t)); + assert (t <> pure_bomb) + ) conv ; + List.iteri (fun i n -> + verbose ((string_of_int i) ^ "::: " ^ (Pure.print n)); + let t = Pure.mwhd (e',n,[]) in + verbose ((string_of_int i) ^ ":: " ^ (Pure.print t)); + assert (t = Scott.mk_n i) + ) ps ; + prerr_endline "-------- --------" + ) +;; (********************** problems *******************) @@ -765,10 +746,8 @@ let append_zero = | _ -> assert false ;; -type t = problem * int * string list;; - -let magic_conv ~div ~conv ~nums cmds = - let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in +let problem_of ~div ~conv ~nums = + let all_tms = (match div with None -> [] | Some div -> print_endline(div);[div]) @ nums @ conv in let all_tms, var_names = parse' all_tms in let div, (tms, conv) = match div with | None -> None, list_cut (List.length nums, all_tms) @@ -777,22 +756,32 @@ let magic_conv ~div ~conv ~nums cmds = if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv) then ( prerr_endline "--- TEST SKIPPED ---"; - {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}, 0, [] + {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0} ) else let tms = sort_uniq ~compare:eta_compare tms in let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) (* casts *) - let div = option_map cast_to_i_var div in - let conv = Util.filter_map (function #i_n_var as t -> Some (cast_to_i_n_var t) | _ -> None) conv in - let tms = List.map cast_to_i_n_var tms in + let div = + match div with + | None -> None + | Some (`I _ as t) -> Some t + | _ -> raise (Failure "div is not an inert or BOT in the initial problem") in + let conv = Util.filter_map ( + function + | #i_n_var as t -> Some t + | `Lam _ -> None + | _ -> raise (Failure "A term in conv is not i_n_var") + ) conv in + let tms = List.map ( + function + | #i_n_var as y -> y + | _ -> raise (Failure "A term in num is not i_n_var") + ) tms in let ps = List.map append_zero tms in (* crea lista applicando zeri o dummies *) let freshno = List.length var_names in let deltas = let dummy = `Var (max_int / 2, -666) in [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in - - {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}, special_k, cmds + {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k} ;; - -let magic strings cmds = magic_conv None [] strings cmds;;