X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Fsimple.ml;h=bfb5ebd71c50d076f070c432aec10451d12cc420;hb=b8b634b6e8907bb7c5e1a228ec173fab2b7b6546;hp=154992dd3f056dad04a1334eff68b75b7be211b7;hpb=640e7671fac6bebe8debe37dba052018c3b4c76f;p=fireball-separation.git

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 154992d..bfb5ebd 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -13,31 +13,6 @@ type t =
  | L of t
 ;;
 
-let delta = L(A(V 0, V 0));;
-
-let eta_eq' =
- let rec aux l1 l2 t1 t2 = match t1, t2 with
-  | L t1, L t2 -> aux l1 l2 t1 t2
-  | L t1, t2 -> aux l1 (l2+1) t1 t2
-  | t1, L t2 -> aux (l1+1) l2 t1 t2
-  | V a, V b -> a + l1 = b + l2
-  | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2
-  | _, _ -> false
- in aux ;;
-let eta_eq = eta_eq' 0 0;;
-
-(* is arg1 eta-subterm of arg2 ? *)
-let eta_subterm u =
- let rec aux lev t = eta_eq' lev 0 u t || match t with
- | L t -> aux (lev+1) t
- | A(t1, t2) -> aux lev t1 || aux lev t2
- | _ -> false
- in aux 0
-;;
-
-(* does NOT lift the argument *)
-let mk_lams = fold_nat (fun x _ -> L x) ;;
-
 let string_of_t =
   let string_of_bvar =
    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in
@@ -57,6 +32,12 @@ let string_of_t =
   in string_of_term_no_pars 0
 ;;
 
+
+let delta = L(A(V 0, V 0));;
+
+(* does NOT lift the argument *)
+let mk_lams = fold_nat (fun x _ -> L x) ;;
+
 type problem = {
    orig_freshno: int
  ; freshno : int
@@ -115,7 +96,7 @@ let rec no_leading_lambdas v n = function
 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)
- | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t
+ | L t -> L (subst (level + 1) delift sub t)
  | A (t1,t2) ->
   let t1 = subst level delift sub t1 in
   let t2 = subst level delift sub t2 in
@@ -134,6 +115,25 @@ and lift n =
 ;;
 let subst = subst 0 false;;
 
+let eta_eq =
+ let rec aux t1 t2 = match t1, t2 with
+  | L t1, L t2 -> aux t1 t2
+  | L t1, t2 -> aux t1 (A(lift 1 t2,V 0))
+  | t1, L t2 -> aux (A(lift 1 t1,V 0)) t2
+  | V a, V b -> a = b
+  | A(t1,t2), A(u1,u2) -> aux t1 u1 && aux t2 u2
+  | _, _ -> false
+ in aux ;;
+
+(* is arg1 eta-subterm of arg2 ? *)
+let eta_subterm u =
+ let rec aux lev t = eta_eq u (lift lev t) || match t with
+ | L t -> aux (lev+1) t
+ | A(t1, t2) -> aux lev t1 || aux lev t2
+ | _ -> false
+ in aux 0
+;;
+
 let subst_in_problem ((v, t) as sub) p =
 print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);
  let sigma = sub::p.sigma in
@@ -206,12 +206,17 @@ let inert_cut_at n t =
 let find_eta_difference p t argsno =
  let t = inert_cut_at argsno t in
  let rec aux t u k = match t, u with
- | V _, V _ -> problem_fail p "no eta difference found (div subterm of conv?)"
+ | V _, V _ -> None
  | A(t1,t2), A(u1,u2) ->
-    if not (eta_eq t2 u2) then (k-1)
-    else aux t1 u1 (k-1)
+    (match aux t1 u1 (k-1) with
+    | None ->
+      if not (eta_eq t2 u2) then Some (k-1)
+      else None
+    | Some j -> Some j)
  | _, _ -> assert false
- in aux p.div t argsno
+ in match aux p.div t argsno with
+ | None -> problem_fail p "no eta difference found (div subterm of conv?)"
+ | Some j -> j
 ;;
 
 let compute_max_lambdas_at hd_var j =
@@ -269,8 +274,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
     let p, v = freshvar p in
     p, A(t, V (v + k + 1))
   ) (p, V 0) n in
- let t = (* apply unused bound variables V_{k-1}..V_1 *)
-  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
+ let t = (* apply bound variables V_k..V_0 *)
+  fold_nat (fun t m -> A(t, V (k-m+1))) t (k+1) in
  let t = mk_lams t (k+1) in (* make leading lambdas *)
  let subst = var, t in
  let p = subst_in_problem subst p in