From: acondolu Date: Thu, 13 Jul 2017 15:38:23 +0000 (+0200) Subject: Tentative commit: tactics dropped and clean-up X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0991fc5486c3158fc361e84cbba5aefa67893ba4;p=fireball-separation.git Tentative commit: tactics dropped and clean-up --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 1be77d1..97a559a 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -9,6 +9,11 @@ open Num 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);; @@ -30,6 +35,7 @@ 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 @@ -677,104 +683,81 @@ let env_of_sigma freshno sigma = 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 (string_of_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 -> assert false - (* let x = var_of_string x in - aux (instantiate p x 1 n) n l *) - | `Auto -> aux (auto p n) n l - in - List.iter - (fun (p,n,cmds) -> - Console.print_hline(); - let p_finale = aux p n cmds in - let freshno,sigma = p_finale.freshno, p_finale.sigma in - prerr_endline ("------- ------\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; +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 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 "------------------"; + 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; - let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in - let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in - let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in + 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 + 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 "------------------"; + 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)); - assert (t = Pure.B) - | None -> ()) div; - List.iter (fun n -> - prerr_endline ("_::: " ^ (Pure.print n)); - let t = Pure.mwhd (e',n,[]) in - prerr_endline ("_:: " ^ (Pure.print t)); - assert (t <> Pure.B) - ) 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 "-----------------"; + (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 "-------- --------" + ) +;; (********************** problems *******************) @@ -787,9 +770,7 @@ let append_zero = | _ -> assert false ;; -type t = problem * int * string list;; - -let magic_conv ~div ~conv ~nums cmds = +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 @@ -799,14 +780,27 @@ 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; trail=[]}, 0, [] + {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 = 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 | 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 @@ -814,7 +808,13 @@ let magic_conv ~div ~conv ~nums cmds = 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}, special_k, cmds + {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} ;; -let magic strings cmds = magic_conv None [] strings cmds;; +let should_fail f = + try + solve (f ()); + failwith "The problem should have failed" + with Fail _ -> + prerr_endline "The problem failed, as expected" +;; diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli index c8a571e..8f6019e 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -1,4 +1,4 @@ -type t -val magic: string list -> string list -> t -val magic_conv: div:(string option) -> conv:string list -> nums:string list -> string list -> t -val main: t list -> unit +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 diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 3c098b9..a11453d 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,149 +1,150 @@ open Lambda4;; +let magic strings = problem_of None [] strings;; +let solve_many = List.iter solve;; -let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"] +let p2 = magic [ "x y"; "x z" ; "x (y z)"] let p4 = magic - [ "x y"; "x (a. a x)" ; "y (y z)" ] ["*"] + [ "x y"; "x (a. a x)" ; "y (y z)" ] let p5 = magic ["a (x. x a) b"; "b (x. x b) a"] - ["*"] ;; let p6 = magic ["a (x. x a) b"; "b (x. x b) (c a)"] - ["*"] + ;; let p7 = magic ["a (x. (x a)(a x x a)(x x) )"] - ["*"] + ;; let p8 = magic ["x x (x x)"] - ["*"] + ;; let p9 = magic ["x x (x x x) (x x (x x)) (x x (x x x)) x x"] - ["*"] + ;; let p10 = magic ["x (y (x a b c))"] - ["*"] + ;; let p11 = magic ["x x"; "x (y.y)"] - ["*"] + ;; let p12 = magic ["x x (x x)"; "x x (x (y.y))"] - ["*"] + ;; let p13 = magic ["x x (x x (x x x x x (x x)))"] - ["*"] + ;; let p14 = magic ["a (a a (a (a a)) (a (a a)))"] - ["*"] + ;; let p15 = magic ["a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))"] - ["*"] + ;; let p16 = magic ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"] - ["*"] + ;; let p17 = magic ["b a"; "b (c.a)"] - ["*"] + ;; let p18 = magic ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"] - ["*"] + ;; let p19 = magic ["a (a a) (a a a (a (a (a a) a)) a)"] - ["*"] + ;; let p20 = magic - ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"]["*"];; + ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"];; let p21 = magic ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))"; "(((z z) x) (y z))"; "((z (y z)) ((y z) (z z)))" -] ["*"];; +] ;; let p22 = magic ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"; "((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))"; -"(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ["*"];; +"(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ;; (* diverging tests *) (* test p23 leads to test p24 *) let p23 = magic -["z z z"; "z (z z) (x. x)"] ["*"];; +["z z z"; "z (z z) (x. x)"] ;; (* because of the last term, the magic number is 1 and we diverge; but setting the magic number to 0 allows to solve the problem; thus our strategy is incomplete *) let p24 = magic -["b b"; "b f"; "f b"; "a (x.x)"] ["*"];; +["b b"; "b f"; "f b"; "a (x.x)"] ;; (* because of the last term, the magic number is 1 and we diverge; but setting the magic number to 0 allows to solve the problem; thus our strategy is incomplete *) let p25 = magic -["b b"; "b f"; "f b"; "f (x.x)"] ["*"];; +["b b"; "b f"; "f b"; "f (x.x)"] ;; (* BUG: 0 (n (d (o.n) ...))) After instantiating n, the magic number (for d) should be 2, not 1! *) let p26 = magic ["(((x y) (z. (y. (y. z)))) (z. y))"; -"(((x y) x) (y y))"] ["*"];; +"(((x y) x) (y y))"] ;; let p27 = magic ["(((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))"; "((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))"; -"(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ["*"];; +"(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ;; let p28 = magic ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))"; - "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ["*"];; + "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ;; let p29 = magic ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))"; -"(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ["*"];; +"(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ;; let p30 = magic ["((b c) (b. (z a)))"; "((v (a. (z v))) ((y (b c)) ((z a) (v y))))"; "((v (v. c)) z)"; "((v y) (v (a. (z v))))"; -"((y (b c)) ((z a) (v y)))"] ["*"];; +"((y (b c)) ((z a) (v y)))"] ;; let p31 = magic [" (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))"; "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))"; "(((((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))"] ["*"];; +"((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ;; let p32 = magic ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))"; @@ -151,7 +152,7 @@ let p32 = magic "(((((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)))))))" -] ["*"];; +] ;; (* Shows an error when the strategy that minimizes special_k is NOT used *) let p33 = magic @@ -161,7 +162,7 @@ let p33 = magic "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))"; "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))"; (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) -] ["*"];; +] ;; let p34 = magic [ "b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a"; @@ -169,7 +170,7 @@ let p34 = magic [ "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a"; "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a"; "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a"; -] ["*"];; +] ;; (* 0: (b c (b c) (c (d j.e)) (b c (b c) j.(c f)) (b f j.k.d) (b j.k.l.(b c (b c)) (b g)) a) 1: (d j.e e j.(c f) j.(c j) b a) 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a) @@ -180,59 +181,59 @@ let p35 = magic [ "(((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))"; "((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))"; "((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))" -] ["*"];; +] ;; let p36 = magic [ "(((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (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))))))))"; "(((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))"; "(((((((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))" -] ["*"];; +] ;; (* issue with eta-equality of terms in ps *) let p37 = magic ["x (a y) z"; "x (a z. y z) w"; "a c"] - ["*"];; + ;; (**********************) -let q1 () = magic_conv +let q1 () = problem_of None ["a d e"] ["a b"; "a c"] - ["*"];; + ;; -let q2 () = magic_conv +let q2 () = problem_of None ["a d e"] ["a b" ] - ["*"];; + ;; -let q3 () = magic_conv +let q3 () = problem_of (Some "x") ["a d e f"] ["a b" ] - ["*"];; + ;; -let q4 () = magic_conv +let q4 () = problem_of None ["f (x.a b c d)"] ["a b" ] - ["*"];; + ;; -let q5 () = magic_conv +let q5 () = problem_of (Some"x") ["(y. x)"] ["x"] - ["*"];; + ;; -let q6 () = magic_conv +let q6 () = problem_of (Some"x") ["(y. x z)"] ["y"] - ["*"];; + ;; -let q7 () = magic_conv +let q7 () = problem_of (Some "(b (c d (e f f k.(g e))) f)") ["(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))"; "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))"; @@ -240,25 +241,25 @@ let q7 () = magic_conv ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)"; "(f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)"; "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)"] - ["*"];; + ;; (**********************) -let q8 () = magic_conv +let q8 () = problem_of (Some"x a") - ["y (x b c)"] ["j"] ["*"] + ["y (x b c)"] ["j"] ;; -let q9 () = magic_conv +let q9 () = problem_of (Some"x a") - ["y x"] ["a (y a b b b)"] ["*"] + ["y x"] ["a (y a b b b)"] ;; -let q11 () = magic_conv +let q11 () = problem_of (Some "x y") - ["a (x z)"] [] ["*"];; + ["a (x z)"] [] ;; -let q10 () = magic_conv +let q10 () = problem_of (Some "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g))) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))") @@ -273,20 +274,20 @@ let q10 () = magic_conv "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)"; "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)"; "e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))"; -] ["*"];; +] ;; -let m1 () = magic_conv None [] +let m1 () = problem_of None [] ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"] - ["*"] + ;; -let m2 () = magic_conv None [] +let m2 () = problem_of None [] ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"] - ["*"] + ;; -let n1 () = magic_conv (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)") +let n1 () = problem_of (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)") [ "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. i))"; "g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. l. g (m. c e) (m. i) (c b) (l c) b) (e c (d d (d c)) (c e (k. f)) (b (c b) (k. l. c b d) (c e) (k. l. m. f)))"; @@ -299,9 +300,9 @@ let n1 () = magic_conv (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e "d h (b (c b) (k. l. c b d) (c e)) (k. g (l. c e) (l. i) (c b) (k c) b) d b (b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (k. c)) a"; "g (k. c e) (k. d d) (k. k k) (e c (d d (d c)) i) (k. g (l. k e) (l. d d)) (g i (b (c b) (k. l. c b d) (e c (d d (d c)) (k. c e (f c)) (k. k (c k) (l. m. c k d) (c e) k (g (l. c e) (l. i) (c k)) (l. c))))) (c b) a"; "g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e) a" -] ["*"];; +] ;; -let n2 () = magic_conv +let n2 () = problem_of (Some"b b (c d) (k. d e) (k. k) (k. l. b)") [ "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))))) (d e (k. d e) g (i (k. k)))"; @@ -315,10 +316,10 @@ let n2 () = magic_conv "d e (k. d e) (k. b (l. h)) (k. l. d e) (d (g (d e) (g (k. e)) h) (g (d e) (k. l. l))) a"; "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (k. l. m. b b) a"; "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (b (b b) (d (g(d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k)))) (k. d e (l. d e) f) a"; -] ["*"] +] ;; -let n3 () = magic_conv +let n3 () = problem_of (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))") [ "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))"; @@ -332,23 +333,73 @@ let n3 () = magic_conv "e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a"; "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a"; "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a"; -] ["*"];; +] ;; (* ************************************************************************** *) -let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];; -let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];; -let o3 () = magic_conv +let o1 () = problem_of None [] ["x a b"; "x (_. BOT) c"] ;; +let o2 () = problem_of None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ;; +let o3 () = problem_of (Some"y (x a1 BOMB c) (x BOMB b1 d)") [ "y (x a2 BOMB c) (x BOMB b1 d)"; - "y (x a1 BOMB c) (x BOMB b2 d)";] [] ["*"];; -let o4 () = magic_conv (Some"x BOMB a1 c") - [ "x y BOMB d"; "x BOMB a2 c" ] [] ["*"];; - - -main [o1() ; o2(); o3(); o4();];; - -main ([ + "y (x a1 BOMB c) (x BOMB b2 d)";] [] ;; +let o4 () = problem_of (Some"x BOMB a1 c") + [ "x y BOMB d"; "x BOMB a2 c" ] [] ;; +let o5 () = problem_of (Some"BOT") [] [] ;; +let o6 () = problem_of (Some"x BOMB") ["x y"] [];; + +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"] []);; + +solve_many [ + problem_of + (* DISPLAY PROBLEM (main) - measure=965 + Discriminating sets (deltas): + 0 <> 1 <> 2 <> 3 <> 4 + *)(* DIVERGENT *) + (Some"b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))") + (* CONVERGENT *) [ + (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (f g)))"; + (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))"; + (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e)"; + (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))"; + (* _ *) "b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c + d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))"; + ] (* NUMERIC *) [ + (* 0 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) a"; + (* 1 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) a"; + (* 2 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a"; + (* 3 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a"; + (* 4 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a"; + ]; problem_of + (* DISPLAY PROBLEM (main) - measure=561 + Discriminating sets (deltas): + 0 <> 1 <> 2 <> 3 <> 4 + *)(* DIVERGENT *) + (Some"b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))") + (* CONVERGENT *) [ + (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))"; + (* _ *) "e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))"; + (* _ *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))"; + (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)"; + (* _ *) "e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))"; + ] (* NUMERIC *) [ + (* 0 *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) a"; + (* 1 *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a"; + (* 2 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a"; + (* 3 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a"; + (* 4 *) "g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a"; + ] +];; + +failwith "OKAy";; + +solve_many ([ p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; diff --git a/ocaml/test.ml b/ocaml/test.ml index 93240b9..f5bf55a 100644 --- a/ocaml/test.ml +++ b/ocaml/test.ml @@ -62,7 +62,7 @@ let call_main4 div convs nums = print_endline "CONV:"; List.iter prerr_endline convs; print_endline "NUMS:"; List.iter prerr_endline nums; prerr_newline (); - ) in Lambda4.main [Lambda4.magic_conv div convs nums ["*"]] + ) in Lambda4.solve (Lambda4.problem_of div convs nums) ;; let main =