From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 16:29:30 +0000 (+0200)
Subject: Fix no_leading_lambdas to account for a step on x on an argument starting with x
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27a3d2f1379f6fff89d7de2d82f7066b8cc0f31a;p=fireball-separation.git

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