X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=72cdab58c2a0ea200a33a463c04b315dedfbe866;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=6910613d29b3b2d2bf778b751e1ce0b268339277;hpb=592b7d81b57ec66e0ee007de336e249b07ae0258;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 6910613d2..72cdab58c 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -81,7 +81,7 @@ let rec add_abst k = function | 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 @@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t = | 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 @@ -107,7 +109,7 @@ let rec opt_letin g st es c name v w t = 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 @@ -146,7 +148,7 @@ and opt_appl g st es c t vs = 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 @@ -183,8 +185,12 @@ 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 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) @@ -255,6 +261,14 @@ 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 @@ -268,9 +282,6 @@ let optimize_obj = function 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, ""