]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/parser.mli
Copied old code back in parser, to make andrea8 great again
[fireball-separation.git] / ocaml / parser.mli
index c073c3af1a7436e537381ea6b88b234a5735dc49..8dba8542ca4548e5f64201a1b80dcc7d88c3d202 100644 (file)
@@ -3,7 +3,23 @@ type term =
   | App of term * term\r
   | Lam of term\r
 \r
-(* parses a string to a term *)\r
-val parse: string -> term\r
-(* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
-val parse_many: string list -> term list * string list\r
+exception ParsingError of string\r
+\r
+(* val problem_of_string:\r
+ string ->\r
+  string (* problem label *)\r
+  * Num.i_var option (* div *)\r
+  * Num.i_n_var list (* conv *)\r
+  * Num.i_n_var list (* ps *)\r
+  * string list (* names of free variables *)\r
+val from_file : string ->\r
+ (string (* problem label *)\r
+ * Num.i_var option (* div *)\r
+ * Num.i_n_var list (* conv *)\r
+ * Num.i_n_var list (* ps *)\r
+ * string list (* names of free variables *)) list *)\r
+\r
+ (* parses a string to a term *)\r
+ val parse: string -> term\r
+ (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
+ val parse_many: string list -> term list * string list\r