From: acondolu Date: Fri, 14 Jul 2017 15:20:42 +0000 (+0200) Subject: Changed logic of entrypoint in Lambda4 X-Git-Tag: weak-reduction-separation~38 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5991691df6dc3d096a08397712040c93d7f873b5;p=fireball-separation.git Changed logic of entrypoint in Lambda4 - removed exception Fail - added "check",which checks if we are in a subproblem of separation on which we know to be complete - "solve" does not raise particular exceptions anymore, and the program raise failure only if there is some bug (cherry picked from commit 608c40045f651c6402b17c437f997de4d63f6afd) --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 355380e..fa9b043 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -244,7 +244,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 ;; @@ -663,33 +663,43 @@ let env_of_sigma freshno sigma should_explode = else ([],Pure.V n,[]))::e in aux 0 ;; +(* ************************************************************************** *) + +type result = [ + | `Separable of (int * Num.nf) list + | `Unseparable of string +] + +let check p = + (* check if there are duplicates in p.ps *) + (* 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 Some "ps contains duplicate entries" + (* check if div occurs somewhere in ps@conv *) + else match p.div with + | None -> None + | Some div -> + if (List.exists (eta_subterm div) (p.ps@p.conv)) + then Some "div occurs as subterm in ps or conv" + else None +;; -let solve p = +let solve p = + prerr_endline (string_of_problem "main" p); + match check p with + | Some s -> `Unseparable s + | None -> 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 (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 ; -*) + Console.print_hline(); + 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; + prerr_endline "-------------------"; let sigma = optimize_numerals p_finale in (* optimize numerals *) let l = Array.to_list (Array.init (freshno + 1) string_of_var) in @@ -704,17 +714,6 @@ let solve p = 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 "------------------"; -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 "-----------------"; let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *) (function Some div -> @@ -735,57 +734,55 @@ in verbose ((string_of_int i) ^ ":: " ^ (Pure.print t)); assert (t = Scott.mk_n i) ) ps ; - prerr_endline "-------- --------" - ) + prerr_endline "-------- --------"; + `Separable 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 + | `Var _ as i -> cast_to_i_n_var (mk_app i zero) + | `N _ -> raise (Parser.ParsingError " numbers in ps") ;; let problem_of ~div ~conv ~nums = let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in let all_tms, var_names = Parser.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} - ) 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 -> 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} + let div, (ps, 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 + + let div = + match div with + | None -> None + | Some (`I _ as t) -> Some t + | _ -> raise (Parser.ParsingError "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 (Parser.ParsingError "A term in conv is not i_n_var") + ) conv in + let ps = List.map ( + function + | #i_n_var as y -> y + | _ -> raise (Parser.ParsingError "A term in num is not i_n_var") + ) ps in + (* DA SPOSTARE NEI TEST: *) + let ps = List.map append_zero ps in (* crea lista applicando zeri o dummies *) + let ps = sort_uniq ~compare:eta_compare (ps :> nf list) in + let ps = List.map (cast_to_i_n_var) ps in + + (* TODO: *) + (* replace div with bottom in problem??? *) + + let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *) + 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 p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k} in + p ;; diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli index 761bef6..d8148d5 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -1,3 +1,9 @@ type problem + +type result = [ + | `Separable of (int * Num.nf) list + | `Unseparable of string +] + val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem -val solve: problem -> unit +val solve: problem -> result diff --git a/ocaml/num.ml b/ocaml/num.ml index f612def..36234ad 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -162,6 +162,7 @@ let cast_to_i_num_var = assert false (* algorithm failed *) let rec set_arity arity = function +(* FIXME because onlt variables should be in branches of matches, one day *) | `Var(n,_) -> `Var(n,arity) | `N _ as t -> t | `Lam(false, t) -> `Lam(false, set_arity arity t) diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 7cb068f..e01a741 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,9 +1,37 @@ open Lambda4;; -let solve_many = List.iter solve;; +open Util;; + +let assert_separable x = + match solve x with + | `Separable _ -> () + | `Unseparable s -> + failwith ("assert_separable: unseparable because: " ^ s ^ ".") +;; + +let assert_unseparable x = + match solve x with + | `Unseparable _ -> () + | `Separable _ -> + failwith ("assert_unseparable: separable.") +;; + +let solve_many = List.iter assert_separable;; + +(* TODO *) +(* div under a lambda in conv *) +(* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *) + +assert_unseparable (problem_of None [] (* 32 *) + ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))"; + "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)"; + "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))"; + "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))"; + "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))" + ]);; (* p-series problems *) -let f x = problem_of None [] x in -solve_many (List.map f [ +let f x = assert_separable (problem_of None [] x) in +List.iter f [ (* 2 *) [ "x y"; "x z" ; "x (y z)"]; (* 4 *) [ "x y"; "x (a. a x)" ; "y (y z)" ]; (* 5 *) ["a (x. x a) b"; "b (x. x b) a"]; @@ -70,13 +98,6 @@ solve_many (List.map f [ "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))"; "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))"; "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"]; - (* 32 *) - ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))"; - "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)"; - "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))"; - "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))"; - "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))" - ]; (* 33 *) (* Shows an error when the strategy that minimizes special_k is NOT used *) [ "((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))"; @@ -100,8 +121,7 @@ solve_many (List.map f [ "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"]; (* 37 *) (* issue with eta-equality of terms in ps *) ["x (a y) z"; "x (a z. y z) w"; "a c"]; - -]);; +];; (* q-series problems *) @@ -130,13 +150,13 @@ let q4 () = problem_of ;; let q5 () = problem_of - (Some"x") - ["(y. x)"] + (Some"x x") + ["x"] ["x"] ;; let q6 () = problem_of - (Some"x") + (Some"x x") ["(y. x z)"] ["y"] ;;