diff options
author | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-30 16:01:18 +0000 |
---|---|---|
committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-30 16:01:18 +0000 |
commit | 7350f5de205ea54e277be1d82cc045788182f82e (patch) | |
tree | ec35cecf8d5d41f5ae9cc1702e05a6d943e05852 /kernel/mod_subst.ml | |
parent | bc96f88c74b487a73bc3312074d114bff63692f4 (diff) |
Memory optimisation for modules and constrs substitutions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9872 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r-- | kernel/mod_subst.ml | 88 |
1 files changed, 71 insertions, 17 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 7cc64af80..a1e15e3c2 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -25,7 +25,7 @@ let apply_opt_resolver resolve kn = match resolve with None -> None | Some resolve -> - try List.assoc kn resolve with Not_found -> assert false + try List.assoc kn resolve with Not_found -> None type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id @@ -110,6 +110,16 @@ let subst_con sub con = None -> con',mkConst con' | Some t -> con',t +let subst_con0 sub con = + let mp,dir,l = repr_con con in + match subst_mp0 sub mp with + None -> None + | Some (mp',resolve) -> + let con' = make_con mp' dir l in + match apply_opt_resolver resolve con with + None -> Some (mkConst con') + | Some t -> Some t + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -119,16 +129,15 @@ let subst_evaluable_reference subst = function | EvalVarRef id -> EvalVarRef id | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn)) -(* -This should be rewritten to prevent duplication of constr's when not -necessary. -For now, it uses map_constr and is rather ineffective -*) + let rec map_kn f f' c = let func = map_kn f f' in match kind_of_term c with - | Const kn -> f' kn + | Const kn -> + (match f' kn with + None -> c + | Some const ->const) | Ind (kn,i) -> (match f kn with None -> c @@ -138,18 +147,63 @@ let rec map_kn f f' c = (match f kn with None -> c | Some kn' -> - mkConstruct ((kn',i),j)) - | Case (ci,p,c,l) -> - let ci' = - { ci with - ci_ind = - let (kn,i) = ci.ci_ind in - match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in - mkCase (ci', func p, func c, array_smartmap func l) - | _ -> map_constr func c + mkConstruct ((kn',i),j)) + | Case (ci,p,ct,l) -> + let ci_ind = + let (kn,i) = ci.ci_ind in + (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in + let p' = func p in + let ct' = func ct in + let l' = array_smartmap func l in + if (ci.ci_ind==ci_ind && p'==p + && l'==l && ct'==ct)then c + else + mkCase ({ci with ci_ind = ci_ind}, + p',ct', l') + | Cast (ct,k,t) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkCast (ct', k, t') + | Prod (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkProd (na, t', ct') + | Lambda (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else mkLambda (na, t', ct') + | LetIn (na,b,t,ct) -> + let ct' = func ct in + let t'= func t in + let b'= func b in + if (t'==t && ct'==ct && b==b') then c + else mkLetIn (na, b', t', ct') + | App (ct,l) -> + let ct' = func ct in + let l' = array_smartmap func l in + if (ct'== ct && l'==l) then c + else mkApp (ct',l') + | Evar (e,l) -> + let l' = array_smartmap func l in + if (l'==l) then c + else mkEvar (e,l') + | Fix (ln,(lna,tl,bl)) -> + let tl' = array_smartmap func tl in + let bl' = array_smartmap func bl in + if (bl == bl'&& tl == tl') then c + else mkFix (ln,(lna,tl',bl')) + | CoFix(ln,(lna,tl,bl)) -> + let tl' = array_smartmap func tl in + let bl' = array_smartmap func bl in + if (bl == bl'&& tl == tl') then c + else mkCoFix (ln,(lna,tl',bl')) + | _ -> c let subst_mps sub = - map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con)) + map_kn (subst_kn0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with |