aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-30 18:48:11 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-30 18:53:32 +0200
commit437b91a3ffd7327975a129b95b24d3f66ad7f3e4 (patch)
tree3e5b4098318c4bbad4024d072c5008825e78c1c9 /library
parentdac4d8952c5fc234f5b6245e39a73c2ca07555ee (diff)
Simplify even further the declaration of primitive projections,
now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml16
-rw-r--r--library/global.ml6
2 files changed, 18 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml
index a18a6a60b..6f0ead941 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -199,7 +199,6 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
{ const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
const_entry_type = types;
- const_entry_proj = None;
const_entry_polymorphic = poly;
const_entry_universes = univs;
const_entry_opaque = opaque;
@@ -244,7 +243,6 @@ let declare_sideff env fix_exn se =
const_entry_feedback = None;
const_entry_polymorphic = cb.const_polymorphic;
const_entry_universes = univs;
- const_entry_proj = None;
});
cst_hyps = [] ;
cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition;
@@ -391,6 +389,19 @@ let inInductive : inductive_obj -> obj =
subst_function = ident_subst_function;
discharge_function = discharge_inductive }
+let declare_projections mind =
+ let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
+ match spec.mind_record with
+ | Some (kns, pjs) ->
+ Array.iteri (fun i kn ->
+ let id = Label.to_id (Constant.label kn) in
+ let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
+ let kn' = declare_constant id (ProjectionEntry entry,
+ IsDefinition StructureComponent)
+ in
+ assert(eq_constant kn kn')) kns
+ | None -> ()
+
(* for initial declaration *)
let declare_mind isrecord mie =
let id = match mie.mind_entry_inds with
@@ -398,6 +409,7 @@ let declare_mind isrecord mie =
| [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
+ declare_projections mind;
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
diff --git a/library/global.ml b/library/global.ml
index 65e895dfd..adfb7cafe 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -152,7 +152,9 @@ let type_of_global_unsafe r =
| VarRef id -> Environ.named_type id env
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- Typeops.type_of_constant_type env cb.Declarations.const_type
+ let univs = Declareops.universes_of_polymorphic_constant cb in
+ let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in
+ Vars.subst_instance_constr (Univ.UContext.instance univs) ty
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
let inst =
@@ -195,7 +197,7 @@ let universes_of_global env r =
| VarRef id -> Univ.UContext.empty
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- Declareops.universes_of_constant cb
+ Declareops.universes_of_polymorphic_constant cb
| IndRef ind ->
let (mib, oib) = Inductive.lookup_mind_specif env ind in
Univ.instantiate_univ_context mib.mind_universes