From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 5 Jun 2018 14:59:15 +0200
Subject: Change the proj_ind field from MutInd.t to inductive.

This is a first step towards the acceptance of mutual record types in the
kernel.
---
 kernel/declarations.ml | 2 +-
 kernel/declareops.ml   | 2 +-
 kernel/indtypes.ml     | 2 +-
 kernel/nativecode.ml   | 5 +++--
 kernel/nativelambda.ml | 3 +--
 kernel/typeops.ml      | 2 +-
 6 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd7d6c9c..bb81f7514 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 *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1b73096f7..ad5167d8b 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;
   }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 14f2a3d8f..5b3bca3a0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -839,7 +839,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 = nparamargs;
                       proj_arg = i; proj_type = projty; } in
         (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 8257dc8b8..914168695 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,7 +1986,7 @@ 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
@@ -2052,7 +2053,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/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
       
-- 
cgit v1.2.3