aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-01 17:30:14 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-05 14:20:11 +0200
commite1e7888ac4519f4b7470cc8469f9fd924514e352 (patch)
treeaa6afb40e01d5c51593f1b17dc9a81b5b75c54fb
parentd8d3e9cea631d253a30dc42760d7bdde72e01c60 (diff)
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.
-rw-r--r--kernel/nativecode.ml102
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/nativevalues.ml2
-rw-r--r--kernel/nativevalues.mli4
-rw-r--r--pretyping/nativenorm.ml16
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