aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/nativecode.ml13
-rw-r--r--kernel/nativeinstr.mli2
-rw-r--r--kernel/nativelambda.ml7
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