X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=eda359ae00d08dc3b92c19eba633c44d1bec1ee1;hb=5d8249a042beefbe21bfeed48619ed1917ebbcb7;hp=a0ff4536266a0739e760845589d1a8e643c57a36;hpb=b609e8cfc37360748de4fcbc4e80bba556fadc87;p=fireball-separation.git diff --git a/ocaml/problems.ml b/ocaml/problems.ml index a0ff453..eda359a 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,299 +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"] - ["*"] -;; - -let p10 = magic - ["x (y (x a b c))"] - ["*"] -;; - -let p11 = magic - ["x x"; "x (y.y)"] - ["*"] -;; - -let p12 = magic - ["x x (x x)"; "x x (x (y.y))"] - ["*"] -;; +- (#) on new line + comment line -let p13 = magic - ["x x (x x (x x x x x (x x)))"] - ["*"] -;; - -let p14 = magic - ["a (a a (a (a a)) (a (a a)))"] - ["*"] -;; +- (D) (C) (N) stand respectively for divergent, convergent, numeric -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)))"] - ["*"] -;; +- lines starting with spaces inherit the type from the last line -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)"] - ["*"] +(* 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 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)"] - ["*"] -;; +(* TODO *) +(* div under a lambda in conv *) -let p19 = magic - ["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 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"] - ["*"] -;; - -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 ; -]);;