X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=eda359ae00d08dc3b92c19eba633c44d1bec1ee1;hb=5d8249a042beefbe21bfeed48619ed1917ebbcb7;hp=15fe980880a155791384577cac5cda70f52d3cba;hpb=e1177d88d7ff54d6cb16d711103c5c71aaccdcc6;p=fireball-separation.git

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 15fe980..eda359a 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,369 +1,39 @@
 open Lambda4;;
+open Util;;
 
-let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"]
+(* Syntax for problem files in problem/ folder:
 
-let p4 = magic
-  [ "x y"; "x (a. a x)" ; "y (y z)" ] ["*"]
+- dollar ($) on newline
+  begin new problem
+  $! means that the problem is expected to be separable,
+  $? means that it is expected to be unseparable
 
-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"]
-  ["*"]
-;;
+- (#) on new line
+  comment line
 
-let p10 = magic
-  ["x (y (x a b c))"]
-  ["*"]
-;;
+- (D) (C) (N) stand respectively for divergent, convergent, numeric
 
-let p11 = magic
-  ["x x"; "x (y.y)"]
-  ["*"]
-;;
+- lines starting with spaces inherit the type from the last line
 
-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)))"]
-  ["*"]
+(* assert_depends solves the problem, and checks if the result was expected *)
+let assert_depends x =
+ let c = String.sub (label_of_problem (fst x)) 0 1 in
+ match solve x with
+ | _, `Unseparable s when c = "!" ->
+    failwith ("assert_depends: unseparable because: " ^ s ^ ".")
+ | _, `Separable _  when c = "?" ->
+    failwith ("assert_depends: separable.")
+ | _ -> ()
 ;;
 
-let p14 = magic
-  ["a (a a (a (a a)) (a (a a)))"]
-  ["*"]
-;;
+(* TODO *)
+(* div under a lambda in conv *)
 
-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)))"]
-  ["*"]
+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 ++ problem_of) (Parser.from_file filename)
+ ) Sys.argv
 ;;
-
-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)))))"]["*"];;
-
-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))))"] ["*"];;
-
-(* diverging tests *)
-(* test p23 leads to test p24 *)
-let p23 = magic
-["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)"] ["*"];;
-
-(* 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)"] ["*"];;
-
-(* 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))"] ["*"];;
-
-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))"] ["*"];;
-
-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)))))" ] ["*"];;
-
-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)"] ["*"];;
-
-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)))"] ["*"];;
-
-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))"] ["*"];;
-
-let p32 = magic
-["(((((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)))))))"
-] ["*"];;
-
-(* Shows an error when the strategy that minimizes special_k is NOT used *)
-let p33 = magic
-[
-"((((((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))))";
-(* "(((((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";
-"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";
-] ["*"];;
-(* 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)
-3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
-4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
-
-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
- None
- ["a d e"]
- ["a b"; "a c"]
- ["*"];;
-
-let q2 () = magic_conv
- None
- ["a d e"]
- ["a b" ]
- ["*"];;
-
-let q3 () = magic_conv
- (Some "x")
- ["a d e f"]
- ["a b" ]
- ["*"];;
-
-let q4 () = magic_conv
- None
- ["f (x.a b c d)"]
- ["a b" ]
- ["*"];;
-
-let q5 () = magic_conv
- (Some"x")
- ["(y. x)"]
- ["x"]
- ["*"];;
-
-let q6 () = magic_conv
- (Some"x")
- ["(y. x z)"]
- ["y"]
- ["*"];;
-
-let q7 () = magic_conv
- (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)))))";
-  "(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)))))"]
- ["(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
- (Some"x a")
- ["y (x b c)"] ["j"] ["*"]
-;;
-
-let q9 () = magic_conv
- (Some"x a")
- ["y x"] ["a (y a b b b)"] ["*"]
-;;
-
-let q11 () = magic_conv
- (Some "x y")
- ["a (x z)"] [] ["*"];;
-
-let q10 () = magic_conv
- (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)))")
-["e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k. l. b (m. c))) (k. l. b (m. c) d (l (f k) (m. k)) (m. n. c)) (c f (k. b (l. c)) (k. b (l. c) d) (k. c k))";
-"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) (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))";
-"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)))"]
-[
-"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)))";
-] ["*"];;
-
-let m1 () = magic_conv None []
- ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
- ["*"]
-;;
-
-let m2 () = magic_conv 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)")
-[
-"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)))";
-"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)))))";
-] [
-"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"
-] ["*"];;
-
-let n2 () = magic_conv
-(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)))";
-"f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (d (g (de) (g (k. e)) h) (g (k. 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))";
-] [
-"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";
-] ["*"]
-;;
-
-let n3 () = magic_conv
-(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))";
-"c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
-"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)";
-][
-"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";
-] ["*"];;
-
-(* ************************************************************************** *)
-
-(* let o1 () = magic_conv (Some"BOT") [] [] ["*"];; *)
-
-let o1 () = magic_conv None [] ["x BOT"] ["*"];;
-
-let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];;
-
-main [o1() ];;
-
-(* main ([
- 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 ;
- p34 ;
- p35 ;
- p36 ;
- p37 ;
- p24 ; p25 ;
-] @ List.map ((|>) ()) ([
- q1 ; q2; q3; q4 ; q5 ; q6 ;
- q7 ;
- q8 ;
- q9 ;
- q10 ;
- q11 ;
- m1 ;
- m2 ;
-] @ [
- n1 ;
- n2 ;
- n3
-]));; *)