X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=e16828fa7244e5d81d9983b3fab7de4f111d715b;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=1953ae7f1b6a5c385fcdbb6aad65b76740a15a28;hpb=fdeb64c7f9e870d43a4eb87153bf72e6f5705f01;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 1953ae7f1..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,23 +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 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, t)) + | v -> + g (C.LetIn (name, v, w, t)) in if es then opt1_term g es c v else g v in @@ -91,13 +103,14 @@ and opt1_lambda g es c name w 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,11 +133,11 @@ 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 _, _ *) -> g (C.Appl (t :: vs)) @@ -132,12 +145,13 @@ and opt1_appl g es c t vs = aux false [] (vs, classes) *) 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