X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=c376f01fe85a195e28f2a9fc0524febf97a70522;hb=87e0182247e9176ec3612eaf3c7f90b81f43b6f5;hp=6c344acf6050b9af4f653fb4da0e65b04b6b380d;hpb=f69cf0859dd68582a4f44df43610f2514bfc0416;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 6c344ac..c376f01 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -11,6 +11,13 @@ 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; type problem = { freshno: int @@ -56,28 +63,28 @@ 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_endline ("\n||||| Displaying problem: " ^ label ^ " |||||"); - let nl = "\n| " in - let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in + prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - "); + let nl = "\n" in + let deltas = String.concat (nl^" ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in let l = Array.to_list (Array.init (freshno + 1) string_of_var) in - nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno - ^ nl ^ "\b> DISCRIMINATING SETS (deltas)" - ^ nl ^ deltas ^ (if deltas = "" then "" else nl) - ^ "\b> DIVERGENT" ^ nl - ^ "*: " ^ (match div with None -> "*" | Some div -> print ~l (div :> nf)) ^ "\n| " - ^ "\b> CONVERGENT" ^ nl - ^ String.concat "\n| " (List.map (fun t -> "_: " ^ (if t = `N (-1) then "_" else print ~l (t :> nf))) conv) ^ - (if conv = [] then "" else "\n| ") - ^ "\b> NUMERIC" ^ nl - ^ String.concat "\n| " (List.mapi (fun i t -> string_of_int i ^ ": " ^ print ~l (t :> nf)) ps) - ^ nl + "measure="^string_of_measure(problem_measure p) (* ^ " freshno = " ^ string_of_int freshno*) + ^ nl ^ " Discriminating sets (deltas):" + ^ nl ^ " " ^ deltas ^ (if deltas = " " then "" else nl) ^ "*)" + ^"(* DIVERGENT *)" ^ nl + ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl + ^" (* CONVERGENT *) [" ^ nl ^ " " + ^ String.concat "\n " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^ + (if conv = [] then "" else nl) + ^ "] (* NUMERIC *) [" ^ nl ^ " " + ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps) + ^ nl ^ "] [\"*\"];;" ^ nl ;; let failwithProblem p reason = - print_endline (print_problem "FAIL" p); + print_endline (string_of_problem "FAIL" p); failwith reason ;; @@ -225,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 ;; @@ -430,10 +437,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) let _ = List.find (fun h -> hd_of t = Some h) showstoppers in t) with Not_found -> match hd_of t with - | None -> assert (t = `N ~-1); t + | None -> assert (t = convergent_dummy); t | Some h -> prerr_endline ("FREEZING " ^ string_of_var h); - `N ~-1 (* convergent dummy*) + convergent_dummy ) (List.combine showstoppers_conv p.conv) in List.iter (fun bs -> @@ -448,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 @@ -524,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 = @@ -650,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 *******************) @@ -763,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) @@ -775,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;;