-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 c t) in
- if vsno < csno then
- let tys, _ = PEH.split_with_whd (c, H.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
- 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 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 H.is_proof c t then opt2_proof g c t else g t
-
-(* object preprocessing *****************************************************)
+let wrap g st c bo =
+ try opt_term g st true c bo
+ with
+ | E.Object_not_found uri ->
+ let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in
+ failwith msg
+ | e ->
+ let msg = "optimize_obj: " ^ Printexc.to_string e in
+ failwith msg