Using more general information for primitive records.

This brings more compatibility with handling of mutual primitive records
in the kernel.

9 files changed, 55 insertions, 31 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c9362bce6..1d5142a5c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -820,10 +820,12 @@ let drop_parameters depth n argstk =
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
+  let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (_,projs,pbs)) when
+    | PrimRecord infos when
         mib.Declarations.mind_finite == Declarations.BiFinite ->
+      let (_, projs, _) = infos.(snd ind) in
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
@@ -834,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
 					 term = FProj (Projection.make p true, right) }) projs in
 	argss, [Zapp hstack]
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+    | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index bb81f7514..58fb5d66b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -109,13 +109,22 @@ v}
 *)
 
 (** Record information:
-    If the record is not primitive, then None
-    Otherwise, we get:
+    If the type is not a record, then NotRecord
+    If the type is a non-primitive record, then FakeRecord
+    If it is a primitive record, for every type in the block, we get:
     - The identifier for the binder name of the record in primitive projections.
     - The constants associated to each projection.
-    - The checked projection bodies. *)
+    - The checked projection bodies.
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
+    The kernel does not exploit the difference between [NotRecord] and
+    [FakeRecord]. It is mostly used by extraction, and should be extruded from
+    the kernel at some point.
+*)
+
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
 
 type regular_inductive_arity = {
   mind_user_arity : types;
@@ -181,7 +190,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** The record information *)
+    mind_record : record_info; (** The record information *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index ad5167d8b..3e6c4858e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -208,14 +208,21 @@ 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.Smart.map (subst_constant sub) ps in
-  let pb' = Array.Smart.map (subst_const_proj sub) pb in
-    if ps' == ps && pb' == pb then r
+let subst_mind_record sub r = match r with
+| NotRecord -> NotRecord
+| FakeRecord -> FakeRecord
+| PrimRecord infos ->
+  let map (id, ps, pb as info) =
+    let ps' = Array.Smart.map (subst_constant sub) ps in
+    let pb' = Array.Smart.map (subst_const_proj sub) pb in
+    if ps' == ps && 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.Smart.map (Option.Smart.map (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);
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3c555f8c7..724ed9ec7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -49,9 +49,9 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
-  mind_entry_record : (Id.t option) option; 
-  (** Some (Some id): primitive record with id the binder name of the record
-      in projections.
+  mind_entry_record : (Id.t array option) option;
+  (** Some (Some ids): primitive records with ids the binder name of each
+      record in their respective projections. Not used by the kernel.
       Some None: non-primitive record *)
   mind_entry_finite : Declarations.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d6c9117b..0e34a7165 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -515,11 +515,12 @@ let template_polymorphic_pind (ind,u) env =
 let add_mind_key kn (mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_projections = match mind.mind_record with
-    | None | Some None -> env.env_globals.env_projections
-    | Some (Some (id, kns, pbs)) ->
-      Array.fold_left2 (fun projs kn pb ->
-          Cmap_env.add kn pb projs)
-        env.env_globals.env_projections kns pbs
+    | NotRecord | FakeRecord -> env.env_globals.env_projections
+    | PrimRecord projs ->
+      Array.fold_left (fun accu (id, kns, pbs) ->
+      Array.fold_left2 (fun accu kn pb ->
+          Cmap_env.add kn pb accu) accu kns pbs)
+        env.env_globals.env_projections projs
   in
   let new_globals =
     { env.env_globals with
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5b3bca3a0..df22e21ad 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -938,6 +938,8 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
     | Some (Some rid) when pkt.mind_kelim == all_sorts
 			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
+      (** FIXME: adapt to mutual records *)
+      let () = assert (Array.length rid == 1) in
       (** The elimination criterion ensures that all projections can be defined. *)
       let u =
         match aiu with
@@ -949,13 +951,13 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
       let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
-	   let kns, projs = 
+            let kn, projs =
              compute_projections indsp nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
-	   in Some (Some (rid, kns, projs))
-	 with UndefinableExpansion -> Some None)
-    | Some _ -> Some None
-    | None -> None
+           in PrimRecord [|rid.(0), kn, projs|]
+         with UndefinableExpansion -> FakeRecord)
+    | Some _ -> FakeRecord
+    | None -> NotRecord
   in
     (* Build the mutual inductive *)
     { mind_record = isrecord;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 090acdf16..9130b8778 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -293,8 +293,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
 let is_private (mib,_) = mib.mind_private = Some true
 let is_primitive_record (mib,_) = 
   match mib.mind_record with
-  | Some (Some _) -> true
-  | _ -> false
+  | PrimRecord _ -> true
+  | NotRecord | FakeRecord -> false
 
 let build_dependent_inductive ind (_,mip) params =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 914168695..6821fc980 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1990,8 +1990,10 @@ let compile_mind prefix ~interactive mb mind stack =
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
     let projs = match mb.mind_record with
-    | None | Some None -> []
-    | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs
+    | NotRecord | FakeRecord -> []
+    | PrimRecord info ->
+      let _, _, pbs = info.(i) in
+      Array.fold_left_i add_proj [] pbs
     in
     projs @ constructors @ gtype :: accu :: stack
   in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8cf588c3e..13701d489 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,8 +226,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     else error NotEqualInductiveAliases
   end;
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x);
-  if mib1.mind_record <> None then begin
+  (** FIXME: this check looks nonsense *)
+  check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x);
+  if mib1.mind_record <> NotRecord then begin
     let rec names_prod_letin t = match kind t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)