From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 09:11:09 +0200 Subject: Stylistic improvements in intf/decl_kinds.mli. We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic". --- ide/texmacspp.ml | 3 +- intf/decl_kinds.mli | 10 +- library/declare.ml | 43 ++++---- library/declare.mli | 13 ++- library/decls.ml | 16 ++- library/decls.mli | 6 +- library/kindops.ml | 4 +- library/lib.ml | 18 +-- library/lib.mli | 6 +- ltac/rewrite.ml | 15 +-- plugins/derive/derive.ml | 5 +- plugins/funind/functional_principles_proofs.ml | 4 +- plugins/funind/functional_principles_types.ml | 8 +- plugins/funind/indfun.ml | 4 +- plugins/funind/indfun_common.ml | 7 +- plugins/funind/invfun.ml | 15 ++- plugins/funind/recdef.ml | 16 ++- printing/ppvernac.ml | 3 +- proofs/pfedit.ml | 9 +- proofs/pfedit.mli | 2 +- proofs/proof_global.ml | 4 +- stm/lemmas.ml | 44 +++++--- tactics/leminv.ml | 2 +- tactics/tactics.ml | 4 +- toplevel/class.ml | 4 +- toplevel/classes.ml | 30 +++-- toplevel/classes.mli | 4 +- toplevel/command.ml | 147 +++++++++++++++---------- toplevel/command.mli | 6 +- toplevel/obligations.ml | 38 ++++--- toplevel/record.ml | 12 +- toplevel/vernacentries.ml | 32 ++++-- 32 files changed, 331 insertions(+), 203 deletions(-) diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 328ddd0cd..637744df3 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -546,7 +546,8 @@ let rec tmpp v loc = | DefineBody (_, None , ce, None) -> ce | DefineBody (_, Some _, ce, Some _) -> ce | DefineBody (_, None , ce, Some _) -> ce in - let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let def_kind = { locality = l; polymorphic = false; object_kind = dk } in + let str_dk = Kindops.string_of_definition_kind def_kind in let str_id = Id.to_string id in (xmlDef str_dk str_id loc [pp_expr e]) | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6a4e18833..29972f2f4 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -49,9 +49,13 @@ type assumption_object_kind = Definitional | Logical | Conjectural Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind +type 'a declaration_kind = { locality : locality; + polymorphic : bool; + object_kind : 'a } -type definition_kind = locality * polymorphic * definition_object_kind +type assumption_kind = assumption_object_kind declaration_kind + +type definition_kind = definition_object_kind declaration_kind (** Kinds used in proofs *) @@ -59,7 +63,7 @@ type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind +type goal_kind = goal_object_kind declaration_kind (** Kinds used in library *) diff --git a/library/declare.ml b/library/declare.ml index cc8415cf4..36a58629e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,7 +44,9 @@ let if_xml f x = if !Flags.xml_export then f x else () type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; + polymorphic : bool; + binding_kind : binding_kind } type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -56,19 +58,22 @@ let cache_variable ((sp,_),o) = if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx + let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum { type_context = (ty,ctx); polymorphic; binding_kind } -> + let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in + binding_kind, true, polymorphic, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; + add_section_variable id impl ~polymorphic ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id (p,opaq,ctx,poly,mk) + add_variable_data id { dir_path = p; + opaque; + universe_context_set = ctx; + polymorphic; + kind = mk } let discharge_variable (_,o) = match o with | Inr (id,_) -> @@ -236,11 +241,11 @@ let declare_constant_common id cst = c let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + ?(polymorphic=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; - const_entry_polymorphic = poly; + const_entry_polymorphic = polymorphic; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; @@ -272,9 +277,9 @@ 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) = + ?(polymorphic=false) id ?types (body,ctx) = let cb = - definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + definition_entry ?types ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -458,10 +463,10 @@ let input_universes : universe_decl -> Libobject.obj = 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 do_universe ~polymorphic l = let in_section = Lib.sections_are_opened () in let () = - if poly && not in_section then + if polymorphic && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in @@ -470,7 +475,7 @@ let do_universe poly l = let lev = Universes.new_univ_level (Global.current_dirpath ()) in (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (poly, l)) + Lib.add_anonymous_leaf (input_universes (polymorphic, l)) type constraint_decl = polymorphic * Univ.constraints @@ -490,7 +495,7 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } -let do_constraint poly l = +let do_constraint ~polymorphic l = let u_of_id = let names, _ = Universes.global_universe_names () in fun (loc, id) -> @@ -500,12 +505,12 @@ let do_constraint poly l = in let in_section = Lib.sections_are_opened () in let () = - if poly && not in_section then + if polymorphic && not in_section then user_err ~hdr:"Constraint" (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = - if poly then () + if polymorphic then () else if p || p' then let loc = if p then loc else loc' in user_err ~loc ~hdr:"Constraint" @@ -519,4 +524,4 @@ let do_constraint poly l = Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) + Lib.add_anonymous_leaf (input_constraints (polymorphic, constraints)) diff --git a/library/declare.mli b/library/declare.mli index 7824506da..760bf437b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,7 +23,9 @@ open Decl_kinds type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalAssum of { type_context : types Univ.in_universe_context_set; + polymorphic : bool; + binding_kind : binding_kind } type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -42,7 +44,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?polymorphic:bool -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -56,7 +58,7 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> + ?local:bool -> ?polymorphic:bool -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant (** Since transparent constants' side effects are globally declared, we @@ -89,5 +91,6 @@ val exists_name : Id.t -> bool (** Global universe names and constraints *) -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 +val do_universe : polymorphic:bool -> Id.t Loc.located list -> unit +val do_constraint : polymorphic:bool -> + (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/decls.ml b/library/decls.ml index 2952c258a..1e9afe968 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -19,18 +19,22 @@ module NamedDecl = Context.Named.Declaration (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind + { dir_path : DirPath.t; + opaque : bool; + universe_context_set : Univ.universe_context_set; + polymorphic : bool; + kind : logical_kind } let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p -let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq -let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k -let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx -let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p +let variable_path id = (Id.Map.find id !vartab).dir_path +let variable_opacity id = (Id.Map.find id !vartab).opaque +let variable_kind id = (Id.Map.find id !vartab).kind +let variable_context id = (Id.Map.find id !vartab).universe_context_set +let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in diff --git a/library/decls.mli b/library/decls.mli index 1ca7f8946..e84a6376b 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -17,7 +17,11 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind + { dir_path : DirPath.t; + opaque : bool; + universe_context_set : Univ.universe_context_set; + polymorphic : bool; + kind : logical_kind } val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t diff --git a/library/kindops.ml b/library/kindops.ml index 21b1bec33..3d737e5ac 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,9 +24,9 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - let (locality, poly, kind) = def in + let locality = def.locality in let error () = CErrors.anomaly (Pp.str "Internal definition kind") in - match kind with + match def.object_kind with | Definition -> begin match locality with | Discharge -> "Let" diff --git a/library/lib.ml b/library/lib.ml index 749cc4ff3..954889fb6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -416,12 +416,12 @@ let check_same_poly p vars = if List.exists pred vars then error "Cannot mix universe polymorphic and monomorphic declarations in sections." -let add_section_variable id impl poly ctx = +let add_section_variable id impl ~polymorphic ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab; + sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -450,11 +450,11 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst -let add_section_replacement f g poly hyps = +let add_section_replacement f g ~polymorphic hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in + let () = check_same_poly polymorphic vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -462,13 +462,13 @@ let add_section_replacement f g poly hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn poly kn = +let add_section_kn ~polymorphic kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic -let add_section_constant poly kn = +let add_section_constant ~polymorphic kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly + add_section_replacement f f ~polymorphic let replacement_context () = pi2 (List.hd !sectab) diff --git a/library/lib.mli b/library/lib.mli index 092643c2d..e905ee57e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -176,11 +176,11 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array 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_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : Decl_kinds.polymorphic -> +val add_section_constant : polymorphic:bool -> Names.constant -> Context.Named.t -> unit -val add_section_kn : Decl_kinds.polymorphic -> +val add_section_kn : polymorphic:bool -> Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index a332e2871..ef9d49998 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1755,7 +1755,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + new_instance ~polymorphic:(Flags.is_universe_polymorphism ()) binders instance (Some (true, CRecord (Loc.ghost,fields))) ~global ~generalize:false ~refine:false None @@ -1828,7 +1828,7 @@ let proper_projection r ty = it_mkLambda_or_LetIn app ctx let declare_projection n instance_id r = - let poly = Global.is_polymorphic r in + let polymorphic = Global.is_polymorphic r in let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in @@ -1858,7 +1858,7 @@ let declare_projection n instance_id r = let typ = it_mkProd_or_LetIn typ ctx in let pl, ctx = Evd.universe_context sigma in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~polymorphic ~univs:ctx term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1942,8 +1942,9 @@ let add_morphism_infer glob m n = poly (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else - let kind = Decl_kinds.Global, poly, - Decl_kinds.DefinitionBody Decl_kinds.Instance + let kind = { locality = Decl_kinds.Global; + polymorphic = poly; + object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance } in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ = function @@ -1962,7 +1963,7 @@ let add_morphism_infer glob m n = let add_morphism glob binders m s n = init_setoid (); - let poly = Flags.is_universe_polymorphism () in + let polymorphic = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = (((Loc.ghost,Name instance_id),None), Explicit, @@ -1971,7 +1972,7 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance + ignore(new_instance ~global:glob ~polymorphic binders instance (Some (true, CRecord (Loc.ghost,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e39d17b52..12fd8359a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,7 +22,10 @@ let start_deriving f suchthat lemma = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + let kind = Decl_kinds.{ locality = Global; + polymorphic = false; + object_kind = DefinitionBody Definition } + in (** create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 527f4f0b1..bba7b3c59 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -996,7 +996,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.{ locality = Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Proof Theorem } evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cc699e5d3..4f5f167c2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -288,7 +288,9 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.{ locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Proof Decl_kinds.Theorem } !evd new_principle_type hook @@ -339,7 +341,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) 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' 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 ce = Declare.definition_entry ~polymorphic:(Flags.is_universe_polymorphism ()) + ~univs:(snd (Evd.universe_context evd')) value + in ignore( Declare.declare_constant name diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898b..efbc1507f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -395,7 +395,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in Command.do_definition fname - (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl + { locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Definition } pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a45effb16..8c6673732 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -148,17 +148,18 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,_,kind) hook = +let save with_clean id const goal_kind hook = let fix_exn = Future.fix_exn_of const.const_entry_body in + let locality = goal_kind.locality in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) | Discharge | Local | Global -> let local = get_locality locality in - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e4833..6d042b3a4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -832,7 +832,9 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) + Decl_kinds.{ locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Proof Decl_kinds.Theorem } !evd typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -893,10 +895,13 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + Lemmas.start_proof lem_id + Decl_kinds.{ locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + sigma + (fst lemmas_types_infos.(i)) + (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f43251bc5..75495ed98 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1348,7 +1348,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in Lemmas.start_proof na - (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) + { locality = Decl_kinds.Global; + polymorphic = false (* FIXME *); + object_kind = Decl_kinds.Proof Decl_kinds.Lemma } sigma gls_type (Lemmas.mk_hook hook); if Indfun_common.is_strict_tcc () @@ -1394,8 +1396,12 @@ let com_terminate hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = let (evmap, env) = Lemmas.get_current_context() in + let goal_kind = { locality = Global; + polymorphic = false; (* FIXME *) + object_kind = Proof Lemma } + in Lemmas.start_proof thm_name - (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) + goal_kind ~sign:(Environ.named_context_val env) ctx (compute_terminate_type nb_args fonctional_ref) hook; ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); @@ -1445,7 +1451,11 @@ let (com_eqn : int -> Id.t -> let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (Lemmas.start_proof eq_name (Global, false, Proof Lemma) + let goal_kind = { locality = Global; + polymorphic = false; + object_kind = Proof Lemma } + in + (Lemmas.start_proof eq_name goal_kind ~sign:(Environ.named_context_val env) evmap equation_lemma_type diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 51fc289b4..9a8ad00d0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -695,7 +695,8 @@ module Make | VernacDefinition (d,id,b) -> (* A verifier... *) let pr_def_token (l,dk) = let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind (l,false,dk)) + keyword (Kindops.string_of_definition_kind + { locality = l; polymorphic = false; object_kind = dk }) in let pr_reduce = function | None -> mt() diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 86c2b7a57..d55d6ce6b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -147,7 +147,10 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = +let default_goal_kind = + { locality = Global; polymorphic = false; object_kind = Proof Theorem } + +let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac = let evd = Evd.from_ctx ctx in let terminator = Proof_global.make_terminator (fun _ -> ()) in start_proof id goal_kind evd sign typ terminator; @@ -161,10 +164,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global, poly, Proof Theorem in + let gk = { locality = Global; polymorphic; object_kind = Proof Theorem } in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index f2f4b11ed..aa01969b7 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -169,7 +169,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2956d623f..911d4ffbc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -320,7 +320,7 @@ let constrain_variables init uctx = let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in - let poly = pi2 strength (* Polymorphic *) in + let poly = strength.Decl_kinds.polymorphic in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in @@ -398,7 +398,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 2ab3b9c59..004dd6801 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -191,11 +191,12 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = +let save ?export_seff id const cstrs pl do_guard + { locality; polymorphic; object_kind } hook = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Kindops.logical_kind_of_goal_kind object_kind in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in @@ -229,16 +230,20 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = +let save_remaining_recthms { locality; polymorphic; object_kind } + norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> (match locality with | Discharge -> - let impl = false in (* copy values from Vernacentries *) + let impl = Explicit in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,ctx),p,impl) in - let _ = declare_variable id (Lib.cwd(),c,k) in + let c = SectionLocalAssum { type_context = (t_i,ctx); + polymorphic; + binding_kind = impl } + in + let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> let k = IsAssumption Conjectural in @@ -248,12 +253,12 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Discharge -> assert false in let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,polymorphic,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> let body = norm body in - let k = Kindops.logical_kind_of_goal_kind kind in + let k = Kindops.logical_kind_of_goal_kind object_kind in let rec body_i t = match kind_of_term t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) @@ -264,7 +269,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p + let const = definition_entry ~types:t_i ~opaque:opaq ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in @@ -277,7 +282,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i, | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~polymorphic ~univs:ctx ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -303,7 +308,10 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident = check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) save ?export_seff save_ident const cstrs pl do_guard - (Global, const.const_entry_polymorphic, Proof kind) hook + { locality = Global; + polymorphic = const.const_entry_polymorphic; + object_kind = Proof kind} + hook (* Admitted *) @@ -314,9 +322,9 @@ let warn_let_as_axiom = let admit (id,k,e) pl hook () = let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in - let () = match k with - | Global, _, _ -> () - | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id + let () = match k.locality with + | Global -> () + | Local | Discharge -> warn_let_as_axiom id in let () = assumption_message id in Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; @@ -463,7 +471,7 @@ let start_proof_com kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); let ids = List.map RelDecl.get_name ctx in - (compute_proof_name (pi1 kind) sopt, + (compute_proof_name kind.locality sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) @@ -477,7 +485,7 @@ let start_proof_com kind thms hook = | Some l -> ignore (Evd.universe_context evd ?names:l) in let evd = - if pi2 kind then evd + if kind.polymorphic then evd else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in @@ -512,7 +520,7 @@ let save_proof ?proof = function let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, k.polymorphic, (typ, ctx), None), universes) | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in @@ -533,7 +541,7 @@ let save_proof ?proof = function let names = Pfedit.get_universe_binders () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.universe_context ?names evd in - Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), + Admitted(id,k,(sec_vars, k.polymorphic, (typ, ctx), None), (universes, Some binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d80e86241..c7b8e6cc0 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = 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 - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) + let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ()) ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9d0e9f084..86c0b9dd5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4888,7 +4888,9 @@ let anon_id = Id.of_string "anonymous" let tclABSTRACT name_op tac = let open Proof_global in - let default_gk = (Global, false, Proof Theorem) in + let default_gk = + { locality = Global; polymorphic = false; object_kind = Proof Theorem } + in let s, gk = match name_op with | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk diff --git a/toplevel/class.ml b/toplevel/class.ml index 0dc799014..9582015a0 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -180,7 +180,7 @@ let error_not_transparent source = user_err ~hdr:"build_id_coercion" (pr_class source ++ str " must be a transparent constant.") -let build_id_coercion idf_opt source poly = +let build_id_coercion idf_opt source ~polymorphic = let env = Global.env () in let sigma = Evd.from_env env in let sigma, vs = match source with @@ -221,7 +221,7 @@ let build_id_coercion idf_opt source poly = 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 ~polymorphic ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ad4a13c21..a0a8d2aaf 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -106,7 +106,7 @@ let instance_hook k pri global imps ?hook cst = Typeclasses.declare_instance pri (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype = +let declare_instance_constant k pri global imps ?hook id pl ~polymorphic evm term termtype = let kind = IsDefinition Instance in let evm = let levels = Univ.LSet.union (Universes.universes_of_constr termtype) @@ -115,7 +115,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty in let pl, uctx = Evd.universe_context ?names:pl evm in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~polymorphic ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -124,7 +124,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty instance_hook k pri global imps ?hook (ConstRef kn); id -let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props +let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~polymorphic ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -197,7 +197,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let pl, ctx = Evd.universe_context ?names:pl !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry - (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,polymorphic,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Universes.register_universe_binders (ConstRef cst) pl; instance_hook k pri global imps ?hook (ConstRef cst); id @@ -294,9 +294,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p 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 - poly evm (Option.get term) termtype + ~polymorphic 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 + let kind = { locality = Decl_kinds.Global; + polymorphic; + object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance } + in if Flags.is_program_mode () then let hook vis gr _ = let cst = match gr with ConstRef kn -> kn | _ -> assert false in @@ -313,8 +316,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p in 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); + let kind = { locality = Global; + polymorphic; + object_kind = Instance } + in + ignore (Obligations.add_definition id ?term:constr + ?pl typ ctx ~kind ~hook obls); id else (Flags.silently @@ -390,8 +397,11 @@ let context poly l = | ExplByPos (_, Some id') -> Id.equal id id' | _ -> false in - let impl = List.exists test impls in - let decl = (Discharge, poly, Definitional) in + let impl = if List.exists test impls then Implicit else Explicit in + let decl = { locality = Discharge; + polymorphic = poly; + object_kind = Definitional } + in let nstatus = pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl Vernacexpr.NoInline (Loc.ghost, id)) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 7beb873e6..fc7371cf7 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -31,7 +31,7 @@ val declare_instance_constant : ?hook:(Globnames.global_reference -> unit) -> Id.t -> (** name *) Id.t Loc.located list option -> - bool -> (* polymorphic *) + polymorphic:bool -> Evd.evar_map -> (* Universes *) Constr.t -> (** body *) Term.types -> (** type *) @@ -41,7 +41,7 @@ val new_instance : ?abstract:bool -> (** Not abstract by default. *) ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) - Decl_kinds.polymorphic -> + polymorphic:bool -> local_binder list -> typeclass_constraint -> (bool * constr_expr) option -> diff --git a/toplevel/command.ml b/toplevel/command.ml index caa20b534..40c65b56f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -90,7 +90,7 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl p red_option c ctypopt = +let interp_definition pl bl ~polymorphic 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 @@ -109,7 +109,7 @@ let interp_definition pl bl p red_option c ctypopt = let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, - definition_entry ~univs:uctx ~poly:p body + definition_entry ~univs:uctx ~polymorphic body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in let subst = evd_comb0 Evd.nf_univ_variables evdref in @@ -133,7 +133,7 @@ let interp_definition pl bl p red_option c ctypopt = let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, - definition_entry ~types:typ ~poly:p + definition_entry ~types:typ ~polymorphic ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps @@ -174,7 +174,8 @@ let warn_definition_not_visible = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals") -let declare_definition ident (local, p, k) ce pl imps hook = +let declare_definition ident def_kind ce pl imps hook = + let { locality = local; object_kind = k; _ } = def_kind in let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with @@ -197,7 +198,7 @@ let _ = Obligations.declare_definition_ref := 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 + interp_definition pl bl k.polymorphic red_option c ctypopt in if Flags.is_program_mode () then let env = Global.env () in @@ -223,43 +224,48 @@ let do_definition ident k pl bl red_option c ctypopt hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = -match local with -| Discharge when Lib.sections_are_opened () -> - let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in - let _ = declare_variable ident decl in - let () = assumption_message ident in - let () = - if is_verbose () && Pfedit.refining () then - Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ - strbrk " is not visible from current goals") - in - let r = VarRef ident in - let () = Typeclasses.declare_instance None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true false in - (r,Univ.Instance.empty,true) - -| Global | Local | Discharge -> - let local = get_locality ident local in - let inl = match nl with - | NoInline -> None - | DefaultInline -> Some (Flags.get_inline_level()) - | InlineAt i -> Some i - in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in - let kn = declare_constant ident ~local decl in - let gr = ConstRef kn in - let () = maybe_declare_manual_implicits false gr imps in - let () = Universes.register_universe_binders gr pl in - let () = assumption_message ident in - let () = Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr local p in - let inst = - if p (* polymorphic *) then Univ.UContext.instance ctx - else Univ.Instance.empty - in - (gr,inst,Lib.is_modtype_strict ()) +let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) = + let { locality = local; polymorphic; object_kind = kind } = assumption_kind in + match local with + | Discharge when Lib.sections_are_opened () -> + let entry = SectionLocalAssum { type_context = (c,ctx); + polymorphic; + binding_kind = impl } + in + let decl = (Lib.cwd(), entry, IsAssumption kind) in + let _ = declare_variable ident decl in + let () = assumption_message ident in + let () = + if is_verbose () && Pfedit.refining () then + Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ + strbrk " is not visible from current goals") + in + let r = VarRef ident in + let () = Typeclasses.declare_instance None true r in + let () = if is_coe then Class.try_add_new_coercion r ~local:true false in + (r,Univ.Instance.empty,true) + + | Global | Local | Discharge -> + let local = get_locality ident local in + let inl = match nl with + | NoInline -> None + | DefaultInline -> Some (Flags.get_inline_level()) + | InlineAt i -> Some i + in + let ctx = Univ.ContextSet.to_context ctx in + let decl = (ParameterEntry (None,polymorphic,(c,ctx),inl), IsAssumption kind) in + let kn = declare_constant ident ~local decl in + let gr = ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = Universes.register_universe_binders gr pl in + let () = assumption_message ident in + let () = Typeclasses.declare_instance None false gr in + let () = if is_coe then Class.try_add_new_coercion gr ~local polymorphic in + let inst = + if polymorphic then Univ.UContext.instance ctx + else Univ.Instance.empty + in + (gr,inst,Lib.is_modtype_strict ()) let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in @@ -278,12 +284,12 @@ let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = in List.rev refs, status -let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = +let do_assumptions_unbound_univs kind nl l = let open Context.Named.Declaration in let env = Global.env () in let evdref = ref (Evd.from_env env) in let l = - if poly then + if kind.polymorphic then (* Separate declarations so that A B : Type puts A and B in different levels. *) List.fold_right (fun (is_coe,(idl,c)) acc -> List.fold_right (fun id acc -> @@ -305,7 +311,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 (nf_evar evd)) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps Explicit nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs @@ -323,13 +329,13 @@ let do_assumptions_bound_univs coe kind nl id pl c = let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls Explicit nl id in st let do_assumptions kind nl l = match l with | [coe, ([id, Some pl], c)] -> - let () = match kind with - | (Discharge, _, _) when Lib.sections_are_opened () -> + let () = match kind.locality with + | Discharge when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ~loc msg @@ -852,8 +858,11 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) kind pl ctx f ((def,_),eff) t imps = + let polymorphic = kind.polymorphic in + let ce = + definition_entry ~opaque ~types:t ~polymorphic ~univs:ctx ~eff def + in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := @@ -937,7 +946,7 @@ let rec telescope = function let nf_evar_context sigma ctx = List.map (map_constr (Evarutil.nf_evar sigma)) ctx -let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = +let build_wellfounded (recname,pl,n,bl,arityc,body) polymorphic r measure notation = Coqlib.check_required_library ["Coq";"Program";"Wf"]; let env = Global.env() in let ctx = Evd.make_evar_universe_context env pl in @@ -1048,7 +1057,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let ty = it_mkProd_or_LetIn top_arity binders_rel in let pl, univs = Evd.universe_context ?names:pl !evdref in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in + let ce = definition_entry ~polymorphic ~types:ty ~univs (Evarutil.nf_evar !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1170,7 +1179,11 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind Option.map (List.map Proofview.V82.tactic) init_tac in let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint) + let goal_kind = { locality = Global; + polymorphic = poly; + object_kind = DefinitionBody Fixpoint } + in + Lemmas.start_proof_with_initialization goal_kind evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) @@ -1186,7 +1199,11 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let evd = Evd.restrict_universe_context evd vars 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 (declare_fix (local, poly, Fixpoint) pl ctx) + let def_kind = { locality = local; + polymorphic = poly; + object_kind = Fixpoint } + in + ignore (List.map4 (declare_fix def_kind pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1207,7 +1224,11 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n Option.map (List.map Proofview.V82.tactic) init_tac in let evd = Evd.from_ctx ctx in - Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) + let goal_kind = { locality = local; + polymorphic = poly; + object_kind = DefinitionBody CoFixpoint } + in + Lemmas.start_proof_with_initialization goal_kind evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ())) else begin (* We shortcut the proof process *) @@ -1220,7 +1241,11 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n 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 (declare_fix (local, poly, CoFixpoint) pl ctx) + let def_kind = { locality = local; + polymorphic = poly; + object_kind = CoFixpoint } + in + ignore (List.map4 (declare_fix def_kind pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -1300,9 +1325,13 @@ let do_program_recursive local p fixkind fixl ntns = fixl end in let ctx = Evd.evar_universe_context evd in - let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, p, Fixpoint) - | Obligations.IsCoFixpoint -> (local, p, CoFixpoint) + let object_kind = match fixkind with + | Obligations.IsFixpoint _ -> Fixpoint + | Obligations.IsCoFixpoint -> CoFixpoint + in + let kind = { locality = local; + polymorphic = p; + object_kind } in Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind diff --git a/toplevel/command.mli b/toplevel/command.mli index d35372429..2ae4cddd0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit (** {6 Definitions/Let} *) val interp_definition : - lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> + lident list option -> local_binder list -> polymorphic:bool -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits @@ -55,10 +55,10 @@ val do_definition : Id.t -> definition_kind -> lident list option -> val declare_assumption : coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + binding_kind -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool -val do_assumptions : locality * polymorphic * assumption_object_kind -> +val do_assumptions : assumption_kind -> Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool (* val declare_assumptions : variable Loc.located list -> *) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index aa1a489c2..ceef929b9 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -490,7 +490,7 @@ let declare_definition prg = Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in let ce = definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) + ~opaque ~types:(nf typ) ~polymorphic:prg.prg_kind.polymorphic ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in let () = progmap_remove prg in @@ -542,7 +542,6 @@ let declare_mutual_definition l = let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,poly,kind) = first.prg_kind in let fixnames = first.prg_deps in let opaque = first.prg_opaque in let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in @@ -567,14 +566,16 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Stm.get_fix_exn () in - let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) + let def_kind = { first.prg_kind with object_kind = kind } in + let kns = List.map4 (!declare_fix_ref ~opaque def_kind ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in - Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; + Lemmas.call_hook fix_exn first.prg_hook first.prg_kind.locality gr + first.prg_ctx; List.iter progmap_remove l; kn let decompose_lam_prod c ty = @@ -633,7 +634,7 @@ let declare_obligation prg obl body ty uctx = | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | force, Evar_kinds.Define opaque -> let opaque = not force && opaque in - let poly = pi2 prg.prg_kind in + let poly = prg.prg_kind.polymorphic in let ctx, body, ty, args = if get_shrink_obligations () && not poly then shrink_body body ty else [], body, ty, [||] @@ -791,9 +792,15 @@ let dependencies obls n = obls; !res -let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition +let goal_kind ~polymorphic = + { locality = Decl_kinds.Local; + polymorphic; + object_kind = Decl_kinds.DefinitionBody Decl_kinds.Definition } -let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma +let goal_proof_kind ~polymorphic = + { locality = Decl_kinds.Local; + polymorphic; + object_kind = Decl_kinds.Proof Decl_kinds.Lemma } let kind_of_obligation poly o = match o with @@ -891,7 +898,7 @@ in let _ = obls.(num) <- obl in let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = - if not (pi2 prg.prg_kind) (* Not polymorphic *) then + if not prg.prg_kind.polymorphic then (* The universe context was declared globally, we continue from the new global environment. *) let evd = Evd.from_env (Global.env ()) in @@ -925,7 +932,7 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in + let kind = kind_of_obligation prg.prg_kind.polymorphic (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in @@ -969,13 +976,13 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + prg.prg_kind.polymorphic (Evd.evar_universe_context evd) in let uctx = Evd.evar_context_universe_context ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) then ( + if def && not (prg.prg_kind.polymorphic) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in @@ -1071,7 +1078,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 default_definition_kind = + { locality = Global; + polymorphic = false; + object_kind = Definition } + +let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_kind) ?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 @@ -1090,7 +1102,7 @@ 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 ?pl ?tactic ?(kind=default_definition_kind) ?(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 diff --git a/toplevel/record.ml b/toplevel/record.ml index de056fa9b..c98599d7f 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -426,7 +426,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def poly ctx id idbuild paramimpls params arity +let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -441,11 +441,11 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = - Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in + Declare.definition_entry ~types:class_type ~polymorphic ~univs:ctx class_body in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let cstu = (cst, if polymorphic then Univ.UContext.instance ctx else Univ.Instance.empty) in let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in let proj_type = @@ -453,8 +453,8 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let proj_body = it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in let proj_entry = - Declare.definition_entry ~types:proj_type ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body + Declare.definition_entry ~types:proj_type ~polymorphic + ~univs:(if polymorphic then ctx else Univ.UContext.empty) proj_body in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) @@ -469,7 +469,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite polymorphic ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 14d9a55c6..b8d44f32b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -469,15 +469,22 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local,p,DefinitionBody k) - [Some (lid,pl), (bl,t,None)] hook + let goal_kind = { locality = local; + polymorphic = p; + object_kind = DefinitionBody k } + in + start_proof_and_print goal_kind [Some (lid,pl), (bl,t,None)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> - let (evc,env)= get_current_context () in - Some (snd (Hook.get f_interp_redexp env evc r)) in - do_definition id (local,p,k) pl bl red_option c typ_opt hook) + let (evc,env)= get_current_context () in + Some (snd (Hook.get f_interp_redexp env evc r)) in + let def_kind = { locality = local; + polymorphic = p; + object_kind = k } + in + do_definition id def_kind pl bl red_option c typ_opt hook) let vernac_start_proof locality p kind l lettop = let local = enforce_locality_exp locality None in @@ -490,7 +497,11 @@ let vernac_start_proof locality p kind l lettop = if lettop then user_err ~hdr:"Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - start_proof_and_print (local, p, Proof kind) l no_hook + let goal_kind = { locality = local; + polymorphic = p; + object_kind = Proof kind } + in + start_proof_and_print goal_kind l no_hook let qed_display_script = ref true @@ -514,7 +525,10 @@ let vernac_exact_proof c = let vernac_assumption locality poly (local, kind) l nl = let local = enforce_locality_exp locality local in let global = local == Global in - let kind = local, poly, kind in + let kind = {locality = local; + polymorphic = poly; + object_kind = kind } + in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> @@ -814,10 +828,10 @@ let vernac_identity_coercion locality poly local id qids qidt = (* Type classes *) -let vernac_instance abst locality poly sup inst props pri = +let vernac_instance abst locality ~polymorphic sup inst props pri = let global = not (make_section_locality locality) in Dumpglob.dump_constraint inst false "inst"; - ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri) + ignore(Classes.new_instance ~abstract:abst ~global ~polymorphic sup inst props pri) let vernac_context poly l = if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom -- cgit v1.2.3