X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=72cdab58c2a0ea200a33a463c04b315dedfbe866;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=20e04d322a1ae41c04a4180f54f7a8eba43ea8f2;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 20e04d322..72cdab58c 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -34,13 +34,28 @@ module HEL = HExtlib module PEH = ProofEngineHelpers module TC = CicTypeChecker module Un = CicUniv +module L = Librarian +module Ut = CicUtil module H = ProceduralHelpers module Cl = ProceduralClassify -(* term preprocessing: optomization 1 ***************************************) +(* debugging ****************************************************************) -let defined_premise = "DEFINED" +let debug = ref false + +(* term optimization ********************************************************) + +let critical = ref true + +type status = { + dummy: unit; + info: string +} + +let info st str = {st with info = st.info ^ str ^ "\n"} + +let defined_premise = "LOCAL" let define c v = let name = C.Name defined_premise in @@ -54,9 +69,9 @@ let clear_absts m = | C.Lambda (_, _, t) when n > 0 -> aux 0 (pred n) (S.lift (-1) t) | t when n > 0 -> - Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t); - assert false - | t -> t + Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t); + assert false + | t -> t in aux m @@ -65,105 +80,117 @@ let rec add_abst k = function | t when k > 0 -> assert false | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t) -let rec opt1_letin g es c name v w t = - let name = H.mk_fresh_name c name in +let rec opt_letin g st es c name v w t = + let name = H.mk_fresh_name true c name in let entry = Some (name, C.Def (v, w)) in - let g t = - if DTI.does_not_occur 1 t then begin + let g st t = + if DTI.does_not_occur 1 t then let x = S.lift (-1) t in - HLog.warn "Optimizer: remove 1"; opt1_proof g true c x - end else - let g = function + opt_proof g (info st "Optimizer: remove 1") true c x + else + let g st = function | C.LetIn (nname, vv, ww, tt) when H.is_proof c v -> let eentry = Some (nname, C.Def (vv, ww)) in - let ttw = H.get_type "opt1_letin 1" (eentry :: c) tt in + let ttw = H.get_type "opt_letin 1" (eentry :: c) tt in let x = C.LetIn (nname, vv, ww, - C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in - HLog.warn "Optimizer: swap 1"; opt1_proof g true c x - | v when H.is_proof c v && H.is_atomic v -> + C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) + in + opt_proof g (info st "Optimizer: swap 1") true c x + | v when H.is_proof c v && H.is_atomic v -> let x = S.subst v t in - HLog.warn "Optimizer: remove 5"; opt1_proof g true c x - | v -> - g (C.LetIn (name, v, w, t)) + opt_proof g (info st "Optimizer: remove 5") true c x +(* | 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 opt1_term g es c v else g v + if es then opt_term g st es c v else g st v in - if es then opt1_proof g es (entry :: c) t else g t + if es then opt_proof g st es (entry :: c) t else g st t -and opt1_lambda g es c name w t = - let name = H.mk_fresh_name c name in +and opt_lambda g st es c name w t = + let name = H.mk_fresh_name true c name in let entry = Some (name, C.Decl w) in - let g t = g (C.Lambda (name, w, t)) in - if es then opt1_proof g es (entry :: c) t else g t + 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 -and opt1_appl g es c t vs = - let g vs = - let g = function +and opt_appl g st es c t vs = + let g (st, vs) = + let g st = function | C.LetIn (mame, vv, tyty, tt) -> let vs = List.map (S.lift 1) vs in let x = C.LetIn (mame, vv, tyty, C.Appl (tt :: vs)) in - HLog.warn "Optimizer: swap 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: swap 2") true c x | C.Lambda (name, ww, tt) -> let v, vs = List.hd vs, List.tl vs in - let w = H.get_type "opt1_appl 1" c v in + let w = H.get_type "opt_appl 1" c v in let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in - HLog.warn "Optimizer: remove 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: remove 2") true c x | C.Appl vvs -> let x = C.Appl (vvs @ vs) in - HLog.warn "Optimizer: nested application"; opt1_proof g true c x + opt_proof g (info st "Optimizer: nested application") true c x | t -> - let rec aux d rvs = function +(* + let rec aux st d rvs = function | [], _ -> let x = C.Appl (t :: List.rev rvs) in - if d then opt1_proof g true c x else g x + if d then opt_proof g st true c x else g st x | v :: vs, (cc, bb) :: cs -> - if H.is_not_atomic v && I.S.mem 0 cc && bb then begin - HLog.warn "Optimizer: anticipate 1"; - aux true (define c v :: rvs) (vs, cs) - end else - aux d (v :: rvs) (vs, cs) + if H.is_not_atomic v && I.S.mem 0 cc && bb then + aux (st info "Optimizer: anticipate 1") true + (define c v :: rvs) (vs, cs) + else + aux st d (v :: rvs) (vs, cs) | _, [] -> assert false in - let h () = - let classes, conclusion = Cl.classify c (H.get_type "opt1_appl 3" c t) in +*) + let h st = + 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 - HLog.warn "Optimizer: anticipate 2"; opt1_proof g true c x + opt_proof g (info st "Optimizer: anticipate 2") true c x else match conclusion, List.rev vs with | Some _, rv :: rvs when csno = vsno && H.is_not_atomic rv -> let x = C.Appl (t :: List.rev rvs @ [define c rv]) in - HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x + opt_proof g (info st "Optimizer: anticipate 3";) true c x | _ (* Some _, _ *) -> - g (C.Appl (t :: vs)) + g st (C.Appl (t :: vs)) (* | None, _ -> aux false [] (vs, classes) *) in - let rec aux h prev = function + let rec aux h st prev = function | C.LetIn (name, vv, tyty, tt) :: vs -> let t = S.lift 1 t in let prev = List.map (S.lift 1) prev in let vs = List.map (S.lift 1) vs in let y = C.Appl (t :: List.rev prev @ tt :: vs) in - let ww = H.get_type "opt1_appl 2" c vv in + let ww = H.get_type "opt_appl 2" c vv in let x = C.LetIn (name, vv, ww, y) in - HLog.warn "Optimizer: swap 3"; opt1_proof g true c x - | v :: vs -> aux h (v :: prev) vs - | [] -> h () + opt_proof g (info st "Optimizer: swap 3") true c x + | v :: vs -> aux h st (v :: prev) vs + | [] -> h st in - aux h [] vs + aux h st [] vs in - if es then opt1_proof g es c t else g t + if es then opt_proof g st es c t else g st t + in + let map h v (st, vs) = + let h st vv = h (st, vv :: vs) in opt_term h st es c v in - if es then H.list_map_cps g (fun h -> opt1_term h es c) vs else g vs + if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs) -and opt1_mutcase g 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 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) @@ -185,111 +212,81 @@ and opt1_mutcase g es c uri tyno outty arg cases = 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 - HLog.warn "Optimizer: remove 3"; opt1_proof g es c x - -and opt1_cast g es c t w = - let g t = HLog.warn "Optimizer: remove 4"; g t in - if es then opt1_proof g es c t else g t - -and opt1_other g es c t = g t - -and opt1_proof g es c = function - | C.LetIn (name, v, ty, t) -> opt1_letin g es c name v ty t - | C.Lambda (name, w, t) -> opt1_lambda g es c name w t - | C.Appl (t :: v :: vs) -> opt1_appl g es c t (v :: vs) - | C.Appl [t] -> opt1_proof g es c t - | C.MutCase (u, n, t, v, ws) -> opt1_mutcase g es c u n t v ws - | C.Cast (t, w) -> opt1_cast g es c t w - | t -> opt1_other g es c t + opt_proof g (info st "Optimizer: remove 3") es c x -and opt1_term g es c t = - if H.is_proof c t then opt1_proof g es c t else g t - -(* term preprocessing: optomization 2 ***************************************) - -let expanded_premise = "EXPANDED" - -let eta_expand g tys t = - assert (tys <> []); - let name i = Printf.sprintf "%s%u" expanded_premise i in - let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in - let arg i = C.Rel (succ i) in - let rec aux i f a = function - | [] -> f, a - | (_, ty) :: tl -> aux (succ i) (H.compose f (lambda i ty)) (arg i :: a) tl - in - let n = List.length tys in - let absts, args = aux 0 H.identity [] tys in - let t = match S.lift n t with - | C.Appl ts -> C.Appl (ts @ args) - | t -> C.Appl (t :: args) +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 - g (absts t) + if es then opt_proof g st es c arg else g st arg -let rec opt2_letin g c name v w t = - let entry = Some (name, C.Def (v, w)) in - let g t = - let g v = g (C.LetIn (name, v, w, t)) in - opt2_term g c v - in - opt2_proof g (entry :: c) t +and opt_mutcase g = + if !critical then opt_mutcase_critical g else opt_mutcase_plain g -and opt2_lambda g c name w t = - let entry = Some (name, C.Decl w) in - let g t = g (C.Lambda (name, w, t)) in - opt2_proof g (entry :: c) t +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 -and opt2_appl g c t vs = - let g vs = - let x = C.Appl (t :: vs) in - let vsno = List.length vs in - let _, csno = PEH.split_with_whd (c, H.get_type "opt2_appl 1" c t) in - if vsno < csno then - let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" c x) in - let tys = List.rev (List.tl tys) in - let tys, _ = HEL.split_nth (csno - vsno) tys in - HLog.warn "Optimizer: eta 1"; eta_expand g tys x - else g x - in - H.list_map_cps g (fun h -> opt2_term h c) vs +and opt_other g st es c t = g st t -and opt2_other g c t = - let tys, csno = PEH.split_with_whd (c, H.get_type "opt2_other" c t) in - if csno > 0 then begin - let tys = List.rev (List.tl tys) in - HLog.warn "Optimizer: eta 2"; eta_expand g tys t - end else g t +and opt_proof g st es c = function + | C.LetIn (name, v, ty, t) -> opt_letin g st es c name v ty t + | C.Lambda (name, w, t) -> opt_lambda g st es c name w t + | C.Appl (t :: v :: vs) -> opt_appl g st es c t (v :: vs) + | C.Appl [t] -> opt_proof g st es c t + | C.MutCase (u, n, t, v, ws) -> opt_mutcase g st es c u n t v ws + | C.Cast (t, w) -> opt_cast g st es c t w + | t -> opt_other g st es c t -and opt2_proof g c = function - | C.LetIn (name, v, w, t) -> opt2_letin g c name v w t - | C.Lambda (name, w, t) -> opt2_lambda g c name w t - | C.Appl (t :: vs) -> opt2_appl g c t vs - | t -> opt2_other g c t +and opt_term g st es c t = + if H.is_proof c t then opt_proof g st es c t else g st t -and opt2_term g c t = - if H.is_proof c t then opt2_proof g c t else g t +(* object optimization ******************************************************) -(* object preprocessing *****************************************************) +let wrap g st c bo = + try opt_term g st true c bo + with + | E.Object_not_found uri -> + let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in + failwith msg + | e -> + let msg = "optimize_obj: " ^ Printexc.to_string e in + failwith msg let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> - let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in - let g bo = - Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" - (Pp.ppterm bo) (I.count_nodes 0 bo); - prerr_string "H.pp_term : "; - H.pp_term prerr_string [] [] bo; prerr_newline (); - let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in - 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 "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" (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 - Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" - name (I.count_nodes 0 bo); - begin try opt1_term g (* (opt2_term g []) *) true [] bo with - | E.Object_not_found uri -> - let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in - failwith msg - | e -> - let msg = "optimize_obj: " ^ Printexc.to_string e in - failwith msg - end - | obj -> obj + wrap g (info st nodes) c bo + | obj -> obj, "" + +let optimize_term c bo = + let st = {info = ""; dummy = ()} in + let bo = H.cic_bc c bo in + let g st bo = bo, st.info in + wrap g st c bo