One garbage pt. 2

[fireball-separation.git] / ocaml / simple.ml

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 5764c3ca60e5a7fab41722ec9f1c3c0b958c4557..b640a0fdb2f2d58e3117a3dd647666854aa586bc 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -24,6 +24,29 @@ let measure_of_t =
  in snd ++ (aux [])\r
 ;;\r
 \r
+let index_of x =\r
+ let rec aux n =\r
+  function\r
+    [] -> None\r
+  | x'::_ when x == x' -> Some n\r
+  | _::xs -> aux (n+1) xs\r
+ in aux 1\r
+;;\r
+\r
+let sep_of_app =\r
+ let apps = ref [] in\r
+ function\r
+    r when not !r -> " "\r
+  | r ->\r
+    let i =\r
+     match index_of r !apps with\r
+        Some i -> i\r
+      | None ->\r
+         apps := !apps @ [r];\r
+         List.length !apps\r
+    in " " ^ string_of_int i ^ ":"\r
+;;\r
+\r
 let string_of_t =\r
   let string_of_bvar =\r
    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
@@ -35,7 +58,7 @@ let string_of_t =
     | A _\r
     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
   and string_of_term_no_pars_app level = function\r
-    | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ (if !b then "," else " ") ^ string_of_term_w_pars level t2\r
+    | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ sep_of_app b ^ string_of_term_w_pars level t2\r
     | _ as t -> string_of_term_w_pars level t\r
   and string_of_term_no_pars level = function\r
     | L(_,t) -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
@@ -105,18 +128,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 +157,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 +350,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
@@ -332,8 +363,11 @@ let problem_of (label, div, convs, ps, var_names) =
  | `Var(v,_) -> V v\r
  | `N _ | `Match _ -> assert false in\r
  assert (List.length ps = 0);\r
- let convs = List.rev convs in\r
- let conv = if List.length convs = 1 then aux (List.hd convs :> Num.nf) else List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let convs = (List.rev convs :> Num.nf list) in\r
+ let conv = aux\r
+  (if List.length convs = 1\r
+   then List.hd convs\r
+   else `I((List.length var_names, min_int), Listx.from_list convs)) in\r
  let var_names = "@" :: var_names in\r
  let div = match div with\r
  | Some div -> aux (div :> Num.nf)\r