aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/entries.mli8
-rw-r--r--kernel/indtypes.ml6
-rw-r--r--kernel/term_typing.ml48
-rw-r--r--kernel/univ.ml5
-rw-r--r--kernel/univ.mli1
-rw-r--r--library/declare.ml16
-rw-r--r--library/global.ml6
-rw-r--r--printing/printer.ml4
-rw-r--r--proofs/proof_global.ml3
-rw-r--r--test-suite/success/primitiveproj.v30
-rw-r--r--toplevel/command.ml1
-rw-r--r--toplevel/ind_tables.ml1
-rw-r--r--toplevel/indschemes.ml1
-rw-r--r--toplevel/obligations.ml1
-rw-r--r--toplevel/record.ml107
15 files changed, 139 insertions, 99 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 0a06eef16..2d7b7bb0f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -57,14 +57,13 @@ type const_entry_body = proof_output Future.computation
type definition_entry = {
const_entry_body : const_entry_body;
- (* List of sectoin variables *)
+ (* List of section variables *)
const_entry_secctx : Context.section_context option;
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
const_entry_polymorphic : bool;
const_entry_universes : Univ.universe_context;
- const_entry_proj : (mutual_inductive * int) option;
const_entry_opaque : bool;
const_entry_inline_code : bool }
@@ -73,9 +72,14 @@ type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
Context.section_context option * bool * types Univ.in_universe_context * inline
+type projection_entry = {
+ proj_entry_ind : mutual_inductive;
+ proj_entry_arg : int }
+
type constant_entry =
| DefinitionEntry of definition_entry
| ParameterEntry of parameter_entry
+ | ProjectionEntry of projection_entry
(** {6 Modules } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 7ae787d22..759d71206 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -782,7 +782,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
| Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
(** The elimination criterion ensures that all projections can be defined. *)
let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
- let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in
+ let u =
+ if p then
+ subst_univs_level_instance subst (Univ.UContext.instance ctx)
+ else Univ.Instance.empty
+ in
(try
let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b603610ce..a3c4d9849 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -122,6 +122,7 @@ let infer_declaration env kn dcl =
let c = Typeops.assumption_of_judgment env j in
let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
Undef nl, RegularArity t, None, poly, univs, false, ctx
+
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_polymorphic = false} as c) ->
@@ -143,6 +144,7 @@ let infer_declaration env kn dcl =
def, RegularArity typ, None, c.const_entry_polymorphic,
c.const_entry_universes,
c.const_entry_inline_code, c.const_entry_secctx
+
| DefinitionEntry c ->
let env = push_context c.const_entry_universes env in
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
@@ -152,35 +154,31 @@ let infer_declaration env kn dcl =
let body = handle_side_effects env body side_eff in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
- let def, typ, proj =
- match c.const_entry_proj with
- | Some (ind, i) -> (* Bind c to a checked primitive projection *)
- let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
- let kn, pb =
- match mib.mind_record with
- | Some (kns, pbs) ->
- if i < Array.length pbs then
- kns.(i), pbs.(i)
- else assert false
- | None -> assert false
- in
- let term = Vars.subst_univs_level_constr usubst (fst pb.proj_eta) in
- let typ = Vars.subst_univs_level_constr usubst (snd pb.proj_eta) in
- Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb
- | None ->
- let j = infer env body in
- let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
- let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
- let def =
- if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
- else Def (Mod_subst.from_val def)
- in
- def, typ, None
+ let j = infer env body in
+ let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+ let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
+ let def =
+ if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+ else Def (Mod_subst.from_val def)
in
feedback_completion_typecheck feedback_id;
- def, typ, proj, c.const_entry_polymorphic,
+ def, typ, None, c.const_entry_polymorphic,
univs, c.const_entry_inline_code, c.const_entry_secctx
+ | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
+ let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
+ let kn, pb =
+ match mib.mind_record with
+ | Some (kns, pbs) ->
+ if i < Array.length pbs then
+ kns.(i), pbs.(i)
+ else assert false
+ | None -> assert false
+ in
+ let term, typ = pb.proj_eta in
+ Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
+ mib.mind_polymorphic, mib.mind_universes, false, None
+
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
| TemplateArity (ctx,_) ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index fbdb5bb0d..b2f251283 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1937,6 +1937,11 @@ let subst_univs_level_universe subst u =
let u' = Universe.smartmap f u in
if u == u' then u
else Universe.sort u'
+
+let subst_univs_level_instance subst i =
+ let i' = Instance.subst_fn (subst_univs_level_level subst) i in
+ if i == i' then i
+ else i'
let subst_univs_level_constraint subst (u,d,v) =
let u' = subst_univs_level_level subst u
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c9b7547f2..7c0c9536f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -374,6 +374,7 @@ val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
val subst_univs_level_universe : universe_level_subst -> universe -> universe
val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
(** Level to universe substitutions. *)
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
diff --git a/printing/printer.ml b/printing/printer.ml
index 55a7d36a3..ed872afc6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -778,7 +778,7 @@ let print_mutual_inductive env mind mib =
str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
prlist_with_sep (fun () -> fnl () ++ str" with ")
(print_one_inductive env mib) inds ++
- pr_universe_ctx mib.mind_universes)
+ pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
let get_fields =
let rec prodec_rec l subst c =
@@ -820,7 +820,7 @@ let print_record env mind mib =
(fun (id,b,c) ->
pr_id id ++ str (if b then " : " else " := ") ++
pr_lconstr_env envpar c) fields) ++ str" }" ++
- pr_universe_ctx mib.mind_universes)
+ pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
let pr_mutual_inductive_body env mind mib =
if mib.mind_record <> None && not !Flags.raw_print then
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b619eafab..82e176f97 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -316,8 +316,7 @@ let close_proof ?feedback_id ~now fpl =
const_entry_inline_code = false;
const_entry_opaque = true;
const_entry_universes = univs;
- const_entry_polymorphic = poly;
- const_entry_proj = None})
+ const_entry_polymorphic = poly})
fpl initial_goals in
{ id = pid; entries = entries; persistence = strength; universes = universes },
Ephemeron.get terminator
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
new file mode 100644
index 000000000..2682df3b7
--- /dev/null
+++ b/test-suite/success/primitiveproj.v
@@ -0,0 +1,30 @@
+Set Primitive Projections.
+Set Record Elimination Schemes.
+Module Prim.
+
+Record F := { a : nat; b : a = a }.
+Record G (A : Type) := { c : A; d : F }.
+
+Check c.
+End Prim.
+Module Univ.
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Record Foo (A : Type) := { foo : A }.
+
+Record G (A : Type) := { c : A; d : c = c; e : Foo A }.
+
+Definition Foon : Foo nat := {| foo := 0 |}.
+
+Definition Foonp : nat := Foon.(foo).
+
+Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}.
+
+Check (Gt.(e)).
+
+Section bla.
+
+ Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }.
+End bla.
+
+End Univ.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 69c0aaea8..d7c96feca 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -592,7 +592,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
impls;
if_verbose msg_info (minductive_message names);
if mie.mind_entry_private == None
- && not (mie.mind_entry_record = Some true)
then declare_default_schemes mind;
mind
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 1f09d7620..8dcb32442 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -126,7 +126,6 @@ let define internal id c p univs =
const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
- const_entry_proj = None;
const_entry_polymorphic = p;
const_entry_universes = Evd.evar_context_universe_context ctx;
const_entry_opaque = false;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index d413564a9..b422e67b1 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -120,7 +120,6 @@ let define id internal ctx c t =
{ const_entry_body = c;
const_entry_secctx = None;
const_entry_type = t;
- const_entry_proj = None;
const_entry_polymorphic = true;
const_entry_universes = Evd.universe_context ctx;
const_entry_opaque = false;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 18e85266e..9694c2d7f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -629,7 +629,6 @@ let declare_obligation prg obl body ty uctx =
{ const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = if List.is_empty ctx then ty else None;
- const_entry_proj = None;
const_entry_polymorphic = poly;
const_entry_universes = uctx;
const_entry_opaque = opaque;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e46a29ba8..fedf63eed 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -240,64 +240,60 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
match fi with
| Anonymous ->
(None::sp_projs,i,NoProjection fi::subst)
- | Name fid ->
- try
- let ccl = subst_projection fid subst ti in
- let body = match optci with
- | Some ci -> subst_projection fid subst ci
- | None ->
- (* [ccl] is defined in context [params;x:rp] *)
- (* [ccl'] is defined in context [params;x:rp;x:rp] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 rp, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
- let ci = Inductiveops.make_case_info env indsp LetStyle in
- mkCase (ci, p, mkRel 1, [|branch|])
- in
- let proj =
- it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
- let projtyp =
- it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
- let kn =
+ | Name fid -> try
+ let kn, term =
+ if optci = None && primitive then
+ (** Already defined in the kernel silently *)
+ let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
+ Declare.definition_message fid;
+ kn, mkProj (kn,mkRel 1)
+ else
+ let ccl = subst_projection fid subst ti in
+ let body = match optci with
+ | Some ci -> subst_projection fid subst ci
+ | None ->
+ (* [ccl] is defined in context [params;x:rp] *)
+ (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+ let ccl' = liftn 1 2 ccl in
+ let p = mkLambda (x, lift 1 rp, ccl') in
+ let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+ let ci = Inductiveops.make_case_info env indsp LetStyle in
+ mkCase (ci, p, mkRel 1, [|branch|])
+ in
+ let proj =
+ it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+ let projtyp =
+ it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
- let makeprim =
- if primitive && optci = None then
- Some (fst indsp, i)
- else None
- in
- let cie = {
- const_entry_body =
- Future.from_val (Term_typing.mk_pure_proof proj);
- const_entry_secctx = None;
- const_entry_type = Some projtyp;
+ let entry = {
+ const_entry_body =
+ Future.from_val (Term_typing.mk_pure_proof proj);
+ const_entry_secctx = None;
+ const_entry_type = Some projtyp;
const_entry_polymorphic = poly;
const_entry_universes = ctx;
- const_entry_proj = makeprim;
- const_entry_opaque = false;
- const_entry_inline_code = false;
- const_entry_feedback = None;
- } in
- let k = (DefinitionEntry cie,IsDefinition kind) in
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ const_entry_feedback = None } in
+ let k = (DefinitionEntry entry,IsDefinition kind) in
let kn = declare_constant ~internal:KernelSilent fid k in
- Declare.definition_message fid;
- kn
+ let constr_fip =
+ let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+ applist (mkConstU (kn,u),proj_args)
+ in
+ Declare.definition_message fid;
+ kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
- raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
- let refi = ConstRef kn in
- Impargs.maybe_declare_manual_implicits false refi impls;
- if coe then begin
- let cl = Class.class_of_global (IndRef indsp) in
+ raise (NotDefinable (BadTypedProj (fid,ctx,te)))
+ in
+ let refi = ConstRef kn in
+ Impargs.maybe_declare_manual_implicits false refi impls;
+ if coe then begin
+ let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
- end;
- let constr_fip =
- if primitive then mkProj (kn,mkRel 1)
- else
- let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
- applist (mkConstU (kn,u),proj_args)
- in
- let i = if Option.is_empty optci then i+1 else i in
- (Some kn::sp_projs, i,
- Projection constr_fip::subst)
+ end;
+ let i = if Option.is_empty optci then i+1 else i in
+ (Some kn::sp_projs, i, Projection term::subst)
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,i,NoProjection fi::subst) in
@@ -358,13 +354,6 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef cstr in
- let () =
- if !primitive_flag then
- (* declare_mutual won't have tried to define the eliminations, we do it now that
- the projections have been defined. *)
- Indschemes.declare_default_schemes kn
- else ()
- in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 21:45:09 +0000