X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.mli;h=8dba8542ca4548e5f64201a1b80dcc7d88c3d202;hb=461dcd3dc0bf5090be9980548bc1874a423dc6cc;hp=c205cb293640fc6ef7c40e287971547cc722a113;hpb=123d64bb5ae7127f6a51cbf44b63341de001a187;p=fireball-separation.git

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c205cb2..8dba854 100644
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,10 +1,25 @@
+type term =
+  | Var of int
+  | App of term * term
+  | Lam of term
+
 exception ParsingError of string
 
-(* parses a string to a term *)
-(* val parse: string -> Num.nf *)
-(* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)
-val parse_many: string list -> Num.nf list * string list
-val parse': string list -> Num.nf list * string list
-val parse_problem:
+(* val problem_of_string:
  string ->
-  Num.i_var option * Num.i_n_var list * Num.i_n_var list
+  string (* problem label *)
+  * Num.i_var option (* div *)
+  * Num.i_n_var list (* conv *)
+  * Num.i_n_var list (* ps *)
+  * string list (* names of free variables *)
+val from_file : string ->
+ (string (* problem label *)
+ * Num.i_var option (* div *)
+ * Num.i_n_var list (* conv *)
+ * Num.i_n_var list (* ps *)
+ * string list (* names of free variables *)) list *)
+
+ (* parses a string to a term *)
+ val parse: string -> term
+ (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)
+ val parse_many: string list -> term list * string list