-let eta_expand g tys t =
- assert (tys <> []);
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in
- let arg i = C.Rel (succ i) in
- let rec aux i f a = function
- | [] -> f, a
- | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl
- in
- let n = List.length tys in
- let absts, args = aux 0 H.identity [] tys in
- let t = match S.lift n t with
- | C.Appl ts -> C.Appl (ts @ args)
- | t -> C.Appl (t :: args)
- in
- g (absts t)
-
-let rec opt2_letin g c name v w t =
- let entry = Some (name, C.Def (v, w)) in
- let g t =
- let g v = g (C.LetIn (name, v, w, t)) in
- opt2_term g c v
- in
- opt2_proof g (entry :: c) t
-
-and opt2_lambda g c name w t =
- let entry = Some (name, C.Decl w) in
- let g t = g (C.Lambda (name, w, t)) in
- opt2_proof g (entry :: c) t
-
-and opt2_appl g c t vs =
- let g vs =
- let x = C.Appl (t :: vs) in
- let vsno = List.length vs in
- let _, csno = PEH.split_with_whd (c, H.get_type "opt2_appl 1" c t) in
- if vsno < csno then
- let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" c x) in
- let tys = List.rev (List.tl tys) in
- let tys, _ = HEL.split_nth (csno - vsno) tys in
- HLog.warn "Optimizer: eta 1"; eta_expand g tys x
- else g x
- in
- H.list_map_cps g (fun h -> opt2_term h c) vs
-
-and opt2_other g c t =
- let tys, csno = PEH.split_with_whd (c, H.get_type "opt2_other" c t) in
- if csno > 0 then begin
- let tys = List.rev (List.tl tys) in
- HLog.warn "Optimizer: eta 2"; eta_expand g tys t
- end else g t
-
-and opt2_proof g c = function
- | C.LetIn (name, v, w, t) -> opt2_letin g c name v w t
- | C.Lambda (name, w, t) -> opt2_lambda g c name w t
- | C.Appl (t :: vs) -> opt2_appl g c t vs
- | t -> opt2_other g c t
-
-and opt2_term g c t =
- if H.is_proof c t then opt2_proof g c t else g t
-
-(* object preprocessing *****************************************************)