Fix: eating a lambda^n.C args is bad

I know eat an argument which is a flexible inert.
What to do if there is none? I think we should backtrack;
for the time being I raise an assert false.

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index c318ebd71482eea1a9a4a784d1f27cf2502e5a01..44b9aa2a871d74619fdcbe88599580ce4c7b2d70 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -100,6 +100,8 @@ let freshvar ({freshno} as p) =
  {p with freshno=freshno+1}, freshno+1\r
 ;;\r
 \r
+(* CSC: rename? is an applied C an inert?\r
+   is_inert and get_inert work inconsistently *)\r
 let rec is_inert =\r
  function\r
  | A(t,_) -> is_inert t\r
@@ -108,6 +110,15 @@ let rec is_inert =
  | L _ | B -> false\r
 ;;\r
 \r
+let rec is_constant =\r
+ function\r
+    C -> true\r
+  | V _ -> false\r
+  | B -> assert false\r
+  | A(t,_)\r
+  | L t -> is_constant t\r
+;;\r
+\r
 let rec get_inert = function\r
  | V _ | C as t -> (t,0)\r
  | A(t, _) -> let hd,args = get_inert t in hd,args+1\r
@@ -211,8 +222,6 @@ let sanity p =
 ;;\r
 \r
 (* drops the arguments of t after the n-th *)\r
-(* FIXME! E' usato in modo improprio contando sul fatto\r
-   errato che ritorna un inerte lungo esattamente n *)\r
 let inert_cut_at n t =\r
  let rec aux t =\r
   match t with\r
@@ -257,6 +266,18 @@ let compute_max_lambdas_at hd_var j =
 \r
 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 \r
+(* returns Some i if i is the smallest integer s.t. p holds for the i-th\r
+   element of the list in input *)\r
+let smallest_such_that p =\r
+ let rec aux i =\r
+  function\r
+     [] -> None\r
+   | hd::_ when (print_endline (string_of_t hd) ; p hd) -> Some i\r
+   | _::tl -> aux (i+1) tl\r
+ in\r
+  aux 0\r
+;;\r
+\r
 (* eat the arguments of the divergent and explode.\r
  It does NOT perform any check, may fail if done unsafely *)\r
 let eat p =\r
@@ -269,17 +290,21 @@ print_cmd "EAT" "";
  let p =\r
   match phase with\r
   | `One ->\r
+      let i =\r
+       match smallest_such_that (fun x -> not (is_constant x)) (args_of_inert p.div) with\r
+          Some i -> i\r
+        | None -> assert false (*CSC: backtrack? *) in\r
       let n = 1 + max\r
-       (compute_max_lambdas_at var (k-1) p.div)\r
-       (compute_max_lambdas_at var (k-1) p.conv) in\r
+       (compute_max_lambdas_at var (k-i-1) p.div)\r
+       (compute_max_lambdas_at var (k-i-1) p.conv) in\r
       (* apply fresh vars *)\r
       let p, t = fold_nat (fun (p, t) _ ->\r
         let p, v = freshvar p in\r
         p, A(t, V (v + k))\r
-      ) (p, V 0) n in\r
+      ) (p, V (k-1-i)) n in\r
       let p = {p with phase=`Two} in\r
       let t = A(t, delta) in\r
-      let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
+      let t = fold_nat (fun t m -> if k-m = i then t else  A(t, V (k-m))) t k in\r
       let subst = var, mk_lams t k in\r
       let p = subst_in_problem subst p in\r
       let _, args = get_inert p.div in\r