Merge PR #7679: Clean native compilation of primitive projections

9 files changed, 85 insertions, 65 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..8257dc8b8 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)
 
@@ -152,6 +152,7 @@ type symbol =
   | SymbMeta of metavariable
   | SymbEvar of Evar.t
   | SymbLevel of Univ.Level.t
+  | SymbProj of (inductive * int)
 
 let dummy_symb = SymbValue (dummy_value ())
 
@@ -166,6 +167,7 @@ let eq_symbol sy1 sy2 =
   | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
   | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2
   | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
+  | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2
   | _, _ -> false
 
 let hash_symbol symb =
@@ -179,6 +181,7 @@ let hash_symbol symb =
   | SymbMeta m -> combinesmall 7 m
   | SymbEvar evk -> combinesmall 8 (Evar.hash evk)
   | SymbLevel l -> combinesmall 9 (Univ.Level.hash l)
+  | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k)
 
 module HashedTypeSymbol = struct
   type t = symbol
@@ -241,6 +244,11 @@ let get_level tbl i =
     | SymbLevel u -> u
     | _ -> anomaly (Pp.str "get_level failed.")
 
+let get_proj tbl i =
+  match tbl.(i) with
+    | SymbProj p -> p
+    | _ -> anomaly (Pp.str "get_proj failed.")
+
 let push_symbol x =
   try HashtblSymbol.find symb_tbl x
   with Not_found ->
@@ -885,6 +893,10 @@ let get_level_code i =
   MLapp (MLglobal (Ginternal "get_level"),
     [|MLglobal symbols_tbl_name; MLint i|])
 
+let get_proj_code i =
+  MLapp (MLglobal (Ginternal "get_proj"),
+    [|MLglobal symbols_tbl_name; MLint i|])
+
 type rlist =
   | Rnil 
   | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' 
@@ -1070,7 +1082,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 +1556,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) ->
@@ -1858,8 +1870,6 @@ and compile_named env sigma univ auxdefs id =
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
 let compile_constant env sigma prefix ~interactive con cb =
-  match cb.const_proj with
-  | false ->
      let no_univs =
        match cb.const_universes with
        | Monomorphic_const _ -> true
@@ -1903,39 +1913,6 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  if interactive then LinkedInteractive prefix
 	  else Linked prefix
     end
-  | true ->
-      let pb = lookup_projection (Projection.make con false) env in
-      let mind = pb.proj_ind in
-      let ind = (mind,0) in
-      let mib = lookup_mind mind env in
-      let oib = mib.mind_packets.(0) in
-      let tbl = oib.mind_reloc_tbl in 
-      (* Building info *)
-      let prefix = get_mind_prefix env mind in
-      let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; 
-		 ci_cstr_nargs = [|0|];
-		 ci_cstr_ndecls = [||] (*FIXME*);
-		 ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
-      let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
-		  asw_reloc = tbl; asw_finite = true } in
-      let c_uid = fresh_lname Anonymous in
-      let cf_uid = fresh_lname Anonymous in
-      let _, arity = tbl.(0) in
-      let ci_uid = fresh_lname Anonymous in
-      let cargs = Array.init arity
-        (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None)
-      in
-      let i = push_symbol (SymbConst con) in
-      let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
-      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
-      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
-          arg|])))::
-            [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
 
 module StringOrd = struct type t = string let compare = String.compare end
 module StringSet = Set.Make(StringOrd)
@@ -1962,10 +1939,12 @@ let arg_name = Name (Id.of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
   let u = Declareops.inductive_polymorphic_context mb in
+  (** Generate data for every block *)
   let f i stack ob =
-    let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
-    let j = push_symbol (SymbInd (mind,i)) in
-    let name = Gind ("", (mind, i)) in
+    let ind = (mind, i) in
+    let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in
+    let j = push_symbol (SymbInd ind) in
+    let name = Gind ("", ind) in
     let accu =
       let args =
 	if Int.equal (Univ.AUContext.size u) 0 then
@@ -1979,12 +1958,41 @@ let compile_mind prefix ~interactive mb mind stack =
       Array.init nparams (fun i -> {lname = param_name; luid = i}) in
     let add_construct j acc (_,arity) = 
       let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in 
-      let c = (mind,i), (j+1) in
+      let c = ind, (j+1) in
 	  Glet(Gconstruct ("", c),
 	     mkMLlam (Array.append params args)
 	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
     in
-    Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl
+    let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
+    let add_proj j acc pb =
+      let tbl = ob.mind_reloc_tbl in
+      (* Building info *)
+      let ci = { ci_ind = ind; ci_npar = nparams;
+                 ci_cstr_nargs = [|0|];
+                 ci_cstr_ndecls = [||] (*FIXME*);
+                 ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
+      let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci;
+                  asw_reloc = tbl; asw_finite = true } in
+      let c_uid = fresh_lname Anonymous in
+      let cf_uid = fresh_lname Anonymous in
+      let _, arity = tbl.(0) in
+      let ci_uid = fresh_lname Anonymous in
+      let cargs = Array.init arity
+        (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None)
+      in
+      let i = push_symbol (SymbProj (ind, j)) in
+      let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
+      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
+      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
+    in
+    projs @ constructors @ gtype :: accu :: stack
   in
   Array.fold_left_i f stack mb.mind_packets
 
@@ -2030,13 +2038,9 @@ let compile_deps env sigma prefix ~interactive init t =
     then init
     else
       let comp_stack, (mind_updates, const_updates) =
-	match cb.const_proj, cb.const_body with
-        | false, Def t ->
+        match cb.const_body with
+        | Def t ->
            aux env lvl init (Mod_subst.force_constr t)
-        | true, _ ->
-          let pb = lookup_projection (Projection.make c false) env in
-          let mind = pb.proj_ind in
-          compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
@@ -2047,8 +2051,9 @@ let compile_deps env sigma prefix ~interactive init t =
       comp_stack, (mind_updates, const_updates)
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
-    let term = mkApp (mkConst (Projection.constant p), [|c|]) in
-    aux env lvl init term
+    let pb = lookup_projection p env in
+    let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in
+    aux env lvl init c
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 42f2cbc2e..684983a87 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -50,6 +50,8 @@ val get_evar : symbols -> int -> Evar.t
 
 val get_level : symbols -> int -> Univ.Level.t
 
+val get_proj : symbols -> int -> inductive * int
+
 val get_symbols : unit -> symbols
 
 type code_location_update
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index c07025660..e97dbd0d6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -114,8 +114,8 @@ and conv_atom env pb lvl a1 a2 cu =
        let cu = conv_val env CONV lvl d1 d2 cu in
        let v = mk_rel_accu lvl in
        conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
-    | Aproj(p1,ac1), Aproj(p2,ac2) ->
-       if not (Constant.equal p1 p2) then raise NotConvertible
+    | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) ->
+       if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
        else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
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
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index cfcb0a485..da4413a0a 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -64,7 +64,7 @@ type atom =
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
   | Aevar of Evar.t * t * t array
-  | Aproj of Constant.t * accumulator
+  | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
 
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 4a58a3c7d..649853f06 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -54,7 +54,7 @@ type atom =
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
   | Aevar of Evar.t * t (* type *) * t array (* arguments *)
-  | Aproj of Constant.t * accumulator
+  | Aproj of (inductive * int) * accumulator
 
 (* Constructors *)
 
@@ -71,7 +71,7 @@ val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
 val mk_cofix_accu : int -> t array -> t array -> t
 val mk_meta_accu : metavariable -> t
 val mk_evar_accu : Evar.t -> t -> t array -> t
-val mk_proj_accu : Constant.t -> accumulator -> t
+val mk_proj_accu : (inductive * int) -> accumulator -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
 val mk_const : tag -> t
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 3fce2f3c6..4b8e0e096 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs =
     bs ci in
   Array.init (Array.length tbl) branch
 
+let get_proj env ((mind, _n), i) =
+  let mib = Environ.lookup_mind mind env in
+  match mib.mind_record with
+  | None | Some None ->
+    CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
+  | Some (Some (_, projs, _)) ->
+    Projection.make projs.(i) true
+
 let rec nf_val env sigma v typ =
   match kind_of_value v with
   | Vaccu accu -> nf_accu env sigma accu
@@ -279,9 +287,10 @@ and nf_atom env sigma atom =
       let codom = nf_type env sigma (codom vn) in
       mkProd(n,dom,codom)
   | Ameta (mv,_) -> mkMeta mv
-  | Aproj(p,c) ->
+  | Aproj (p, c) ->
       let c = nf_accu env sigma c in
-	mkProj(Projection.make p true,c)
+      let p = get_proj env p in
+      mkProj(p, c)
   | _ -> fst (nf_atom_type env sigma atom)
 
 and nf_atom_type env sigma atom =
@@ -357,7 +366,8 @@ and nf_atom_type env sigma atom =
   | Aproj(p,c) ->
       let c,tc = nf_accu_type env sigma c in
       let cj = make_judge c tc in
-      let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
+      let p = get_proj env p in
+      let uj = Typeops.judge_of_projection env p cj in
       uj.uj_val, uj.uj_type