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