- pp_proof g ht es c x
-
-and pp_proof g ht es c t =
-(* Printf.eprintf "IN: |- %s\n" (*CicPp.ppcontext c*) (CicPp.ppterm t);
- let g t proof decurry =
- Printf.eprintf "OUT: %b %u |- %s\n" proof decurry (CicPp.ppterm t);
- g t proof decurry
- in *)
-(* let g t proof decurry = add g ht t proof decurry in *)
- match t with
- | C.Cast (t, v) -> pp_cast g ht es c t v
- | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
- | C.LetIn (name, v, t) -> pp_letin g ht es c name v t
- | C.Appl (t :: vs) -> pp_appl g ht es c t vs
- | C.MutCase (u, n, t, v, ws) -> pp_mutcase g ht es c u n t v ws
- | t -> pp_atomic g ht es c t
-
-and pp_term g ht es c t =
- if is_proof c t then pp_proof g ht es c t else g t false 0
+ HLog.warn "Optimizer: remove 3"; opt1_proof g es c x
+
+and opt1_cast g es c t w =
+ let g t = HLog.warn "Optimizer: remove 4"; g t in
+ if es then opt1_proof g es c t else g t
+
+and opt1_other g es c t = g t
+
+and opt1_proof g es c = function
+ | C.LetIn (name, v, t) -> opt1_letin g es c name v t
+ | C.Lambda (name, w, t) -> opt1_lambda g es c name w t
+ | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs)
+ | C.Appl [t] -> opt1_proof g es c t
+ | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws
+ | C.Cast (t, w) -> opt1_cast g es c t w
+ | t -> opt1_other g es c t
+
+and opt1_term g es c t =
+ if is_proof c t then opt1_proof g es c t else g t
+
+(* term preprocessing: optomization 2 ***************************************)
+
+let expanded_premise = "EXPANDED"
+
+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) (comp f (lambda i ty)) (arg i :: a) tl
+ in
+ let n = List.length tys in
+ let absts, args = aux 0 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 t =
+ let entry = Some (name, C.Def (v, None)) in
+ let g t =
+ let g v = g (C.LetIn (name, v, 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, get_type c t) in
+ if vsno < csno then
+ let tys, _ = PEH.split_with_whd (c, get_type 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
+ 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, get_type 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, t) -> opt2_letin g c name v 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 is_proof c t then opt2_proof g c t else g t