From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Jun 2018 21:31:30 +0000 (+0200)
Subject: quantic measure (partially) fixed
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc7b3bd553626969b2c22a5ec3e431f67fcd2ff1;p=fireball-separation.git

quantic measure (partially) fixed

- all simple.[0-2] tests now pass
- simple.evil does not

Ideas:
1) when stepping over a term, its (shared) boolean is
   turned to false
2) when reducing a step, the booleans are propagated
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 5764c3c..f61ce5e 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -105,18 +105,26 @@ let rec no_leading_lambdas v n = function
  | V v' -> if v = v' then n else 0
 ;;
 
-(* b' defaults to false *)
+(* b' is true iff we are substituting the argument of a step
+   and the application of the redex was true. Therefore we need to
+   set the new app to true.  *)
 let rec subst b' 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)
  | L(b,t) -> L(b, subst b' (level + 1) delift sub t)
- | A(_,t1,(V v as t2)) when !b' && v = level + fst sub ->
-    mk_app b' (subst b' level delift sub t1) (subst b' level delift sub t2)
+ | A(_,t1,(V v as t2)) when b' && v = level + fst sub ->
+    mk_app (ref true) (subst b' level delift sub t1) (subst b' level delift sub t2)
  | A(b,t1,t2) ->
     mk_app b (subst b' level delift sub t1) (subst b' level delift sub t2)
+(* b is
+   - a fresh ref true if we want to create a real application from scratch
+   - a shared ref true if we substituting in the head of a real application *)
 and mk_app b' t1 t2 = if t1 = delta && t2 = delta then raise B
  else match t1 with
- | L(b,t1) -> subst (ref (!b' && not b)) 0 true (0, t2) t1
+ | L(b,t1) ->
+    let last_lam = match t1 with L _ -> false | _ -> true in
+    if not b && last_lam then b' := false ;
+    subst (!b' && not b && not last_lam) 0 true (0, t2) t1
  | _ -> A (b', t1, t2)
 and lift n =
  let rec aux lev =
@@ -126,8 +134,8 @@ and lift n =
   | A (b,t1, t2) -> A (b,aux lev t1, aux lev t2)
  in aux 0
 ;;
-let subst = subst (ref false) 0 false;;
-let mk_app = mk_app (ref true);;
+let subst = subst false 0 false;;
+let mk_app t1 = mk_app (ref true) t1;;
 
 let eta_eq =
  let rec aux t1 t2 = match t1, t2 with
@@ -319,7 +327,7 @@ let rec auto p =
   let p = step j k p in
   let m2 = measure_of_t p.div in
   (if m2 >= m1 then
-    (print_string "WARNING! Measure did not decrease (press <Enter>)";
+    (print_string ("WARNING! Measure did not decrease : " ^ string_of_int m2 ^ " >= " ^ string_of_int m1 ^ " (press <Enter>)");
     ignore(read_line())));
   auto p
 ;;