Embarassing bug in eta_eq fixed

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index aa91996027a513fc5f8eaface109bdd8d0bf9600..bfb5ebd71c50d076f070c432aec10451d12cc420 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -13,31 +13,6 @@ type t =
  | L of t\r
 ;;\r
 \r
-let delta = L(A(V 0, V 0));;\r
-\r
-let eta_eq' =\r
- let rec aux l1 l2 t1 t2 = match t1, t2 with\r
-  | L t1, L t2 -> aux l1 l2 t1 t2\r
-  | L t1, t2 -> aux l1 (l2+1) t1 t2\r
-  | t1, L t2 -> aux (l1+1) l2 t1 t2\r
-  | V a, V b -> a + l1 = b + l2\r
-  | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
-  | _, _ -> false\r
- in aux ;;\r
-let eta_eq = eta_eq' 0 0;;\r
-\r
-(* is arg1 eta-subterm of arg2 ? *)\r
-let eta_subterm u =\r
- let rec aux lev t = eta_eq' lev 0 u t || match t with\r
- | L t -> aux (lev+1) t\r
- | A(t1, t2) -> aux lev t1 || aux lev t2\r
- | _ -> false\r
- in aux 0\r
-;;\r
-\r
-(* does NOT lift the argument *)\r
-let mk_lams = fold_nat (fun x _ -> L x) ;;\r
-\r
 let string_of_t =\r
   let string_of_bvar =\r
    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
@@ -57,6 +32,12 @@ let string_of_t =
   in string_of_term_no_pars 0\r
 ;;\r
 \r
+\r
+let delta = L(A(V 0, V 0));;\r
+\r
+(* does NOT lift the argument *)\r
+let mk_lams = fold_nat (fun x _ -> L x) ;;\r
+\r
 type problem = {\r
    orig_freshno: int\r
  ; freshno : int\r
@@ -134,6 +115,25 @@ and lift n =
 ;;\r
 let subst = subst 0 false;;\r
 \r
+let eta_eq =\r
+ let rec aux t1 t2 = match t1, t2 with\r
+  | L t1, L t2 -> aux t1 t2\r
+  | L t1, t2 -> aux t1 (A(lift 1 t2,V 0))\r
+  | t1, L t2 -> aux (A(lift 1 t1,V 0)) t2\r
+  | V a, V b -> a = b\r
+  | A(t1,t2), A(u1,u2) -> aux t1 u1 && aux t2 u2\r
+  | _, _ -> false\r
+ in aux ;;\r
+\r
+(* is arg1 eta-subterm of arg2 ? *)\r
+let eta_subterm u =\r
+ let rec aux lev t = eta_eq u (lift lev t) || match t with\r
+ | L t -> aux (lev+1) t\r
+ | A(t1, t2) -> aux lev t1 || aux lev t2\r
+ | _ -> false\r
+ in aux 0\r
+;;\r
+\r
 let subst_in_problem ((v, t) as sub) p =\r
 print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\r
  let sigma = sub::p.sigma in\r