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
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 x = H.refine c (C.Appl args) in
opt_proof g (info st "Optimizer: remove 3") es c x
+and opt_mutcase_plain g st es c uri tyno outty arg cases =
+ let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ g st arg cases
+
+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
if es then opt_proof g st es c t else g st t
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