X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=f2812775b2a3dc43dcf94e210ead6076e6b1c011;hb=666a228779e465d08a0deea2e35c0cccf5722b40;hp=f073d29cd001a54edebd8c197f509a43b5e7e563;hpb=f2bc82e223757ea40ba639cd521d69affa29b69d;p=fireball-separation.git

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index f073d29..f281277 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -1,6 +1,22 @@
 open Lambda4;;
 open Util;;
 
+(* Syntax for problem files in problem/ folder:
+
+- dollar ($) on newline
+  begin new problem
+  $! means that the problem is expected to be separable,
+  $? means that it is expected to be unseparable
+
+- (#) on new line
+  comment line
+
+- (D) (C) (N) stand respectively for divergent, convergent, numeric
+
+- lines starting with spaces inherit the type from the last line
+
+*)
+
 let assert_separable x =
  match solve x with
  | _, `Separable _ -> ()
@@ -15,13 +31,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
+ if c = "!" then assert_separable x
+  else if c = "?" then assert_unseparable x
+   else (solve 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 +55,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 +95,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 +128,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 +154,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 +171,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 +187,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"] [];;
+List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/o");
 
-solve_many (List.map ((|>) ()) [
- o1; o2; o3; o4; o6
-]);;
-
-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 +236,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 +266,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
+;;