From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 2 Jun 2018 15:58:19 +0000 (+0200)
Subject: Copied files from strong_simple branch + Implemented andrea's finish
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84b6cd9687af3603acc8f67061d38d708bcada4d;p=fireball-separation.git

Copied files from strong_simple branch + Implemented andrea's finish

- Fixes parser, problems
---

diff --git a/ocaml/Makefile b/ocaml/Makefile
index 701d50a..b76514c 100644
--- a/ocaml/Makefile
+++ b/ocaml/Makefile
@@ -1,11 +1,14 @@
 OCAMLC = ocamlopt -g -rectypes
 LIB = unix.cmxa str.cmxa
-UTILS = util.cmx console.cmx parser.cmx
+UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx problems.cmx
 
-all: andrea.out
+all: simple.out simple_test.out
 
-andrea.out: $(UTILS) andrea.ml
-	$(OCAMLC) -o andrea.out $(LIB) $(UTILS) andrea.ml
+simple.out: $(UTILS) simple.cmx
+	$(OCAMLC) -o simple.out $(LIB) $^
+
+simple_test.out: $(UTILS) simple.cmx simple_test.ml
+	$(OCAMLC) -o simple_test.out $(LIB) $^
 
 %.cmi: %.mli
 	$(OCAMLC) -c $<
diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
deleted file mode 100644
index 24db4c9..0000000
--- a/ocaml/andrea.ml
+++ /dev/null
@@ -1,331 +0,0 @@
-let (++) f g x = f (g x);;
-let id x = x;;
-let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;
-
-let print_hline = Console.print_hline;;
-
-type var = int;;
-type t =
- | V of var
- | A of t * t
- | L of t
- | B (* bottom *)
-;;
-
-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
-;;
-
-(* does NOT lift t *)
-let mk_lams = fold_nat (fun x _ -> L x) ;;
-
-let string_of_t =
-  let string_of_bvar =
-   let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
-   let bvarsno = List.length bound_vars in
-   fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in
-  let rec string_of_term_w_pars level = function
-    | V v -> if v >= level then "`" ^ string_of_int (v-level) else
-       string_of_bvar (level - v-1)
-    | A _
-    | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"
-    | B -> "BOT"
-  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 level = function
-    | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t
-    | _ as t -> string_of_term_no_pars_app level t
-  in string_of_term_no_pars 0
-;;
-
-type problem = {
-   orig_freshno: int
- ; freshno : int
- ; div : t
- ; conv : t
- ; sigma : (var * t) list (* substitutions *)
- ; stepped : var list
-}
-
-let string_of_problem p =
- let lines = [
-  "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);
-  "[DV] " ^ string_of_t p.div;
-  "[CV] " ^ string_of_t p.conv;
- ] in
- String.concat "\n" lines
-;;
-
-exception Done of (var * t) list (* substitution *);;
-exception Fail of int * string;;
-
-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 -> false
-;;
-
-let is_var = function V _ -> true | _ -> false;;
-let is_lambda = function L _ -> true | _ -> false;;
-
-let rec no_leading_lambdas = function
- | L t -> 1 + no_leading_lambdas t
- | _ -> 0
-;;
-
-let rec get_inert = function
- | V n -> (n,0)
- | A(t, _) -> let hd,args = get_inert t in hd,args+1
- | _ -> assert false
-;;
-
-let rec subst level delift 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 sub t)
- | A (t1,t2) ->
-  let t1 = subst level delift sub t1 in
-  let t2 = subst level delift sub t2 in
-  mk_app t1 t2
- | B -> B
-and mk_app t1 t2 = match t1 with
- | B | _ when t2 = B -> B
- | L t1 -> subst 0 true (0, t2) t1
- | t1 -> A (t1, t2)
-and lift n =
- let rec aux lev =
-  function
-  | V m -> V (if m >= lev then m + n else m)
-  | L t -> L (aux (lev+1) t)
-  | A (t1, t2) -> A (aux lev t1, aux lev t2)
-  | B -> B
- in aux 0
-;;
-let subst = subst 0 false;;
-
-let subst_in_problem (sub: var * t) (p: problem) =
-print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));
- {p with
-  div=subst sub p.div;
-  conv=subst sub p.conv;
-  stepped=(fst sub)::p.stepped;
-  sigma=sub::p.sigma}
-;;
-
-let get_subterm_with_head_and_args hd_var n_args =
- let rec aux lev = function
- | V _ | B -> None
- | L t -> aux (lev+1) t
- | A(t1,t2) as t ->
-   let hd_var', n_args' = get_inert t1 in
-   if hd_var' = hd_var + lev && n_args <= 1 + n_args'
-    then Some (lift ~-lev t)
-    else match aux lev t2 with
-    | None -> aux lev t1
-    | Some _ as res -> res
- in aux 0
-;;
-
-let sanity p =
- print_endline (string_of_problem p); (* non cancellare *)
- if p.conv = B then problem_fail p "p.conv diverged";
- if p.div = B then raise (Done p.sigma);
- if not (is_inert p.div) then problem_fail p "p.div converged"
-;;
-
-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, n = get_inert p.div in
- let subst = var, mk_lams B n in
- let p = subst_in_problem subst p in
- sanity p; p
-;;
-
-(* step on the head of div, on the k-th argument, with n fresh vars *)
-let step k n p =
- let var, _ = get_inert p.div in
-print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");
- let p, t = (* apply fresh vars *)
-  fold_nat (fun (p, t) _ ->
-    let p, v = freshvar p in
-    p, A(t, V (v + k + 1))
-  ) (p, V 0) n in
- let t = (* apply unused bound variables V_{k-1}..V_1 *)
-  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
- let t = mk_lams t (k+1) in (* make leading lambdas *)
- let subst = var, t in
- let p = subst_in_problem subst p in
- sanity p; p
-;;
-
-let parse strs =
-  let rec aux level = function
-  | Parser.Lam t -> L (aux (level + 1) t)
-  | Parser.App (t1, t2) ->
-   if level = 0 then mk_app (aux level t1) (aux level t2)
-    else A(aux level t1, aux level t2)
-  | Parser.Var v -> V v in
-  let (tms, free) = Parser.parse_many strs in
-  (List.map (aux 0) tms, free)
-;;
-
-let problem_of div conv =
- print_hline ();
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in
- let varno = List.length var_names in
- let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in
- (* initial sanity check *)
- sanity p; 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 _ -> ()
-;;
-
-(* drops the arguments of t after the n-th *)
-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 t2) ^ " <> " ^ (string_of_t u2)); k)
-    else aux t1 u1 (k-1)
- | _, _ -> assert false
- in aux p.div t n_args
-;;
-
-let compute_max_lambdas_at hd_var j =
- let rec aux hd = function
- | A(t1,t2) ->
-    (if get_inert t1 = (hd, j)
-      then max ( (*FIXME*)
-       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd
-        then let hd', j' = get_inert t2 in j - j'
-        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, n_args = get_inert p.div in
- match get_subterm_with_head_and_args hd_var n_args p.conv with
- | None ->
-    (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())
- | Some t ->
-  let j = find_eta_difference p t n_args - 1 in
-  let k = 1 + 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 auto' a b = auto (problem_of a (conv_join b));;
-
-(* Example usage of exec, interactive:
-
-exec
- "x x"
- (conv_join["x y"; "y y"; "y x"])
- [ step 0 1; eat ]
-;;
-
-interactive "x y"
- "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]
-;;
-
-*)
-
-auto' "x x" ["x y"; "y y"; "y x"] ;;
-auto' "x y" ["x (_. x)"; "y z"; "y x"] ;;
-auto' "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)"] ;;
-
-auto' "x (y. x y y)" ["x (y. x y x)"] ;;
-
-auto' "x a a a a" [
- "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' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
- "x a a a a (_. a) b b b";
- "x a a a a (_. _. _. _. x. y. x y)";
-] ;;
-
-
-print_hline();
-print_endline "ALL DONE. "
diff --git a/ocaml/console.ml b/ocaml/console.ml
index 696a74d..f3fbef6 100644
--- a/ocaml/console.ml
+++ b/ocaml/console.ml
@@ -40,7 +40,7 @@ let cols =
 ;;
 
 let writeall s =
-  let _ = Unix.send socket s 0 (String.length s) [] in ()
+  let _ = Unix.send socket (Bytes.of_string s) 0 (String.length s) [] in ()
 ;;
 
 let concat ls = (String.concat sepx ls) ^ endx;;
diff --git a/ocaml/listx.ml b/ocaml/listx.ml
new file mode 100644
index 0000000..821e281
--- /dev/null
+++ b/ocaml/listx.ml
@@ -0,0 +1,71 @@
+(* Non-empty lists *)
+type 'a listx =
+  | Nil of 'a
+  | Cons of ('a * 'a listx)
+
+let rec fold_left f acc l =
+  match l with
+  | Nil x -> f acc x
+  | Cons (x, l') -> fold_left f (f acc x) l'
+
+let hd =
+ function
+  | Nil x
+  | Cons (x,_) -> x
+
+let rec map f =
+  function
+  | Nil x -> Nil (f x)
+  | Cons (x, l') -> Cons (f x, map f l')
+
+let rec append l =
+  function
+  | Nil x -> Cons (x, l)
+  | Cons (x, l') -> Cons (x, append l l')
+
+let rec length = function
+  | Nil _ -> 1
+  | Cons (_, xs) -> 1 + (length xs)
+
+let rec assoc x = function
+  | Nil (y,t)
+  | Cons ((y,t),_) when x=y -> t
+  | Nil _ -> raise Not_found
+  | Cons (_,l) -> assoc x l
+
+let rec to_list =
+ function
+    Nil x -> [x]
+  | Cons (x,l) -> x::to_list l
+
+let rec from_list =
+ function
+    [] -> raise (Failure "from_list: empty list")
+  | [x] -> Nil x
+  | x::l -> Cons(x,from_list l)
+
+let rec split_nth n l =
+ match n,l with
+    0,_ -> []
+ | 1,Nil x -> [x]
+ | n,Cons (hd,tl) -> hd::split_nth (n-1) tl
+ | _,_ -> raise (Failure "split_nth: not enough args")
+
+let rec max =
+  function
+  | Nil x -> x
+  | Cons (x, l) -> Pervasives.max x (max l)
+
+let rec last =
+  function
+  | Nil x -> x
+  | Cons (_, l) -> last l
+(*
+let rec nth i l = match l, i with
+ | Cons (x, _), 1  -> x
+ | _, n when n <= 0 -> raise (Invalid_argument "Listx.nth")
+ | Cons (_, xs), n -> nth (n-1) xs
+ | Nil x, 1        -> x
+ | Nil _, _        -> raise (Invalid_argument "Listx.nth")
+;;
+*)
diff --git a/ocaml/listx.mli b/ocaml/listx.mli
new file mode 100644
index 0000000..a43bc4e
--- /dev/null
+++ b/ocaml/listx.mli
@@ -0,0 +1,12 @@
+type 'a listx = Nil of 'a | Cons of ('a * 'a listx)
+val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b listx -> 'a
+val hd : 'a listx -> 'a
+val map : ('a -> 'b) -> 'a listx -> 'b listx
+val append : 'a listx -> 'a listx -> 'a listx
+val length : 'a listx -> int
+val assoc : 'a -> ('a * 'b) listx -> 'b
+val to_list : 'a listx -> 'a list
+val from_list : 'a list -> 'a listx
+val split_nth : int -> 'a listx -> 'a list
+val max : 'a listx -> 'a
+val last : 'a listx -> 'a
diff --git a/ocaml/num.ml b/ocaml/num.ml
new file mode 100644
index 0000000..dda88a7
--- /dev/null
+++ b/ocaml/num.ml
@@ -0,0 +1,364 @@
+open Util
+open Util.Vars
+open Pure
+
+(* debug options *)
+let debug_display_arities = false;;
+
+(************ Syntax ************************************)
+
+(* Normal forms*)
+
+(* Var n = n-th De Bruijn index, 0-based *)
+
+(*type nf =
+  | Lam of nf
+  | Var of int
+  | i
+and i =
+  | I of int * nf listx
+;;*)
+type var = int * (* arity of variable*) int;;
+type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
+type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
+type 'nf i_num_var_ = [
+  | 'nf i_n_var_
+  | `Match of 'nf i_num_var_ * (* originating var *) var * (*lift*) int * (*branches*)(int * 'nf) list ref * (*args*)'nf list
+]
+type 'nf nf_ = [ `Lam of (* was_unpacked *) bool * 'nf nf_ | 'nf i_num_var_ ]
+type nf = nf nf_
+type i_var = nf i_var_;;
+type i_n_var = nf i_n_var_;;
+type i_num_var = nf i_num_var_;;
+
+let hd_of_i_var =
+ function
+   `I ((v,_),_)
+ | `Var (v,_) -> v
+
+let hd_of =
+ function
+   `I ((v,_),_)
+ | `Var(v,_) -> Some v
+ | `N _ -> None
+ | `Match _ -> assert false
+
+let arity_of_hd =
+function
+  `I ((_,a),_)
+| `Var(_,a) -> a
+| _ -> 0 (* FIXME? *)
+
+let lift m (t : nf) =
+ let aux_var l (n, ar) = (if n < l then n else n+m), ar in
+ let rec aux_i_num_var l =
+  function
+    `I(v,args) -> `I(aux_var l v, Listx.map (aux l) args)
+   | `Var v -> `Var(aux_var l v)
+   | `N _ as x -> x
+   | `Match(t,v,lift,bs,args) ->
+      `Match(aux_i_num_var l t, v, lift + m, bs, List.map (aux l) args)
+ and aux l =
+  function
+     #i_num_var as x -> (aux_i_num_var l x :> nf)
+   | `Lam(b,nf) -> `Lam (b, aux (l+1) nf)
+ in
+  (aux 0 t : nf)
+;;
+
+(* put t under n lambdas, lifting t accordingtly *)
+let rec make_lams t =
+ function
+   0 -> t
+ | n when n > 0 -> `Lam (false, lift 1 (make_lams t (n-1)))
+ | _ -> assert false
+
+let free_vars' =
+ let rec aux n = function
+    `N _ -> []
+  | `Var(x,ar) -> if x < n then [] else [(x-n,ar)]
+  | `I((x,ar),args) ->
+      (if x < n then [] else [(x-n,ar)]) @
+      List.concat (List.map (aux n) (Listx.to_list args))
+  | `Lam(_,t) -> aux (n+1) t
+  | `Match(t,_,liftno,bs,args) ->
+      aux n (t :> nf) @
+      List.concat (List.map (fun (_,t) -> aux (n-liftno) t) !bs) @
+      List.concat (List.map (aux n) args)
+  in aux 0
+;;
+let free_vars = (List.map fst) ++ free_vars';;
+
+module ToScott =
+struct
+
+let delta = let open Pure in L(A(V 0, V 0))
+
+let bomb = ref(`Var(-1, -666));;
+
+let rec t_of_i_num_var =
+ function
+  | `N n -> Scott.mk_n n
+  | `Var(v,_) as x -> assert (x <> !bomb); Pure.V v
+  | `Match(t,_,liftno,bs,args) ->
+      let bs = List.map (
+        function (n,t) -> n,
+         (if t = !bomb then delta
+          else Pure.L (t_of_nf (lift (liftno+1) t)))
+        ) !bs in
+      let t = t_of_i_num_var t in
+      let m = Scott.mk_match t bs in
+      let m = Pure.A(m,delta) in
+      List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
+  | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
+and t_of_nf =
+ function
+  | #i_num_var as x -> t_of_i_num_var x
+  | `Lam(b,f) -> Pure.L (t_of_nf f)
+
+end
+
+
+(************ Pretty-printing ************************************)
+
+(* let rec string_of_term l  = fun _ -> "";; *)
+
+let string_of_term =
+ let boundvar x = "v" ^ string_of_int x in
+ let varname lev l n =
+  if n < lev then boundvar (lev-n-1)
+   else if n - lev < List.length l then List.nth l (n-lev)
+    else "`" ^ string_of_int (n-lev) in
+ let rec string_of_term_w_pars lev l  = function
+  | `Var(n,ar) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "")
+  | `N n -> string_of_int n
+  | `I _ as t -> "(" ^ string_of_term_no_pars_app lev l t ^ ")"
+  | `Lam _ as t -> "(" ^ string_of_term_no_pars_lam lev l t ^ ")"
+  | `Match(t,(v,ar),bs_lift,bs,args) ->
+      (* assert (bs_lift = lev); *)
+     "(["^ varname 0 l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
+     " with " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ string_of_term l (t :> nf)) !bs) ^ "] " ^
+     String.concat " " (List.map (string_of_term l) (args :> nf list)) ^ ")"
+ and string_of_term_no_pars_app lev l  = function
+  | `I((n,ar), args) -> varname lev l n ^ (if debug_display_arities then ":" ^ string_of_int ar else "") ^ " " ^ String.concat " " (List.map (string_of_term_w_pars lev l) (Listx.to_list args :> nf list))
+  | #nf as t -> string_of_term_w_pars lev l t
+ and string_of_term_no_pars_lam lev l  = function
+  | `Lam(_,t) -> "λ" ^ boundvar lev ^ ". " ^ (string_of_term_no_pars_lam (lev+1) l t)
+  | _ as t -> string_of_term_no_pars lev l t
+ and string_of_term_no_pars lev l = function
+  | `Lam _ as t -> string_of_term_no_pars_lam lev l t
+  | #nf as t -> string_of_term_no_pars_app lev l t
+ and string_of_term t = string_of_term_no_pars 0 t in
+ string_of_term
+;;
+
+let print ?(l=[]) = string_of_term l;;
+let string_of_nf t = string_of_term [] (t:>nf);;
+
+(************ Hereditary substitutions ************************************)
+
+let cast_to_i_var =
+ function
+    #i_var as y -> (y : i_var)
+  | t ->
+    prerr_endline (print (t :> nf));
+    assert false (* algorithm failed *)
+
+let cast_to_i_n_var =
+ function
+    #i_n_var as y -> (y : i_n_var)
+  | t ->
+    prerr_endline (print (t :> nf));
+    assert false (* algorithm failed *)
+
+let cast_to_i_num_var =
+ function
+    #i_num_var as y -> (y : i_num_var)
+  | t ->
+    prerr_endline (print (t :> nf));
+    assert false (* algorithm failed *)
+
+let rec set_arity arity = function
+(* FIXME because onlt variables should be in branches of matches, one day *)
+| `Var(n,_) -> `Var(n,arity)
+| `N _ as t -> t
+| `Lam(false, t) -> `Lam(false, set_arity arity t)
+| `Match(t,(n,_),bs_lift,bs,args) -> `Match(t,(n,arity),bs_lift,bs,args)
+| `I _ | `Lam _ -> assert false
+
+let minus1 n = if n = min_int then n else n - 1;;
+
+let rec mk_app (h : nf) (arg : nf) =
+(*let res =*)
+ match h with
+    `I(v,args) -> `I(v,Listx.append (Listx.Nil arg) args)
+  | `Var v -> `I(v, Listx.Nil arg)
+  | `Lam(truelam,nf) -> subst truelam true 0 arg (nf : nf) (* AC FIXME sanity check on arity *)
+  | `Match(t,v,lift,bs,args) -> `Match(t,v,lift,bs,List.append args [arg])
+  | `N _ -> assert false (* Numbers cannot be applied *)
+(*in let l = ["v0";"v1";"v2"] in
+prerr_endline ("mk_app h:" ^ print ~l h ^ " arg:" ^ print ~l:l arg ^ " res:" ^ print ~l:l res); res*)
+
+and mk_appl h args =
+ (*prerr_endline ("MK_APPL: " ^ print h ^ " " ^ String.concat " " (List.map print args));*)
+ List.fold_left mk_app h args
+
+and mk_appx h args = Listx.fold_left mk_app h args
+
+and mk_match t (n,ar) bs_lift bs args =
+ (*prerr_endline ("MK_MATCH: ([" ^ print t ^ "] " ^ String.concat " " (Listx.to_list (Listx.map (fun (n,t) -> string_of_int n ^ " => " ^ print t) bs)) ^ ") " ^ String.concat " " (List.map print args));*)
+ match t with
+    `N m ->
+      (try
+        let h = List.assoc m !bs in
+        let h = set_arity (minus1 ar) h in
+        let h = lift bs_lift h in
+        mk_appl h args
+       with Not_found ->
+        `Match (t,(n,ar),bs_lift,bs,args))
+  | `I _ | `Var _ | `Match _ -> `Match(t,(n,ar),bs_lift,bs,args)
+
+and subst truelam delift_by_one what (with_what : nf) (where : nf) =
+ let rec aux_propagate_arity ar = function
+ | `Lam(false, t) when not delift_by_one -> `Lam(false, aux_propagate_arity ar t)
+ | `Match(`I(v,args),(x,_),liftno,bs,args') when not delift_by_one ->
+    `Match(`I(v,args),(x,ar),liftno,bs,args')
+ | `Var(i,oldar) -> `Var(i, if truelam then (assert (oldar = min_int); ar) else oldar)
+ | _ as t -> t in
+ let rec aux_i_num_var l =
+  function
+     `I((n,ar),args) ->
+       if n = what + l then
+        mk_appx (lift l (aux_propagate_arity ar with_what)) (Listx.map (aux l) args)
+       else
+        `I (((if delift_by_one && n >= l then n-1 else n), ar), Listx.map (aux l) args)
+   | `Var(n,ar) ->
+       if n = what + l then
+        lift l (aux_propagate_arity ar with_what)
+       else
+        `Var((if delift_by_one && n >= l then n-1 else n), ar)
+   | `N _ as x -> x
+   | `Match(t,v,bs_lift,bs,args) ->
+       let bs_lift = bs_lift + if delift_by_one then -1 else 0 in
+       (* Warning! It now applies again the substitution in branches of matches.
+          But careful, it does it many times, for every occurrence of
+          the match. This is okay because what does not occur in with_what. *)
+       let l' = l - bs_lift  in
+       let with_what' = lift l' (with_what :> nf) in
+       (* The following line should be the identity when delift_by_one = true because we
+          are assuming the ts to not contain lambda-bound variables. *)
+       bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
+       let body = cast_to_i_num_var (aux_i_num_var l t) in
+       mk_match body v bs_lift bs (List.map (aux l) (args :> nf list))
+ and aux l(*lift*) =
+(*function iii -> let res = match iii with*)
+  function
+   | #i_num_var as x -> aux_i_num_var l x
+   | `Lam(b, nf) -> `Lam(b, aux (l+1) nf)
+(*in let ll = ["v0";"v1";"v2"] in
+prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool delift_by_one ^ " what:" ^ (List.nth ll what) ^ " with_what:" ^ print ~l:ll with_what ^ " where:" ^ print ~l:ll iii ^ " res:" ^ print ~l:ll res); res*)
+ in
+  aux 0 where
+;;
+
+(************** Algorithm(s) ************************)
+
+let eta_compare x y =
+ (* let clex a b = let diff = ? a b in if diff = 0 then cont () else 0 in *)
+ let clex aux1 aux2 (a1,a2) (b1,b2) =
+  let diff = aux1 a1 b1 in if diff = 0 then aux2 a2 b2 else diff in
+ let rec lex aux l1 l2 =
+  match l1,l2 with
+ | [], [] -> 0
+ | [], _ -> -1
+ | _, [] -> 1
+ | x::xs, y::ys -> clex aux (lex aux) (x,xs) (y,ys) in
+ let rec aux t1 t2 = match t1, t2 with
+  | `Var(n,_) , `Var(m,_) -> compare n m
+  | `I((n1,_), l1), `I((n2,_), l2) ->
+    clex compare (lex aux) (n1, Listx.to_list l1) (n2, Listx.to_list l2)
+  | `Lam _, `N _ -> -1
+  | `N _, `Lam _ -> 1
+  | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
+  | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
+  | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
+  | `N n1, `N n2 -> compare n1 n2
+  | `Match(u,_,bs_lift,bs,args), `Match(u',_,bs_lift',bs',args') ->
+    let bs = List.sort (fun (n,_) (m,_) -> compare n m) !bs in
+    let bs' = List.sort (fun (n,_) (m,_) -> compare n m) !bs' in
+    clex aux (clex (lex (clex compare aux)) (lex aux)) ((u :> nf), (bs, args)) ((u' :> nf), (bs', args'))
+  | `Match _, _ -> -1
+  | _, `Match _ -> 1
+  | `N _, _ -> -1
+  | _, `N _ -> 1
+  | `I _, _ -> -1
+  | _, `I _ -> 1
+  in aux x y
+;;
+
+let eta_eq (#nf as x) (#nf as y) = 0 = eta_compare x y ;;
+
+let rec eta_subterm sub t =
+ if eta_eq sub t then true else
+  match t with
+  | `Lam(_,t') -> eta_subterm (lift 1 sub) t'
+  | `Match(u,ar,liftno,bs,args) ->
+     eta_subterm sub (u :> nf)
+     || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
+     || List.exists (eta_subterm sub) (args :> nf list)
+  | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+   | `Var(v',_) -> v = v'
+   | `I((v',_), args') -> v = v'
+    && Listx.length args' < Listx.length args
+    && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
+   | _ -> false
+   )
+  | `N _ | `Var _ -> false
+;;
+
+let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
+
+
+let max_arity_tms n =
+ let max a b = match a, b with
+  | None, None -> None
+  | None, Some x
+  | Some x, None -> Some x
+  | Some x, Some y -> Some (Pervasives.max x y) in
+ let aux_var l (m,a) = if n + l = m then Some a else None in
+ let rec aux l = function
+  | `Var v -> aux_var l v
+  | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
+  | `Lam(_,t) -> aux (l+1) t
+  | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
+  | `N _ -> None
+ and aux_tms l =
+  List.fold_left (fun acc t -> max acc (aux l t)) None in
+ fun tms -> aux_tms 0 (tms :> nf list)
+;;
+
+let get_first_args var =
+let rec aux l = function
+| `Lam(_,t) -> aux (l+1) t
+| `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
+| `I((n,_), args) -> if n = var + l then [Listx.last args] else []
+| `N _
+| `Var _ -> []
+in aux 0
+;;
+
+let compute_arities m =
+ let rec aux n tms =
+  if n = 0
+   then []
+   else
+    let tms = Util.filter_map (function `Lam(_,t) -> Some t | _ -> None ) tms in
+    let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
+     arity :: (aux (n-1) tms)
+ in fun tms -> List.rev (aux m tms)
+;;
+
+let compute_arities var special_k all_tms =
+ let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
+ compute_arities special_k tms
+;;
diff --git a/ocaml/num.mli b/ocaml/num.mli
new file mode 100644
index 0000000..f1ea4f8
--- /dev/null
+++ b/ocaml/num.mli
@@ -0,0 +1,49 @@
+type var = int * int
+type 'nf i_var_ = [ `I of var * 'nf Listx.listx | `Var of var ]
+type 'nf i_n_var_ = [ `N of int | 'nf i_var_ ]
+type 'nf i_num_var_ =
+    [ `I of var * 'nf Listx.listx
+    | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list
+    | `N of int
+    | `Var of var ]
+type 'nf nf_ =
+    [ `I of var * 'nf Listx.listx
+    | `Lam of bool * 'nf nf_
+    | `Match of 'nf i_num_var_ * var * int * (int * 'nf) list ref * 'nf list
+    | `N of int
+    | `Var of var ]
+type nf = nf nf_
+type i_var = nf i_var_
+type i_n_var = nf i_n_var_
+type i_num_var = nf i_num_var_
+val hd_of_i_var : i_var -> int
+val hd_of : i_n_var -> int option
+val arity_of_hd : i_n_var -> int
+(* put t under n lambdas, lifting t accordingtly *)
+val make_lams : nf -> int -> nf
+val lift : int -> nf -> nf
+val free_vars' : nf -> var list
+val free_vars : nf -> int list
+module ToScott :
+  sig
+    val bomb : nf ref
+    val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t
+    val t_of_nf : nf -> Pure.Pure.t
+  end
+val print : ?l:string list -> nf -> string
+val string_of_nf : [<nf] -> string
+val cast_to_i_var : [< nf > `I `Var] -> i_var
+val cast_to_i_n_var : [< nf > `I `N `Var] -> i_n_var
+val cast_to_i_num_var : [< nf > `I `N `Match `Var] -> i_num_var
+val set_arity : int -> nf -> nf
+val mk_app : nf -> nf -> nf
+val mk_appl : nf -> nf list -> nf
+val mk_appx : nf -> nf Listx.listx -> nf
+val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf
+val subst : bool -> bool -> int -> nf -> nf -> nf
+val eta_compare : nf -> nf -> int
+val eta_eq : [< nf ] -> [< nf ] -> bool
+val eta_subterm : [< nf ] -> [< nf ] -> bool
+val max_arity_tms : int -> [< nf] list -> int option
+val compute_arities : int -> int -> nf list -> int list
+val minus1 : int -> int
diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index fbce730..8003226 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -1,15 +1,9 @@
-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 mk_app x y = Num.mk_app x y;;
+let mk_lam x = `Lam(true, x);;
+let mk_var x = `Var(x, -666);;
+
 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' ;;
@@ -36,11 +30,11 @@ let explode s =
 ;;
 
 let implode l =
-  let res = String.create (List.length l) in
+  let res = Bytes.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
+    | c :: l -> Bytes.set res i c; aux (i + 1) l in
+  Bytes.to_string (aux 0 l)
 ;;
 
 let rec strip_spaces = function
@@ -139,20 +133,7 @@ let parse_many 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 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
@@ -177,7 +158,7 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
   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 div = if div_provided then div else "xxxxxx" in
  let strs = [div] @ ps @ conv in
 
  if List.length ps = 0 && List.length conv = 0
@@ -185,37 +166,28 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
 
  (* 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)
+ if v = lev + n_bot then failwith "Example with `Bottom"
+  else if v = lev + n_pac then failwith "Example with `Pacman"
+   else if v = lev + n_bomb then failwith "Example with `Bomb"
     else if v = lev then `Var(v, min_int) (* zero *)
-     else `Var(v,1) in (* 1 by default when variable not applied *)
+      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)
+ let rec aux lev : nf -> nf = function
+ | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 1) + Listx.length args), Listx.map (aux lev) 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
+ | `Match _ | `N _ -> 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
+let div = if not div_provided
  then None
  else match div with
   | `I _ as t -> Some t
@@ -247,20 +219,4 @@ let from_file path =
  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.mli b/ocaml/parser.mli
index 8dba854..d131edb 100644
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,11 +1,6 @@
-type term =
-  | Var of int
-  | App of term * term
-  | Lam of term
-
 exception ParsingError of string
 
-(* val problem_of_string:
+val problem_of_string:
  string ->
   string (* problem label *)
   * Num.i_var option (* div *)
@@ -17,9 +12,4 @@ val from_file : string ->
  * 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
+ * string list (* names of free variables *)) list
diff --git a/ocaml/problems.ml b/ocaml/problems.ml
new file mode 100644
index 0000000..28edceb
--- /dev/null
+++ b/ocaml/problems.ml
@@ -0,0 +1,27 @@
+open Util;;
+
+(* Syntax for problem files in problem/ folder:
+
+- dollar ($) on newline
+  begin new problem
+  $! means that the problem is expected to be separable,
+  $? means that it is expected to be unseparable
+
+- (#) on new line
+  comment line
+
+- (D) (C) (N) stand respectively for divergent, convergent, numeric
+
+- lines starting with spaces inherit the type from the last line
+
+*)
+
+let main f =
+ print_endline Sys.executable_name;
+ try ignore (Str.search_forward (Str.regexp_string "test") Sys.executable_name 0)
+ with Not_found ->
+  (if Array.length Sys.argv = 1
+   then failwith "no command line args. Please use e.g. ./cmd.out problems/*"
+   else Array.iteri (fun i filename -> if i > 0 then
+    List.iter f (Parser.from_file filename)) Sys.argv)
+;;
diff --git a/ocaml/problems.mli b/ocaml/problems.mli
new file mode 100644
index 0000000..5315cc7
--- /dev/null
+++ b/ocaml/problems.mli
@@ -0,0 +1,4 @@
+val main :
+  (string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *
+   string list -> unit) ->
+  unit
diff --git a/ocaml/problems/simple.0 b/ocaml/problems/simple.0
new file mode 100644
index 0000000..4942099
--- /dev/null
+++ b/ocaml/problems/simple.0
@@ -0,0 +1,46 @@
+$ simple.0/0
+D x x
+C x y
+C y y
+C y x
+
+$ simple.0/1
+D x y
+C x (_. x)
+C y z
+C y x
+
+$ simple.0/2
+D a (x. x b) (x. x c)
+C a (x. b b) @
+C a @ c
+C a (x. x x) a
+C a (a a a) (a c c)
+
+$ simple.0/3
+D x (y. x y y)
+C x (y. x y x)
+
+$ simple.0/4
+D x a a a a
+C x b a a a
+C x a b a a
+C x a a b a
+C x a a a b
+
+$ simple.0/5
+# Controesempio ad usare un conto dei lambda che non considera le permutazioni
+D x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b
+C x a a a a (_. a) b b b
+C x a a a a (_. _. _. _. x. y. x y)
+
+$ simple.0/6
+# bug in eat that was erasing terms in convergent that then diverged
+D x y z
+C x @ @
+C z (y @ (y @))
+
+$ simple.0/7
+# bug in no_leading_lambdas where x in j-th position
+D v0 (v1 v2) (x. y. v0 v3 v4 v2)
+C v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))
diff --git a/ocaml/pure.ml b/ocaml/pure.ml
new file mode 100644
index 0000000..be08bb4
--- /dev/null
+++ b/ocaml/pure.ml
@@ -0,0 +1,182 @@
+open Util.Vars
+
+module Pure =
+struct
+
+type t =
+  | V of int
+  | A of t * t
+  | L of t
+  | B
+
+let rec print ?(l=[]) =
+ function
+    V n -> print_name l n
+  | A(t1,t2) -> "(" ^ print ~l t1 ^ " " ^ print ~l t2 ^ ")"
+  | L t ->
+     let name = string_of_var (List.length l) in
+     "λ" ^ name ^ "." ^ print ~l:(name::l) t
+  | B -> "B"
+
+let lift m =
+ let rec aux l =
+  function
+   | V n -> V (if n >= l then n+m else n)
+   | A (t1,t2) -> A (aux l t1, aux l t2)
+   | L t -> L (aux (l+1) t)
+   | B -> B
+ in
+  aux 0
+
+(* Reference implementation.
+   Reduction machine used below *)
+let subst delift_by_one what with_what =
+ let rec aux l =
+  function
+   | A(t1,t2) -> A(aux l t1, aux l t2)
+   | V n ->
+       if (if what < 0 then n = what else n = what + l) then
+        lift l with_what
+       else
+        V (if delift_by_one && n >= l then n-1 else n)
+   | L t -> L (aux (l+1) t)
+   | B -> B
+ in
+  aux 0
+
+(* let rec whd =
+ function
+  | A(t1, t2) ->
+     let t2 = whd t2 in
+     let t1 = whd t1 in
+      (match t1 with
+        | L f -> whd (subst true 0 t2 f)
+        | V _
+        | A _ -> A(t1,t2))
+  | V _
+  | L _ as t -> t
+*)
+
+let unwind ?(tbl = Hashtbl.create 317) m =
+ let rec unwind (e,t,s) =
+  let cache_unwind m =
+   try
+    Hashtbl.find tbl m
+   with
+    Not_found ->
+     let t = unwind m in
+      Hashtbl.add tbl m t ;
+      t in
+  let s = List.map cache_unwind s in
+  let rec aux l =
+   function
+    | A(t1,t2) -> A(aux l t1, aux l t2)
+    | V n as x when n < l -> x
+    | V n ->
+       (try
+         lift l (cache_unwind (List.nth e (n - l)))
+        with Failure _ -> V n)
+    | L t -> L (aux (l+1) t)
+    | B -> B in
+  let t = aux 0 t in
+  List.fold_left (fun f a -> A(f,a)) t s
+in
+ unwind m
+
+
+(* let rec print_machine (e,t,s) =
+ "[" ^ String.concat "," (List.map print_machine e) ^
+     "|" ^ print t ^ "|" ^
+     String.concat "," (List.map print_machine s) ^ "]"
+;; *)
+
+  let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
+
+  let rec is_divergent =
+   function
+      t when t = omega -> true
+    | A(t,_) -> is_divergent t
+    | L(t) -> is_divergent t
+    | _ -> false
+
+  let mwhd m =
+   let rec aux g =
+    function
+    (* mmm -> print_endline (print_machine mmm); match mmm with *)
+        m when is_divergent (unwind m) -> [], B, []
+     | (e,A(t1,t2),s) ->
+         let t2' = aux g (e,t2,[]) in
+         let (_,t,_) = t2' in
+         if t = B
+          then t2'
+          else aux g (e,t1,t2'::s)
+     | (e,L t,x::s) -> aux g (x::e,t,s)
+     | (e,V n,s) as m ->
+        (try
+          let e,t,s' = List.nth e n in
+          aux g (e,t,s'@s)
+         with Invalid_argument _ | Failure _ -> m
+         )
+     | (e, B, _) -> (e, B, [])
+     | (e, L t, []) ->
+      let t = subst true 0 (V g) t in
+      (* print_endline ("." ^ string_of_int g ^ " " ^ print_machine ((e,t,[]))); *)
+      let m' = aux (g-1) (e, t, []) in
+      let t' = unwind m' in
+      (* print_endline ("=" ^ print t');
+      print_endline ("==" ^ print (lift 1 t')); *)
+      let t' = subst false g (V 0) (lift 1 t') in
+      (* print_endline ("===" ^ print t'); *)
+      [], (if t' = B then t' else L t'), []
+
+   in
+    unwind (aux ~-2 m)
+;;
+
+let omega should_explode =
+ if should_explode
+  then let f t = A(t,t) in f (L (f (V 0)))
+  else B
+;;
+
+let diverged = (=) B;;
+
+(* Note: maps only variables <= freshno *)
+let env_of_sigma freshno sigma =
+ let rec aux n =
+  if n > freshno then
+   []
+  else
+   let e = aux (n+1) in
+   (try
+    e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
+   with
+    Not_found -> ([], V n, []) ) :: e
+ in aux 0
+
+end
+
+module Scott =
+struct
+
+open Pure
+
+let rec mk_n n =
+ if n = 0 then L (L (A (V 1, L (V 0)))) else L (L (A (V 0, mk_n (n-1))))
+
+let dummy = V (max_int / 2)
+
+let mk_match t bs =
+ let bs = List.sort (fun (n1,_) (n2,_) -> compare n1 n2) bs in
+ let rec aux m t =
+  function
+     [] -> dummy
+   | (n,p)::tl as l ->
+      if n = m then
+       A (A (t, L (lift (m+1) p)), L (aux (m+1) (V 0) tl))
+      else
+       A (A (t, dummy), L (aux (m+1) (V 0) l))
+ in
+  aux 0 t bs
+
+end
diff --git a/ocaml/pure.mli b/ocaml/pure.mli
new file mode 100644
index 0000000..9b683b3
--- /dev/null
+++ b/ocaml/pure.mli
@@ -0,0 +1,17 @@
+module Pure :
+  sig
+    type t = V of int | A of t * t | L of t | B
+    val print : ?l:string list -> t -> string
+    val lift : int -> t -> t
+    val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t
+    val omega : bool -> t
+    val diverged : t -> bool
+    val env_of_sigma : int -> (int * t) list -> (('a * t * ('b list as 'c) as 'b) list as 'a)
+  end
+
+module Scott :
+  sig
+    val mk_n : int -> Pure.t
+    val dummy : Pure.t
+    val mk_match : Pure.t -> (int * Pure.t) list -> Pure.t
+  end
diff --git a/ocaml/simple.ml b/ocaml/simple.ml
new file mode 100644
index 0000000..c8daad1
--- /dev/null
+++ b/ocaml/simple.ml
@@ -0,0 +1,351 @@
+let (++) f g x = f (g x);;
+let id x = x;;
+let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;
+
+let print_hline = Console.print_hline;;
+
+open Pure
+
+type var = int;;
+type t =
+ | V of var
+ | A of t * t
+ | L of t
+;;
+
+let delta = L(A(V 0, V 0));;
+
+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 ;;
+let eta_eq = eta_eq' 0 0;;
+
+(* is arg1 eta-subterm of arg2 ? *)
+let eta_subterm u =
+ let rec aux lev t = eta_eq' lev 0 u t || match t with
+ | L t -> aux (lev+1) t
+ | A(t1, t2) -> aux lev t1 || aux lev t2
+ | _ -> false
+ in aux 0
+;;
+
+(* does NOT lift the argument *)
+let mk_lams = fold_nat (fun x _ -> L x) ;;
+
+let string_of_t =
+  let string_of_bvar =
+   let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
+   let bvarsno = List.length bound_vars in
+   fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in
+  let rec string_of_term_w_pars level = function
+    | V v -> if v >= level then "`" ^ string_of_int (v-level) else
+       string_of_bvar (level - v-1)
+    | A _
+    | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"
+  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 level = function
+    | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t
+    | _ as t -> string_of_term_no_pars_app level t
+  in string_of_term_no_pars 0
+;;
+
+type problem = {
+   orig_freshno: int
+ ; freshno : int
+ ; div : t
+ ; conv : t
+ ; sigma : (var * t) list (* substitutions *)
+}
+
+let string_of_problem p =
+ let lines = [
+  "[DV] " ^ string_of_t p.div;
+  "[CV] " ^ string_of_t p.conv;
+  "";
+ ] in
+ String.concat "\n" lines
+;;
+
+exception B;;
+exception Done of (var * t) list (* substitution *);;
+exception Fail of int * string;;
+
+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 _ -> false
+;;
+
+let is_var = function V _ -> true | _ -> false;;
+let is_lambda = function L _ -> true | _ -> false;;
+
+let rec get_inert = function
+ | V n -> (n,0)
+ | A(t, _) -> let hd,args = get_inert t in hd,args+1
+ | _ -> assert false
+;;
+
+(* precomputes the number of leading lambdas in a term,
+   after replacing _v_ w/ a term starting with n lambdas *)
+let rec no_leading_lambdas v n = function
+ | L t -> 1 + no_leading_lambdas (v+1) n t
+ | A _ as t -> let v', m = get_inert t in if v = v' then max 0 (n - m) else 0
+ | V v' -> if v = v' then n else 0
+;;
+
+let rec subst level delift 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 sub t)
+ | A (t1,t2) ->
+  let t1 = subst level delift sub t1 in
+  let t2 = subst level delift sub t2 in
+  mk_app t1 t2
+and mk_app t1 t2 = if t1 = delta && t2 = delta then raise B
+ else match t1 with
+ | L t1 -> subst 0 true (0, t2) t1
+ | _ -> A (t1, t2)
+and lift n =
+ let rec aux lev =
+  function
+  | V m -> V (if m >= lev then m + n else m)
+  | L t -> L (aux (lev+1) t)
+  | A (t1, t2) -> A (aux lev t1, aux lev t2)
+ in aux 0
+;;
+let subst = subst 0 false;;
+
+let subst_in_problem ((v, t) as sub) p =
+print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);
+ let sigma = sub::p.sigma in
+ let div = try subst sub p.div with B -> raise (Done sigma) in
+ let conv = try subst sub p.conv with B -> raise (Fail(-1,"p.conv diverged")) in
+ {p with div; conv; sigma}
+;;
+
+let get_subterm_with_head_and_args hd_var n_args =
+ let rec aux lev = function
+ | V _ -> None
+ | L t -> aux (lev+1) t
+ | A(t1,t2) as t ->
+   let hd_var', n_args' = get_inert t1 in
+   if hd_var' = hd_var + lev && n_args <= 1 + n_args'
+    (* the `+1` above is because of t2 *)
+    then Some (lift ~-lev t)
+    else match aux lev t2 with
+    | None -> aux lev t1
+    | Some _ as res -> res
+ in aux 0
+;;
+
+let rec purify = function
+ | L t -> Pure.L (purify t)
+ | A (t1,t2) -> Pure.A (purify t1, purify t2)
+ | V n -> Pure.V n
+;;
+
+let check p sigma =
+ print_endline "Checking...";
+ let div = purify p.div in
+ let conv = purify p.conv in
+ let sigma = List.map (fun (v,t) -> v, purify t) sigma in
+ let freshno = List.fold_right (max ++ fst) sigma 0 in
+ let env = Pure.env_of_sigma freshno sigma in
+ assert (Pure.diverged (Pure.mwhd (env,div,[])));
+ print_endline " D diverged.";
+ assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));
+ print_endline " C converged.";
+ ()
+;;
+
+let sanity p =
+ print_endline (string_of_problem p); (* non cancellare *)
+ if p.div = delta then raise (Done p.sigma);
+ if not (is_inert p.div) then problem_fail p "p.div converged";
+ p
+;;
+
+(* drops the arguments of t after the n-th *)
+(* FIXME! E' usato in modo improprio contando sul fatto
+   errato che ritorna un inerte lungo esattamente n *)
+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)
+;;
+
+(* return the index of the first argument with a difference
+   (the first argument is 0)
+   precondition: p.div and t have n+1 arguments
+   *)
+let find_eta_difference p t argsno =
+ let t = inert_cut_at argsno t in
+ let rec aux t u k = match t, u with
+ | V _, V _ -> problem_fail p "no eta difference found (div subterm of conv?)"
+ | A(t1,t2), A(u1,u2) ->
+    if not (eta_eq t2 u2) then (k-1)
+    else aux t1 u1 (k-1)
+ | _, _ -> assert false
+ in aux p.div t argsno
+;;
+
+let compute_max_lambdas_at hd_var j =
+ let rec aux hd = function
+ | A(t1,t2) ->
+    (if get_inert t1 = (hd, j)
+      then max ( (*FIXME*)
+       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd
+        then let hd', j' = get_inert t2 in j - j'
+        else no_leading_lambdas hd_var j t2)
+      else id) (max (aux hd t1) (aux hd t2))
+ | L t -> aux (hd+1) t
+ | V _ -> 0
+ in aux hd_var
+;;
+
+let compute_max_arity =
+ let rec aux n = function
+ | A(t1, t2) -> max (aux (n+1) t1) (aux 0 t2)
+ | L t -> max n (aux 0 t)
+ | V _ -> n
+ in aux 0
+;;
+
+let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
+
+(* step on the head of div, on the k-th argument, with n fresh vars *)
+let step k p (flag(*add arity*)) =
+ let var, _ = get_inert p.div in
+ let arity = if flag then compute_max_arity p.conv else 0 in
+ let n = 1 + arity + max
+  (compute_max_lambdas_at var k p.div)
+  (compute_max_lambdas_at var k p.conv) in
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");
+ let p, t = (* apply fresh vars *)
+  fold_nat (fun (p, t) _ ->
+    let p, v = freshvar p in
+    p, A(t, V (v + k + 1))
+  ) (p, V 0) n in
+ let t = (* apply unused bound variables V_{k-1}..V_1 *)
+  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
+ let t = mk_lams t (k+1) in (* make leading lambdas *)
+ let subst = var, t in
+ let p = subst_in_problem subst p in
+ sanity p
+;;
+
+let finish p =
+print_cmd "FINISH" "";
+ let div_hd, div_nargs = get_inert p.div in
+ let j = div_nargs - 1 in
+ let p = step j p true in
+ let div_hd, div_nargs = get_inert p.div in
+ let rec aux m = function
+  A(t1,t2) -> if is_var t2 then
+   (let delta_var, _ = get_inert t2 in
+     if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None
+      then m, delta_var
+      else aux (m-1) t1) else aux (m-1) t1
+  | _ -> assert false in
+ let m, delta_var = aux div_nargs p.div in
+ let p = subst_in_problem (delta_var, delta) p in
+ let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in
+ sanity p
+;;
+
+
+let rec auto p =
+ let hd_var, n_args = get_inert p.div in
+ match get_subterm_with_head_and_args hd_var n_args p.conv with
+ | None ->
+   (try
+     problem_fail (finish p) "Auto did not complete the problem"
+    with Done sigma -> sigma)
+ | Some t ->
+  let j = find_eta_difference p t n_args in
+  let p = step j p false in
+  auto p
+;;
+
+let problem_of (label, div, convs, ps, var_names) =
+ print_hline ();
+ let rec aux = function
+ | `Lam(_, t) -> L (aux t)
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args
+ | `Var(v,_) -> V v
+ | `N _ | `Match _ -> assert false in
+ assert (List.length ps = 0);
+ let convs = List.rev convs in
+ let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in
+ let var_names = "@" :: var_names in
+ let div = match div with
+ | Some div -> aux (div :> Num.nf)
+ | None -> assert false in
+ let varno = List.length var_names in
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]} in
+ (* initial sanity check *)
+ sanity p
+;;
+
+let solve p =
+ if eta_subterm p.div p.conv
+  then print_endline "!!! div is subterm of conv. Problem was not run !!!"
+  else check p (auto p)
+;;
+
+Problems.main (solve ++ problem_of);
+
+(* Example usage of interactive: *)
+
+(* 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 _ -> ()
+;; *)
+
+(* interactive "x y"
+ "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]
+;; *)
diff --git a/ocaml/simple.mli b/ocaml/simple.mli
new file mode 100644
index 0000000..bdc6328
--- /dev/null
+++ b/ocaml/simple.mli
@@ -0,0 +1,5 @@
+type problem
+val solve : problem -> unit
+val problem_of :
+  string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *
+  string list -> problem
diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
new file mode 100644
index 0000000..438b7b5
--- /dev/null
+++ b/ocaml/simple_test.ml
@@ -0,0 +1,55 @@
+open Simple;;
+open Util;;
+
+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 take' l n =
+    if n = 0 then []
+    else match l with
+    | [] -> []
+    | [_] -> assert false
+    | x::_::xs -> x :: take' xs (n-1) in
+  let rec aux n inerts lams =
+    if n = 0 then List.hd inerts, take' (Util.sort_uniq (List.tl inerts)) 5
+    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 rec repeat f n =
+  prerr_endline "\n########################### NEW TEST ###########################";
+  f () ;
+  if n > 0 then repeat f (n-1)
+;;
+
+let main =
+  Random.self_init ();
+  let num = 100 in
+  let complex = 100 in
+  let no_bound_vars = 10 in
+  let vars = Array.to_list
+   (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in
+
+  repeat (fun _ ->
+    let div, convs = gen complex vars in
+    let str = "$ random simple test \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
+    print_endline str;
+    let open Simple in
+    (solve ++ problem_of ++ Parser.problem_of_string) str
+  ) num ;
+
+  prerr_endline "\n---- ALL TESTS COMPLETED ----"
+;;