From f72a67569ec8cb9160d161699302b67919da5686 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 27 Jul 2017 14:54:41 +0200 Subject: Allow declaring universe constraints at definition level. Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions. --- vernac/classes.ml | 22 ++++++++-------- vernac/classes.mli | 4 +-- vernac/command.ml | 70 ++++++++++++++++++++++++++------------------------ vernac/command.mli | 20 +++++++-------- vernac/lemmas.ml | 50 ++++++++++++++++++------------------ vernac/lemmas.mli | 8 +++--- vernac/obligations.ml | 19 +++++++------- vernac/obligations.mli | 4 +-- vernac/record.ml | 7 ++--- vernac/record.mli | 2 +- 10 files changed, 105 insertions(+), 101 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index ab1892a18..c21345a2a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -111,14 +111,14 @@ let instance_hook k info global imps ?hook cst = Typeclasses.declare_instance (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k info global imps ?hook id pl poly evm term termtype = +let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = let kind = IsDefinition Instance in let evm = let levels = Univ.LSet.union (Univops.universes_of_constr termtype) (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let pl, uctx = Evd.universe_context ?names:pl evm in + let pl, uctx = Evd.check_univ_decl evm decl in let entry = Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in @@ -129,13 +129,13 @@ let declare_instance_constant k info global imps ?hook id pl poly evm term termt instance_hook k info global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props - ?(generalize=true) - ?(tac:unit Proofview.tactic option) ?hook pri = +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) + poly ctx (instid, bk, cl) props ?(generalize=true) + ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let ((loc, instid), pl) = instid in - let uctx = Evd.make_evar_universe_context env pl in - let evars = ref (Evd.from_ctx uctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evars = ref evd in let tclass, ids = match bk with | Decl_kinds.Implicit -> @@ -202,7 +202,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let pl, ctx = Evd.universe_context ?names:pl !evars in + let pl, ctx = Evd.check_univ_decl !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) @@ -302,7 +302,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then - declare_instance_constant k pri global imps ?hook id pl + declare_instance_constant k pri global imps ?hook id decl poly evm (Option.get term) termtype else if Flags.is_program_mode () || refine || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in @@ -323,7 +323,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let hook = Lemmas.mk_hook hook in let ctx = Evd.evar_universe_context evm in ignore (Obligations.add_definition id ?term:constr - ?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls); + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls); id else (Flags.silently @@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p the refinement manually.*) let gls = List.rev (Evd.future_goals evm) in let evm = Evd.reset_future_goals evm in - Lemmas.start_proof id ?pl kind evm (EConstr.of_constr termtype) + Lemmas.start_proof id ~pl:decl kind evm (EConstr.of_constr termtype) (Lemmas.mk_hook (fun _ -> instance_hook k pri global imps ?hook)); (* spiwack: I don't know what to do with the status here. *) diff --git a/vernac/classes.mli b/vernac/classes.mli index fc2fdbbf3..fcdb5c3bc 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -30,7 +30,7 @@ val declare_instance_constant : Impargs.manual_explicitation list -> (** implicits *) ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) - Id.t Loc.located list option -> + Univdecls.universe_decl -> bool -> (* polymorphic *) Evd.evar_map -> (* Universes *) Constr.t -> (** body *) @@ -43,7 +43,7 @@ val new_instance : ?refine:bool -> (** Allow refinement *) Decl_kinds.polymorphic -> local_binder_expr list -> - typeclass_constraint -> + Vernacexpr.typeclass_constraint -> (bool * constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> diff --git a/vernac/command.ml b/vernac/command.ml index 32ab5401a..15dacb776 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -91,8 +91,8 @@ let warn_implicits_in_term = let interp_definition pl bl p red_option c ctypopt = let env = Global.env() in - let ctx = Evd.make_evar_universe_context env pl in - let evdref = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evdref = ref evd in let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in let nb_args = Context.Rel.nhyps ctx in @@ -108,7 +108,7 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.check_univ_decl evd decl in imps1@(Impargs.lift_implicits nb_args imps2), pl, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> @@ -134,20 +134,20 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.universe_context ?names:pl ctx in + let pl, uctx = Evd.check_univ_decl ctx decl in imps1@(Impargs.lift_implicits nb_args impsty), pl, definition_entry ~types:typ ~poly:p ~univs:uctx body in - red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps + red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps -let check_definition (ce, evd, _, imps) = +let check_definition (ce, evd, _, _, imps) = check_evars_are_solved (Global.env ()) evd Evd.empty; ce -let do_definition ident k pl bl red_option c ctypopt hook = - let (ce, evd, pl', imps as def) = - interp_definition pl bl (pi2 k) red_option c ctypopt +let do_definition ident k univdecl bl red_option c ctypopt hook = + let (ce, evd, univdecl, pl', imps as def) = + interp_definition univdecl bl (pi2 k) red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in @@ -164,8 +164,8 @@ let do_definition ident k pl bl red_option c ctypopt hook = in let ctx = Evd.evar_universe_context evd in let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in - ignore(Obligations.add_definition - ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) + ignore(Obligations.add_definition + ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in ignore(DeclareDef.declare_definition ident k ce pl' imps (Lemmas.mk_hook @@ -270,15 +270,15 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in - let ctx = Evd.make_evar_universe_context env pl in - let evdref = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evdref = ref evd in let ty, impls = interp_type_evars_impls env evdref c in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.check_univ_decl evd decl in let uctx = Univ.ContextSet.of_context uctx in let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in st @@ -318,7 +318,7 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : lident list option; + ind_univs : Vernacexpr.universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -526,8 +526,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.iter check_param paramsl; let env0 = Global.env() in let pl = (List.hd indl).ind_univs in - let ctx = Evd.make_evar_universe_context env0 pl in - let evdref = ref Evd.(from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in + let evdref = ref evd in let impls, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in @@ -576,7 +576,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let pl, uctx = Evd.universe_context ?names:pl evd in + let pl, uctx = Evd.check_univ_decl evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -797,7 +797,7 @@ let check_mutuality env evd isfix fixl = type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : lident list option; + fix_univs : universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; @@ -917,8 +917,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in - let ctx = Evd.make_evar_universe_context env pl in - let evdref = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env pl in + let evdref = ref evd in let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in @@ -1019,6 +1019,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in + let pl = Option.map (fun d -> d.univdecl_instance) pl in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in @@ -1052,7 +1053,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp in let ctx = Evd.evar_universe_context !evdref in - ignore(Obligations.add_definition recname ~term:evars_def ?pl + ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl evars_typ ctx evars ~hook) let interp_recursive isfix fixl notations = @@ -1068,11 +1069,12 @@ let interp_recursive isfix fixl notations = | None , acc -> acc | x , None -> x | Some ls , Some us -> - if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then + let lsu = ls.univdecl_instance and usu = us.univdecl_instance in + if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in - let ctx = Evd.make_evar_universe_context env all_universes in - let evdref = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in + let evdref = ref evd in let fixctxs, fiximppairs, fixannots = List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in let fixctximpenvs, fixctximps = List.split fiximppairs in @@ -1122,7 +1124,7 @@ let interp_recursive isfix fixl notations = let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) - (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots + (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env evd Evd.empty; @@ -1145,14 +1147,14 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) + List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) - evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -1165,8 +1167,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in + let pl, ctx = Evd.check_univ_decl evd pl in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let pl, ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) @@ -1179,14 +1181,14 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps)))) + List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) - evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) + evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in @@ -1197,8 +1199,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.universe_context ?names:pl evd in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) + let pl, ctx = Evd.check_univ_decl evd pl in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -1281,7 +1283,7 @@ let do_program_recursive local p fixkind fixl ntns = | Obligations.IsFixpoint _ -> (local, p, Fixpoint) | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) in - Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind + Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in diff --git a/vernac/command.mli b/vernac/command.mli index 8d17f27c3..afa97aa24 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -26,11 +26,11 @@ val do_constraint : polymorphic -> (** {6 Definitions/Let} *) val interp_definition : - lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - Universes.universe_binders * Impargs.manual_implicits + Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits -val do_definition : Id.t -> definition_kind -> lident list option -> +val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -49,7 +49,7 @@ val declare_assumption : coercion_flag -> assumption_kind -> global_reference * Univ.Instance.t * bool val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool + Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool (* val declare_assumptions : variable Loc.located list -> *) (* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *) @@ -62,7 +62,7 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : lident list option; + ind_univs : Vernacexpr.universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -102,7 +102,7 @@ val do_mutual_inductive : type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : lident list option; + fix_univs : Vernacexpr.universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; @@ -127,24 +127,24 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * lident list option * Evd.evar_universe_context * + recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context * (EConstr.rel_context * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * lident list option * Evd.evar_universe_context * + recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context * (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : locality -> polymorphic -> - recursive_preentry * lident list option * Evd.evar_universe_context * + recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context * (Context.Rel.t * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> - recursive_preentry * lident list option * Evd.evar_universe_context * + recursive_preentry * Univdecls.universe_decl * Evd.evar_universe_context * (Context.Rel.t * Impargs.manual_implicits * int option) list -> decl_notation list -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 645320c60..d78cd14f6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -210,11 +210,11 @@ let compute_proof_name locality = function locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (pr_id id ++ str " already exists."); - id, pl + id | None -> - next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None + next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()) -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -222,7 +222,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,ctx),p,impl) in + let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -232,7 +232,6 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Global -> false | Discharge -> assert false in - let ctx = Univ.ContextSet.to_context ctx in let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) @@ -250,12 +249,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, match locality with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:(Univ.ContextSet.to_context ctx) body_i in + ~univs:ctx body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) | Local | Global -> - let ctx = Univ.ContextSet.to_context ctx in let local = match locality with | Local -> true | Global -> false @@ -369,7 +367,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun ((id,_),(t,_)) -> (id,EConstr.of_constr t)) thms with + match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -377,11 +375,11 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun ((id,_),(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with + in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization kind ctx recguard thms snl hook = +let start_proof_with_initialization kind ctx decl recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tacticals.New.tclMAP (function | Name id -> Tactics.intro_mustbe_force id @@ -406,7 +404,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with | [] -> anomaly (Pp.str "No proof to start.") - | ((id,pl),(t,(_,imps)))::other_thms -> + | (id,(t,(_,imps)))::other_thms -> let hook ctx strength ref = let ctx = match ctx with | None -> Evd.empty_evar_universe_context @@ -418,22 +416,24 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.context_set (*FIXME*) ctx in + let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in + List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ?pl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in - let levels = Option.map snd (fst (List.hd thms)) in - let evdref = ref (match levels with - | None -> Evd.from_env env0 - | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l)) - in + let decl = fst (List.hd thms) in + let evd, decl = + match decl with + | None -> Evd.from_env env0, Univdecls.default_univ_decl + | Some decl -> + Univdecls.interp_univ_decl_opt env0 (snd decl) in + let evdref = ref evd in let thms = List.map (fun (sopt,(bl,t)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in @@ -449,16 +449,16 @@ let start_proof_com ?inference_hook kind thms hook = let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = - match levels with - | None -> () - | Some l -> ignore (Evd.universe_context evd ?names:l) + if not decl.Misctypes.univdecl_extensible_instance then + ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance) + else () in let evd = if pi2 kind then evd else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_proof_with_initialization kind evd recguard thms snl hook + start_proof_with_initialization kind evd decl recguard thms snl hook (* Saving a proof *) @@ -507,9 +507,9 @@ let save_proof ?proof = function let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in - let names = Proof_global.get_universe_binders () in + let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let binders, ctx = Evd.universe_context ?names evd in + let binders, ctx = Evd.check_univ_decl evd decl in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index a8c09c0fe..1e23c7314 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -20,13 +20,13 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit -val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> +val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> +val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -38,9 +38,9 @@ val start_proof_com : unit declaration_hook -> unit val start_proof_with_initialization : - goal_kind -> Evd.evar_map -> + goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t (* name of thm *) * Proof_global.universe_binders option) * + (Id.t (* name of thm *) * (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a4fe49020..c71feb52b 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -304,7 +304,7 @@ type program_info_aux = { prg_body: constr; prg_type: constr; prg_ctx: Evd.evar_universe_context; - prg_pl: Id.t Loc.located list option; + prg_univdecl: Univdecls.universe_decl; prg_obligations: obligations; prg_deps : Id.t list; prg_fixkind : fixpoint_kind option ; @@ -474,8 +474,7 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let pl, ctx = - Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in + let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) @@ -658,7 +657,7 @@ let declare_obligation prg obl body ty uctx = else Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } -let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind +let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind notations obls impls kind reduce hook = let obls', b = match b with @@ -679,7 +678,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind obls, b in { prg_name = n ; prg_body = b; prg_type = reduce t; - prg_ctx = ctx; prg_pl = pl; + prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; @@ -1068,11 +1067,12 @@ let show_term n = Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) -let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic +let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl) + ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -1087,13 +1087,14 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res | _ -> res) -let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) +let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic + ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Decls.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook in progmap_add n (CEphemeron.create prg)) l; let _defined = diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 5614403ba..11c2553ae 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -53,7 +53,7 @@ val default_tactic : unit Proofview.tactic ref val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> Evd.evar_universe_context -> - ?pl:(Id.t Loc.located list) -> (* Universe binders *) + ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -71,7 +71,7 @@ val add_mutual_definitions : (Names.Id.t * Term.constr * Term.types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> Evd.evar_universe_context -> - ?pl:(Id.t Loc.located list) -> (* Universe binders *) + ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> diff --git a/vernac/record.ml b/vernac/record.ml index a2e443e5f..4fb607dec 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -95,8 +95,8 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def id pl t ps nots fs = let env0 = Global.env () in - let ctx = Evd.make_evar_universe_context env0 pl in - let evars = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in + let evars = ref evd in let _ = let error bk (loc, name) = match bk, name with @@ -165,9 +165,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let newps = List.map (EConstr.to_rel_decl evars) newps in let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in + let univs = Evd.check_univ_decl evars decl in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs + univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with diff --git a/vernac/record.mli b/vernac/record.mli index 9a0c9ef9d..aea474581 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -39,7 +39,7 @@ val declare_structure : val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list * + Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference -- cgit v1.2.3 From 8966c9241207b6f5d4ee38508246ee97ed006e72 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 31 Jul 2017 16:49:06 +0200 Subject: proof_global: cleanup and comment close_proof evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. --- engine/evd.mli | 2 +- engine/uState.ml | 28 +++++++++++------- engine/uState.mli | 2 +- proofs/proof_global.ml | 78 +++++++++++++++++++++++++------------------------- vernac/lemmas.ml | 6 ++-- 5 files changed, 63 insertions(+), 53 deletions(-) (limited to 'vernac') diff --git a/engine/evd.mli b/engine/evd.mli index 76fa69e31..8c3771cd9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : diff --git a/engine/uState.ml b/engine/uState.ml index 312502491..979a9b086 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,16 +101,6 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty - let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -242,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> diff --git a/engine/uState.mli b/engine/uState.mli index ba0305869..0b67bb71f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -108,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e8266f5c8..cd4d1dcf6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -318,8 +318,7 @@ let get_open_goals () = let constrain_variables init uctx = let levels = Univ.Instance.levels (Univ.UContext.instance init) in - let cstrs = UState.constrain_variables levels uctx in - Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + UState.constrain_variables levels uctx type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -332,6 +331,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in + let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in + let binders = if poly then Some binders else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -355,55 +356,54 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let initunivs = Evd.evar_context_universe_context initial_euctx in let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to - * complement the univ constraints of the typ with the ones of - * the body. So we keep the two sets distinct. *) + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = Univops.restrict_universe_context ctx used_univs in - (initunivs, typ), ((body, ctx_body), eff) + let ctx_body = UState.restrict ctx used_univs in + let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in + (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff) else - let initunivs = Univ.UContext.empty in - let ctx = constrain_variables initunivs universes in (* Since the proof is computed now, we can simply have 1 set of - * constraints in which we merge the ones for the body and the ones - * for the typ *) + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = Univops.restrict_universe_context ctx used_univs in - let univs = Univ.ContextSet.to_context ctx in + let ctx = UState.restrict universes used_univs in + let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context initial_euctx in - Future.from_val (initunivs, nf t), + Future.from_val (univctx, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,constrain_variables initunivs (Future.force univs)),eff) + (* Deferred proof, we already checked the universe declaration with + the initial universes, ensure that the final universes respect + the declaration as well. If the declaration is non-extensible, + this will prevent the body from adding universes and constraints. *) + let bodyunivs = constrain_variables univctx (Future.force univs) in + let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in + (pt,Univ.ContextSet.of_context univs),eff) in - let entries = - Future.map2 (fun p (_, t) -> - let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - let univs = - if poly then Entries.Polymorphic_const_entry univs - else Entries.Monomorphic_const_entry univs - in - { Entries. - const_entry_body = body; - const_entry_secctx = section_vars; - const_entry_feedback = feedback_id; - const_entry_type = Some typ; - const_entry_inline_code = false; - const_entry_opaque = true; - const_entry_universes = univs; - }) - fpl initial_goals in - let binders = - if not poly || (List.is_empty universe_decl.Misctypes.univdecl_instance && - universe_decl.Misctypes.univdecl_extensible_instance) then None - else - Some (fst (Evd.check_univ_decl (Evd.from_ctx universes) universe_decl)) + let entry_fn p (_, t) = + let t = EConstr.Unsafe.to_constr t in + let univstyp, body = make_body t p in + let univs, typ = Future.force univstyp in + let univs = + if poly then Entries.Polymorphic_const_entry univs + else Entries.Monomorphic_const_entry univs + in + {Entries. + const_entry_body = body; + const_entry_secctx = section_vars; + const_entry_feedback = feedback_id; + const_entry_type = Some typ; + const_entry_inline_code = false; + const_entry_opaque = true; + const_entry_universes = univs; } in + let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, fun pr_ending -> CEphemeron.get terminator pr_ending diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d78cd14f6..793022377 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -510,8 +510,10 @@ let save_proof ?proof = function let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.check_univ_decl evd decl in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), - (universes, Some binders)) + let poly = pi2 k in + let binders = if poly then Some binders else None in + Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (is_opaque,idopt) -> -- cgit v1.2.3 From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 9 Sep 2017 14:00:42 +0200 Subject: Don't lose names in UState.universe_context. We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. --- API/API.mli | 2 +- engine/evd.ml | 25 ++------ engine/evd.mli | 8 +-- engine/uState.ml | 92 +++++++++++++++++---------- engine/uState.mli | 8 ++- kernel/univ.mli | 1 + plugins/funind/functional_principles_types.ml | 15 +++-- plugins/funind/recdef.ml | 5 +- plugins/ltac/rewrite.ml | 2 +- plugins/setoid_ring/newring.ml | 2 +- tactics/leminv.ml | 2 +- test-suite/output/UnivBinders.out | 6 ++ test-suite/output/UnivBinders.v | 6 ++ vernac/class.ml | 3 +- vernac/command.ml | 7 +- vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 4 +- vernac/obligations.ml | 2 +- vernac/vernacentries.ml | 2 +- 19 files changed, 111 insertions(+), 83 deletions(-) (limited to 'vernac') diff --git a/API/API.mli b/API/API.mli index 83f4a3c50..bb644c388 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2308,7 +2308,7 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map -> + val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> (Names.Id.t * Univ.Level.t) list * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map diff --git a/engine/evd.ml b/engine/evd.ml index 06b257a9e..f1b5419de 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -748,27 +748,10 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ?names evd = UState.universe_context ?names evd.universes - -open Misctypes -type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl - -let check_implication evd cstrs ctx = - let uctx = evar_universe_context evd in - let gr = UState.initial_graph uctx in - let grext = UGraph.merge_constraints cstrs gr in - let cstrs' = Univ.UContext.constraints ctx in - if UGraph.check_constraints cstrs' grext then () - else CErrors.user_err ~hdr:"check_univ_decl" - (str "Universe constraints are not implied by the ones declared.") - -let check_univ_decl evd decl = - let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in - let pl, ctx = universe_context ?names:pl evd in - if not decl.univdecl_extensible_constraints then - check_implication evd decl.univdecl_constraints ctx; - pl, ctx +let universe_context ~names ~extensible evd = + UState.universe_context ~names ~extensible evd.universes + +let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } diff --git a/engine/evd.mli b/engine/evd.mli index 8c3771cd9..abcabe815 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -547,15 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> +val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t -type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl - -val check_univ_decl : evar_map -> universe_decl -> Universes.universe_binders * Univ.universe_context +val check_univ_decl : evar_map -> UState.universe_decl -> + Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 979a9b086..13a9bb373 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -257,41 +257,63 @@ let pr_uctx_level uctx = with Not_found | Option.IsNone -> Universes.pr_with_global_universes l -let universe_context ?names ctx = - match names with - | None -> [], Univ.ContextSet.to_context ctx.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels ctx.uctx_local in - let newinst, map, left = - List.fold_right - (fun (loc,id) (newinst, map, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") - in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) - pl ([], [], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in - info.uloc - with Not_found -> None - in - user_err ?loc ~hdr:"universe_context" - ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) - else - let inst = Univ.Instance.of_array (Array.of_list newinst) in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) - in map, ctx +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let universe_context ~names ~extensible ctx = + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err ?loc ~hdr:"universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.LSet.remove l acc)) + names ([], levels) + in + if not extensible && not (Univ.LSet.is_empty left) then + let n = Univ.LSet.cardinal left in + let loc = + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + info.uloc + with Not_found -> None + in + user_err ?loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + else + let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let inst = Array.append (Array.of_list newinst) left in + let inst = Univ.Instance.of_array inst in + let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints ctx.uctx_local) in + map, ctx + +let check_implication uctx cstrs ctx = + let gr = initial_graph uctx in + let grext = UGraph.merge_constraints cstrs gr in + let cstrs' = Univ.UContext.constraints ctx in + if UGraph.check_constraints cstrs' grext then () + else CErrors.user_err ~hdr:"check_univ_decl" + (str "Universe constraints are not implied by the ones declared.") + +let check_univ_decl uctx decl = + let open Misctypes in + let pl, ctx = universe_context + ~names:decl.univdecl_instance + ~extensible:decl.univdecl_extensible_instance + uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx decl.univdecl_constraints ctx; + pl, ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index 0b67bb71f..21145e7e6 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -120,7 +120,13 @@ val normalize : t -> t (** {5 TODO: Document me} *) -val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context +val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> + (Id.t * Univ.Level.t) list * Univ.universe_context + +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context val update_sigma_env : t -> Environ.env -> t diff --git a/kernel/univ.mli b/kernel/univ.mli index a4f2e26b6..94116e473 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -411,6 +411,7 @@ sig val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) + val sort_levels : Level.t array -> Level.t array val to_context : t -> universe_context val of_context : universe_context -> t diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index ef1654fdf..409bb89ee 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -338,13 +338,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in - let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - let evd',value = change_property_sort evd' s new_principle_type new_princ_name in - let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in - (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in + let evd' = Evd.from_env (Global.env ()) in + let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in + let evd',value = change_property_sort evd' s new_principle_type new_princ_name in + let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant name diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 41a10cba3..d43fd78f3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1543,7 +1543,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + let functional_ref = + let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 75b665aad..3d01cbe8d 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,7 +1884,7 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let pl, ctx = Evd.universe_context sigma in + let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d0fe1f957..b8fae2494 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context evd) + Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 967ec2a71..7c488f524 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn c !ownSign in let invProof = EConstr.Unsafe.to_constr invProof in let p = Evarutil.nf_evars_universes sigma invProof in - p, Evd.universe_context sigma + p, Evd.universe_context ~names:[] ~extensible:true sigma let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 128bc7767..904ff68aa 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,3 +4,9 @@ bar@{u} = nat *) bar is universe polymorphic +foo@{u Top.8 v} = +Type@{Top.8} -> Type@{v} -> Type@{u} + : Type@{max(u+1, Top.8+1, v+1)} +(* u Top.8 v |= *) + +foo is universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index d9e89e43c..8656ff1a3 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,7 +1,13 @@ Set Universe Polymorphism. Set Printing Universes. +Unset Strict Universe Declaration. Class Wrap A := wrap : A. Instance bar@{u} : Wrap@{u} Set. Proof nat. Print bar. + +(* The universes in the binder come first, then the extra universes in + order of appearance. *) +Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Print foo. diff --git a/vernac/class.ml b/vernac/class.ml index be682977e..3915148a0 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -222,9 +222,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in + let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) + (definition_entry ~types:typ_f ~poly ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/vernac/command.ml b/vernac/command.ml index 15dacb776..59f59e530 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1019,15 +1019,16 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in - let pl = Option.map (fun d -> d.univdecl_instance) pl in - let hook, recname, typ = + let pl, plext = Option.cata + (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in + let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ?names:pl !evdref in + let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index facebd096..90168843a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -108,7 +108,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ctx in + let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 793022377..391e78bcd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context uctx in + let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -450,7 +450,7 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance) + ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) else () in let evd = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c71feb52b..89b18d254 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -888,7 +888,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ctx' in + let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4fd08b42d..c90d038f6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1556,7 +1556,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = -- cgit v1.2.3