| 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
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
let rec subst 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 t -> let t = subst (level + 1) delift sub t in if t = B then B else L t\r
+ | L t -> L (subst (level + 1) delift sub t)\r
| A (t1,t2) ->\r
let t1 = subst level delift sub t1 in\r
let t2 = subst level delift sub t2 in\r
;;\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
let find_eta_difference p t argsno =\r
let t = inert_cut_at argsno t in\r
let rec aux t u k = match t, u with\r
- | V _, V _ -> problem_fail p "no eta difference found (div subterm of conv?)"\r
+ | V _, V _ -> None\r
| A(t1,t2), A(u1,u2) ->\r
- if not (eta_eq t2 u2) then (k-1)\r
- else aux t1 u1 (k-1)\r
+ (match aux t1 u1 (k-1) with\r
+ | None ->\r
+ if not (eta_eq t2 u2) then Some (k-1)\r
+ else None\r
+ | Some j -> Some j)\r
| _, _ -> assert false\r
- in aux p.div t argsno\r
+ in match aux p.div t argsno with\r
+ | None -> problem_fail p "no eta difference found (div subterm of conv?)"\r
+ | Some j -> j\r
;;\r
\r
let compute_max_lambdas_at hd_var j =\r
let p, v = freshvar p in\r
p, A(t, V (v + k + 1))\r
) (p, V 0) n in\r
- let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
- fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
+ let t = (* apply bound variables V_k..V_0 *)\r
+ fold_nat (fun t m -> A(t, V (k-m+1))) t (k+1) in\r
let t = mk_lams t (k+1) in (* make leading lambdas *)\r
let subst = var, t in\r
let p = subst_in_problem subst p in\r