]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems.ml
Fixes to parser
[fireball-separation.git] / ocaml / problems.ml
index 0374b4787472f9ac910f778c90bea30d28b43f62..f2812775b2a3dc43dcf94e210ead6076e6b1c011 100644 (file)
@@ -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 _ -> ()
@@ -17,9 +33,9 @@ let assert_unseparable x =
 
 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
+ if c = "!" then assert_separable x
+  else if c = "?" then assert_unseparable x
+   else (solve x; ())
 ;;
 
 let main () =