Fix no_leading_lambdas to account for a step on x on an argument starting with x

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 28603258c04539410f98afb02d2ac301f97c793c..b068791d4d55a3fda859c36ab01a5e643bb065e7 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -105,17 +105,18 @@ let rec is_inert =
 let is_var = function V _ -> true | _ -> false;;\r
 let is_lambda = function L _ -> true | _ -> false;;\r
 \r
-let rec no_leading_lambdas = function\r
- | L t -> 1 + no_leading_lambdas t\r
- | _ -> 0\r
-;;\r
-\r
 let rec get_inert = function\r
  | V n -> (n,0)\r
  | A(t, _) -> let hd,args = get_inert t in hd,args+1\r
  | _ -> assert false\r
 ;;\r
 \r
+let rec no_leading_lambdas hd_var j = function\r
+ | L t -> 1 + no_leading_lambdas (hd_var+1) j t\r
+ | A _ as t -> let hd_var', n = get_inert t in if hd_var = hd_var' then max 0 (j - n) else 0\r
+ | V n -> if n = hd_var then j else 0\r
+ | B | C _ -> 0\r
+;;\r
 let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
@@ -144,7 +145,7 @@ and lift n =
 ;;\r
 let subst = subst 0 false;;\r
 \r
-let subst_in_problem (sub: var * t) (p: problem) =\r
+let subst_in_problem sub p =\r
 print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
  {p with\r
   div=subst sub p.div;\r
@@ -230,7 +231,7 @@ let compute_max_lambdas_at hd_var j =
       then max ( (*FIXME*)\r
        if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
         then let hd', j' = get_inert t2 in j - j'\r
-        else no_leading_lambdas t2)\r
+        else no_leading_lambdas hd_var j t2)\r
       else id) (max (aux hd t1) (aux hd t2))\r
  | L t -> aux (hd+1) t\r
  | V _ -> 0\r
@@ -385,5 +386,10 @@ run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
  "x a a a a (_. _. _. _. x. y. x y)";\r
 ] ;;\r
 \r
+(* bug in no_leading_lambdas where x in j-th position *)\r
+run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
+["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)))"]\r
+;;\r
+\r
 print_hline();\r
 print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r