X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;h=b640a0fdb2f2d58e3117a3dd647666854aa586bc;hb=9d007f52d02d23ed95d28c7b805b65bbdc47de6a;hp=5764c3ca60e5a7fab41722ec9f1c3c0b958c4557;hpb=74df5ba0526545acae8d23350c41c45c9c480789;p=fireball-separation.git

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