X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=776d52645901dbbb316b6caea9ee03a9d9c01637;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=88ad74a661a94c55e86d741464de7592770bfb8e;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 88ad74a66..776d52645 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,10 +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.empty_ugraph in + ty +with e -> failwith (msg ^ ": " ^ Printexc.to_string e) + +let define c v = let name = C.Name defined_premise in - (*CSC: here we need the type of v *) - C.LetIn (name, v, assert false, 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 @@ -61,27 +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 - (*CSC: here we need the type of v *) - let entry = Some (name, C.Def (v, assert false)) 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, tyty, tt) when H.is_proof c v -> - (*CSC: here we need the type of v *) - let x = C.LetIn (nname, vv, tyty, - C.LetIn (name, tt, assert false, 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 -> - (*CSC: here we need the type of v *) - g (C.LetIn (name, v, assert false, t)) + | v -> + g (C.LetIn (name, v, w, t)) in if es then opt1_term g es c v else g v in @@ -102,8 +109,8 @@ and opt1_appl g es c t vs = 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 - (*CSC: here we need the type of v *) - let x = C.Appl (C.LetIn (name, v, assert false, 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 @@ -116,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 @@ -126,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)) @@ -143,8 +150,8 @@ and opt1_appl g es c t vs = 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 - (*CSC: here we need the type of vv *) - let x = C.LetIn (name, vv, assert false, 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 () @@ -191,8 +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 - (*CSC: what to do now that we have also ty? *) - | C.LetIn (name, v, ty, t) -> assert false (*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 @@ -224,12 +230,10 @@ let eta_expand g tys t = in g (absts t) -let rec opt2_letin g c name v t = - (*CSC: here we need the type of v *) - let entry = Some (name, C.Def (v, assert false)) in +let rec opt2_letin g c name v w t = + let entry = Some (name, C.Def (v, w)) in let g t = - (*CSC: here we need the type of v *) - let g v = g (C.LetIn (name, v, assert false, 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 @@ -261,11 +265,10 @@ and opt2_other g c t = end else g t and opt2_proof g c = function - (*CSC: what to do now that we have also ty? *) - | C.LetIn (name, v, ty, t) -> assert false (*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