type var = int;;\r
type t =\r
| V of var\r
- | A of bool * t * t\r
+ | A of (bool ref) * t * t\r
| L of (bool * t)\r
;;\r
\r
-let rec measure_of_t = function\r
- | V _ -> 0\r
- | A(b,t1,t2) -> (if b then 1 else 0) + measure_of_t t1 + measure_of_t t2\r
- | L(b,t) -> if b then measure_of_t t else 0\r
+let measure_of_t =\r
+ let rec aux acc = function\r
+ | V _ -> acc, 0\r
+ | A(b,t1,t2) ->\r
+ let acc, m1 = aux acc t1 in\r
+ let acc, m2 = aux acc t2 in\r
+ if not (List.memq b acc) && !b then b::acc, 1 + m1 + m2 else acc, m1 + m2\r
+ | L(b,t) -> if b then aux acc t else acc, 0\r
+ 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
| 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
;;\r
\r
\r
-let delta = L(true,A(true,V 0, V 0));;\r
+let delta = L(true,A(ref true,V 0, V 0));;\r
\r
(* does NOT lift the argument *)\r
let mk_lams = fold_nat (fun x _ -> L(false,x)) ;;\r
| 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
+ 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 (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
in aux 0\r
;;\r
let subst = subst false 0 false;;\r
-let mk_app = mk_app true;;\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
| L(_,t1), L(_,t2) -> aux t1 t2\r
- | L(_,t1), t2 -> aux t1 (A(true,lift 1 t2,V 0))\r
- | t1, L(_,t2) -> aux (A(true,lift 1 t1,V 0)) t2\r
+ | L(_,t1), t2 -> aux t1 (A(ref true,lift 1 t2,V 0))\r
+ | t1, L(_,t2) -> aux (A(ref true,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
\r
let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
\r
-(* eat the arguments of the divergent and explode.\r
- It does NOT perform any check, may fail if done unsafely *)\r
-let eat p =\r
-print_cmd "EAT" "";\r
- let var, k = get_inert p.div in\r
- let phase = p.phase in\r
- let p =\r
- match phase with\r
- | `One ->\r
- let n = 1 + max\r
- (compute_max_lambdas_at var (k-1) p.div)\r
- (compute_max_lambdas_at var (k-1) p.conv) in\r
- (* apply fresh vars *)\r
- let p, t = fold_nat (fun (p, t) _ ->\r
- let p, v = freshvar p in\r
- p, A(false, t, V (v + k))\r
- ) (p, V 0) n in\r
- let p = {p with phase=`Two} in\r
- let t = A(false, t, delta) in\r
- let t = fold_nat (fun t m -> A(false, t, V (k-m))) t (k-1) in\r
- let subst = var, mk_lams t k in\r
- let p = subst_in_problem subst p in\r
- let _, args = get_inert p.div in\r
- {p with div = inert_cut_at (args-k) p.div}\r
- | `Two ->\r
- let subst = var, mk_lams delta k in\r
- subst_in_problem subst p in\r
- sanity p\r
-;;\r
-\r
(* step on the head of div, on the k-th argument, with n fresh vars *)\r
let step k n p =\r
let var, _ = get_inert p.div in\r
let p, t = (* apply fresh vars *)\r
fold_nat (fun (p, t) _ ->\r
let p, v = freshvar p in\r
- p, A(false, t, V (v + k + 1))\r
+ p, A(ref false, t, V (v + k + 1))\r
) (p, V 0) n in\r
let t = (* apply bound variables V_k..V_0 *)\r
- fold_nat (fun t m -> A(false, t, V (k-m+1))) t (k+1) in\r
+ fold_nat (fun t m -> A(ref false, 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
sanity p\r
;;\r
\r
+let finish p =\r
+ let compute_max_arity =\r
+ let rec aux n = function\r
+ | A(_,t1,t2) -> max (aux (n+1) t1) (aux 0 t2)\r
+ | L(_,t) -> max n (aux 0 t)\r
+ | V _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let j = div_nargs - 1 in\r
+ let arity = compute_max_arity p.conv in\r
+ let n = 1 + arity + max\r
+ (compute_max_lambdas_at div_hd j p.div)\r
+ (compute_max_lambdas_at div_hd j p.conv) in\r
+ let p = step j n p in\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let rec aux m = function\r
+ A(_,t1,t2) -> if is_var t2 then\r
+ (let delta_var, _ = get_inert t2 in\r
+ if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None\r
+ then m, delta_var\r
+ else aux (m-1) t1) else aux (m-1) t1\r
+ | _ -> assert false in\r
+ let m, delta_var = aux div_nargs p.div in\r
+ let p = subst_in_problem (delta_var, delta) p in\r
+ let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
+ sanity p\r
+;;\r
+\r
let rec auto p =\r
let hd_var, n_args = get_inert p.div in\r
match get_subterm_with_head_and_args hd_var n_args p.conv with\r
| None ->\r
+ (try problem_fail (finish p) "Auto.2 did not complete the problem"\r
+ with Done sigma -> sigma)\r
+ (*\r
(try\r
let phase = p.phase in\r
let p = eat p in\r
then problem_fail p "Auto.2 did not complete the problem"\r
else auto p\r
with Done sigma -> sigma)\r
+ *)\r
| Some t ->\r
let j = find_eta_difference p t n_args in\r
let k = 1 + max\r
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
| `N _ | `Match _ -> assert false in\r
assert (List.length ps = 0);\r
let convs = List.rev convs in\r
- let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) 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 var_names = "@" :: var_names in\r
let div = match div with\r
| Some div -> aux (div :> Num.nf)\r
projects / fireball-separation.git / blobdiff