X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.mli;h=d131edbf79b65b46315d19510ec9e96583b9f58e;hb=refs%2Fheads%2Fstrong_simple_measure;hp=c073c3af1a7436e537381ea6b88b234a5735dc49;hpb=e4aa4a66dd0a4946607245a0f43eab803f2770c4;p=fireball-separation.git

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c073c3a..d131edb 100644
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,9 +1,15 @@
-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 -> 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
+val problem_of_string:
+ 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 *)
+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