X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=e16828fa7244e5d81d9983b3fab7de4f111d715b;hb=790eccfa6b94dc82826d919691f8d4bfadb04573;hp=fe06207d38b9c99dfdb3e2a7424c63b79e2dae35;hpb=93afc8e27cf27754ff73b426e0b1d4df97224dee;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index fe06207d3..e16828fa7 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -30,6 +30,8 @@ module S = CicSubstitution module DTI = DoubleTypeInference module HEL = HExtlib module PEH = ProofEngineHelpers +module TC = CicTypeChecker +module Un = CicUniv module H = ProceduralHelpers module Cl = ProceduralClassify @@ -38,9 +40,16 @@ module Cl = ProceduralClassify let defined_premise = "DEFINED" -let define v = +let get_type msg c bo = +try + let ty, _ = TC.type_of_aux' [] c bo Un.oblivion_ugraph in + ty +with e -> failwith (msg ^ ": " ^ Printexc.to_string e) + +let define c v = let name = C.Name defined_premise in - C.LetIn (name, v, C.Rel 1) + let ty = get_type "define" c v in + C.LetIn (name, v, ty, C.Rel 1) let clear_absts m = let rec aux k n = function @@ -60,20 +69,26 @@ 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 t = +let rec opt1_letin g es c name v w t = let name = H.mk_fresh_name c name in - let entry = Some (name, C.Def (v, None)) in + let entry = Some (name, C.Def (v, w)) in let g t = if DTI.does_not_occur 1 t then begin let x = S.lift (-1) t in HLog.warn "Optimizer: remove 1"; opt1_proof g true c x end else let g = function - | C.LetIn (nname, vv, tt) when H.is_proof c v -> - let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in + | C.LetIn (nname, vv, ww, tt) when H.is_proof c v -> + let eentry = Some (nname, C.Def (vv, ww)) in + let ttw = get_type "opt1_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 -> - g (C.LetIn (name, v, t)) + | 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)) in if es then opt1_term g es c v else g v in @@ -82,22 +97,20 @@ let rec opt1_letin g es c name v t = and opt1_lambda g es c name w t = let name = H.mk_fresh_name c name in let entry = Some (name, C.Decl w) in - let g t = - let name = if DTI.does_not_occur 1 t then C.Anonymous else name in - g (C.Lambda (name, w, t)) - in + let g t = g (C.Lambda (name, w, t)) in if es then opt1_proof g es (entry :: c) t else g t and opt1_appl g es c t vs = let g vs = let g = function - | C.LetIn (mame, vv, tt) -> + | C.LetIn (mame, vv, tyty, tt) -> let vs = List.map (S.lift 1) vs in - let x = C.LetIn (mame, vv, C.Appl (tt :: 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 | C.Lambda (name, ww, tt) -> let v, vs = List.hd vs, List.tl vs in - let x = C.Appl (C.LetIn (name, v, tt) :: vs) in + let w = get_type "opt1_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 | C.Appl vvs -> let x = C.Appl (vvs @ vs) in @@ -110,7 +123,7 @@ and opt1_appl g es c t vs = | 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 v :: rvs) (vs, cs) + aux true (define c v :: rvs) (vs, cs) end else aux d (v :: rvs) (vs, cs) | _, [] -> assert false @@ -120,24 +133,25 @@ and opt1_appl g es c t vs = let csno, vsno = List.length classes, List.length vs in if csno < vsno then let vvs, vs = HEL.split_nth csno vs in - let x = C.Appl (define (C.Appl (t :: vvs)) :: 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 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 rv]) in + let x = C.Appl (t :: List.rev rvs @ [define c rv]) in HLog.warn "Optimizer: anticipate 3"; opt1_proof g true c x - | Some _, _ -> + | _ (* Some _, _ *) -> g (C.Appl (t :: vs)) - | None, _ -> +(* | None, _ -> aux false [] (vs, classes) - in +*) in let rec aux h prev = function - | C.LetIn (name, vv, tt) :: vs -> + | 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 x = C.LetIn (name, vv, y) in + let ww = get_type "opt1_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 () @@ -184,7 +198,7 @@ and opt1_cast g es c t w = and opt1_other g es c t = g t and opt1_proof g es c = function - | C.LetIn (name, v, t) -> opt1_letin g es c name v t + | 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 @@ -216,10 +230,10 @@ let eta_expand g tys t = in g (absts t) -let rec opt2_letin g c name v t = - let entry = Some (name, C.Def (v, None)) in +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, t)) in + let g v = g (C.LetIn (name, v, w, t)) in opt2_term g c v in opt2_proof g (entry :: c) t @@ -251,10 +265,10 @@ and opt2_other g c t = end else g t and opt2_proof g c = function - | C.LetIn (name, v, t) -> opt2_letin g c name v 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 + | 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 opt2_term g c t = if H.is_proof c t then opt2_proof g c t else g t @@ -263,12 +277,15 @@ and opt2_term g c t = 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\n" (Pp.ppterm bo); + Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" + (Pp.ppterm bo) (I.count_nodes 0 bo); let _ = H.get_type [] (C.Cast (bo, ty)) in C.Constant (name, Some bo, ty, pars, attrs) in - Printf.eprintf "BEGIN: %s\n" name; - begin try opt1_term (opt2_term g []) true [] bo + 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 -> failwith ("PPP: " ^ Printexc.to_string e) end | obj -> obj