From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 12:48:49 +0000 (+0200)
Subject: Simple algorithm by Andrea
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c0471d4d46eba3d99476f08c35292500a9fb43f;p=fireball-separation.git

Simple algorithm by Andrea

Cherry-picked from f260
---

diff --git a/ocaml/Makefile b/ocaml/Makefile
index 138cc99..5859d51 100644
--- a/ocaml/Makefile
+++ b/ocaml/Makefile
@@ -1,8 +1,8 @@
 OCAMLC = ocamlopt -g -rectypes
 LIB = unix.cmxa str.cmxa
-UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx
+UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx parser_andrea.cmx
 
-all: a.out test4.out
+all: a.out test4.out andrea.out
 
 run: test4.out
 	bash run
@@ -13,6 +13,9 @@ a.out: $(UTILS) lambda4.cmx problems.cmx
 test4.out: $(UTILS) lambda4.cmx test.ml
 	$(OCAMLC) -o test4.out $(LIB) $^
 
+andrea.out: $(UTILS) andrea.ml
+	$(OCAMLC) -o andrea.out $(LIB) $(UTILS) andrea.ml
+
 %.cmi: %.mli
 	$(OCAMLC) -c $<
 
diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
new file mode 100644
index 0000000..f1cfc01
--- /dev/null
+++ b/ocaml/andrea.ml
@@ -0,0 +1,405 @@
+let (++) f g x = f (g x);;
+let id x = x;;
+
+let print_hline = Console.print_hline;;
+
+type var = int;;
+type t =
+ | V of var
+ | A of t * t
+ | L of t
+ | B (* bottom *)
+ | P (* pacman *)
+;;
+
+let eta_eq =
+ let rec aux l1 l2 t1 t2 = match t1, t2 with
+  | L t1, L t2 -> aux l1 l2 t1 t2
+  | L t1, t2 -> aux l1 (l2+1) t1 t2
+  | t1, L t2 -> aux (l1+1) l2 t1 t2
+  | V a, V b -> a + l1 = b + l2
+  | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2
+  | _, _ -> false
+ in aux 0 0
+;;
+
+type problem = {
+   orig_freshno: int
+ ; freshno : int
+ ; div : t
+ ; conv : t
+ ; sigma : (var * t) list (* substitutions *)
+ ; stepped : var list
+}
+
+exception Done of (var * t) list (* substitution *);;
+exception Fail of int * string;;
+
+let string_of_t p =
+  let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
+  let rec string_of_term_w_pars level = function
+    | V v -> if v >= level then "`" ^ string_of_int (v-level) else
+     let nn = level - v-1 in
+      if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4))
+    | A _
+    | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"
+    | B -> "BOT"
+    | P -> "PAC"
+  and string_of_term_no_pars_app level = function
+    | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)
+    | _ as t -> string_of_term_w_pars level t
+  and string_of_term_no_pars_lam level = function
+    | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)
+    | _ as t -> string_of_term_no_pars level t
+  and string_of_term_no_pars level = function
+    | L _ as t -> string_of_term_no_pars_lam level t
+    | _ as t -> string_of_term_no_pars_app level t
+  in string_of_term_no_pars 0
+;;
+
+let string_of_problem p =
+ let lines = [
+  "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);
+  "[DV] " ^ (string_of_t p p.div);
+  "[CV] " ^ (string_of_t p p.conv);
+ ] in
+ String.concat "\n" lines
+;;
+
+let problem_fail p reason =
+ print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
+ print_endline (string_of_problem p);
+ raise (Fail (-1, reason))
+;;
+
+let freshvar ({freshno} as p) =
+ {p with freshno=freshno+1}, freshno+1
+;;
+
+let rec is_inert =
+ function
+ | A(t,_) -> is_inert t
+ | V _ -> true
+ | L _ | B | P -> false
+;;
+
+let is_var = function V _ -> true | _ -> false;;
+let is_lambda = function L _ -> true | _ -> false;;
+
+let rec head_of_inert = function
+ | V n -> n
+ | A(t, _) -> head_of_inert t
+ | _ -> assert false
+;;
+
+let rec args_no = function
+ | V _ -> 0
+ | A(t, _) -> 1 + args_no t
+ | _ -> assert false
+;;
+
+let rec subst level delift fromdiv sub =
+ function
+ | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)
+ | L t -> L (subst (level + 1) delift fromdiv sub t)
+ | A (t1,t2) ->
+  let t1 = subst level delift fromdiv sub t1 in
+  let t2 = subst level delift fromdiv sub t2 in
+  if t1 = B || t2 = B then B else mk_app fromdiv t1 t2
+ | B -> B
+ | P -> P
+and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
+ | B | _ when t2 = B -> B
+ | L t1 -> subst 0 true fromdiv (0, t2) t1
+ | t1 -> A (t1, t2)
+and lift n =
+ let rec aux n' =
+  function
+  | V m -> V (if m >= n' then m + n else m)
+  | L t -> L (aux (n'+1) t)
+  | A (t1, t2) -> A (aux n' t1, aux n' t2)
+  | B -> B
+  | P -> P
+ in aux 0
+;;
+let subst = subst 0 false;;
+
+let subst_in_problem (sub: var * t) (p: problem) =
+print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));
+ let p = {p with stepped=(fst sub)::p.stepped} in
+ let conv = subst false sub p.conv in
+ let div = subst true sub p.div in
+ let p = {p with div; conv} in
+ (* print_endline ("after sub: \n" ^ string_of_problem p); *)
+ {p with sigma=sub::p.sigma}
+;;
+
+let get_subterm_with_head_and_args hd_var n_args =
+ let rec aux = function
+ | V _ | L _ | B | P -> None
+ | A(t1,t2) as t ->
+   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1
+    then Some t
+    else match aux t2 with
+    | None -> aux t1
+    | Some _ as res -> res
+ in aux
+;;
+
+(* let rec simple_explode p =
+ match p.div with
+ | V var ->
+  let subst = var, B in
+  sanity (subst_in_problem subst p)
+ | _ -> p *)
+
+let sanity p =
+ print_endline (string_of_problem p); (* non cancellare *)
+ if p.div = B then raise (Done p.sigma);
+ if not (is_inert p.div) then problem_fail p "p.div converged";
+ if p.conv = B then problem_fail p "p.conv diverged";
+ (* let p = if is_var p.div then simple_explode p else p in *)
+ p
+;;
+
+let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
+
+(* eat the arguments of the divergent and explode.
+ It does NOT perform any check, may fail if done unsafely *)
+let eat p =
+print_cmd "EAT" "";
+ let var = head_of_inert p.div in
+ let n = args_no p.div in
+ let rec aux m t =
+  if m = 0
+   then lift n t
+   else L (aux (m-1) t) in
+ let subst = var, aux n B in
+ sanity (subst_in_problem subst p)
+;;
+
+(* step on the head of div, on the k-th argument, with n fresh vars *)
+let step k n p =
+ let var = head_of_inert p.div in
+ print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
+ let rec aux' p m t =
+  if m < 0
+   then p, t
+    else
+     let p, v = freshvar p in
+     let p, t = aux' p (m-1) t in
+      p, A(t, V (v + k + 1)) in
+ let p, t = aux' p n (V 0) in
+ let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in
+ let rec aux m t =
+  if m < 0
+   then aux' (k-1) t
+   else L (aux (m-1) t) in
+ let t = aux k t in
+ let subst = var, t in
+ sanity (subst_in_problem subst p)
+;;
+
+let parse strs =
+  let rec aux level = function
+  | Parser_andrea.Lam t -> L (aux (level + 1) t)
+  | Parser_andrea.App (t1, t2) ->
+   if level = 0 then mk_app false (aux level t1) (aux level t2)
+    else A(aux level t1, aux level t2)
+  | Parser_andrea.Var v -> V v
+  in let (tms, free) = Parser_andrea.parse_many strs
+  in (List.map (aux 0) tms, free)
+;;
+
+let problem_of div conv =
+ print_hline ();
+ let all_tms, var_names = parse ([div; conv]) in
+ let div, conv = List.hd all_tms, List.hd (List.tl all_tms) in
+ let varno = List.length var_names in
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in
+ (* activate bombs *)
+ let p = try
+  let subst = Util.index_of "BOMB" var_names, L B in
+   subst_in_problem subst p
+  with Not_found -> p in
+ (* activate pacmans *)
+ let p = try
+  let subst = Util.index_of "PACMAN" var_names, P in
+   let p = subst_in_problem subst p in
+   (print_endline ("after subst in problem " ^ string_of_problem p); p)
+  with Not_found -> p in
+ (* initial sanity check *)
+ sanity p
+;;
+
+let exec div conv cmds =
+ let p = problem_of div conv in
+ try
+  problem_fail (List.fold_left (|>) p cmds) "Problem not completed"
+ with
+ | Done _ -> ()
+;;
+
+let inert_cut_at n t =
+ let rec aux t =
+  match t with
+  | V _ as t -> 0, t
+  | A(t1,_) as t ->
+    let k', t' = aux t1 in
+     if k' = n then n, t'
+      else k'+1, t
+  | _ -> assert false
+ in snd (aux t)
+;;
+
+let find_eta_difference p t n_args =
+ let t = inert_cut_at n_args t in
+ let rec aux t u k = match t, u with
+ | V _, V _ -> assert false (* div subterm of conv *)
+ | A(t1,t2), A(u1,u2) ->
+    if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)
+    else aux t1 u1 (k-1)
+ | _, _ -> assert false
+ in aux p.div t n_args
+;;
+
+let rec no_leading_lambdas = function
+ | L t -> 1 + no_leading_lambdas t
+ | _ -> 0
+;;
+
+let compute_max_lambdas_at hd_var j =
+ let rec aux hd = function
+ | A(t1,t2) ->
+    (if head_of_inert t1 = hd && args_no t1 = j
+      then max (
+       if is_inert t2 && head_of_inert t2 = hd
+        then j - args_no t2
+        else no_leading_lambdas t2)
+      else id) (max (aux hd t1) (aux hd t2))
+ | L t -> aux (hd+1) t
+ | V _ -> 0
+ | _ -> assert false
+ in aux hd_var
+;;
+
+let rec auto p =
+ let hd_var = head_of_inert p.div in
+ let n_args = args_no p.div in
+ match get_subterm_with_head_and_args hd_var n_args p.conv with
+ | None ->
+    (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())
+ | Some t ->
+  let j = find_eta_difference p t n_args - 1 in
+  let k = max
+   (compute_max_lambdas_at hd_var j p.div)
+    (compute_max_lambdas_at hd_var j p.conv) in
+  let p = step j k p in
+  auto p
+;;
+
+let interactive div conv cmds =
+ let p = problem_of div conv in
+ try (
+ let p = List.fold_left (|>) p cmds in
+ let rec f p cmds =
+  let nth spl n = int_of_string (List.nth spl n) in
+  let read_cmd () =
+   let s = read_line () in
+   let spl = Str.split (Str.regexp " +") s in
+   s, let uno = List.hd spl in
+    try if uno = "eat" then eat
+    else if uno = "step" then step (nth spl 1) (nth spl 2)
+    else failwith "Wrong input."
+    with Failure s -> print_endline s; (fun x -> x) in
+  let str, cmd = read_cmd () in
+  let cmds = (" " ^ str ^ ";")::cmds in
+  try
+   let p = cmd p in f p cmds
+  with
+  | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)
+ in f p []
+ ) with Done _ -> ()
+;;
+
+let rec conv_join = function
+ | [] -> "@"
+ | x::xs -> conv_join xs ^ " ("^ x ^")"
+;;
+
+let _ = exec
+ "x x"
+ (conv_join["x y"; "y y"; "y x"])
+ [ step 0 0; eat ]
+;;
+
+auto (problem_of "x x" "@ (x y) (y y) (y x)");;
+auto (problem_of "x y" "@ (x (_. x)) (y z) (y x)");;
+auto (problem_of "a (x. x b) (x. x c)" "@ (a (x. b b) @) (a @ c) (a (x. x x) a) (a (a a a) (a c c))");;
+
+interactive "x y"
+"@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;
+
+auto (problem_of "x (y. x y y)" "x (y. x y x)");;
+
+auto (problem_of "x a a a a" (conv_join[
+ "x b a a a";
+ "x a b a a";
+ "x a a b a";
+ "x a a a b";
+]));
+
+(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)
+auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[
+ "x a a a a (_. a) b b b";
+ "x a a a a (_. _. _. _. x. y. x y)";
+]));
+
+
+print_hline();
+print_endline "ALL DONE. "
+
+(* TEMPORARY TESTING FACILITY BELOW HERE *)
+
+let acaso l =
+    let n = Random.int (List.length l) in
+    List.nth l n
+;;
+
+let acaso2 l1 l2 =
+  let n1 = List.length l1 in
+  let n = Random.int (n1 + List.length l2) in
+  if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n
+;;
+
+let gen n vars =
+  let rec aux n inerts lams =
+    if n = 0 then List.hd inerts, List.hd (Util.sort_uniq (List.tl inerts))
+    else let inerts, lams = if Random.int 2 = 0
+      then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
+      else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
+    in aux (n-1) inerts lams
+  in aux (2*n) vars []
+;;
+
+let f () =
+  let complex = 200 in
+  let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
+  gen complex vars
+
+  let rec repeat f n =
+    prerr_endline "\n########################### NEW TEST ###########################";
+    f () ;
+    if n > 0 then repeat f (n-1)
+  ;;
+
+
+let main () =
+ Random.self_init ();
+ repeat (fun _ ->
+   let div, conv = f () in
+   auto (problem_of div conv)
+ ) 100;
+;;
+
+(* main ();; *)
diff --git a/ocaml/parser_andrea.ml b/ocaml/parser_andrea.ml
new file mode 100644
index 0000000..fbce730
--- /dev/null
+++ b/ocaml/parser_andrea.ml
@@ -0,0 +1,266 @@
+type term =
+  | Var of int
+  | App of term * term
+  | Lam of term
+;;
+
+let mk_app x y = App(x, y);;
+let mk_lam x = Lam x;;
+let mk_var x = Var x;;
+
+exception ParsingError of string;;
+
+let isAlphaNum c = let n = Char.code c in
+ (48 <= n && n <= 90) || (95 <= n && n <= 122) ;;
+let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;
+
+(* FIXME *)
+let mk_var' (bound, free) x =
+  if x <> "@" && List.mem x bound
+  then free, mk_var (Util.index_of x bound)
+  else if x <> "@" && List.mem x free
+       then free, mk_var (List.length bound + Util.index_of x free)
+       else (free @ [x]), mk_var (List.length bound + List.length free)
+;;
+
+let mk_app' = function
+  | [] ->  assert false
+  | t :: ts -> List.fold_left mk_app t ts
+;;
+
+let explode s =
+ let len = String.length s in
+  let rec aux i l =
+    if i >= len || s.[i] = '#' then l else aux (i+1) (s.[i] :: l)
+  in List.rev (aux 0 [])
+;;
+
+let implode l =
+  let res = String.create (List.length l) in
+  let rec aux i = function
+    | [] -> res
+    | c :: l -> String.set res i c; aux (i + 1) l in
+  aux 0 l
+;;
+
+let rec strip_spaces = function
+  | c::cs when isSpace c -> strip_spaces cs
+  | cs -> cs
+;;
+
+let read_var s =
+  let rec aux = function
+  | [] -> None, []
+  | c::cs as x ->
+    if c = '@' then
+     (if cs <> [] && (let hd = List.hd cs in hd = '@' || isAlphaNum hd)
+     then raise (ParsingError ("Unexpected `"^String.make 1 (List.hd cs)^"` after `@`."))
+     else Some['@'], cs)
+    else if isAlphaNum c
+    then match aux cs with
+         | (Some x), cs' -> Some (c :: x), cs'
+         | None, cs' -> (Some [c]), cs'
+    else None, x
+  in match aux s with
+    | None, y -> None, y
+    | Some x, y -> Some (implode x), y
+;;
+
+let read_var' (bound, free as vars) s =
+  match read_var s with
+  | Some varname, cs ->
+    let free, v = mk_var' vars varname in
+    Some [v], cs, (bound, free)
+  | None, _ -> raise (ParsingError ("Can't read variable"))
+;;
+
+let rec read_smt vars =
+  let check_if_lambda cs = match read_var cs with
+    | None, _ -> false
+    | Some x, cs -> match strip_spaces cs with
+      | [] -> false
+      | c::_ -> c = '.'
+  in let read_lambda (bound, free) cs = (
+    match read_var (strip_spaces cs) with
+      | Some varname, cs ->
+      let vars' = (varname::bound, free) in
+      (match strip_spaces cs with
+        | [] -> raise (ParsingError "Lambda expression incomplete")
+        | c::cs -> (if c = '.' then (match read_smt vars' cs with
+          | None, _, _ -> raise (ParsingError "Lambda body expected")
+          | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)
+          | Some _, _, _ -> assert false
+          ) else raise (ParsingError "Expected `.` after variable in lambda")
+        ))
+      | _, _ -> assert false
+ ) in let rec aux vars cs =
+  match strip_spaces cs with
+  | [] -> None, [], vars
+  | c::_ as x ->
+      let tms, cs, vars = (
+           if c = '(' then read_pars vars x
+      else if c = ')' then (None, x, vars)
+      else if check_if_lambda x then read_lambda vars x
+      else read_var' vars x) in
+      match tms with
+      | Some [tm] -> (
+        match aux vars cs with
+          | None, cs, vars -> Some [tm], cs, vars
+          | Some ts, cs, vars -> Some (tm :: ts), cs, vars
+        )
+      | Some _ -> assert false
+      | None -> None, x, vars
+  in fun cs -> match aux vars cs with
+    | None, cs, vars -> None, cs, vars
+    | Some ts, cs, vars -> Some [mk_app' ts], cs, vars
+and read_pars vars = function
+  | [] -> None, [], vars
+  | c::cs -> if c = '(' then (
+    let tm, cs, vars = read_smt vars cs in
+    let cs = strip_spaces cs in
+    match cs with
+      | [] -> None, [], vars
+      | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError "Missing `)`")
+    ) else assert false
+;;
+
+let parse x =
+  match read_smt ([],[]) (explode x) with
+  | Some [y], [], _ -> y
+  | _, _, _ -> assert false
+;;
+
+let parse_many strs =
+  let f (x, y) z = match read_smt y (explode z) with
+  | Some[tm], [], vars -> (tm :: x, vars)
+  | _, _, _ -> assert false
+  in let aux = List.fold_left f ([], ([], []))
+  in let (tms, (_, free)) = aux strs
+  in (List.rev tms, free)
+;;
+
+(**********************************************************************
+
+let rec string_of_term = function
+  | Tvar n -> string_of_int n
+  | Tapp(t1, t2) -> "(" ^ string_of_term t1 ^ " " ^ string_of_term t2 ^ ")"
+  | Tlam(t1) -> "(\\" ^ string_of_term t1 ^ ")"
+;;
+
+let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j"));;
+
+
+*******************************************************************************)
+
+(* let problem_of_string s =
+ let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in
+ let head, lines = List.hd lines, List.tl lines in
+ let name = String.trim (String.sub head 1 (String.length head - 1)) in
+ let lines = List.filter ((<>) "") lines in
+ let aux (last, div, conv, ps) line =
+  let chr = String.sub line 0 1 in
+  let line = String.trim (String.sub line 1 (String.length line - 1)) in
+  if line = "" then chr, div, conv, ps else
+  let rec aux' chr line =
+   if chr = "#"
+    then chr, div, conv, ps
+   else if chr = "D"
+    then chr, line, conv, ps
+   else if chr = "C"
+    then chr, div, line::conv, ps
+   else if chr = "N"
+    then chr, div, conv, line::ps
+   else if chr = " "
+    then aux' last line
+   else raise (ParsingError
+     ("Unexpected at beginning of problem: `" ^ chr ^ "` " ^ line)) in
+  aux' chr line in
+ let _, 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
+
+ if List.length ps = 0 && List.length conv = 0
+  then raise (ParsingError "Parsed empty problem");
+
+ (* parse' *)
+ let (tms, free) = parse_many strs in
+ (* Replace pacmans and bottoms *)
+ let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in
+ let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in
+ let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in
+ let fix lev v =
+  if v = lev + n_bot then `Bottom
+   else if v = lev + n_pac then `Pacman
+    else if v = lev + n_bomb then `Lam(true, `Bottom)
+    else if v = lev then `Var(v, min_int) (* zero *)
+     else `Var(v,1) in (* 1 by default when variable not applied *)
+ (* Fix arity *)
+ let open Num in
+ let exclude_bottom = function
+ | #nf_nob as t -> t
+ (* actually, the following may be assert false *)
+ | `Bottom -> raise (ParsingError "Input term not in normal form") in
+ let rec aux_nob lev : nf_nob -> nf = function
+ | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args)
+ | `Var(n,_) -> fix lev n
+ | `Lam(_,t) -> `Lam (true, aux (lev+1) t)
+ | `Match _ | `N _ -> assert false
+ | `Pacman -> `Pacman
+ and aux lev : Num.nf -> Num.nf = function
+  | #nf_nob as t -> aux_nob lev t
+  | `Bottom -> assert false in
+let all_tms = List.map (aux 0) (tms :> Num.nf list) in
+
+(* problem_of *)
+let div, (ps, conv) = List.hd all_tms, Util.list_cut (List.length ps, List.tl all_tms) in
+
+let div = if not div_provided || div = `Bottom
+ then None
+ else match div with
+  | `I _ as t -> Some t
+  | _ -> raise (ParsingError "D is not an inert in the initial problem") in
+let conv = Util.filter_map (
+ function
+ | #i_n_var as t -> Some t
+ | `Lam _ -> None
+ | _ -> raise (ParsingError "A C-term is not i_n_var")
+ ) conv in
+let ps = List.map (
+ function
+  | #i_n_var as y -> y
+  | _ -> raise (ParsingError "An N-term is not i_n_var")
+ ) 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 "[\n\r]+\\$") txt in
+ List.map problem_of_string (List.tl (List.map ((^) "$") problems))
+;; *)
+
+let parse x =
+  match read_smt ([],[]) (explode x) with
+  | Some [y], [], _ -> y
+  | _, _, _ -> assert false
+;;
+
+
+let parse_many strs =
+  let f (x, y) z = match read_smt y (explode z) with
+  | Some[tm], [], vars -> (tm :: x, vars)
+  | _, _, _ -> assert false
+  in let aux = List.fold_left f ([], ([], []))
+  in let (tms, (_, free)) = aux strs
+  in (List.rev tms, free)
+;;
diff --git a/ocaml/parser_andrea.mli b/ocaml/parser_andrea.mli
new file mode 100644
index 0000000..8dba854
--- /dev/null
+++ b/ocaml/parser_andrea.mli
@@ -0,0 +1,25 @@
+type term =
+  | Var of int
+  | App of term * term
+  | Lam of term
+
+exception ParsingError of string
+
+(* 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 *)
+
+ (* 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