-(* 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(t, V (v + k))\r
- ) (p, V 0) n in\r
- let p = {p with phase=`Two} in\r
- let t = A(t, delta) in\r
- let t = fold_nat (fun t m -> A(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
+let step var j n p =\r
+ let atsnd f (a,b) = (a, f b) in\r
+ let p, alphas = (* make fresh vars *)\r
+ fold_nat (fun (p, vs) _ ->\r
+ let p, v = freshvar p in\r
+ p, v::vs\r
+ ) (p, []) n in let alphas = List.rev alphas in\r
+ let rec aux lev (inside:bool) = function\r
+ | L t -> L (aux (lev+1) inside t)\r
+ | _ as x ->\r
+ let hd, args = explode x in\r
+ if hd = V (var+lev) then\r
+ (let nargs = List.length args in\r
+ let k = max 0 (j + 1 - nargs) in\r
+ let args = List.mapi\r
+ (fun i (f, t) -> f, lift k (aux lev (if i=j then true else inside) t)) args in\r
+ let bound = fold_nat (fun x n -> (false,V(n-1)) :: x) [] k in\r
+ let args = args @ bound in\r
+ let _, head = List.nth args j in\r
+ let args = List.mapi\r
+ (fun i (f, t) -> (if i=j && not inside then false else f), if i=j && not inside then erase t else t) args in\r
+ let head = (if inside then erase else id) head in\r
+ print_endline ("HEAD: " ^ string_of_t head);\r
+ let alphas = List.map (fun v -> false, V(lev+k+v)) alphas in\r
+ let t = mk_apps head (alphas @ args) in\r
+ let t = mk_lams t k in\r
+ t\r
+ ) else\r
+ (let args = List.map (atsnd (aux lev inside)) args in\r
+ implode hd args) in\r
+ let sigma = (var, aux 0 false (V var)) :: p.sigma in\r
+ {p with tms=List.map (aux 0 false) p.tms; sigma}\r