From 1284d4c268ae3a687e95b3eeebd741001ec83007 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jun 2018 17:36:55 +0200
Subject: [PATCH] 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.
---
 ocaml/simple.ml | 37 +++++++++++++++++++++++++++++++------
 1 file changed, 31 insertions(+), 6 deletions(-)

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