From: acondolu Date: Fri, 14 Jul 2017 15:20:42 +0000 (+0200) Subject: Changed logic of entrypoint in Lambda4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=608c40045f651c6402b17c437f997de4d63f6afd;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 --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index b0e4bc9..5422704 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -35,7 +35,6 @@ type problem = 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 @@ -275,7 +274,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 ;; @@ -700,139 +699,150 @@ 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 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 +;; -(* - 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 "-------- --------" - ) +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" ;; -(********************** problems *******************) +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 `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 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; 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 should_fail f = - try - solve (f ()); - failwith "The problem should have failed" - with Fail _ -> - prerr_endline "The problem failed, as expected" + 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 | Some `Bottom -> 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 trail = [] in + let p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} in + p, check p ;; diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli index 8f6019e..0b92ad9 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -1,4 +1,17 @@ type problem -val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem -val solve: problem -> unit -val should_fail: (unit -> problem) -> unit + +type response = [ + | `CompleteSeparable of string + | `CompleteUnseparable of string + | `Uncomplete +] + +type result = [ + `Complete | `Uncomplete +] * [ + | `Separable of (int * Num.nf) list + | `Unseparable of string +] + +val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem * response +val solve: problem * response -> result diff --git a/ocaml/num.ml b/ocaml/num.ml index d9cdf37..962feaf 100644 --- a/ocaml/num.ml +++ b/ocaml/num.ml @@ -172,6 +172,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 _ | `Bottom | `Pacman as t -> t | `Lam(false, t) -> `Lam(false, set_arity arity t) diff --git a/ocaml/problems.ml b/ocaml/problems.ml index b49cf77..55ed9e9 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,9 +1,29 @@ 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)"] []);; *) (* 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"]; @@ -100,8 +120,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 *) @@ -260,9 +279,9 @@ solve_many (List.map ((|>) ()) [ o1; o2; o3; o4; o5; o6 ]);; -should_fail(fun () -> problem_of None ["BOT"] []);; -should_fail(fun () -> problem_of (Some"x y") ["x BOMB"] []);; -should_fail(fun () -> problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);; +assert_unseparable(problem_of None ["BOT"] []);; +assert_unseparable(problem_of (Some"x y") ["x BOMB"] []);; +assert_unseparable(problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);; solve_many [ problem_of