X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=7b669ca3789880e524c6d6870d1111a64999cfba;hb=a34071ed728b8de44b198de4e73a52207557ed81;hp=6ceb9f387d516d401301f821c8d3e6cb16960f54;hpb=58f1518398346a81ccd8d0b14a14565b8bff5276;p=fireball-separation.git diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 6ceb9f3..7b669ca 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -27,15 +27,18 @@ type problem = ; sigma: (int * nf) list (* the computed substitution *) ; deltas: discriminating_set ref list (* collection of all branches *) ; initialSpecialK: int + ; label : string + ; var_names : string list (* names of the original free variables *) ; trail: discriminating_set list list };; +let label_of_problem {label} = label;; + (* exceptions *) exception Pacman exception Bottom exception Backtrack of string -exception Fail of string let first bound p var f = let p = {p with trail = (List.map (!) p.deltas)::p.trail} in @@ -76,7 +79,7 @@ let string_of_measure = string_of_int;; let string_of_problem label ({freshno; div; conv; ps; deltas} as p) = Console.print_hline (); - prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - "); + prerr_string ("\n(* DISPLAY PROBLEM (" ^ p.label ^ " - " ^ 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 @@ -113,7 +116,7 @@ let make_fresh_vars p arities = let simple_expand_match ps = let rec aux_nob level = function - | #i_num_var as t -> aux_i_num_var level t + | #i_num_var as t -> (aux_i_num_var level t :> nf) | `Lam(b,t) -> `Lam(b,aux (level+1) t) | `Pacman as t -> t and aux level = function @@ -121,20 +124,20 @@ let simple_expand_match ps = | #nf_nob as t -> aux_nob level t and aux_i_num_var level = function | `Match(u,v,bs_lift,bs,args) as torig -> - let u = aux_i_num_var level u in + let (u : i_num_var) = aux_i_num_var level u in bs := List.map (fun (n, x) -> n, aux 0 x) !bs; (try (match u with | #i_n_var as u -> - let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *) - in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in + let i = index_of ~eq:eta_eq (lift (-level) u) (ps :> nf list) in (* can raise Not_found *) + let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in if t <> torig then - aux level (t :> nf) - else raise Not_found + aux_i_num_var level t + else raise Not_found | _ -> raise Not_found) with Not_found -> - mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args)) - | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args)) + cast_to_i_num_var (mk_appl (`Match(u,v,bs_lift,bs,[])) (List.map (aux_nob level) args))) + | `I(v,args) -> cast_to_i_num_var (mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args))) | `N _ | `Var _ as t -> t in aux_i_num_var 0 ;; @@ -157,7 +160,7 @@ let super_simplify ({div; ps; conv} as p) = let div = option_map (fun div -> let divs = super_simplify_ps p.ps ([div] :> i_n_var list) in List.hd divs) div in - {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv} + {p with div=option_map cast_to_i_var div; ps; conv} let cast_to_ps_with_match = function @@ -275,7 +278,7 @@ exception Dangerous let arity_of arities k = let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in - let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | _ -> assert false in + let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in arity + if pos = -1 then - 1 else 0 ;; @@ -573,7 +576,7 @@ let choose_step (n,p) = with Not_found -> let arity_of_x = max_arity_tms x (all_terms p) in - assert (Util.option_get arity_of_x > 0); + 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 @@ -700,139 +703,116 @@ let env_of_sigma freshno sigma = Not_found -> ([],Pure.V n,[]))::e in aux 0 ;; +(* ************************************************************************** *) + +type response = [ + | `CompleteSeparable of string + | `CompleteUnseparable of string + | `Uncomplete +] + +type result = [ + `Complete | `Uncomplete +] * [ + | `Separable of (int * Num.nf) list + | `Unseparable of string +] + +let run p = + 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 "); + 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; -let solve p = - 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 = - try - auto p p.initialSpecialK - with Backtrack _ -> raise (Fail "Unsolvable problem, apparently") 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 (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 scott_of_nf t = ToScott.scott_of_nf (t :> nf) in - let div = option_map scott_of_nf p.div in - let conv = List.map scott_of_nf p.conv in - let ps = List.map scott_of_nf p.ps in - - let sigma' = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in - let e' = env_of_sigma freshno sigma' in - -(* - prerr_endline "------------------"; -let rec print_e 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 "-----------------"; - (function Some div -> - print_endline (Pure.print div); - let t = Pure.mwhd (e',div,[]) in - prerr_endline ("*:: " ^ (Pure.print t)); - assert (t = Pure.B) - | None -> ()) div; - List.iter (fun n -> - verbose ("_::: " ^ (Pure.print n)); - let t = Pure.mwhd (e',n,[]) in - verbose ("_:: " ^ (Pure.print t)); - assert (t <> Pure.B) - ) 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 "-------- --------" - ) + 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 scott_of_nf t = ToScott.scott_of_nf (t :> nf) in + let div = option_map scott_of_nf p.div in + let conv = List.map scott_of_nf p.conv in + let ps = List.map scott_of_nf p.ps in + + let sigma' = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in + let e' = env_of_sigma freshno sigma' in + + prerr_endline "-----------------"; + (function Some div -> + print_endline (Pure.print div); + let t = Pure.mwhd (e',div,[]) in + prerr_endline ("*:: " ^ (Pure.print t)); + assert (t = Pure.B) + | None -> ()) div; + List.iter (fun n -> + verbose ("_::: " ^ (Pure.print n)); + let t = Pure.mwhd (e',n,[]) in + verbose ("_:: " ^ (Pure.print t)); + assert (t <> Pure.B) + ) 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 "-------- --------"; + p_finale.sigma ;; -(********************** problems *******************) - -let zero = `Var(0,0);; - -let append_zero = - function - | `I _ - | `Var _ as i -> cast_to_i_n_var (mk_app i zero) - | _ -> assert false +let solve (p, todo) = + let completeness, to_run = + match todo with + | `CompleteUnseparable s -> `Complete, `False s + | `CompleteSeparable _ -> `Complete, `True + | `Uncomplete -> `Uncomplete, `True in + match to_run with + | `False s -> completeness, `Unseparable s + | `True -> + try + let sigma = run p in + completeness, `Separable sigma + with + | Backtrack _ -> completeness, `Unseparable "backtrack" ;; -let problem_of ~div ~conv ~nums = - let all_tms = (match div with None -> [] | Some 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) - | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in - - 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; trail=[]} - ) 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 = - match div with - | None | Some `Bottom -> None - | Some (`I _ as t) -> Some t - | _ -> raise (Fail "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 (Fail "A term in conv is not i_n_var") - ) conv in - let tms = List.map ( - function - | #i_n_var as y -> y - | _ -> raise (Fail "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 - let trail = [] in - {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} +let check p = + (* TODO check if there are duplicates in p.ps + before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *) + (* FIXME what about initial fragments? *) + if (let rec f = function + | [] -> false + | hd::tl -> List.exists (eta_eq hd) tl || f tl in + f p.ps) + then `CompleteUnseparable "ps contains duplicates" + (* check if div occurs somewhere in ps@conv *) + else if (match p.div with + | None -> true + | Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv)) + ) && false (* TODO no bombs && pacmans *) + then `CompleteSeparable "no bombs, pacmans and div" + else if false (* TODO bombs or div fuori da lambda in ps@conv *) + then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" + else if p.div = None + then `CompleteSeparable "no div" + else `Uncomplete ;; -let should_fail f = - try - solve (f ()); - failwith "The problem should have failed" - with Fail _ -> - prerr_endline "The problem failed, as expected" +let problem_of (label, div, conv, ps, var_names) = + (* TODO: replace div with bottom in problem??? *) + let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ ps @ conv in + if all_tms = [] then failwith "problem_of: empty problem"; + let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in + 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 + let trail = [] in + let sigma = [] in + let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK; trail; var_names; label} in + p, check p ;;