| 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
let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in
let csno, vsno = List.length classes, List.length vs in
if csno < vsno then
- let vvs, vs = HEL.split_nth csno vs in
+ let vvs, vs = HEL.split_nth "PO 1" csno vs in
let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
opt_proof g (info st "Optimizer: anticipate 2") true c x
else match conclusion, List.rev vs with
let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in
- let lps, rps = HEL.split_nth lpsno ps in
+ let lps, rps = HEL.split_nth "PO 2" lpsno ps in
let rpsno = List.length rps in
+ if rpsno = 0 && sort_disp = 0 then
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ opt_mutcase_plain g st es c uri tyno outty arg cases
+ else
let predicate = clear_absts rpsno (1 - sort_disp) outty in
let is_recursive t =
I.S.mem tyno (I.get_mutinds_of_uri uri t)
let optimize_obj = function
| C.Constant (name, Some bo, ty, pars, attrs) ->
- let count_nodes = I.count_nodes ~implicit:false 0 in
+ 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, ""