More straightforward native compilation of primitive projections.

Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.

6 files changed, 73 insertions, 57 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2d4327173..8257dc8b8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -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' 
@@ -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,40 +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
-      (** 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
-          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)
@@ -1963,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
@@ -1980,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
 
@@ -2031,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 =
@@ -2048,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/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 978ceed1e..7666ce0eb 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