Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.

4 files changed, 38 insertions, 35 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cb50245d5a..c87768b190 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2059,6 +2059,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CProj (pr, c) ->
       match intern_reference pr with
       | ConstRef p ->
+        let p = Option.get @@ Recordops.find_primitive_projection p in
         DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
       | _ ->
         raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
diff --git a/interp/declare.ml b/interp/declare.ml
index fcb62ac8c4..0222aeb283 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,40 +382,44 @@ let inInductive : inductive_obj -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = infer_inductive_subtyping }
 
+let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
+  let id = Label.to_id label in
+  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
+  Recordops.declare_primitive_projection p;
+  (* ^ needs to happen before declaring the constant, otherwise
+     Heads gets confused. *)
+  let univs = match univs with
+    | Monomorphic_ind_entry _ ->
+      (** Global constraints already defined through the inductive *)
+      Monomorphic_const_entry Univ.ContextSet.empty
+    | Polymorphic_ind_entry ctx ->
+      Polymorphic_const_entry ctx
+    | Cumulative_ind_entry ctx ->
+      Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+  in
+  let term, types = match univs with
+    | Monomorphic_const_entry _ -> term, types
+    | Polymorphic_const_entry ctx ->
+      let u = Univ.UContext.instance ctx in
+      Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+  in
+  let entry = definition_entry ~types ~univs term in
+  ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent))
+
 let declare_projections univs mind =
   let env = Global.env () in
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
   | PrimRecord info ->
-    let iter i (_, kns, _) =
-      let mind = (mind, i) in
-      let projs = Inductiveops.compute_projections env mind in
-      Array.iter2 (fun kn (term, types) ->
-	let id = Label.to_id (Constant.label kn) in
-        let univs = match univs with
-        | Monomorphic_ind_entry _ ->
-          (** Global constraints already defined through the inductive *)
-          Monomorphic_const_entry Univ.ContextSet.empty
-        | Polymorphic_ind_entry ctx ->
-          Polymorphic_const_entry ctx
-        | Cumulative_ind_entry ctx ->
-          Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
-        in
-        let term, types = match univs with
-        | Monomorphic_const_entry _ -> term, types
-        | Polymorphic_const_entry ctx ->
-          let u = Univ.UContext.instance ctx in
-          Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
-        in
-        let entry = definition_entry ~types ~univs term in
-        let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
-        assert (Constant.equal kn kn')
-      ) kns projs
+    let iter_ind i (_, labs, _) =
+      let ind = (mind, i) in
+      let projs = Inductiveops.compute_projections env ind in
+      Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
     in
-    let () = Array.iteri iter info in
-    true, true
-  | FakeRecord -> true, false
-  | NotRecord -> false, false
+    let () = Array.iteri iter_ind info in
+    true
+  | FakeRecord -> false
+  | NotRecord -> false
 
 (* for initial declaration *)
 let declare_mind mie =
@@ -424,7 +428,7 @@ let declare_mind mie =
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
-  let isrecord,isprim = declare_projections mie.mind_entry_universes mind in
+  let isprim = declare_projections mie.mind_entry_universes mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8aa1e62504..e542b818f6 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -689,8 +689,8 @@ let check_rigidity isrigid =
     user_err  (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let projection_implicits env p impls = 
-  let pb = Environ.lookup_projection p env in
-    CList.skipn_at_least pb.Declarations.proj_npars impls
+  let npars = Projection.npars p in
+  CList.skipn_at_least npars impls
 
 let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ab0bf9c6fe..7cde563cd2 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -641,11 +641,9 @@ let rec subst_notation_constr subst bound raw =
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
   | NProj (p, c) ->
-    let kn = Projection.constant p in
-    let b = Projection.unfolded p in
-    let kn' = subst_constant subst kn in
+    let p' = subst_proj subst p in
     let c' = subst_notation_constr subst bound c in
-    if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c')
+    if p' == p && c' == c then raw else NProj(p', c')
 
 
 let subst_interpretation subst (metas,pat) =