1 files changed, 45 insertions, 33 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3652a1ce..51ec3def 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -21,6 +21,7 @@ let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
   conv_oracle = oracle;
+  share_reduction = true;
 }
 
 (** {6 Arities } *)
@@ -42,7 +43,7 @@ let map_decl_arity f g = function
 
 let hcons_template_arity ar =
   { template_param_levels = ar.template_param_levels;
-      (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
+      (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
     template_level = Univ.hcons_univ ar.template_level }
 
 (** {6 Constants } *)
@@ -70,7 +71,7 @@ let is_opaque cb = match cb.const_body with
 let subst_rel_declaration sub =
   RelDecl.map_constr (subst_mps sub)
 
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub)
 
 let subst_const_type sub arity =
   if is_empty_subst sub then arity
@@ -83,25 +84,18 @@ let subst_const_def sub def = match def with
   | Def c -> Def (subst_constr sub c)
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
-let subst_const_proj sub pb =
-  { pb with proj_ind = subst_mind sub pb.proj_ind;
-    proj_type = subst_mps sub pb.proj_type;
-    proj_body = subst_const_type sub pb.proj_body }
-
 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
-    let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
-      && proj' == cb.const_proj then cb
+    then cb
     else
       { const_hyps = [];
         const_body = body';
         const_type = type';
-        const_proj = proj';
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
@@ -117,7 +111,7 @@ let subst_const_body sub cb =
 let hcons_rel_decl =
   RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons
 
-let hcons_rel_context l = List.smartmap hcons_rel_decl l
+let hcons_rel_context l = List.Smart.map hcons_rel_decl l
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
@@ -178,7 +172,7 @@ let recarg_length p j =
   let (_,cstrs) = Rtree.dest_node p in
   Array.length (snd (Rtree.dest_node cstrs.(j-1)))
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 (** {7 Substitution of inductive declarations } *)
 
@@ -198,10 +192,10 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
@@ -210,14 +204,20 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
-let subst_mind_record sub (id, ps, pb as r) =
-  let ps' = Array.smartmap (subst_constant sub) ps in
-  let pb' = Array.smartmap (subst_const_proj sub) pb in
-    if ps' == ps && pb' == pb then r
-    else (id, ps', pb')
+let subst_mind_record sub r = match r with
+| NotRecord -> NotRecord
+| FakeRecord -> FakeRecord
+| PrimRecord infos ->
+  let map (id, ps, pb as info) =
+    let pb' = Array.Smart.map (subst_mps sub) pb in
+    if pb' == pb then info
+    else (id, ps, pb')
+  in
+  let infos' = Array.Smart.map map infos in
+  if infos' == infos then r else PrimRecord infos'
 
 let subst_mind_body sub mib =
-  { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ;
+  { mind_record = subst_mind_record sub mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
@@ -225,7 +225,7 @@ let subst_mind_body sub mib =
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
@@ -249,6 +249,25 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
+let inductive_make_projection ind mib ~proj_arg =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    Some (Names.Projection.Repr.make ind
+            ~proj_npars:mib.mind_nparams
+            ~proj_arg
+            (pi2 infos.(snd ind)).(proj_arg))
+
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (** {6 Hash-consing of inductive declarations } *)
 
 let hcons_regular_ind_arity a =
@@ -263,15 +282,15 @@ let hcons_ind_arity =
 (** Substitution of inductive declarations *)
 
 let hcons_mind_packet oib =
-  let user = Array.smartmap Constr.hcons oib.mind_user_lc in
-  let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in
+  let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
+  let nf = Array.Smart.map Constr.hcons 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_ind_arity oib.mind_arity;
-    mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+    mind_consnames = Array.Smart.map Names.Id.hcons oib.mind_consnames;
     mind_user_lc = user;
     mind_nf_lc = nf }
 
@@ -283,17 +302,10 @@ let hcons_mind_universes miu =
 
 let hcons_mind mib =
   { mib with
-    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
+    mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
-(** {6 Stm machinery } *)
-
-let string_of_side_effect { Entries.eff } = match eff with
-  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")"
-  | Entries.SEscheme (cl,_) ->
-      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")"
-
 (** Hashconsing of modules *)
 
 let hcons_functorize hty he hself f = match f with
@@ -331,7 +343,7 @@ and hcons_structure_body sb =
     let sfb' = hcons_structure_field_body sfb in
     if l == l' && sfb == sfb' then fb else (l', sfb')
   in
-  List.smartmap map sb
+  List.Smart.map map sb
 
 and hcons_module_signature ms =
   hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms