Copied old code back in parser, to make andrea8 great again

[fireball-separation.git] / ocaml / parser.mli

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index 47cfb28aaee6f814d43d319c99e754a68e2b0256..8dba8542ca4548e5f64201a1b80dcc7d88c3d202 100644 (file)
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,7 +1,11 @@
+type term =\r
+  | Var of int\r
+  | App of term * term\r
+  | Lam of term\r
+\r
 exception ParsingError of string\r
 \r
-val parse': string list -> Num.nf list * string list\r
-val problem_of_string:\r
+(* val problem_of_string:\r
  string ->\r
   string (* problem label *)\r
   * Num.i_var option (* div *)\r
@@ -13,4 +17,9 @@ val from_file : string ->
  * 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
+ * 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