X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.ml;h=726d076357f77539add48e69cdb04b9efb975367;hb=71f8eb7befd85ff4911658136597b41ed177ff8c;hp=61dbf832d6d75c95123eef63f71aeafb2bf5e82d;hpb=8b69a4c59242b64294c7065a4e85437ce3cbc32d;p=fireball-separation.git

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 61dbf83..726d076 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -171,22 +171,31 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
 ;;
 
 let problem_of_string s =
+prerr_endline (s);
  let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in
+ let lines = List.map String.trim lines in
  let lines = List.filter ((<>) "") lines in
  prerr_endline("number of lines" ^ string_of_int (List.length lines));
- let aux (name, div, conv, ps) line =
+ let aux (last, name, div, conv, ps) line =
   let chr = String.sub line 0 1 in
   let line = String.sub line 1 (String.length line - 1) in
-  if chr = ":"
-   then line, div, conv, ps
-  else if chr = "D"
-   then name, line, conv, ps
-  else if chr = "C"
-   then name, div, line::conv, ps
-  else if chr = "N"
-   then name, div, conv, line::ps
-  else raise (ParsingError ("Unexpected at beginning of line: " ^ chr)) in
- let name, div, conv, ps = List.fold_left aux ("?", "", [], []) lines in
+  if line = "" then chr, name, div, conv, ps else
+  let rec aux' chr line =
+   if chr = "#"
+    then chr, name, div, conv, ps
+   else if chr = "$"
+    then "#", line, div, conv, ps
+   else if chr = "D"
+    then chr, name, line, conv, ps
+   else if chr = "C"
+    then chr, name, div, line::conv, ps
+   else if chr = "N"
+    then chr, name, div, conv, line::ps
+   else if last = ""
+    then raise (ParsingError ("Unexpected at beginning of problem: " ^ chr))
+   else aux' last (chr ^ line) in
+  aux' chr line in
+ let _, name, div, conv, ps = List.fold_left aux ("#", "?", "", [], []) lines in
  let div_provided = div <> "" in
  let div = if div_provided then div else "BOT" in
  let strs = [div] @ ps @ conv in
@@ -235,8 +244,22 @@ let conv = Util.filter_map (
 let ps = List.map (
  function
   | #i_n_var as y -> y
-  | _ -> raise (ParsingError "A term in num is not i_n_var")
+  | _ as y -> raise (ParsingError ("A term in num is not i_n_var" ^ Num.string_of_nf y))
  ) ps in
-
  name, div, conv, ps, free
 ;;
+
+
+let from_file path =
+ let lines = ref [] in
+ let chan = open_in path in
+ let _ = try
+  while true; do
+    lines := input_line chan :: !lines
+  done
+ with End_of_file ->
+  close_in chan in
+ let txt = String.concat "\n" (List.rev !lines) in
+ let problems = Str.split (Str.regexp "\\$") txt in
+ List.map problem_of_string (List.tl (List.map ((^) "$") problems))
+;;