Declareops + Modops : more clever substitutions

 We try harder to preserve pointer equality when substituting.
 This will probably have little effect (for instance the
 constr_substituted are anyway _never_ substituted in place),
 but it cannot harm.

 Two particular cases:
 - we try to share (and maintain shared) mind_user_lc and mind_nf_lc
 - we try to share (and maintain shared) mod_expr and mod_type

 TODO: check that native compiler is still ok, since we might have
 less (ref NotLinked) now. Having references in constant_body and co
 is anyway a Very Bad Idea (TM).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 112 insertions, 76 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 76d9876c49..da945b67b7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -14,7 +14,7 @@ open Util
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
-(** Constants *)
+(** {6 Constants } *)
 
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
@@ -29,40 +29,54 @@ let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Undef _ | Def _ -> false
 
-(** Constant substitutions *)
+(** {7 Constant substitutions } *)
 
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
-  if copt == copt' & t == t' then x else (id,copt',t')
+  if copt == copt' && t == t' then x else (id,copt',t')
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-(* TODO: these substitution functions could avoid duplicating things
-   when the substitution have preserved all the fields *)
+let subst_const_type sub arity = match arity with
+  | NonPolymorphicType s ->
+    let s' = subst_mps sub s in
+    if s==s' then arity else NonPolymorphicType s'
+  | PolymorphicArity (ctx,s) ->
+    let ctx' = subst_rel_context sub ctx in
+    if ctx==ctx' then arity else PolymorphicArity (ctx',s)
 
-let subst_const_type sub arity =
-  if is_empty_subst sub then arity
-  else match arity with
-    | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
-    | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+(** No need here to check for physical equality after substitution,
+    at least for Def due to the delayed substitution [subst_constr_subst]. *)
 
-let subst_const_def sub = function
-  | Undef inl -> Undef inl
+let subst_const_def sub def = match def with
+  | Undef _ -> def
   | Def c -> Def (subst_constr_subst sub c)
   | OpaqueDef lc ->
-      OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
-
-let subst_const_body sub cb = {
-  const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
-  const_body = subst_const_def sub cb.const_body;
-  const_type = subst_const_type sub cb.const_type;
-  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
-  const_constraints = cb.const_constraints;
-  const_native_name = ref NotLinked;
-  const_inline_code = cb.const_inline_code }
-
-(** Hash-consing of constants *)
+    OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+
+let subst_const_body sub cb =
+  assert (List.is_empty cb.const_hyps); (* we're outside sections *)
+  if is_empty_subst sub then cb
+  else
+    let body' = subst_const_def sub cb.const_body in
+    let type' = subst_const_type sub cb.const_type in
+    if body' == cb.const_body && type' == cb.const_type then cb
+    else
+      { const_hyps = [];
+        const_body = body';
+        const_type = type';
+        const_body_code =
+          Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+        const_constraints = cb.const_constraints;
+        const_native_name = ref NotLinked;
+        const_inline_code = cb.const_inline_code }
+
+(** {7 Hash-consing of constants } *)
+
+(** This hash-consing is currently quite partial : we only
+    share internal fields (e.g. constr), and not the records
+    themselves. But would it really bring substantial gains ? *)
 
 let hcons_rel_decl ((n,oc,t) as d) =
   let n' = Names.Name.hcons n
@@ -103,7 +117,7 @@ let hcons_const_body cb =
           (Univ.hcons_constraints (Future.force cb.const_constraints))
       else cb.const_constraints }
 
-(** Inductive types *)
+(** {6 Inductive types } *)
 
 let eq_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> true
@@ -113,10 +127,12 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let subst_recarg sub r = match r with
   | Norec -> r
-  | Mrec (kn,i) -> let kn' = subst_ind sub kn in
-      if kn==kn' then r else Mrec (kn',i)
-  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
-      if kn==kn' then r else Imbr (kn',i)
+  | Mrec (kn,i) ->
+    let kn' = subst_ind sub kn in
+    if kn==kn' then r else Mrec (kn',i)
+  | Imbr (kn,i) ->
+    let kn' = subst_ind sub kn in
+    if kn==kn' then r else Imbr (kn',i)
 
 let mk_norec = Rtree.mk_node Norec [||]
 
@@ -142,61 +158,79 @@ let recarg_length p j =
 
 let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
 
-(** Substitution of inductive declarations *)
-
-let subst_indarity sub = function
-| Monomorphic s ->
-    Monomorphic {
-      mind_user_arity = subst_mps sub s.mind_user_arity;
-      mind_sort = s.mind_sort;
-    }
-| Polymorphic s as x -> x
-
-let subst_mind_packet sub mbp =
-  { mind_consnames = mbp.mind_consnames;
-    mind_consnrealdecls = mbp.mind_consnrealdecls;
-    mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
-    mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
-    mind_arity = subst_indarity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
-    mind_nrealargs = mbp.mind_nrealargs;
-    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
-    mind_kelim = mbp.mind_kelim;
-    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
-    mind_nb_constant = mbp.mind_nb_constant;
-    mind_nb_args = mbp.mind_nb_args;
-    mind_reloc_tbl = mbp.mind_reloc_tbl }
+(** {7 Substitution of inductive declarations } *)
+
+let subst_indarity sub ar = match ar with
+  | Monomorphic s ->
+    let uar' = subst_mps sub s.mind_user_arity in
+    if uar' == s.mind_user_arity then ar
+    else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort }
+  | Polymorphic _ -> ar
+
+let subst_mind_packet sub mip =
+  let { mind_nf_lc = nf;
+        mind_user_lc = user;
+        mind_arity_ctxt = ctxt;
+        mind_arity = ar;
+        mind_recargs = ra } = mip
+  in
+  let nf' = Array.smartmap (subst_mps sub) nf in
+  let user' =
+    (* maintain sharing of [mind_user_lc] and [mind_nf_lc] *)
+    if user==nf then nf'
+    else Array.smartmap (subst_mps sub) user
+  in
+  let ctxt' = subst_rel_context sub ctxt in
+  let ar' = subst_indarity sub ar in
+  let ra' = subst_wf_paths sub ra in
+  if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra'
+  then mip
+  else
+    { mip with
+      mind_nf_lc = nf';
+      mind_user_lc = user';
+      mind_arity_ctxt = ctxt';
+      mind_arity = ar';
+      mind_recargs = ra' }
 
 let subst_mind sub mib =
-  { mind_record = mib.mind_record ;
-    mind_finite = mib.mind_finite ;
-    mind_ntypes = mib.mind_ntypes ;
-    mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
-    mind_nparams = mib.mind_nparams;
-    mind_nparams_rec = mib.mind_nparams_rec;
-    mind_params_ctxt =
-      Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_constraints = mib.mind_constraints;
-    mind_native_name = ref NotLinked }
-
-(** Hash-consing of inductive declarations *)
+  assert (List.is_empty mib.mind_hyps); (* we're outside sections *)
+  if is_empty_subst sub then mib
+  else
+    let params = mib.mind_params_ctxt in
+    let params' = Context.map_rel_context (subst_mps sub) params in
+    let packets = mib.mind_packets in
+    let packets' = Array.smartmap (subst_mind_packet sub) packets in
+    if params==params' && packets==packets' then mib
+    else
+      { mib with
+        mind_params_ctxt = params';
+        mind_packets = packets';
+        mind_native_name = ref NotLinked }
+
+(** {6 Hash-consing of inductive declarations } *)
+
+(** Just as for constants, this hash-consing is quite partial *)
 
 let hcons_indarity = function
   | Monomorphic a ->
-    Monomorphic { mind_user_arity = Term.hcons_constr a.mind_user_arity;
-		  mind_sort = Term.hcons_sorts a.mind_sort }
+    Monomorphic
+      { mind_user_arity = Term.hcons_constr a.mind_user_arity;
+        mind_sort = Term.hcons_sorts a.mind_sort }
   | Polymorphic a -> Polymorphic (hcons_polyarity a)
 
 let hcons_mind_packet oib =
- { oib with
-   mind_typename = Names.Id.hcons oib.mind_typename;
-   mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
-   mind_arity = hcons_indarity oib.mind_arity;
-   mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
-   mind_user_lc = Array.smartmap Term.hcons_types oib.mind_user_lc;
-   mind_nf_lc = Array.smartmap Term.hcons_types oib.mind_nf_lc }
+  let user = Array.smartmap Term.hcons_types oib.mind_user_lc in
+  let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in
+  (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
+  let nf = if Array.equal (==) user nf then user else nf in
+  { oib with
+    mind_typename = Names.Id.hcons oib.mind_typename;
+    mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
+    mind_arity = hcons_indarity oib.mind_arity;
+    mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+    mind_user_lc = user;
+    mind_nf_lc = nf }
 
 let hcons_mind mib =
   { mib with
@@ -204,6 +238,8 @@ let hcons_mind mib =
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_constraints = Univ.hcons_constraints mib.mind_constraints }
 
+(** {6 Stm machinery } *)
+
 let join_constant_body cb =
   ignore(Future.join cb.const_constraints);
   match cb.const_body with