| t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
let rec opt_letin g st es c name v w t =
- let name = H.mk_fresh_name c name in
+ let name = H.mk_fresh_name true c name in
let entry = Some (name, C.Def (v, w)) in
let g st t =
if DTI.does_not_occur 1 t then
| v when H.is_proof c v && H.is_atomic v ->
let x = S.subst v t in
opt_proof g (info st "Optimizer: remove 5") true c x
- | v ->
+(* | v when t = C.Rel 1 ->
+ g (info st "Optimizer: remove 6") v
+*) | v ->
g st (C.LetIn (name, v, w, t))
in
if es then opt_term g st es c v else g st v
if es then opt_proof g st es (entry :: c) t else g st t
and opt_lambda g st es c name w t =
- let name = H.mk_fresh_name c name in
+ let name = H.mk_fresh_name true c name in
let entry = Some (name, C.Decl w) in
let g st t = g st (C.Lambda (name, w, t)) in
if es then opt_proof g st es (entry :: c) t else g st t
| C.Constant (name, Some bo, ty, pars, attrs) ->
let count_nodes = I.count_nodes ~meta:false 0 in
let st, c = {info = ""; dummy = ()}, [] in
+ L.time_stamp ("PO: OPTIMIZING " ^ name);
+ let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
+ if !debug then begin
+ Printf.eprintf "BEGIN: %s\n" name;
+ Printf.eprintf "Initial : %s\n" (Pp.ppterm bo);
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
+ end;
let bo, ty = H.cic_bc c bo, H.cic_bc c ty in
let g st bo =
if !debug then begin
L.time_stamp ("PO: DONE " ^ name);
C.Constant (name, Some bo, ty, pars, attrs), st.info
in
- L.time_stamp ("PO: OPTIMIZING " ^ name);
- if !debug then Printf.eprintf "BEGIN: %s\n" name;
- let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
wrap g (info st nodes) c bo
| obj -> obj, ""