Merge PR #7750: Handle mutual records in the kernel

12 files changed, 93 insertions, 68 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 7bd7d6c9c..58fb5d66b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,7 +50,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : MutInd.t;
+  proj_ind : inductive;
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
@@ -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 1b73096f7..3e6c4858e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,7 +84,7 @@ let subst_const_def sub def = match def with
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
 let subst_const_proj sub pb =
-  { pb with proj_ind = subst_mind sub pb.proj_ind;
+  { pb with proj_ind = subst_ind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
   }
 
@@ -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 14f2a3d8f..e63f43849 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,15 +797,23 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u) nparamargs params
-    mind_consnrealdecls mind_consnrealargs paramslet ctx =
+let compute_projections (kn, i as ind) mib =
+  let pkt = mib.mind_packets.(i) in
+  let u = match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Instance.empty
+  | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+  | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
+  in
+  let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
+  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
   let paramsletsubst =
     (* [Ind inst] is typed in context [params-wo-let] *)
-    let inst' = rel_list 0 nparamargs in
+    let inst' = rel_list 0 mib.mind_nparams in
     (* {params-wo-let |- subst:params] *)
     let subst = subst_of_rel_context_instance paramslet inst' in
     (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
@@ -839,7 +847,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let body = { proj_ind = fst ind; proj_npars = nparamargs;
+        let body = { proj_ind = ind; proj_npars = mib.mind_nparams;
                       proj_arg = i; proj_type = projty; } in
         (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
@@ -932,33 +940,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in
-  let isrecord = 
-    match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts
-			   && Array.length pkt.mind_consnames == 1
-			   && pkt.mind_consnrealargs.(0) > 0 ->
-      (** The elimination criterion ensures that all projections can be defined. *)
-      let u =
-        match aiu with
-        | Monomorphic_ind _ -> Univ.Instance.empty
-        | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
-        | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
-      in
-      let indsp = ((kn, 0), u) in
-      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 = 
-             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
-    (* Build the mutual inductive *)
-    { mind_record = isrecord;
+  let mib =
+      (* Build the mutual inductive *)
+    { mind_record = NotRecord;
       mind_ntypes = ntypes;
       mind_finite = isfinite;
       mind_hyps = hyps;
@@ -970,6 +954,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
+  in
+  let record_info = match isrecord with
+  | Some (Some rid) ->
+    let is_record pkt =
+      pkt.mind_kelim == all_sorts
+      && Array.length pkt.mind_consnames == 1
+      && pkt.mind_consnrealargs.(0) > 0
+    in
+    (** The elimination criterion ensures that all projections can be defined. *)
+    if Array.for_all is_record packets then
+      let map i id =
+        let kn, projs = compute_projections (kn, i) mib in
+        (id, kn, projs)
+      in
+      try PrimRecord (Array.mapi map rid)
+      with UndefinableExpansion -> FakeRecord
+    else FakeRecord
+  | Some None -> FakeRecord
+  | None -> NotRecord
+  in
+  { mib with mind_record = record_info }
 
 (************************************************************************)
 (************************************************************************)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 45228e35e..7c36dac67 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,5 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive ->
-  int -> Context.Rel.t -> int array -> int array -> 
-  Context.Rel.t -> Context.Rel.t -> 
-  (Constant.t array * projection_body array)
+val compute_projections : inductive ->
+  mutual_inductive_body -> (Constant.t array * projection_body array)
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 8257dc8b8..6821fc980 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1965,6 +1965,7 @@ let compile_mind prefix ~interactive mb mind stack =
     in
     let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
     let add_proj j acc pb =
+      let () = assert (eq_ind ind pb.proj_ind) in
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
@@ -1985,12 +1986,14 @@ let compile_mind prefix ~interactive mb mind stack =
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
       let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
-      let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in
+      let gn = Gproj ("", ind, pb.proj_arg) in
       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
@@ -2052,7 +2055,7 @@ let compile_deps env sigma prefix ~interactive init t =
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let pb = lookup_projection p env in
-    let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in
+    let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in
     aux env lvl init c
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 0325a00b4..a809e1b18 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -520,8 +520,7 @@ let rec lambda_of_constr env sigma c =
 
   | Proj (p, c) ->
     let pb = lookup_projection p !global_env in
-    (** FIXME: handle mutual records *)
-    let ind = (pb.proj_ind, 0) in
+    let ind = pb.proj_ind in
     let prefix = get_mind_prefix !global_env (fst ind) in
     mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|]
 
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)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 325d5cecd..34ed2afb2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -301,7 +301,7 @@ let type_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(MutInd.equal pb.proj_ind (fst ind));
+  assert(eq_ind pb.proj_ind ind);
   let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
   substl (c :: CList.rev args) ty