aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/declare.ml93
-rw-r--r--library/declare.mli4
-rw-r--r--library/lib.ml39
-rw-r--r--library/lib.mli2
-rw-r--r--library/universes.ml3
-rw-r--r--test-suite/bugs/closed/4390.v37
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/command.mli5
-rw-r--r--toplevel/vernacentries.ml25
9 files changed, 147 insertions, 65 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 16803b3bf..0004f45a2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -27,7 +27,7 @@ open Decls
open Decl_kinds
(** flag for internal message display *)
-type internal_flag =
+type internal_flag =
| UserAutomaticRequest (* kernel action, a message is displayed *)
| InternalTacticRequest (* kernel action, no message is displayed *)
| UserIndividualRequest (* user action, a message is displayed *)
@@ -63,7 +63,7 @@ let cache_variable ((sp,_),o) =
add_variable_data id (p,opaq,ctx,poly,mk)
let discharge_variable (_,o) = match o with
- | Inr (id,_) ->
+ | Inr (id,_) ->
if variable_polymorphic id then None
else Some (Inl (variable_context id))
| Inl _ -> Some o
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry =
+let dummy_constant_entry =
ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
let dummy_constant cst = {
@@ -185,7 +185,7 @@ let declare_constant_common id cst =
Notation.declare_ref_arguments_scope (ConstRef c);
c
-let definition_entry ?(opaque=false) ?(inline=false) ?types
+let definition_entry ?(opaque=false) ?(inline=false) ?types
?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
{ const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
@@ -212,11 +212,11 @@ let declare_sideff env fix_exn se =
in
let ty_of cb =
match cb.Declarations.const_type with
- | Declarations.RegularArity t -> Some t
+ | Declarations.RegularArity t -> Some t
| Declarations.TemplateArity _ -> None in
let cst_of cb pt =
let pt, opaque = pt_opaque_of cb pt in
- let univs, subst =
+ let univs, subst =
if cb.const_polymorphic then
let univs = Univ.instantiate_univ_context cb.const_universes in
univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
@@ -240,7 +240,7 @@ let declare_sideff env fix_exn se =
} in
let exists c =
try ignore(Environ.lookup_constant c env); true
- with Not_found -> false in
+ with Not_found -> false in
let knl =
CList.map_filter (fun (c,cb,pt) ->
if exists c then None
@@ -287,7 +287,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
let declare_definition ?(internal=UserIndividualRequest)
?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
?(poly=false) id ?types (body,ctx) =
- let cb =
+ let cb =
definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
in
declare_constant ~internal ~local id
@@ -383,12 +383,12 @@ let inInductive : inductive_obj -> obj =
let declare_projections mind =
let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
match spec.mind_record with
- | Some (Some (_, kns, pjs)) ->
- Array.iteri (fun i kn ->
+ | Some (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)
+ IsDefinition StructureComponent)
in
assert(eq_constant kn kn')) kns; true
| Some None | None -> false
@@ -442,52 +442,69 @@ let assumption_message id =
(** Global universe names, in a different summary *)
-type universe_names =
+type universe_names =
(Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
-let input_universes : universe_names -> Libobject.obj =
- let open Libobject in
- declare_object
- { (default_object "Global universe name state") with
- cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi);
- load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi);
- discharge_function = (fun (_, a) -> Some a);
- classify_function = (fun a -> Keep a) }
+(* Discharged or not *)
+type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
-let do_universe l =
+let cache_universes (p, l) =
let glob = Universes.global_universe_names () in
- let glob', ctx =
- List.fold_left (fun ((idl,lid),ctx) (l, id) ->
- let lev = Universes.new_univ_level (Global.current_dirpath ()) in
- ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
- Univ.ContextSet.add_universe lev ctx))
+ let glob', ctx =
+ List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
+ ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
+ Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
Global.push_context_set false ctx;
- Lib.add_anonymous_leaf (input_universes glob')
+ if p then Lib.add_section_context ctx;
+ Universes.set_global_universe_names glob'
+
+let input_universes : universe_decl -> Libobject.obj =
+ declare_object
+ { (default_object "Global universe name state") with
+ cache_function = (fun (na, pi) -> cache_universes pi);
+ load_function = (fun _ (_, pi) -> cache_universes pi);
+ discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+ classify_function = (fun a -> Keep a) }
+
+let do_universe poly l =
+ let l =
+ List.map (fun (l, id) ->
+ let lev = Universes.new_univ_level (Global.current_dirpath ()) in
+ (id, lev)) l
+ in
+ Lib.add_anonymous_leaf (input_universes (poly, l))
+
+type constraint_decl = polymorphic * Univ.constraints
+
+let cache_constraints (na, (p, c)) =
+ Global.add_constraints c;
+ if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+let discharge_constraints (_, (p, c as a)) =
+ if p then None else Some a
-let input_constraints : Univ.constraints -> Libobject.obj =
- let open Libobject in
+let input_constraints : constraint_decl -> Libobject.obj =
+ let open Libobject in
declare_object
{ (default_object "Global universe constraints") with
- cache_function = (fun (na, c) -> Global.add_constraints c);
- load_function = (fun _ (_, c) -> Global.add_constraints c);
- discharge_function = (fun (_, a) -> Some a);
+ cache_function = cache_constraints;
+ load_function = (fun _ -> cache_constraints);
+ discharge_function = discharge_constraints;
classify_function = (fun a -> Keep a) }
-let do_constraint l =
- let u_of_id =
+let do_constraint poly l =
+ let u_of_id =
let names, _ = Universes.global_universe_names () in
- fun (loc, id) ->
+ fun (loc, id) ->
try Idmap.find id names
with Not_found ->
- user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+ user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
in
let constraints = List.fold_left (fun acc (l, d, r) ->
let lu = u_of_id l and ru = u_of_id r in
Univ.Constraint.add (lu, d, ru) acc)
Univ.Constraint.empty l
in
- Lib.add_anonymous_leaf (input_constraints constraints)
-
+ Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declare.mli b/library/declare.mli
index 76538a624..7ed451c3f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -85,5 +85,5 @@ val exists_name : Id.t -> bool
(** Global universe names and constraints *)
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
diff --git a/library/lib.ml b/library/lib.ml
index f4f52db53..cdc888903 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -392,10 +392,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
+type secentry =
+ | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+ Decl_kinds.polymorphic * Univ.universe_context_set)
+ | Context of Univ.universe_context_set
+
let sectab =
- Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind *
- Decl_kinds.polymorphic * Univ.universe_context_set) list *
- Opaqueproof.work_list * abstr_list) list)
+ Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
~name:"section-context"
let add_section () =
@@ -406,21 +409,29 @@ let add_section_variable id impl poly ctx =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
- sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
+ sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+
+let add_section_context ctx =
+ match !sectab with
+ | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+ | (vars,repl,abs)::sl ->
+ sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
let rec aux = function
- | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+ | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
let l, r = aux (idl,hyps) in
(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
- | ((_,_,poly,ctx)::idl,hyps) ->
+ | (Variable (_,_,poly,ctx)::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, if poly then Univ.ContextSet.union r ctx else r
+ | (Context ctx :: idl, hyps) ->
+ let l, r = aux (idl, hyps) in
+ l, Univ.ContextSet.union r ctx
| [], _ -> [],Univ.ContextSet.empty
in aux (secs,ohyps)
let instance_from_variable_context sign =
-
let rec inst_rec = function
| (id,b,None,_) :: sign -> id :: inst_rec sign
| _ :: sign -> inst_rec sign
@@ -437,7 +448,8 @@ let add_section_replacement f g hyps =
let ctx = Univ.ContextSet.to_context ctx in
let subst, ctx = Univ.abstract_universes true ctx in
let args = instance_from_variable_context (List.rev sechyps) in
- sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl
+ sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+ g (sechyps,subst,ctx) abs)::sl
let add_section_kn kn =
let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -457,10 +469,13 @@ let section_segment_of_mutual_inductive kn =
let section_instance = function
| VarRef id ->
- if List.exists (fun (id',_,_,_) -> Names.id_eq id id')
- (pi1 (List.hd !sectab))
- then Univ.Instance.empty, [||]
- else raise Not_found
+ let eq = function
+ | Variable (id',_,_,_) -> Names.id_eq id id'
+ | Context _ -> false
+ in
+ if List.exists eq (pi1 (List.hd !sectab))
+ then Univ.Instance.empty, [||]
+ else raise Not_found
| ConstRef con ->
Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
diff --git a/library/lib.mli b/library/lib.mli
index 9c4d26c5b..b67b2b873 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -172,7 +172,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na
val is_in_section : Globnames.global_reference -> bool
val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
-
+val add_section_context : Univ.universe_context_set -> unit
val add_section_constant : bool (* is_projection *) ->
Names.constant -> Context.named_context -> unit
val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
diff --git a/library/universes.ml b/library/universes.ml
index 0656188eb..30d38eb2a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -16,7 +16,8 @@ open Univ
type universe_names =
Univ.universe_level Idmap.t * Id.t Univ.LMap.t
-let global_universes = Summary.ref ~name:"Global universe names"
+let global_universes =
+ Summary.ref ~name:"Global universe names"
((Idmap.empty, Univ.LMap.empty) : universe_names)
let global_universe_names () = !global_universes
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
new file mode 100644
index 000000000..a96a13700
--- /dev/null
+++ b/test-suite/bugs/closed/4390.v
@@ -0,0 +1,37 @@
+Module A.
+Set Printing All.
+Set Printing Universes.
+
+Module M.
+Section foo.
+Universe i.
+End foo.
+End M.
+
+Check Type@{i}.
+(* Succeeds *)
+
+Fail Check Type@{j}.
+(* Error: Undeclared universe: j *)
+
+Definition foo@{j} : Type@{i} := Type@{j}.
+(* ok *)
+End A.
+
+Set Universe Polymorphism.
+Fail Universes j.
+Monomorphic Universe j.
+Section foo.
+ Universes i.
+ Constraint i < j.
+ Definition foo : Type@{j} := Type@{i}.
+ Definition foo' : Type@{j} := Type@{i}.
+End foo.
+
+Check eq_refl : foo@{i} = foo'@{i}.
+
+Definition bar := foo.
+Monomorphic Definition bar'@{k} := foo@{k}.
+
+Fail Constraint j = j.
+Monomorphic Constraint i = i.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7c86d2d05..3995c4b1b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,8 +38,8 @@ open Indschemes
open Misctypes
open Vernacexpr
-let do_universe l = Declare.do_universe l
-let do_constraint l = Declare.do_constraint l
+let do_universe poly l = Declare.do_universe poly l
+let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
if Int.equal n 0 then snd (f env sigma c) else
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b1e1d7d06..b400f0fde 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -20,8 +20,9 @@ open Pfedit
(** This file is about the interpretation of raw commands into typed
ones and top-level declaration of the main Gallina objects *)
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic ->
+ (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
(** {6 Hooks for Pcoq} *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d04d6c9ed..2879947a9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -552,12 +552,12 @@ let vernac_inductive poly lo finite indl =
Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
| [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
vernac_record (match b with Class true -> Class false | _ -> b)
- poly finite id bl c oc fs
+ poly finite id bl c oc fs
| [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
let f =
let (coe, ((loc, id), ce)) = l in
let coe' = if coe then Some true else None in
- (((coe', AssumExpr ((loc, Name id), ce)), None), [])
+ (((coe', AssumExpr ((loc, Name id), ce)), None), [])
in vernac_record (Class true) poly finite id bl c None [f]
| [ ( id , bl , c , Class true, _), _ ] ->
Errors.error "Definitional classes must have a single method"
@@ -602,8 +602,19 @@ let vernac_combined_scheme lid l =
List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
Indschemes.do_combined_scheme lid l
-let vernac_universe l = do_universe l
-let vernac_constraint l = do_constraint l
+let vernac_universe loc poly l =
+ if poly && not (Lib.sections_are_opened ()) then
+ user_err_loc (loc, "vernac_universe",
+ str"Polymorphic universes can only be declared inside sections, " ++
+ str "use Monomorphic Universe instead");
+ do_universe poly l
+
+let vernac_constraint loc poly l =
+ if poly && not (Lib.sections_are_opened ()) then
+ user_err_loc (loc, "vernac_constraint",
+ str"Polymorphic universe constraints can only be declared"
+ ++ str " inside sections, use Monomorphic Constraint instead");
+ do_constraint poly l
(**********************)
(* Modules *)
@@ -1870,8 +1881,8 @@ let interp ?proof ~loc locality poly c =
| VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
- | VernacUniverse l -> vernac_universe l
- | VernacConstraint l -> vernac_constraint l
+ | VernacUniverse l -> vernac_universe loc poly l
+ | VernacConstraint l -> vernac_constraint loc poly l
(* Modules *)
| VernacDeclareModule (export,lid,bl,mtyo) ->
@@ -2034,7 +2045,7 @@ let check_vernac_supports_polymorphism c p =
| VernacCoercion _ | VernacIdentityCoercion _
| VernacInstance _ | VernacDeclareInstances _
| VernacHints _ | VernacContext _
- | VernacExtend _ ) -> ()
+ | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
| Some _, _ -> Errors.error "This command does not support Polymorphism"
let enforce_polymorphism = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 05:44:29 +0000