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

2 files changed, 86 insertions, 36 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 7cc64af808..a1e15e3c25 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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3e89112ae3..8770afe131 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -266,26 +266,22 @@ and constants_of_modtype env mp modtype =
 (* returns a resolver for kn that maps mbid to mp *)
 let resolver_of_environment mbid modtype mp env =
  let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = 
-   List.map
-     (fun (con,expecteddef) ->
-	let con' = replace_mp_in_con (MPbound mbid) mp con in
-	let constr =
-	  try
-	    if expecteddef.Declarations.const_inline then
-              let constant = lookup_constant con' env in
-		if constant.Declarations.const_opaque then
-		  None
-		else
-		  option_map Declarations.force
-		    constant.Declarations.const_body
-	    else
-              None
-	  with Not_found -> error_no_such_label (con_label con')
-	in
-	  con,constr
-     ) constants
+ let rec make_resolve = function
+   | [] -> []
+   | (con,expecteddef)::r ->
+       let con' = replace_mp_in_con (MPbound mbid) mp con in
+	 try
+	   if expecteddef.Declarations.const_inline then
+	     let constant = lookup_constant con' env in
+	     if (not constant.Declarations.const_opaque) then
+	       let constr = option_map Declarations.force
+		 constant.Declarations.const_body in
+		 (con,constr)::(make_resolve r)
+	     else make_resolve r
+	   else make_resolve r
+	 with Not_found -> error_no_such_label (con_label con')
  in
+ let resolve = make_resolve constants in
    Mod_subst.make_resolver resolve
 
 let strengthen_const env mp l cb =