Use projection indices in native compilation rather than constant names.

4 files changed, 14 insertions, 10 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 913c13173..7bd70c050 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -52,7 +52,7 @@ type inline = int option
 type projection_body = {
   proj_ind : MutInd.t;
   proj_npars : int;
-  proj_arg : int;
+  proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
   proj_eta : constr * types; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility with VMs only, the match version *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 5174eeea8..2d4327173 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -53,7 +53,7 @@ type gname =
   | Gind of string * inductive (* prefix, inductive name *)
   | Gconstruct of string * constructor (* prefix, constructor name *)
   | Gconstant of string * Constant.t (* prefix, constant name *)
-  | Gproj of string * Constant.t (* prefix, constant name *)
+  | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
   | Gcase of Label.t option * int
   | Gpred of Label.t option * int
   | Gfixtype of Label.t option * int
@@ -108,7 +108,7 @@ let gname_hash gn = match gn with
 | Ginternal s -> combinesmall 9 (String.hash s)
 | Grel i -> combinesmall 10 (Int.hash i)
 | Gnamed id -> combinesmall 11 (Id.hash id)
-| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p))
+| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i))
 
 let case_ctr = ref (-1)
 
@@ -1070,7 +1070,7 @@ let ml_of_instance instance u =
   | Lconst (prefix, (c, u)) ->
      let args = ml_of_instance env.env_univ u in
      mkMLapp (MLglobal(Gconstant (prefix, c))) args
-  | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c))
+  | Lproj (prefix, ind, i) -> MLglobal(Gproj (prefix, ind, i))
   | Lprim _ ->
       let decl,cond,paux = extract_prim (ml_of_lam env l) t in
       compile_prim decl cond paux
@@ -1544,8 +1544,8 @@ let string_of_gname g =
       Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
   | Gconstant (prefix, c) ->
       Format.sprintf "%sconst_%s" prefix (string_of_con c)
-  | Gproj (prefix, c) ->
-      Format.sprintf "%sproj_%s" prefix (string_of_con c)
+  | Gproj (prefix, (mind, n), i) ->
+      Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i
   | Gcase (l,i) ->
       Format.sprintf "case_%s_%i" (string_of_label_def l) i
   | Gpred (l,i) ->
@@ -1930,7 +1930,8 @@ let compile_constant env sigma prefix ~interactive con cb =
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_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 ("",con) in
+      (** FIXME: handle mutual records *)
+      let gn = Gproj ("", (pb.proj_ind, 0), pb.proj_arg) in
       let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in
       let arg = fargs.(pb.proj_npars) in
         Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index c319be32d..eaad8ee0c 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -31,7 +31,7 @@ and lambda =
   | Llet          of Name.t * lambda * lambda
   | Lapp          of lambda * lambda array
   | Lconst        of prefix * pconstant
-  | Lproj         of prefix * Constant.t (* prefix, projection name *)
+  | Lproj         of prefix * inductive * int (* prefix, inductive, index starting from 0 *)
   | Lprim         of prefix * Constant.t * CPrimitives.t * lambda array
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 6db75c89a..0325a00b4 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -519,8 +519,11 @@ let rec lambda_of_constr env sigma c =
   | Construct _ ->  lambda_of_app env sigma c empty_args
 
   | Proj (p, c) ->
-    let kn = Projection.constant p in
-      mkLapp (Lproj (get_const_prefix !global_env kn, kn)) [|lambda_of_constr env sigma c|]
+    let pb = lookup_projection p !global_env in
+    (** FIXME: handle mutual records *)
+    let ind = (pb.proj_ind, 0) in
+    let prefix = get_mind_prefix !global_env (fst ind) in
+    mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|]
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in