From 42eb14bc4443ce5a9bb893654db97a9c41486f06 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2017 15:38:27 +0200
Subject: [PATCH 01/16] Failing case found

---
 ocaml/problems/bugs | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 ocaml/problems/bugs

diff --git a/ocaml/problems/bugs b/ocaml/problems/bugs
new file mode 100644
index 0000000..2cea8d3
--- /dev/null
+++ b/ocaml/problems/bugs
@@ -0,0 +1,12 @@
+$! randomly generated test
+D ((((z b) (w v)) (v. (v z))) (a. (v y)))
+C (((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b))))) ((y (y. (c v))) w))
+C ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((z b) (w v)) y))
+C ((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b)))))
+C ((((((y v) v) ((z b) (w v))) c) c) (((((z b) (w v)) (v. (v z))) (a. (v x))) v))
+C (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a))
+N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((c (w v)) ((w v) z)) (c w))) Z
+N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (c. (((c v) ((c w) (b. a))) (v. (c. (w. b)))))) Z
+N ((((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v)))) (y. (c. ((((y v) v) (z. (y. (w. (b b))))) (((z b) (w v)) (v. (v z))))))) (z. (y. (b. a)))) Z
+N (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (((y v) v) ((z b) (w v)))) Z
+N (((((b b) (a. (y v))) (a. (b. (b b)))) (((w v) z) (y. (c v)))) (y. (c. c))) Z
-- 
2.39.2


From aa18ab71f3030f746de14168b9dae21c255e9b81 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2017 17:55:29 +0200
Subject: [PATCH 02/16] Missing parenthesis fixed

---
 ocaml/num.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 4e44c79..7e52482 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -132,7 +132,7 @@ let rec string_of_term =
   | `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 lev l v ^ (if debug_display_arities then ":"^ string_of_int ar else "") ^",match " ^ string_of_term_no_pars lev l (t :> nf) ^
+     "(["^ varname lev 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)) ^ ")"
   | `Bottom -> "BOT"
-- 
2.39.2


From 180710db0f9d6f81edd7a5cc1bfce41e3b3e620a Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 20:59:55 +0200
Subject: [PATCH 03/16] Simplified not-working example

---
 ocaml/problems/bugs | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

diff --git a/ocaml/problems/bugs b/ocaml/problems/bugs
index 2cea8d3..b9bb726 100644
--- a/ocaml/problems/bugs
+++ b/ocaml/problems/bugs
@@ -1,12 +1,3 @@
 $! randomly generated test
-D ((((z b) (w v)) (v. (v z))) (a. (v y)))
-C (((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b))))) ((y (y. (c v))) w))
-C ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((z b) (w v)) y))
-C ((((((b b) (a. (y v))) (a. (b. (b b)))) (w. (x. (a (y v))))) (((w v) z) (v. (((y v) v) ((z b) (w v)))))) ((((y v) v) (z. (y. (w. (b b))))) (y. (w. (b b)))))
-C ((((((y v) v) ((z b) (w v))) c) c) (((((z b) (w v)) (v. (v z))) (a. (v x))) v))
-C (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a))
-N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (((c (w v)) ((w v) z)) (c w))) Z
-N ((((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (b. a)) (c. (((c v) ((c w) (b. a))) (v. (c. (w. b)))))) Z
-N ((((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v)))) (y. (c. ((((y v) v) (z. (y. (w. (b b))))) (((z b) (w v)) (v. (v z))))))) (z. (y. (b. a)))) Z
-N (((((b b) (a. (y v))) (a. (b. (b b)))) ((((w v) z) (v. (((y v) v) ((z b) (w v))))) (y (y. (c v))))) (((y v) v) ((z b) (w v)))) Z
-N (((((b b) (a. (y v))) (a. (b. (b b)))) (((w v) z) (y. (c v)))) (y. (c. c))) Z
+D z (_. (v y))
+C u (z (_. (v x)))
-- 
2.39.2


From 5682bf463b89edb7756020fe7b838eb846d6c771 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 21:00:26 +0200
Subject: [PATCH 04/16] Fixed computation of arity for top-level inerts

---
 ocaml/lambda4.ml | 16 +++++++++-------
 ocaml/parser.ml  |  2 +-
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index b15c360..2e96fc3 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -70,16 +70,18 @@ let all_terms p =
  @ p.ps
 ;;
 
-let sum_arities p =
+let measure_of_term, measure_of_terms =
  let rec aux = function
  | `N _ | `Bottom | `Pacman -> 0
  | `Var(_,ar) -> if ar = min_int then 0 else max 0 ar (*assert (ar >= 0); ar*)
  | `Lam(_,t) -> aux t
  | `I(v,args) -> aux (`Var v) + aux_many (Listx.to_list args :> nf list)
- | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar = min_int then 0 else ar - 1) + aux_many (args :> nf list)
+ | `Match(u,(_,ar),_,_,args) -> aux (u :> nf) + (if ar <= 0 then 0 else ar - 1) + aux_many (args :> nf list)
  and aux_many tms = List.fold_right ((+) ++ aux) tms 0 in
- aux_many (all_terms p :> nf list)
- ;;
+ (fun t -> aux (t :> nf)), (fun l -> aux_many (l :> nf list))
+;;
+
+let sum_arities p = measure_of_terms (all_terms p)
 
 let problem_measure p = sum_arities p;;
 let string_of_measure = string_of_int;;
@@ -96,10 +98,10 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
    ) else "# ";
   "#";
   "$" ^ p.label;
-  (match div with None -> "# no D" | Some div -> "D " ^ print ~l (div :> nf));
+  (match div with None -> "# no D" | Some div -> "D ("^string_of_int (measure_of_term div)^")"^ print ~l (div :> nf));
   ]
-  @ List.map (fun t -> if t = convergent_dummy then "#C" else "C " ^ print ~l (t :> nf)) conv
-  @ List.mapi (fun i t -> string_of_int i ^ " " ^ print ~l (t :> nf)) ps
+  @ List.map (fun t -> if t = convergent_dummy then "#C" else "C ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) conv
+  @ List.mapi (fun i t -> string_of_int i ^ " ("^string_of_int (measure_of_term t)^") " ^ print ~l (t :> nf)) ps
   @ [""])
 ;;
 
diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 4b02b12..6bcb70d 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -189,7 +189,7 @@ let problem_of_string s =
  | #nf_nob as t -> t
  | `Bottom -> raise (ParsingError "Input term not in normal form") in
  let rec aux_nob lev : nf_nob -> nf = function
- | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args)
+ | `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
-- 
2.39.2


From 4c81587c5f911c4d5f818765106bb5373967d715 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 21:34:23 +0200
Subject: [PATCH 05/16] Simplified arity_of, precompute_edible_data,
 critical_showsteppers

---
 ocaml/lambda4.ml | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 2e96fc3..dfe0da1 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -284,10 +284,9 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
 
 exception Dangerous
 
-let arity_of arities k =
- let _,pos,y = List.find (fun (v,_,_) -> v=k) arities in
- let arity = match y with `Var _ -> 0 | `I(_,args) -> Listx.length args | `N _ -> assert false in
- arity + if pos = -1 then - 1 else 0
+let arity_of arities hd =
+ let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in
+ nargs + if pos = -1 then - 1 else 0
 ;;
 
 let rec dangerous arities showstoppers =
@@ -388,11 +387,14 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
 ;;
 
 let precompute_edible_data {ps; div} xs =
- (match div with None -> [] | Some div -> [hd_of_i_var div, -1, (div :> i_n_var)]) @
-  List.map (fun hd ->
+ let aux t = match t with `Var _ -> 0 | `I(_, args) -> Listx.length args | `N _ -> assert false in
+ (fun l -> match div with
+  | None -> l
+  | Some div -> (-1, hd_of_i_var div, aux div) :: l)
+  (List.map (fun hd ->
    let i, tm = Util.findi (fun y -> hd_of y = Some hd) ps in
-    hd, i, tm
-   ) xs
+    i, hd, aux tm
+   ) xs)
 ;;
 
 let critical_showstoppers p =
@@ -434,23 +436,21 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv =
-   edible p arities showstoppers in
-  let l = List.filter (fun (x,_,_) -> not (List.mem x showstoppers)) arities in
+  let showstoppers, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
   let p =
-  List.fold_left (fun p (x,pos,(xx : i_n_var)) -> if pos = -1 then p else
-   let n = match xx with `I(_,args) -> Listx.length args | _ -> 0 in
+  List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
    let v = `N(pos) in
-   let inst = make_lams v n in
-prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names x ^ " := " ^ string_of_term p inst);
-   { p with sigma = p.sigma @ [x,inst] }
+   let inst = make_lams v nargs in
+prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
+   { p with sigma = p.sigma @ [hd,inst] }
    ) p l in
   (* to avoid applied numbers in safe positions that
      trigger assert failures subst_in_problem x inst p*)
  let ps =
   List.map (fun t ->
    try
-    let _,j,_ = List.find (fun (h,_,_) -> hd_of t = Some h) l in
+    let j,_,_ = List.find (fun (_,hd,_) -> hd_of t = Some hd) l in
     `N j
    with Not_found -> t
   ) ps in
-- 
2.39.2


From dc829653c03f7bf0977addabe480e7c8b178bad1 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 21:58:31 +0200
Subject: [PATCH 06/16] Renamed in critical_showstoppers: showstoppers ->
 inedible (I don't know why)

---
 ocaml/lambda4.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index dfe0da1..392784f 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -436,11 +436,11 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv = edible p arities showstoppers in
-  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
+  let inedible, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
   let p =
   List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N(pos) in
+   let v = `N pos in
    let inst = make_lams v nargs in
 prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
    { p with sigma = p.sigma @ [hd,inst] }
@@ -457,7 +457,7 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
  let p = match p.div with
   | None -> p
   | Some div ->
-   if List.mem (hd_of_i_var div) showstoppers
+   if List.mem (hd_of_i_var div) inedible
    then p
    else
     let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
@@ -465,14 +465,14 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
     let inst = make_lams `Bottom n in
     subst_in_problem x inst p in
  let dangerous_conv = showstoppers_conv in
-let _ = prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; in
+prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
+List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
  let conv =
    List.map (function s,t ->
     try
      if s <> [] then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
-     let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
+     let _ = List.find (fun h -> hd_of t = Some h) inedible in
       t)
     with Not_found -> match hd_of t with
      | None -> assert (t = convergent_dummy); t
-- 
2.39.2


From 0a50c398d9eef65620f18f99ef675770b50a920c Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 22:35:44 +0200
Subject: [PATCH 07/16] Comments, fix indentation and

---
 ocaml/lambda4.ml | 35 ++++++++++++++++++++---------------
 1 file changed, 20 insertions(+), 15 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 392784f..4826263 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -58,7 +58,7 @@ let first bound p var f =
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
      aux (i+1)
  in
   aux 1
@@ -368,22 +368,22 @@ let rec edible ({div; conv; ps} as p) arities showstoppers =
            aux showstoppers xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps
-  in
-    let showstoppers = sort_uniq (aux showstoppers ps) in
-    let dangerous_conv =
-     List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+            aux (sort_uniq (h::showstoppers)) ps in
+
+ let showstoppers = sort_uniq (aux showstoppers ps) in
+ let dangerous_conv =
+  List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
 
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
 List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
 
-    let showstoppers' = showstoppers @ List.concat dangerous_conv in
-    let showstoppers' = sort_uniq (match div with
-     | None -> showstoppers'
-     | Some div ->
-       if List.exists ((=) (hd_of_i_var div)) showstoppers'
-       then showstoppers' @ free_vars (div :> nf) else showstoppers') in
-    if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+ let showstoppers' = showstoppers @ List.concat dangerous_conv in
+ let showstoppers' = sort_uniq (match div with
+  | None -> showstoppers'
+  | Some div ->
+    if List.exists ((=) (hd_of_i_var div)) showstoppers'
+    then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+ if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
 ;;
 
 let precompute_edible_data {ps; div} xs =
@@ -397,6 +397,11 @@ let precompute_edible_data {ps; div} xs =
    ) xs)
 ;;
 
+(** Returns (p, showstoppers_step, showstoppers_eat) where:
+    - showstoppers_step are the heads occurring twice
+      in the same discriminating set
+    - showstoppers_eat are the heads in ps having different number
+      of arguments *)
 let critical_showstoppers p =
   let p = super_simplify p in
   let hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
@@ -426,8 +431,8 @@ let critical_showstoppers p =
   let showstoppers_eat = List.filter
     (fun x -> not (List.mem x showstoppers_step))
     showstoppers_eat in
-  List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-  List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
   p, showstoppers_step, showstoppers_eat
   ;;
 
-- 
2.39.2


From 6f8c64dcbe6b864cb0f9417bfab284e398337ae3 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 00:33:00 +0200
Subject: [PATCH 08/16] Change to compute_special_k

Now the special_k taked into account the number or arguments (arity) of
terms. This solves problem "low special_k" in problems/w
---
 ocaml/lambda4.ml | 92 ++++++++++++++++--------------------------------
 1 file changed, 30 insertions(+), 62 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 4826263..9ab675e 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -447,7 +447,7 @@ let eat p =
   List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
    let v = `N pos in
    let inst = make_lams v nargs in
-prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
+prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
    { p with sigma = p.sigma @ [hd,inst] }
    ) p l in
   (* to avoid applied numbers in safe positions that
@@ -516,8 +516,8 @@ let safe_arity_of_var p x =
  List.fold_left (fun acc t -> Pervasives.min acc (aux t)) max_int tms
 ;;
 
-let instantiate p x perm n =
- let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in
+let instantiate p x perm =
+ let n = (prerr_endline ("WARNING: using constant initialSpecialK=" ^ string_of_int p.initialSpecialK)); p.initialSpecialK in
  let arities = Array.to_list (Array.make (n+1) min_int) in
  let p,vars = make_fresh_vars p arities in
  (* manual lifting of vars by perm in next line *)
@@ -545,15 +545,28 @@ let compute_special_k tms =
  | `Bottom
  | `Pacman
  | `Var _ -> 0
- ) in Listx.max (Listx.map (aux 0) tms)
+ ) in
+ let rec aux' top t = match t with
+ | `Lam(_,t) -> aux' false t
+ | `I((_,ar), tms) -> max ar
+     (Listx.max (Listx.map (aux' false) (tms :> nf Listx.listx)))
+ | `Match(t, _, liftno, bs, args) ->
+     List.fold_left max 0 (List.map (aux' false) ((t :> nf)::(args :> nf list)@List.map snd !bs))
+ | `N _
+ | `Bottom
+ | `Pacman
+ | `Var _ -> 0 in
+ Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
 ;;
 
-let choose_step (n,p) =
+let choose_step p =
  let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
  let x =
   match showstoppers_step, showstoppers_eat with
   | [], y::_ ->
-     prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var p.var_names y); y
+     prerr_endline ("INSTANTIATING (critical eat) : " ^ string_of_var p.var_names y); y
+  | x::_, _ ->
+     prerr_endline ("INSTANTIATING (critical step): " ^ string_of_var p.var_names x); x
   | [], [] ->
      let heads =
       (* Choose only variables still alive (with arity > 0) *)
@@ -568,10 +581,7 @@ let choose_step (n,p) =
            Not_found -> assert false)
       | x::_ ->
          prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var p.var_names x);
-         x)
-  | x::_, _ ->
-      prerr_endline ("INSTANTIATING " ^ string_of_var p.var_names x);
-      x in
+         x) in
 (* Strategy that  decreases the special_k to 0 first (round robin)
 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
  let x =
@@ -602,81 +612,39 @@ let x =
  with
   Not_found -> x
 in*)
- let special_k =
-     compute_special_k (Listx.from_list (all_terms p :> nf list) )in
- if special_k < n then
-  prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@");
  let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
  let safe_arity_of_x = safe_arity_of_var p x in
- x, min arity_of_x safe_arity_of_x, special_k
+ x, min arity_of_x safe_arity_of_x
+;;
 
-let rec auto_eat (n,p) =
+let rec auto_eat p =
  prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}";
  let m = problem_measure p in
- let x, arity_of, n = choose_step (n,p) in
+ let x, arity_of = choose_step p in
  first arity_of p x (fun p j ->
-  let p' = instantiate p x j n in
+  let p' = instantiate p x j in
   match eat p' with
   | `Finished p -> p
   | `Continue p ->
       prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
       let delta = problem_measure p - m in
-      (* let delta = m - problem_measure p' in *)
       if delta >= 0
        then
         (failwith
         ("Measure did not decrease (+=" ^ string_of_int delta ^ ")"))
-       else prerr_endline ("$ Measure decreased of " ^ string_of_int delta);
-      auto_eat (n,p))
+       else prerr_endline ("$ Measure decreased: " ^ string_of_int delta);
+      auto_eat p)
 ;;
 
 let auto p n =
- prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@");
+prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@");
  match eat p with
  | `Finished p -> p
- | `Continue p -> auto_eat (n,p)
+ | `Continue p -> auto_eat p
 ;;
 
-(*
-0 = snd
-
-      x y = y 0    a y = k  k z = z 0  c y = k   y u = u h1 h2 0          h2 a = h3
-1 x a c    1 a 0 c  1 k c    1 c 0      1 k        1 k                     1 k
-2 x a y    2 a 0 y  2 k y    2 y 0      2 y 0      2 h2 0                  2 h3
-3 x b y    3 b 0 y  3 b 0 y  3 b 0 y    3 b 0 y    3 b 0 (\u. u h1 h2 0)   3 b 0 (\u. u h1 (\w.h3) 0)
-4 x b c    4 b 0 c  4 b 0 c  4 b 0 c    4 b 0 c    4 b 0 c                 4 b 0 c
-5 x (b e)  5 b e 0  5 b e 0  5 b e 0    5 b e 0    5 b e 0                 5 b e 0
-6 y y      6 y y    6 y y    6 y y      6 y y      6 h1 h1 h2 0 h2 0       6 h1 h1 (\w. h3) 0 (\w. h3) 0
-
-                                l2 _ = l3
-b u = u l1 l2 0                 e _ _ _ _ = f                         l3 n = n j 0
-1 k                             1 k                                  1 k
-2 h3                            2 h3                                 2 h3
-3 l2 0 (\u. u h1 (\w. h3) 0)    3 l3 (\u. u h1 (\w. h3) 0)           3 j h1 (\w. h3) 0 0
-4 l2 0 c                        4 l3 c                               4 c j 0
-5 e l1 l2 0 0                   5 f                                  5 f
-6 h1 h1 (\w. h3) 0 (\w. h3) 0   6 h1 h1 (\w. h3) 0 (\w. h3) 0        6 h1 h1 (\w. h3) 0 (\w. h3) 0
-*)
-
-(*
-                x n = n 0 ?
-x a (b (a c))   a 0 = 1 ? (b (a c))   8
-x a (b d')      a 0 = 1 ? (b d')      7
-x b (a c)       b 0 = 1 ? (a c)       4
-x b (a c')      b 0 = 1 ? (a c')      5
-
-c = 2
-c' = 3
-a 2 = 4  (* a c *)
-a 3 = 5  (* a c' *)
-d' = 6
-b 6 = 7  (* b d' *)
-b 4 = 8  (* b (a c) *)
-b 0 = 1
-a 0 = 1
-*)
 
-(************** Tests ************************)
+(******************************************************************************)
 
 let optimize_numerals p =
   let replace_in_sigma perm =
-- 
2.39.2


From aa3affff98814e20da10d5130b7dcefef9992f01 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 09:31:07 +0200
Subject: [PATCH 09/16] Cleanup in w, added names, uncommented test for low
 special_k

---
 ocaml/problems/w | 46 +++++++++++++++-------------------------------
 1 file changed, 15 insertions(+), 31 deletions(-)

diff --git a/ocaml/problems/w b/ocaml/problems/w
index c10a3f6..e3a5dd2 100644
--- a/ocaml/problems/w
+++ b/ocaml/problems/w
@@ -1,60 +1,44 @@
-$?
+$? w1
 D x y
 C x BOMB
 
-$?
+$? w2
 D x y z
 C x BOMB z
   x y y
 
-$!
- (* DISPLAY PROBLEM (main) - measure=965
-    Discriminating sets (deltas):
-    0 <> 1 <> 2 <> 3 <> 4
- *)(* DIVERGENT  *)
+$! w3
 D b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))
-#   (* CONVERGENT *) [
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (f g)))
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e)
 C b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))
 C b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))
-#  ] (* NUMERIC    *) [
 N b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) Z
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) Z
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) Z
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) Z
   b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) Z
-#  ];
 
-$!
- problem_of
- (* DISPLAY PROBLEM (main) - measure=561
-    Discriminating sets (deltas):
-    0 <> 1 <> 2 <> 3 <> 4
- *)(* DIVERGENT  *)
+$! w4
 D b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))
-#   (* CONVERGENT *) [
 C c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))
   e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))
   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))
   c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)
   e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))
-# ] (* NUMERIC    *) [
 N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) Z
   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) Z
   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) Z
   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) Z
   g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f Z
-#  ]
- ];
 
-# This fails, but shouldnt: commented out
-# $!
- D x PAC PAC PAC PAC PAC a
- C x PAC PAC PAC PAC PAC b
- N y x
-   y z
+# This was failing because special_k was too low
+$! low special_k
+D x PAC PAC PAC PAC PAC a
+C x PAC PAC PAC PAC PAC b
+N y x
+  y z
 # In general:
   DIV x (n times PAC) a
   CON x (n times PAC) b
@@ -64,13 +48,13 @@ N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e
   y must apply n+m+1 variables
   Thus special_k must be >=n+m+1
 
-# todo:
-  (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)
+$! eatable right away
+D y y
+C x (_. y y)
 
 
-#$! new failing problem
-# it is backtracking, but it shouldn't
-# why? well, D occurs in some C's
+#$? should raise a parsing error
+# (div occurs as subterm at top-level in conv and ps)
  D (a b)
  C ((((((((a (v (y. y))) (v c)) ((x ((a (v (y. y))) (v c))) y)) (((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))) (((v (x. (v c))) (v (x. (v c)))) (((((z z) b) (c. a)) (z z)) (b c))))) (a. ((((z z) b)(c. a)) (z z)))) (y. (z z))) (((a (v (y. y))) w) (z. x))) (w. (z. (v (y. y)))))
  C ((((((((z z) b) (c. a)) (z z)) ((v (y. y)) a)) (v (y. y))) ((((a (v (y. y))) (v c)) (z z)) ((a (v (y. y))) (((v c) ((((z z) b) (c. a)) (w (c. (v c))))) (w. (v. (z. (v (y. y))))))))) (z. ((v (y. y)) a)))
-- 
2.39.2


From bd3a8ee424e495ab4003f6d4cb88579f29e3bc3a Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 09:59:00 +0200
Subject: [PATCH 10/16] Revert subst in branches of matches

Actually, it could be moved in susbt_in_problem,
hence doing it only once (on the deltas), instead
of replacing multiple times like now (useless).
---
 ocaml/num.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 7e52482..1822e38 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -250,11 +250,14 @@ and subst truelam delift_by_one what (with_what : nf(*_nob*)) (where : nf) =
    | `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
-       (* let l' = l - bs_lift  in *)
-       (* let with_what' = lift l' (with_what :> nf) 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 ; *)
+       bs := List.map (fun (n,t) -> n,subst truelam false what with_what' t) !bs ;
        let body = 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*) =
-- 
2.39.2


From b277f630cb63b40ae983282ea81ffefe288d3e8f Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 22:22:41 +0200
Subject: [PATCH 11/16] Check for absence of bombs and pacmans

---
 ocaml/lambda4.ml | 18 +++++++++++-------
 ocaml/num.ml     |  4 ++--
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9ab675e..2f6a0a0 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -757,23 +757,27 @@ let solve (p, todo) =
        Backtrack _ -> `Unseparable "backtrack"
 ;;
 
+let no_bombs_pacmans p =
+    not (List.exists (eta_subterm `Bottom) (p.ps@p.conv))
+ && not (List.exists (eta_subterm `Pacman) p.ps)
+ && Util.option_map (eta_subterm `Pacman) p.div <> Some true
+;;
+
 let check p =
- (* TODO check if there are duplicates in p.ps
-     before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
- (* FIXME what about initial fragments? *)
  if (let rec f = function
      | [] -> false
      | hd::tl -> List.exists (eta_eq hd) tl || f tl in
-   f p.ps)
+   f p.ps) (* FIXME what about initial fragments of numbers? *)
   then `CompleteUnseparable "ps contains duplicates"
  (* check if div occurs somewhere in ps@conv *)
  else if (match p.div with
   | None -> true
   | Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv))
-  ) && false (* TODO no bombs && pacmans *)
+  ) && no_bombs_pacmans p
   then `CompleteSeparable "no bombs, pacmans and div"
- else if false (* TODO bombs or div fuori da lambda in ps@conv *)
-  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv"
+  (* il check seguente e' spostato nel parser e lancia un ParsingError *)
+ (* else if false (* TODO bombs or div fuori da lambda in ps@conv *)
+  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" *)
  else if p.div = None
   then `CompleteSeparable "no div"
  else `Uncomplete
diff --git a/ocaml/num.ml b/ocaml/num.ml
index 1822e38..1e630f4 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -295,8 +295,8 @@ let eta_compare x y =
   | `Pacman, `Pacman -> 0
   | `Lam _, `N _ -> -1
   | `N _, `Lam _ -> 1
-  | `Bottom, `Lam _
-  | `Lam _, `Bottom -> assert false (* TO BE UNDERSTOOD *)
+  | `Bottom, `Lam(_,t) -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux `Bottom t
+  | `Lam(_,t), `Bottom -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux t `Bottom
   | `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)))
-- 
2.39.2


From 54e55518261ee5f3c68758ea070b1bac41400e54 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 22:23:34 +0200
Subject: [PATCH 12/16] Better error messages in parser

---
 ocaml/parser.ml | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 6bcb70d..34b62ba 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -18,7 +18,7 @@ let mk_var' (bound, free) x =
 ;;
 
 let mk_app' = function
-  | [] ->  raise (ParsingError "bug")
+  | [] ->  assert false
   | t :: ts -> List.fold_left mk_app t ts
 ;;
 
@@ -73,12 +73,12 @@ let rec read_smt vars =
       | Some varname, cs ->
       let vars' = (varname::bound, free) in
       (match strip_spaces cs with
-        | [] -> raise (ParsingError "manca dopo variabile lambda")
+        | [] -> raise (ParsingError "Lambda expression incomplete")
         | c::cs -> (if c = '.' then (match read_smt vars' cs with
-          | None, _, _ -> raise (ParsingError "manca corpo lambda")
+          | None, _, _ -> raise (ParsingError "Lambda body expected")
           | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)
-          | Some _, _, _ -> raise (ParsingError "???")
-          ) else raise (ParsingError "manca . nel lambda")
+          | Some _, _, _ -> assert false
+          ) else raise (ParsingError "Expected `.` after variable in lambda")
         ))
       | _, _ -> assert false
  ) in let rec aux vars cs =
@@ -96,7 +96,7 @@ let rec read_smt vars =
           | None, cs, vars -> Some [tm], cs, vars
           | Some ts, cs, vars -> Some (tm :: ts), cs, vars
         )
-      | Some _ -> raise (ParsingError "bug")
+      | Some _ -> assert false
       | None -> None, x, vars
   in fun cs -> match aux vars cs with
     | None, cs, vars -> None, cs, vars
@@ -108,20 +108,20 @@ and read_pars vars = function
     let cs = strip_spaces cs in
     match cs with
       | [] -> None, [], vars
-      | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError ") mancante")
-    ) else raise (ParsingError "???")
+      | 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
-  | _, _, _ -> raise (ParsingError "???")
+  | _, _, _ -> assert false
 ;;
 
 let parse_many strs =
   let f (x, y) z = match read_smt y (explode z) with
   | Some[tm], [], vars -> (tm :: x, vars)
-  | _, _, _ -> raise (ParsingError "???")
+  | _, _, _ -> assert false
   in let aux = List.fold_left f ([], ([], [])) (* index zero is reserved *)
   in let (tms, (_, free)) = aux strs
   in (List.rev tms, free)
@@ -169,7 +169,7 @@ let problem_of_string s =
  let strs = [div] @ ps @ conv in
 
  if List.length ps = 0 && List.length conv = 0
-  then raise (ParsingError "empty problem");
+  then raise (ParsingError "Parsed empty problem");
 
  (* parse' *)
  let (tms, free) = parse_many strs in
@@ -187,6 +187,7 @@ let problem_of_string s =
  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)
@@ -206,17 +207,17 @@ let div = if not div_provided || div = `Bottom
  then None
  else match div with
   | `I _ as t -> Some t
-  | _ -> raise (ParsingError "div is not an inert or BOT in the initial problem") in
+  | _ -> 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 term in conv is not i_n_var")
+ | _ -> raise (ParsingError "A C-term is not i_n_var")
  ) conv in
 let ps = List.map (
  function
   | #i_n_var as y -> y
-  | _ as y -> raise (ParsingError ("A term in num is not i_n_var" ^ Num.string_of_nf y))
+  | _ -> raise (ParsingError "An N-term is not i_n_var")
  ) ps in
  name, div, conv, ps, free
 ;;
-- 
2.39.2


From 2c7cb84589a53b27d30f2d3ae6333bb175d0d7d8 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 14:05:08 +0200
Subject: [PATCH 13/16] Removed special strategies in choose_step

---
 ocaml/lambda4.ml | 60 ++++++++++++------------------------------------
 1 file changed, 15 insertions(+), 45 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 2f6a0a0..21cd5ca 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -58,7 +58,7 @@ let first bound p var f =
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
      aux (i+1)
  in
   aux 1
@@ -368,22 +368,22 @@ let rec edible ({div; conv; ps} as p) arities showstoppers =
            aux showstoppers xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps in
-
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
-  List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+            aux (sort_uniq (h::showstoppers)) ps
+  in
+    let showstoppers = sort_uniq (aux showstoppers ps) in
+    let dangerous_conv =
+     List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
 
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
 List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
 
- let showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
-  | None -> showstoppers'
-  | Some div ->
-    if List.exists ((=) (hd_of_i_var div)) showstoppers'
-    then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+    let showstoppers' = showstoppers @ List.concat dangerous_conv in
+    let showstoppers' = sort_uniq (match div with
+     | None -> showstoppers'
+     | Some div ->
+       if List.exists ((=) (hd_of_i_var div)) showstoppers'
+       then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+    if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
 ;;
 
 let precompute_edible_data {ps; div} xs =
@@ -431,8 +431,8 @@ let critical_showstoppers p =
   let showstoppers_eat = List.filter
     (fun x -> not (List.mem x showstoppers_step))
     showstoppers_eat in
-List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+  List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+  List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
   p, showstoppers_step, showstoppers_eat
   ;;
 
@@ -582,36 +582,6 @@ let choose_step p =
       | x::_ ->
          prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var p.var_names x);
          x) in
-(* Strategy that  decreases the special_k to 0 first (round robin)
-1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
- let x =
-  try
-   match
-    hd_of (List.find (fun t ->
-     compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
-     ) (all_terms p))
-   with
-    | None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var p.var_names x);
-       x
-  with
-   Not_found ->
-    let arity_of_x = max_arity_tms x (all_terms p) in
-    assert (Util.option_get arity_of_x > 0);
-    x in
-(* Instantiate in decreasing order of compute_special_k
-1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
-let x =
- try
-  (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) (all_terms p))))) with
-      None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
-       x)
- with
-  Not_found -> x
-in*)
  let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
  let safe_arity_of_x = safe_arity_of_var p x in
  x, min arity_of_x safe_arity_of_x
-- 
2.39.2


From 704fd9d9db0c01619264527d4174afe74bdff53d Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 13:09:05 +0200
Subject: [PATCH 14/16] Fixed eta_compare in the case Lam vs. Bot

---
 ocaml/num.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 1e630f4..aa9338c 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -295,8 +295,8 @@ let eta_compare x y =
   | `Pacman, `Pacman -> 0
   | `Lam _, `N _ -> -1
   | `N _, `Lam _ -> 1
-  | `Bottom, `Lam(_,t) -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux `Bottom t
-  | `Lam(_,t), `Bottom -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux t `Bottom
+  | `Bottom, `Lam(_,t) -> -1
+  | `Lam(_,t), `Bottom ->  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)))
-- 
2.39.2


From d996cf6c47fdea2409dfb2e94430b0d080b8e8ae Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 14:44:47 +0200
Subject: [PATCH 15/16] Added very simple generator of tests with
 bombs/pacmans, run it with --with-pac

---
 ocaml/test.ml | 57 ++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 47 insertions(+), 10 deletions(-)

diff --git a/ocaml/test.ml b/ocaml/test.ml
index 3b6d904..32d60aa 100644
--- a/ocaml/test.ml
+++ b/ocaml/test.ml
@@ -12,6 +12,16 @@ let acaso2 l1 l2 =
   if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n
 ;;
 
+(** with bombs and pacmans too *)
+let acaso3 l1 l2 =
+ if Random.int 10 = 0 then (
+  if Random.int 2 = 0 then "BOMB" else "PAC"
+ ) else
+  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 rec take l n =
   if n = 0 then []
   else match l with
@@ -35,6 +45,22 @@ let gen n vars =
   in aux (2*n) vars []
 ;;
 
+let gen_pac n vars =
+ let rec take' l n =
+  if n = 0 then [], []
+  else match l with
+  | [] -> [], []
+  | [_] -> assert false
+  | x1::x2::xs -> let a, b = take' xs (n-1) in x1::a,x2::b 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 ^ ". " ^ acaso3 inerts lams ^ ")") :: lams
+    else ("(" ^ acaso inerts ^ " " ^ acaso3 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 ###########################";
@@ -54,16 +80,27 @@ let solve div convs nums =
 ;;
 
 let main =
-  Random.self_init ();
-  let num = 100 in
-  let complex = 200 in
-  let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
+ Random.self_init ();
+ (* num = number of tests to run *)
+ let num = 100 in
+ (* if flag --with-pac active, then more general tests *)
+ let with_pac = List.mem "--with-pac" (Array.to_list Sys.argv) in
+
+ let f = if with_pac
+  then (
+   let complex = 10 in
+   let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
+   fun () -> gen_pac complex vars
+  ) else (
+   let complex = 200 in
+   let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in
+   fun () -> gen complex vars
+   ) in
 
-  repeat (fun _ ->
-    let div, (conv, nums) = gen complex vars in
-    solve div conv nums
-  ) num
-  ;
+ repeat (fun _ ->
+   let div, (conv, nums) = f () in
+   solve div conv nums
+ ) num;
 
-  prerr_endline "\n---- ALL TESTS COMPLETED ----"
+ prerr_endline "\n---- ALL TESTS COMPLETED ----"
 ;;
-- 
2.39.2


From 2dc40f471a59b3e192d5c9db14746292958315db Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 24 Jul 2017 14:55:04 +0200
Subject: [PATCH 16/16] Added exception Lambda, which may be caught when a conv
 becomes a lambda

---
 ocaml/lambda4.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 21cd5ca..336f6b1 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -6,6 +6,7 @@ open Num
 (* exceptions *)
 exception Pacman
 exception Bottom
+exception Lambda
 exception Backtrack of string
 
 (*
@@ -208,7 +209,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
       let freshno,new_t,acc_new_ps =
        try
         expand_match (freshno,ps,acc_new_ps) t
-       with Pacman -> freshno,convergent_dummy,acc_new_ps
+       with Pacman | Lambda -> freshno,convergent_dummy,acc_new_ps
           | Bottom -> raise (Backtrack "Bottom in conv") in
       aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
@@ -257,7 +258,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
          let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
 (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
           expand_match (freshno,acc_ps,acc_new_ps) t
-   | `Lam _ -> assert false (* algorithm invariant/loose typing *)
+   | `Lam _ -> raise Lambda (* assert false (* algorithm invariant/loose typing *) *)
    | `Bottom -> raise Bottom
    | `Pacman -> raise Pacman
    | #i_n_var as x ->
-- 
2.39.2