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 1e978f281336137234264b00068e869fa43ade8d..18b0bc0d79b490c18959473b70c0ac7ccaf66a99 100644 (file)
--- 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 c8a40bfa8c719694f0796ec429c13943ac3cf200..8e89903e92a1c322b890e94538f367f7f35f722b 100644 (file)
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -7,9 +7,7 @@ type result = [
  | `Unseparable of string\r
 ]\r
 \r
-val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem\r
-(* the following will soon replace the one above *)\r
-val tmp: (string (* problem label *)\r
+val problem_of: (string (* problem label *)\r
 * Num.i_var option (* div *)\r
 * Num.i_n_var list (* conv *)\r
 * Num.i_n_var list (* ps *)\r

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 902da8d38bfdb8473d14f05dd5fbedee2e55da51..abd4309f5fd591d5208109bcd82e0f2cd422d86a 100644 (file)
--- 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\r
    let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in\r
    let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in\r
+   let n_z = try Util.index_of "Z" free with Not_found -> min_int in\r
    let fix lev v =\r
     if v = lev + n_bot then failwith "Example with `Bottom"\r
      else if v = lev + n_pac then failwith "Example with `Pacman"\r
       else if v = lev + n_bomb then failwith "Example with `Bomb"\r
-       else `Var(v,1) in (* 1 by default when variable not applied *)\r
+       else if v = lev + n_z then `Var(lev, 0) (* FIXME why zero? *)\r
+         else `Var(v,1) in (* 1 by default when variable not applied *)\r
    (* Fix arity *)\r
    let open Num in\r
    let rec aux lev : nf -> nf = function\r

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 0678a13e697df9a78fc50bd9bb65ce96ed3d08e1..5f86177db4e18de320e94239a4f80d4fcf1744c0 100644 (file)
--- 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 64b6ad3450cc7390cd86d56bd5451c9c3bb6a66f..716e4d4ff743c55268e88fe9690c2755805bdfa7 100644 (file)
--- a/ocaml/problems/m
+++ b/ocaml/problems/m
@@ -1,13 +1,13 @@
 $! m1\r
-N y z\r
-  x z\r
-  x (a k) u\r
-  x (a r)\r
-  x (a k) v\r
+N y z Z\r
+  x z Z\r
+  x (a k) u Z\r
+  x (a r) Z\r
+  x (a k) v Z\r
 \r
 $! m2\r
-N y z\r
-  x z\r
-  x (a k) u\r
-  x (a r)\r
-  x (a k) v\r
+N y z Z\r
+  x z Z\r
+  x (a k) u Z\r
+  x (a r) Z\r
+  x (a k) v Z\r

diff --git a/ocaml/problems/n b/ocaml/problems/n
index 2352457d9c0d57bf23f4e127f35f344007eb0660..25d53780d111f7245022f2e3619daf4bf834ed44 100644 (file)
--- 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))\r
   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)\r
   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)))))\r
-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\r
-  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\r
-  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\r
-  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\r
-  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"\r
+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\r
+  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\r
+  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\r
+  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\r
+  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\r
 \r
 $! n2\r
 D b b (c d) (k. d e) (k. k) (k. l. b)\r
@@ -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))\r
   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)))))\r
   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))\r
-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\r
-  d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a\r
-  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\r
-  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\r
-  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\r
+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\r
+  d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) Z\r
+  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\r
+  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\r
+  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\r
 \r
 $! n3\r
 D b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))\r
@@ -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)))\r
   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)\r
   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)\r
-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\r
-  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\r
-  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\r
-  f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a\r
-  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\r
+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\r
+  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\r
+  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\r
+  f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) Z\r
+  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\r

diff --git a/ocaml/problems/o b/ocaml/problems/o
new file mode 100644 (file)
index 0000000..95c3c3d
--- /dev/null
+++ b/ocaml/problems/o
@@ -0,0 +1,21 @@
+$! o1\r
+N x a b Z\r
+  x (_. BOT) c Z\r
+\r
+$! o2\r
+N x (y (_. BOT) a) c Z\r
+  x (y a PAC) d Z\r
+\r
+$! o3\r
+D y (x a1 BOMB c) (x BOMB b1 d)\r
+C y (x a2 BOMB c) (x BOMB b1 d)\r
+  y (x a1 BOMB c) (x BOMB b2 d)\r
+\r
+\r
+$! o4\r
+D x BOMB a1 c\r
+  x y BOMB d\r
+\r
+$! o6\r
+D x BOMB\r
+C x y\r

diff --git a/ocaml/problems/p b/ocaml/problems/p
index a2155a6d2a79c617fbffde7c94ccd3a69d742215..27315d04a1f84867e2e4fe649ed9a3b032eb577f 100644 (file)
--- a/ocaml/problems/p
+++ b/ocaml/problems/p
@@ -1,171 +1,172 @@
 \r
 $! p2\r
-N x y\r
-  x z\r
-  x (y z)\r
+N x y Z\r
+  x z Z\r
+  x (y z) Z\r
 \r
 $! p4\r
-N x y\r
-  x (a. a x)\r
-  y (y z)\r
+N x y Z\r
+  x (a. a x) Z\r
+  y (y z) Z\r
 \r
 $! p5\r
-N a (x. x a) b\r
-  b (x. x b) a\r
+N a (x. x a) b Z\r
+  b (x. x b) a Z\r
 \r
 $! p6\r
-N a (x. x a) b\r
-  b (x. x b) (c a)\r
+N a (x. x a) b Z\r
+  b (x. x b) (c a) Z\r
 \r
 $! p7\r
-N a (x. (x a) (a x x a) (x x) )\r
+N a (x. (x a) (a x x a) (x x) ) Z\r
 \r
 $! p8\r
-N x x (x x)\r
+N x x (x x) Z\r
 \r
 $! p9\r
-N x x (x x x) (x x (x x)) (x x (x x x)) x x\r
+N x x (x x x) (x x (x x)) (x x (x x x)) x x Z\r
 \r
 $! p10\r
-N x (y (x a b c))\r
+N x (y (x a b c)) Z\r
 \r
 $! p11\r
-N x x\r
-  x (y.y)\r
+N x x Z\r
+  x (y.y) Z\r
 \r
 $! p12\r
-N x x (x x)\r
-  x x (x (y.y))\r
+N x x (x x) Z\r
+  x x (x (y.y)) Z\r
 \r
 $! p13\r
-N x x (x x (x x x x x (x x)))\r
+N x x (x x (x x x x x (x x))) Z\r
 \r
 $! p14\r
-N a (a a (a (a a)) (a (a a)))\r
+N a (a a (a (a a)) (a (a a))) Z\r
 \r
 $! p15\r
-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)))\r
+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\r
 \r
 $! p16:\r
-N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))\r
+N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z\r
 \r
 $! p17\r
-N b a\r
-  b (c.a)\r
+N b a Z\r
+  b (c.a) Z\r
 \r
 $! p18\r
-N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))\r
-  a a\r
-  a (a a)\r
+N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z\r
+  a a Z\r
+  a (a a) Z\r
 \r
 $! p19\r
-N a (a a) (a a a (a (a (a a) a)) a)\r
+N a (a a) (a a a (a (a (a a) a)) a) Z\r
 \r
 $! p20\r
-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)))))\r
+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\r
 \r
 $! p21\r
-N (((y z) (y z)) ((z (y z)) ((y z) (z z))))\r
-  (((z z) x) (y z))\r
-  ((z (y z)) ((y z) (z z)))\r
+N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z\r
+  (((z z) x) (y z)) Z\r
+  ((z (y z)) ((y z) (z z))) Z\r
 \r
 $! p22\r
-N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))\r
-  ((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)))))\r
-  (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))\r
+N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
+  ((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\r
+  (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
 \r
 $! p23\r
 # (* diverging tests *) (* test p23 leads to test p24 *)\r
-N z z z\r
-  z (z z) (x. x)\r
+N z z z Z\r
+  z (z z) (x. x) Z\r
 \r
 $! p24\r
 # (* because of the last term, the magic number is 1 and we diverge\r
      but setting the magic number to 0 allows to solve the problem\r
      thus our strategy is incomplete *)\r
-N b b\r
-  b f\r
-  f b\r
-  a (x.x)\r
+N b b Z\r
+  b f Z\r
+  f b Z\r
+  a (x.x) Z\r
 \r
 $! p25\r
 # (* because of the last term, the magic number is 1 and we diverge\r
      but setting the magic number to 0 allows to solve the problem\r
      thus our strategy is incomplete *)\r
-N b b\r
-  b f\r
-  f b\r
-  f (x.x)\r
+N b b Z\r
+  b f Z\r
+  f b Z\r
+  f (x.x) Z\r
 \r
 $! p26\r
   (* BUG:\r
      0 (n (d (o.n) ...)))\r
      After instantiating n, the magic number (for d) should be 2, not 1! *)\r
-N (((x y) (z. (y. (y. z)))) (z. y))\r
-  (((x y) x) (y y))\r
+N (((x y) (z. (y. (y. z)))) (z. y)) Z\r
+  (((x y) x) (y y)) Z\r
 \r
 $! p27\r
-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))))\r
-  ((((((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)))\r
-  (((((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))\r
+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\r
+  ((((((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\r
+  (((((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\r
 \r
 $! p28\r
-N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))\r
-   (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))\r
+N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z\r
+  (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z\r
 \r
 $! p29\r
-N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))\r
-  (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)\r
+N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z\r
+  (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z\r
 \r
 $! p30\r
-N ((b c) (b. (z a)))\r
-  ((v (a. (z v))) ((y (b c)) ((z a) (v y))))\r
-  ((v (v. c)) z)\r
-  ((v y) (v (a. (z v))))\r
-  ((y (b c)) ((z a) (v y)))\r
+N ((b c) (b. (z a))) Z\r
+  ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z\r
+  ((v (v. c)) z) Z\r
+  ((v y) (v (a. (z v)))) Z\r
+  ((y (b c)) ((z a) (v y))) Z\r
 \r
 $! p31\r
-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)))\r
-   ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))\r
-   (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))\r
-    (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))\r
-      ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))\r
-\r
-$! p32\r
-N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))\r
-  (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)\r
-  (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))\r
-  ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))\r
-  ((((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)))))))\r
+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\r
+   ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z\r
+   (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z\r
+    (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z\r
+      ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z\r
+\r
+$? p32\r
+# should fail because the first and second terms are eta-eq\r
+N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z\r
+  (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z\r
+  (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z\r
+  ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z\r
+  ((((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\r
 \r
 $! p33\r
   (* Shows an error when the strategy that minimizes special_k is NOT used *)\r
-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)))))))\r
-  ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))\r
-  (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))\r
-  (((((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))))\r
+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\r
+  ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z\r
+  (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z\r
+  (((((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\r
 #  (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)\r
 \r
 $! p34\r
-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\r
-  d (j. e) e (j. c f) (j. c j) b a\r
-  d (j. e) e (j. c f) b (b c (b c) (j. c f)) a\r
-  d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a\r
-  d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a\r
+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\r
+  d (j. e) e (j. c f) (j. c j) b a Z\r
+  d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z\r
+  d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z\r
+  d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z\r
 \r
 $! p35\r
-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)))))))\r
-  ((((((((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))))))))))\r
-  ((((((((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)))\r
+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\r
+  ((((((((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\r
+  ((((((((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\r
 \r
 $! p36\r
-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))))))))\r
-  (((((((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)))\r
-  (((((((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))\r
+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\r
+  (((((((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\r
+  (((((((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\r
 \r
 \r
 $! p37\r
   issue with eta-equality of terms in ps\r
-N x (a y) z\r
-  x (a z. y z) w\r
-  a c\r
+N x (a y) z Z\r
+  x (a z. y z) w Z\r
+  a c Z\r

diff --git a/ocaml/problems/q b/ocaml/problems/q
index 9f432359bc657bf8dacd280f02cefed96d7aac07..01ec75481a6b387f681f19b2d49f1a56cb82480a 100644 (file)
--- a/ocaml/problems/q
+++ b/ocaml/problems/q
@@ -1,20 +1,20 @@
 $! q1\r
 C a d e\r
-N a b\r
-  a c\r
+N a b Z\r
+  a c Z\r
 \r
 $! q2\r
 C a d e\r
-N a b\r
+N a b Z\r
 \r
 $! q3\r
 D x y\r
 C a d e f\r
-N a b\r
+N a b Z\r
 \r
 $! q4\r
 C f (x.a b c d)\r
-N a b\r
+N a b Z\r
 \r
 $! q5\r
 D x y\r
@@ -24,28 +24,28 @@ N x
 $! q6\r
 D x w\r
 C (y. x z)\r
-N y\r
+N y Z\r
 \r
 $! q7\r
 D (b (c d (e f f k.(g e))) f)\r
 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)))\r
   (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)))))\r
   (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)))))\r
-N (f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)\r
-  (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)\r
-  (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)\r
+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\r
+  (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\r
+  (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\r
 \r
 ################################################################################\r
 \r
 $! q8\r
 D x a\r
 C y (x b c)\r
-N j\r
+N j Z\r
 \r
 $! q9\r
 D x a\r
 C y x\r
-N a (y a b b b)\r
+N a (y a b b b) Z\r
 \r
 $! q11\r
 D x y\r
@@ -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)))\r
   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)))\r
 \r
-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)))\r
-  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))\r
-  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)\r
-  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)\r
-  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)))\r
+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\r
+  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\r
+  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\r
+  b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b) Z\r
+  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\r

diff --git a/ocaml/problems/w b/ocaml/problems/w
index ec35dd04a5075104c640c8bc176e9d24ab060bb7..e86007cd0931e5ec5a9833fc1c7c7c3cbeb0aa3c 100644 (file)
--- 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)))\r
 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)))\r
 #  ] (* NUMERIC    *) [\r
-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\r
-  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\r
-  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\r
-  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\r
-  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\r
+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\r
+  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\r
+  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\r
+  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\r
+  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\r
 #  ];\r
 \r
 $!\r
@@ -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)\r
   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))))\r
 # ] (* NUMERIC    *) [\r
-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\r
-  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\r
-  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\r
-  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\r
-  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\r
+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\r
+  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\r
+  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\r
+  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\r
+  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\r
 #  ]\r
  ];\r
 \r

diff --git a/ocaml/test.ml b/ocaml/test.ml
index f5bf55a50280c7ac20c3048761d8f0e9bc984065..da6dbda7a7f813e0496ccb3d31d2647b4982c42f 100644 (file)
--- 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
   ;