From: acondolu Date: Sat, 15 Jul 2017 14:41:39 +0000 (+0200) Subject: Important: added special variable "Z" for zero. X-Git-Tag: weak-reduction-separation~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38ecafd7f8a1b5137f642bfa433d27cef8de2908;p=fireball-separation.git Important: added special variable "Z" for zero. - Removed append_zero in Lambda4 - Now tests append "Z" at the end of ps' - Manually appended "Z" at the end of all problems - Removed tmp function in Lambda4, renamed to problem_of (cherry picked from commit 82dd1911598932af386c4de46398624453e1fc31) --- diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 1e978f2..18b0bc0 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -675,7 +675,8 @@ type result = [ ] let check p = - (* check if there are duplicates in p.ps *) + (* 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 @@ -742,25 +743,10 @@ let solve p = `Separable p_finale.sigma ;; -let zero = `Var(0,0);; - -let append_zero = - function - | `I _ - | `Var _ as i -> cast_to_i_n_var (mk_app i zero) - | `N _ -> raise (Parser.ParsingError " numbers in ps") -;; - -let tmp (label, div, conv, nums, var_names) = - (* DA SPOSTARE NEI TEST: *) - let ps = List.map append_zero nums 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 all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in - if all_tms = [] then failwith "FIXME: empty problem"; +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 = @@ -768,29 +754,3 @@ let tmp (label, div, conv, nums, var_names) = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label} ;; - -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, (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 - tmp("missing label", div, conv, ps, var_names) -;; diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli index c8a40bf..8e89903 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -7,9 +7,7 @@ type result = [ | `Unseparable of string ] -val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem -(* the following will soon replace the one above *) -val tmp: (string (* problem label *) +val problem_of: (string (* problem label *) * Num.i_var option (* div *) * Num.i_n_var list (* conv *) * Num.i_n_var list (* ps *) diff --git a/ocaml/parser.ml b/ocaml/parser.ml index 902da8d..abd4309 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -148,11 +148,13 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j") let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in + let n_z = try Util.index_of "Z" free with Not_found -> min_int in let fix lev v = if v = lev + n_bot then failwith "Example with `Bottom" else if v = lev + n_pac then failwith "Example with `Pacman" else if v = lev + n_bomb then failwith "Example with `Bomb" - else `Var(v,1) in (* 1 by default when variable not applied *) + else if v = lev + n_z then `Var(lev, 0) (* FIXME why zero? *) + else `Var(v,1) in (* 1 by default when variable not applied *) (* Fix arity *) let open Num in let rec aux lev : nf -> nf = function diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 0678a13..5f86177 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -44,6 +44,6 @@ let assert_depends x = if Array.length Sys.argv = 1 then failwith "no command line args. Please use e.g. ./a.out problems/*" else Array.iteri (fun i filename -> if i > 0 then - List.iter (assert_depends ++ Lambda4.tmp) (Parser.from_file filename) + List.iter (assert_depends ++ problem_of) (Parser.from_file filename) ) Sys.argv ;; diff --git a/ocaml/problems/m b/ocaml/problems/m index 64b6ad3..716e4d4 100644 --- a/ocaml/problems/m +++ b/ocaml/problems/m @@ -1,13 +1,13 @@ $! m1 -N y z - x z - x (a k) u - x (a r) - x (a k) v +N y z Z + x z Z + x (a k) u Z + x (a r) Z + x (a k) v Z $! m2 -N y z - x z - x (a k) u - x (a r) - x (a k) v +N y z Z + x z Z + x (a k) u Z + x (a r) Z + x (a k) v Z diff --git a/ocaml/problems/n b/ocaml/problems/n index 2352457..25d5378 100644 --- a/ocaml/problems/n +++ b/ocaml/problems/n @@ -5,11 +5,11 @@ C 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 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. l. m. c c g) (e c (b (k. f))) (k. f c) c (c e) (e c (d d (d c)) (k. c e (f c))) (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. c e (l. f) (k (l. c e) (l. i)))) (k. l. l (m. c e) (m. i) (c b) (f c) b) (k. l. c k) (f (f c) (b (c b) (k. l. c b d) (c 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. l. m. c c g) (e c (b (k. f))))) -N b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (h (g (k. c e) (k. i) (c b) (c (c e)))) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a - c c g (k. b (c b) (l. m. c b k) (c e)) (k. b (c b) (l. m. c b d) (c k) b) (k. e c (d h) k) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a - 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" +N b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (h (g (k. c e) (k. i) (c b) (c (c e)))) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a Z + c c g (k. b (c b) (l. m. c b k) (c e)) (k. b (c b) (l. m. c b d) (c k) b) (k. e c (d h) k) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a Z + 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 Z + 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 Z + 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 Z $! n2 D b b (c d) (k. d e) (k. k) (k. l. b) @@ -18,11 +18,11 @@ C 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 ( f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. l. l) (k. g (d e) (l. m. m)) 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 (g (d e) (g (k. e)) h) (g (g (d e)) (d e (k. d e) (k. b (l. h)) (k. l. d e))) (b (k. h) (k. k e (l. m. b b)) (k. k (k k) (l. l))) (k. b) (b b (k. l. i)(k. c)) -N 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. l. d (g (d k) (g (m. k)) h) (d k (m. n. b b))) (e (c d) (e (c d))) a - d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a - 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 +N 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. l. d (g (d k) (g (m. k)) h) (d k (m. n. b b))) (e (c d) (e (c d))) Z + d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) Z + 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))) Z + 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) Z + 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) Z $! n3 D b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n)) @@ -31,8 +31,8 @@ C b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) ( f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e))) f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e) 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) -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)) a - c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a - 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 +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)) Z + c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) Z + 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) Z + f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) Z + 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))))) Z diff --git a/ocaml/problems/o b/ocaml/problems/o new file mode 100644 index 0000000..95c3c3d --- /dev/null +++ b/ocaml/problems/o @@ -0,0 +1,21 @@ +$! o1 +N x a b Z + x (_. BOT) c Z + +$! o2 +N x (y (_. BOT) a) c Z + x (y a PAC) d Z + +$! o3 +D y (x a1 BOMB c) (x BOMB b1 d) +C y (x a2 BOMB c) (x BOMB b1 d) + y (x a1 BOMB c) (x BOMB b2 d) + + +$! o4 +D x BOMB a1 c + x y BOMB d + +$! o6 +D x BOMB +C x y diff --git a/ocaml/problems/p b/ocaml/problems/p index a2155a6..27315d0 100644 --- a/ocaml/problems/p +++ b/ocaml/problems/p @@ -1,171 +1,172 @@ $! p2 -N x y - x z - x (y z) +N x y Z + x z Z + x (y z) Z $! p4 -N x y - x (a. a x) - y (y z) +N x y Z + x (a. a x) Z + y (y z) Z $! p5 -N a (x. x a) b - b (x. x b) a +N a (x. x a) b Z + b (x. x b) a Z $! p6 -N a (x. x a) b - b (x. x b) (c a) +N a (x. x a) b Z + b (x. x b) (c a) Z $! p7 -N a (x. (x a) (a x x a) (x x) ) +N a (x. (x a) (a x x a) (x x) ) Z $! p8 -N x x (x x) +N x x (x x) Z $! p9 -N x x (x x x) (x x (x x)) (x x (x x x)) x x +N x x (x x x) (x x (x x)) (x x (x x x)) x x Z $! p10 -N x (y (x a b c)) +N x (y (x a b c)) Z $! p11 -N x x - x (y.y) +N x x Z + x (y.y) Z $! p12 -N x x (x x) - x x (x (y.y)) +N x x (x x) Z + x x (x (y.y)) Z $! p13 -N x x (x x (x x x x x (x x))) +N x x (x x (x x x x x (x x))) Z $! p14 -N a (a a (a (a a)) (a (a a))) +N a (a a (a (a a)) (a (a a))) Z $! p15 -N 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))) +N 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))) Z $! p16: -N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) +N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z $! p17 -N b a - b (c.a) +N b a Z + b (c.a) Z $! p18 -N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) - a a - a (a a) +N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z + a a Z + a (a a) Z $! p19 -N a (a a) (a a a (a (a (a a) a)) a) +N a (a a) (a a a (a (a (a a) a)) a) Z $! p20 -N 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))))) +N 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))))) Z $! p21 -N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) - (((z z) x) (y z)) - ((z (y z)) ((y z) (z z))) +N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z + (((z z) x) (y z)) Z + ((z (y z)) ((y z) (z z))) Z $! p22 -N ((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)))) +N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z 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))))) Z + (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z $! p23 # (* diverging tests *) (* test p23 leads to test p24 *) -N z z z - z (z z) (x. x) +N z z z Z + z (z z) (x. x) Z $! p24 # (* 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 *) -N b b - b f - f b - a (x.x) +N b b Z + b f Z + f b Z + a (x.x) Z $! p25 # (* 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 *) -N b b - b f - f b - f (x.x) +N b b Z + b f Z + f b Z + f (x.x) Z $! p26 (* BUG: 0 (n (d (o.n) ...))) After instantiating n, the magic number (for d) should be 2, not 1! *) -N (((x y) (z. (y. (y. z)))) (z. y)) - (((x y) x) (y y)) +N (((x y) (z. (y. (y. z)))) (z. y)) Z + (((x y) x) (y y)) Z $! p27 -N (((((((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)) +N (((((((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 + ((((((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 + (((((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 $! p28 -N ((((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))))) +N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z + (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z $! p29 -N ((((((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) +N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z + (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z $! p30 -N ((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))) +N ((b c) (b. (z a))) Z + ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z + ((v (v. c)) z) Z + ((v y) (v (a. (z v)))) Z + ((y (b c)) ((z a) (v y))) Z $! p31 -N (((((((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)) - -$! p32 -N (((((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))))))) +N (((((((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))) Z + ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z + (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z + (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z + ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z + +$? p32 +# should fail because the first and second terms are eta-eq +N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z + (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z + (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z + ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z + ((((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))))))) Z $! p33 (* Shows an error when the strategy that minimizes special_k is NOT used *) -N ((((((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))))))) - ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) - (((((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)))) +N ((((((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))))))) Z + ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z + (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z + (((((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)))) Z # (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) $! p34 -N 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 - d (j. e) e (j. c f) (j. c j) b a - 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 +N 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 Z + d (j. e) e (j. c f) (j. c j) b a Z + d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z + d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z + d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z $! p35 -N (((((((((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))) +N (((((((((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))))))) Z + ((((((((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)) Z (((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)))))))))) Z + ((((((((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))) Z $! p36 -N (((((((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)) +N (((((((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 + (((((((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 + (((((((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)) Z $! p37 issue with eta-equality of terms in ps -N x (a y) z - x (a z. y z) w - a c +N x (a y) z Z + x (a z. y z) w Z + a c Z diff --git a/ocaml/problems/q b/ocaml/problems/q index 9f43235..01ec754 100644 --- a/ocaml/problems/q +++ b/ocaml/problems/q @@ -1,20 +1,20 @@ $! q1 C a d e -N a b - a c +N a b Z + a c Z $! q2 C a d e -N a b +N a b Z $! q3 D x y C a d e f -N a b +N a b Z $! q4 C f (x.a b c d) -N a b +N a b Z $! q5 D x y @@ -24,28 +24,28 @@ N x $! q6 D x w C (y. x z) -N y +N y Z $! q7 D (b (c d (e f f k.(g e))) f) C (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))))) (b (g (e f)) f k.e k.l.(f d (e f)) (c d (e f f k.(g e)) (g k.(e f f))) (h f (i (h k.(i b l.m.n.e))))) -N (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) +N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a) Z + (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) Z + (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) Z ################################################################################ $! q8 D x a C y (x b c) -N j +N j Z $! q9 D x a C y x -N a (y a b b b) +N a (y a b b b) Z $! q11 D x y @@ -59,8 +59,8 @@ C e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k. b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (b (k. c) (k. e) (k. l. m. b (n. c))) (e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k))) 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))) -N 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))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e))) - b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h)) - 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))) +N 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))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e))) Z + b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h)) Z + 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) Z + b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b) Z + 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))) Z diff --git a/ocaml/problems/w b/ocaml/problems/w index ec35dd0..e86007c 100644 --- a/ocaml/problems/w +++ b/ocaml/problems/w @@ -20,11 +20,11 @@ C 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 ( C 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))) C 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 *) [ -N 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 - 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 - 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 - 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 - 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 +N 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)) Z + 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)) Z + 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)) Z + 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))) Z + 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)))) Z # ]; $! @@ -41,11 +41,11 @@ C 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 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 *) [ -N 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 - 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 - 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 - 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 - 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 +N 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) Z + 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) Z + e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) Z + 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) Z + 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 Z # ] ]; diff --git a/ocaml/test.ml b/ocaml/test.ml index f5bf55a..da6dbda 100644 --- a/ocaml/test.ml +++ b/ocaml/test.ml @@ -1,4 +1,5 @@ open Lambda4;; +open Util;; let acaso l = let n = Random.int (List.length l) in @@ -57,12 +58,14 @@ let rec repeat f n = ) in Lambda3.main [Lambda3.magic tms ["*"]] ;; *) let call_main4 div convs nums = - let _ = ( - (match div with Some div -> prerr_endline ("DIV: " ^ div) | None -> ()); - print_endline "CONV:"; List.iter prerr_endline convs; - print_endline "NUMS:"; List.iter prerr_endline nums; - prerr_newline (); - ) in Lambda4.solve (Lambda4.problem_of div convs nums) + let p = String.concat "\n" ( + "$! randomly generated test" :: + ("D " ^ div) :: + List.map ((^) "C ") convs @ + List.map (fun s -> "N " ^ s ^ " Z") nums + ) in + prerr_endline p; + (Lambda4.solve ++ Lambda4.problem_of ++ Parser.problem_of_string) p ;; let main = @@ -80,7 +83,7 @@ let main = else *) repeat (fun _ -> let div, (conv, nums) = test4 complex vars in - call_main4 (Some div) conv nums + call_main4 div conv nums ) num ;