From ed7af646f2e486b7e96812ba2335e644756b70fd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 27 Oct 2015 13:55:45 -0400 Subject: Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names structure. --- library/declare.ml | 93 +++++++++++++++++++++++++------------------ library/declare.mli | 4 +- library/lib.ml | 39 ++++++++++++------ library/lib.mli | 2 +- library/universes.ml | 3 +- test-suite/bugs/closed/4390.v | 37 +++++++++++++++++ toplevel/command.ml | 4 +- toplevel/command.mli | 5 ++- toplevel/vernacentries.ml | 25 ++++++++---- 9 files changed, 147 insertions(+), 65 deletions(-) create mode 100644 test-suite/bugs/closed/4390.v 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 -- cgit v1.2.3