-(* 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