Command line arguments to ./a.out

For example:
 ./a.out problems/*
 ./a.out problems/p

Moved "o"-problems to problems/o

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index f073d29cd001a54edebd8c197f509a43b5e7e563..0374b4787472f9ac910f778c90bea30d28b43f62 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -15,13 +15,23 @@ let assert_unseparable x =
    failwith ("assert_unseparable: separable.")
 ;;
 
-let solve_many = List.iter assert_separable;;
+let assert_depends x =
+ let c = String.sub (Lambda4.label_of_problem (fst x)) 0 1 in
+ prerr_endline(Lambda4.label_of_problem (fst x)); assert (c = "!" || c="?");
+ let q = c = "!" in
+ (if q then assert_separable else assert_unseparable) x
+;;
+
+let main () =
+((* <main> *)
+
+let solve_many = List.iter assert_separable in
 
 (* TODO *)
 (* div under a lambda in conv *)
 (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)
 
-List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/p");;
+List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/p");
 
 (* q-series problems *)
 
@@ -29,37 +39,37 @@ let q1 () = problem_of
  None
  ["a d e"]
  ["a b"; "a c"]
- ;;
+ in
 
 let q2 () = problem_of
  None
  ["a d e"]
  ["a b" ]
- ;;
+ in
 
 let q3 () = problem_of
  (Some "x y")
  ["a d e f"]
  ["a b" ]
- ;;
+ in
 
 let q4 () = problem_of
  None
  ["f (x.a b c d)"]
  ["a b" ]
- ;;
+ in
 
 let q5 () = problem_of
  (Some"x y")
  ["(y. x)"]
  ["x"]
- ;;
+ in
 
 let q6 () = problem_of
  (Some"x w")
  ["(y. x z)"]
  ["y"]
- ;;
+ in
 
 let q7 () = problem_of
  (Some "(b (c d (e f f k.(g e))) f)")
@@ -69,23 +79,23 @@ let q7 () = problem_of
  ["(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)"]
- ;;
+ in
 
 (**********************)
 
 let q8 () = problem_of
  (Some"x a")
  ["y (x b c)"] ["j"]
-;;
+in
 
 let q9 () = problem_of
  (Some"x a")
  ["y x"] ["a (y a b b b)"]
-;;
+in
 
 let q11 () = problem_of
  (Some "x y")
- ["a (x z)"] [] ;;
+ ["a (x z)"] [] in
 
 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)
@@ -102,17 +112,17 @@ let q10 () = problem_of
 "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)))";
-] ;;
+] in
 
 let m1 () = problem_of None []
  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 
-;;
+in
 
 let m2 () = problem_of None []
  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 
-;;
+in
 
 
 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)")
@@ -128,7 +138,7 @@ let n1 () = problem_of (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"
-] ;;
+] in
 
 let n2 () = problem_of
 (Some"b b (c d) (k. d e) (k. k) (k. l. b)")
@@ -145,7 +155,7 @@ let n2 () = problem_of
 "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";
 ]
-;;
+in
 
 let n3 () = problem_of
 (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
@@ -161,26 +171,14 @@ let n3 () = problem_of
 "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";
-] ;;
+] in
 
 (* ************************************************************************** *)
 
-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 () = problem_of (Some"x BOMB a1 c")
- [ "x y BOMB d"; "x BOMB a2 c" ] [] ;;
-let o6 () = problem_of (Some"x BOMB") ["x y"] [];;
-
-solve_many (List.map ((|>) ()) [
- o1; o2; o3; o4; o6
-]);;
+List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/o");
 
-assert_unseparable(problem_of (Some"x y") ["x BOMB"] []);;
-assert_unseparable(problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);;
+assert_unseparable(problem_of (Some"x y") ["x BOMB"] []);
+assert_unseparable(problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);
 
 solve_many [
  problem_of
@@ -222,7 +220,7 @@ solve_many [
    (* 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";
  ]
-];;
+];
 
 (* This fails *)
 (* solve (problem_of
@@ -252,4 +250,13 @@ solve_many (List.map ((|>) ()) ([
  n1 ;
  n2 ;
  n3
-]));;
+]));
+
+(* </main> *));;
+
+if Array.length Sys.argv = 1
+ then main ()
+else Array.iteri (fun i filename -> if i > 0 then
+ List.iter (assert_depends ++ Lambda4.tmp) (Parser.from_file filename)
+ ) Sys.argv
+;;

diff --git a/ocaml/problems/o b/ocaml/problems/o
new file mode 100644 (file)
index 0000000..67fa90b
--- /dev/null
+++ b/ocaml/problems/o
@@ -0,0 +1,21 @@
+$! o1\r
+N x a b\r
+x (_. BOT) c\r
+\r
+$! o2\r
+N x (y (_. BOT) a) c\r
+x (y a PAC) d\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 5e7283cbec99277c0bc13524f2fdfd094af0d2ed..6f1e0622cf6c636630114c87d6a9d3ac02969944 100644 (file)
--- a/ocaml/problems/p
+++ b/ocaml/problems/p
@@ -1,85 +1,85 @@
-# p2\r
+$! p2\r
 N x y\r
   x z\r
   x (y z)\r
 \r
-# p4\r
+$! p4\r
 N x y\r
   x (a. a x)\r
   y (y z)\r
 \r
-# p5\r
+$! p5\r
 N a (x. x a) b\r
   b (x. x b) a\r
 \r
-# p6\r
+$! p6\r
 N a (x. x a) b\r
   b (x. x b) (c a)\r
 \r
-# p7\r
+$! p7\r
 N a (x. (x a) (a x x a) (x x) )\r
 \r
-# p8\r
+$! p8\r
 N x x (x x)\r
 \r
-# p9\r
+$! p9\r
 N x x (x x x) (x x (x x)) (x x (x x x)) x x\r
 \r
-# p10\r
+$! p10\r
 N x (y (x a b c))\r
 \r
-# p11\r
+$! p11\r
 N x x\r
   x (y.y)\r
 \r
-# p12\r
+$! p12\r
 N x x (x x)\r
   x x (x (y.y))\r
 \r
-# p13\r
+$! p13\r
 N x x (x x (x x x x x (x x)))\r
 \r
-# p14\r
+$! p14\r
 N a (a a (a (a a)) (a (a a)))\r
 \r
-# p15\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
 \r
-# p16:\r
+$! p16:\r
 N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))\r
 \r
-# p17\r
+$! p17\r
 N b a\r
   b (c.a)\r
 \r
-# p18\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
 \r
-# p19\r
+$! p19\r
 N a (a a) (a a a (a (a (a a) a)) a)\r
 \r
-# p20\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
 \r
-# p21\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
 \r
-# p22\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
 \r
-# p23\r
-  (* diverging tests *) (* test p23 leads to test p24 *)\r
+$! p23\r
+# (* diverging tests *) (* test p23 leads to test p24 *)\r
 N z z z\r
   z (z z) (x. x)\r
 \r
-# p24\r
-  (* because of the last term, the magic number is 1 and we diverge\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
@@ -87,8 +87,8 @@ N b b
   f b\r
   a (x.x)\r
 \r
-# p25\r
-  (* because of the last term, the magic number is 1 and we diverge\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
@@ -96,48 +96,48 @@ N b b
   f b\r
   f (x.x)\r
 \r
-# p26\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
 \r
-# p27\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
 \r
-# p28\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
 \r
-# p29\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
 \r
-# p30\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
 \r
-# p31\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
+$! 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
 \r
-# p33\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
@@ -145,25 +145,25 @@ N ((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a
   (((((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
 #  (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)\r
 \r
-# p34\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
 \r
-# p35\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
 \r
-# p36\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
 \r
 \r
-# p37\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