module TC = CicTypeChecker
module Un = CicUniv
module L = Librarian
+module Ut = CicUtil
module H = ProceduralHelpers
module Cl = ProceduralClassify
(* term optimization ********************************************************)
+let critical = ref true
+
type status = {
dummy: unit;
info: string
aux 0 (pred n) (S.lift (-1) t)
| t when n > 0 ->
Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
- assert false
- | t -> t
+ assert false
+ | t -> t
in
aux m
| 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
in
if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs)
-and opt_mutcase g st es c uri tyno outty arg cases =
+and opt_mutcase_critical g st es c uri tyno outty arg cases =
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 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
+ if H.occurs c ~what:(C.Rel 0) ~where:predicate 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 is_recursive t =
I.S.mem tyno (I.get_mutinds_of_uri uri t)
in
in
let lifted_cases = List.map2 map2 cases constructors in
let args = eliminator :: lps @ predicate :: lifted_cases @ rps @ [arg] in
- let x = H.refine c (C.Appl args) in
- opt_proof g (info st "Optimizer: remove 3") es c x
+ try
+ let x = H.refine c (C.Appl args) in
+ opt_proof g (info st "Optimizer: remove 3") es c x
+ with e ->
+(* FG: the transformation is not possible, we fall back into the plain case *)
+ let st = info st ("Optimizer: refine_error: " ^ Printexc.to_string e) in
+ opt_mutcase_plain g st es c uri tyno outty arg cases
+
+and opt_mutcase_plain g st es c uri tyno outty arg cases =
+ let g st v =
+ let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ let map h v (st, vs) =
+ let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+ in
+ if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+ in
+ if es then opt_proof g st es c arg else g st arg
+
+and opt_mutcase g =
+ if !critical then opt_mutcase_critical g else opt_mutcase_plain g
and opt_cast g st es c t w =
let g st t = g (info st "Optimizer: remove 4") t in
let optimize_obj = function
| 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
Printf.eprintf "Optimized : %s\n" (Pp.ppterm bo);
- prerr_string "H.pp_term : ";
- H.pp_term prerr_string [] c bo; prerr_newline ()
+ prerr_string "Ut.pp_term : ";
+ Ut.pp_term prerr_string [] c bo; prerr_newline ()
end;
(* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
- let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in
+ let nodes = Printf.sprintf "Optimized nodes: %u" (count_nodes bo) in
let st = info st nodes in
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" (I.count_nodes 0 bo) in
wrap g (info st nodes) c bo
| obj -> obj, ""