diff options
119 files changed, 2493 insertions, 1158 deletions
diff --git a/META.coq.in b/META.coq.in index ef5de8da2b..f7922e0ac2 100644 --- a/META.coq.in +++ b/META.coq.in @@ -244,14 +244,12 @@ package "idetop" ( ) -# XXX Depends on way less than toplevel package "ide" ( description = "Coq IDE Libraries" version = "8.10" -# XXX Add GTK - requires = "coq.toplevel" + requires = "coq.lib, coq.ideprotocol, lablgtk3, lablgtk3-sourceview3" directory = "ide" archive(byte) = "ide.cma" @@ -259,6 +257,19 @@ package "ide" ( ) +package "ideprotocol" ( + + description = "Coq IDE protocol" + version = "8.10" + + requires = "coq.toplevel" + directory = "ide/protocol" + + archive(byte) = "ideprotocol.cma" + archive(native) = "ideprotocol.cmxa" + +) + package "plugins" ( description = "Coq built-in plugins" diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh new file mode 100644 index 0000000000..d133bc9993 --- /dev/null +++ b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then + + elpi_CI_REF=proof+recthms + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + equations_CI_REF=proof+recthms + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=proof+recthms + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=proof+recthms + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + quickchick_CI_REF=proof+recthms + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh new file mode 100644 index 0000000000..3122f953de --- /dev/null +++ b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then + + equations_CI_REF=desync-entry-proof + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + quickchick_CI_REF=desync-entry-proof + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 51d90df89f..ab9df12766 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -13,13 +13,31 @@ Proof state: Proofs that are attached to a top-level constant (such as lemmas) are represented by `Lemmas.t`, as they do contain additional - information related to the constant declaration. + information related to the constant declaration. Some functions have + been renamed from `start_proof` to `start_lemma` + Plugins that require access to the information about currently opened lemmas can add one of the `![proof]` attributes to their `mlg` entry, which will refine the type accordingly. See documentation in `vernacentries` for more information. + Proof `terminators` have been removed in favor of a principled + proof-saving path. This should not affect the regular API user, but + if plugin writes need special handling of the proof term they should + now work with Coq upstream to unsure the provided API does work and + is principled. Closing `hooks` are still available for simple + registration on constant save path, and essentially they do provide + the same power as terminators, but don't encourage their use other + than for simple tasks [such as adding a constant to a database] + + Additionally, the API for proof/lemma handling has been refactored, + triples have been split into named arguments, and a few bits of + duplicated information among layers has been cleaned up. Most proof + information is now represented in a direct-style, as opposed to it + living inside closures in previous Coq versions; thus, proof + manipulation possibilities have been improved. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index eb8161c2bb..68ae5628db 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,14 +1,12 @@ -let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let declare_definition ~poly ident sigma body = - let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ident k ~opaque:false sigma udecl body None [] - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 36eeff6192..3036648b08 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -850,8 +850,17 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. -Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited -to the use of standalone function calls. +Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can +be done via an explicit annotation to the :n:`ltac1` quotation. + +.. productionlist:: coq + ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) + +The return type of this expression is a function of the same arity as the number +of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax +will bind the variables in the quoted Ltac1 code as if they had been bound from +Ltac1 itself. Similarly, the arguments applied to the quotation will be passed +at runtime to the Ltac1 code. Low-level API +++++++++++++ @@ -869,6 +878,9 @@ focus is very hard. This is why some functions return a continuation-passing style value, as it can dispatch dynamically between focused and unfocused behaviour. +The same mechanism for explicit binding of variables as described in the +previous section applies. + Ltac2 from Ltac1 ~~~~~~~~~~~~~~~~ diff --git a/engine/uState.ml b/engine/uState.ml index 6a1282203a..5ed016e0d0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -214,7 +214,8 @@ let process_universe_constraints ctx cstrs = | Inr l, Inl r | Inl r, Inr l -> let alg = LSet.mem l ctx.uctx_univ_algebraic in let inst = univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) + if alg && not (LSet.mem l (Universe.levels inst)) then + (instantiate_variable l inst vars; local) else let lu = Universe.make l in if univ_level_mem l r then @@ -452,9 +453,9 @@ let restrict ctx vars = let uctx' = restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } -let demote_seff_univs entry uctx = +let demote_seff_univs universes uctx = let open Entries in - match entry.const_entry_universes with + match universes with | Polymorphic_entry _ -> uctx | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in diff --git a/engine/uState.mli b/engine/uState.mli index 204e97eb15..9689f2e961 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -100,7 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t universes are preserved. *) val restrict : t -> Univ.LSet.t -> t -val demote_seff_univs : 'a Entries.definition_entry -> t -> t +val demote_seff_univs : Entries.universes_entry -> t -> t type rigid = | UnivRigid diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 0010229f9b..b46ab49771 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -50,6 +50,41 @@ and comment = parse | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } +and quotation o c n l = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then quotation_nesting o c n l 1 lexbuf + else if x = c then + if n = 1 && l = 1 then () + else quotation_closing o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_nesting o c n l v = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then + if n = v+1 then quotation o c n (l+1) lexbuf + else quotation_nesting o c n l (v+1) lexbuf + else if x = c then quotation_closing o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_closing o c n l v = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = c then + if n = v+1 then + if l = 1 then () + else quotation o c n (l-1) lexbuf + else quotation_closing o c n l (v+1) lexbuf + else if x = o then quotation_nesting o c n l 1 lexbuf + else quotation o c n l lexbuf +} + +and quotation_start o c n = parse | eof { raise Unterminated } | _ { + let x = Lexing.lexeme lexbuf in + if x = o then quotation_start o c (n+1) lexbuf + else quotation o c n 1 lexbuf +} + (** NB : [mkiter] should be called on increasing offsets *) and sentence initial stamp = parse @@ -83,6 +118,18 @@ and sentence initial stamp = parse if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; sentence initial stamp lexbuf } + | ['a'-'z' 'A'-'Z'] ":{" { + quotation_start "{" "}" 1 lexbuf; + sentence false stamp lexbuf + } + | ['a'-'z' 'A'-'Z'] ":[" { + quotation_start "[" "]" 1 lexbuf; + sentence false stamp lexbuf + } + | ['a'-'z' 'A'-'Z'] ":(" { + quotation_start "(" ")" 1 lexbuf; + sentence false stamp lexbuf + } | space+ { (* Parsing spaces is the only situation preserving initiality *) sentence initial stamp lexbuf diff --git a/interp/interp.mllib b/interp/interp.mllib index 52978a2ab6..33573edcce 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -17,4 +17,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Declare diff --git a/kernel/entries.ml b/kernel/entries.ml index de1ce609fd..2d29c3ee19 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -60,15 +60,14 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type 'a definition_entry = { - const_entry_body : 'a const_entry_body; +type definition_entry = { + const_entry_body : constr Univ.in_universe_context_set; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_universes : universes_entry; - const_entry_opaque : bool; const_entry_inline_code : bool } type section_def_entry = { @@ -78,6 +77,16 @@ type section_def_entry = { secdef_type : types option; } +type 'a opaque_entry = { + opaque_entry_body : 'a; + (* List of section variables *) + opaque_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + opaque_entry_feedback : Stateid.t option; + opaque_entry_type : types; + opaque_entry_universes : universes_entry; +} + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = @@ -90,7 +99,8 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of 'a definition_entry + | DefinitionEntry of definition_entry + | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/names.ml b/kernel/names.ml index 655bf50087..85dc8267bb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -671,6 +671,7 @@ module InductiveOrdered_env = struct let compare = ind_user_ord end +module Indset = Set.Make(InductiveOrdered) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 44e8dd4a83..65c5d6c139 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -481,6 +481,7 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) +module Indset : CSig.SetS with type elt = inductive module Indmap : CSig.MapS with type key = inductive module Constrmap : CSig.MapS with type key = constructor module Indmap_env : CSig.MapS with type key = inductive diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a980d22e42..a0cc2974d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff = | OpaqueDef b -> b | Def b -> Mod_subst.force_constr b | _ -> assert false in + if Declareops.is_opaque cb then + OpaqueEntry { + opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_secctx = None; + opaque_entry_feedback = None; + opaque_entry_type = cb.const_type; + opaque_entry_universes = univs; + } + else DefinitionEntry { - const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_body = (p, Univ.ContextSet.empty); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } let export_eff eff = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 165feca1b6..eca22869d2 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,11 +115,10 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in let proofterm = Future.chain body begin fun ((body,uctx),side_eff) -> @@ -151,17 +150,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = false; + cook_context = c.opaque_entry_secctx; } - (** Similar case for polymorphic entries. TODO: also delay type-checking of - the body. *) + (** Similar case for polymorphic entries. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; - const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in let sbst, auctx = Univ.abstract_universes nas uctx in @@ -190,21 +187,16 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = false; + cook_context = c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - (* Opaque constants must be provided with a non-empty const_entry_type, - and thus should have been treated above. *) - let () = assert (not c.const_entry_opaque) in - let body, ctx = match trust with - | Pure -> - let (body, ctx), () = Future.join body in - body, ctx + let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let () = match trust with + | Pure -> () | SideEffects _ -> assert false in let env, usubst, univs = match c.const_entry_universes with @@ -368,14 +360,13 @@ let translate_recipe env _kn r = let translate_local_def env _id centry = let open Cooking in - let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in + let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { const_entry_body = body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; - const_entry_opaque = false; const_entry_inline_code = false; } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 0e2ef95739..6eb582baef 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -10,16 +10,8 @@ (** Informal mathematical status of declarations *) -type discharge = DoDischarge | NoDischarge - -type import_status = ImportDefaultBehavior | ImportNeedQualified - -type locality = Discharge | Global of import_status - type binding_kind = Explicit | Implicit -type polymorphic = bool - type private_flag = bool type cumulative_inductive_flag = bool @@ -58,17 +50,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind - (** Kinds used in proofs *) type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * polymorphic * goal_object_kind - (** Kinds used in library *) type logical_kind = diff --git a/library/decls.ml b/library/decls.ml index ef60a44ac7..5cb35323dd 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -17,19 +17,24 @@ open Libnames (** Datas associated to section variables and local definitions *) -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind +type variable_data = { + path:DirPath.t; + opaque:bool; + univs:Univ.ContextSet.t; + poly: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 = let {path} = Id.Map.find id !vartab in path +let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque +let variable_kind id = let {kind} = Id.Map.find id !vartab in kind +let variable_context id = let {univs} = Id.Map.find id !vartab in univs +let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly 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 0d09499b51..f88958bb04 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -18,8 +18,13 @@ open Decl_kinds (** Registration and access to the table of variable *) -type variable_data = - DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind +type variable_data = { + path:DirPath.t; + opaque:bool; + univs:Univ.ContextSet.t; + poly:bool; + kind:logical_kind; +} val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t @@ -27,7 +32,7 @@ val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool val variable_context : variable -> Univ.ContextSet.t -val variable_polymorphic : variable -> polymorphic +val variable_polymorphic : variable -> bool val variable_exists : variable -> bool (** Registration and access to the table of constants *) diff --git a/library/goptions.ml b/library/goptions.ml index e25672ccf2..c7024ca81d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -53,9 +53,9 @@ module MakeTable = functor (A : sig type t - type key - val compare : t -> t -> int - val table : (string * key table_of_A) list ref + type key + module Set : CSig.SetS with type elt = t + val table : (string * key table_of_A) list ref val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -74,7 +74,7 @@ module MakeTable = if String.List.mem_assoc nick !A.table then user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") - module MySet = Set.Make (struct type t = A.t let compare = A.compare end) + module MySet = A.Set let t = Summary.ref MySet.empty ~name:nick @@ -119,8 +119,9 @@ module MakeTable = } let _ = A.table := (nick, table_of_A)::!A.table - let active c = MySet.mem c !t - let elements () = MySet.elements !t + + let v () = !t + let active x = A.Set.mem x !t end let string_table = ref [] @@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) -> struct type t = string type key = string - let compare = String.compare + module Set = CString.Set let table = string_table let encode _env x = x let subst _ x = x @@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t - val compare : t -> t -> int + module Set : CSig.SetS with type elt = t val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = qualid - let compare = A.compare + module Set = A.Set let table = ref_table let encode = A.encode let subst = A.subst diff --git a/library/goptions.mli b/library/goptions.mli index 2989221975..29af196654 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -70,8 +70,8 @@ module MakeStringTable : val member_message : string -> bool -> Pp.t end) -> sig + val v : unit -> CString.Set.t val active : string -> bool - val elements : unit -> string list end (** The functor [MakeRefTable] declares a new table of objects of type @@ -87,19 +87,19 @@ end module MakeRefTable : functor (A : sig - type t - val compare : t -> t -> int - val encode : Environ.env -> qualid -> t - val subst : substitution -> t -> t - val printer : t -> Pp.t - val key : option_name - val title : string - val member_message : t -> bool -> Pp.t - end) -> - sig - val active : A.t -> bool - val elements : unit -> A.t list - end + type t + module Set : CSig.SetS with type elt = t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> +sig + val v : unit -> A.Set.t + val active : A.t -> bool +end (** {6 Options. } *) diff --git a/library/lib.ml b/library/lib.ml index ae657dbd70..3eb74808e4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -411,8 +411,12 @@ type abstr_info = { type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = - | Variable of (Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.ContextSet.t) + | Variable of { + id:Names.Id.t; + kind:Decl_kinds.binding_kind; + poly:bool; + univs:Univ.ContextSet.t; + } | Context of Univ.ContextSet.t let sectab = @@ -424,16 +428,16 @@ let add_section () = (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab let check_same_poly p vars = - let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + let pred = function Context _ -> p = false | Variable {poly} -> p != poly in if List.exists pred vars then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") -let add_section_variable id impl poly ctx = +let add_section_variable ~name ~kind ~poly univs = 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 + sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl let add_section_context ctx = match !sectab with @@ -448,7 +452,7 @@ let is_polymorphic_univ u = let open Univ in List.iter (fun (vars,_,_) -> List.iter (function - | Variable (_,_,poly,(univs,_)) -> + | Variable {poly;univs=(univs,_)} -> if LSet.mem u univs then raise (PolyFound poly) | Context (univs,_) -> if LSet.mem u univs then raise (PolyFound true) @@ -459,12 +463,12 @@ let is_polymorphic_univ u = let extract_hyps (secs,ohyps) = let rec aux = function - | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in - (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r - | (Variable (_,_,poly,ctx)::idl,hyps) -> + (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r + | (Variable {poly;univs}::idl,hyps) -> let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r ctx else r + l, if poly then Univ.ContextSet.union r univs else r | (Context ctx :: idl, hyps) -> let l, r = aux (idl, hyps) in l, Univ.ContextSet.union r ctx @@ -509,11 +513,11 @@ let add_section_replacement f g poly hyps = } in sectab := (vars,f (inst,args) exps, g info abs) :: sl -let add_section_kn poly kn = +let add_section_kn ~poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in add_section_replacement f f poly -let add_section_constant poly kn = +let add_section_constant ~poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in add_section_replacement f f poly @@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr = let section_instance = function | VarRef id -> let eq = function - | Variable (id',_,_,_) -> Names.Id.equal id id' + | Variable {id=id'} -> Names.Id.equal id id' | Context _ -> false in if List.exists eq (pi1 (List.hd !sectab)) diff --git a/library/lib.mli b/library/lib.mli index f6bd61e2da..2cd43b66b3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit -val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Constr.named_context -> unit -val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Constr.named_context -> unit +val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit +val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list val is_polymorphic_univ : Univ.Level.t -> bool diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index 67e1402efd..a27d6450b7 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -548,7 +548,7 @@ let peek_marker s = | ('a'..'z' | 'A'..'Z' | '_') -> ImmediateAsciiIdent | _ -> raise Stream.Failure -let parse_quotation loc s = +let parse_quotation loc bp s = match peek_marker s with | ImmediateAsciiIdent -> let c = Stream.next s in @@ -556,34 +556,42 @@ let parse_quotation loc s = try ident_tail loc (store 0 c) s with Stream.Failure -> raise (Stream.Error "") in - get_buff len + get_buff len, set_loc_pos loc bp (Stream.count s) | Delimited (lenmarker, bmarker, emarker) -> let b = Buffer.create 80 in let commit1 c = Buffer.add_char b c; Stream.junk s in let commit l = List.iter commit1 l in - let rec quotation depth = + let rec quotation loc depth = match Stream.npeek lenmarker s with | l when l = bmarker -> commit l; - quotation (depth + 1) + quotation loc (depth + 1) | l when l = emarker -> commit l; - if depth > 1 then quotation (depth - 1) + if depth > 1 then quotation loc (depth - 1) else loc + | '\n' :: cs -> + commit1 '\n'; + let loc = bump_loc_line_last loc (Stream.count s) in + quotation loc depth | c :: cs -> commit1 c; - quotation depth + quotation loc depth | [] -> raise Stream.Failure in - quotation 0; - Buffer.contents b + let loc = quotation loc 0 in + Buffer.contents b, set_loc_pos loc bp (Stream.count s) -let find_keyword loc id s = +let find_keyword loc id bp s = let tt = ttree_find !token_tree id in match progress_further loc tt.node 0 tt s with | None -> raise Not_found - | Some (c,NoQuotation) -> KEYWORD c - | Some (c,Quotation) -> QUOTATION(c, parse_quotation loc s) + | Some (c,NoQuotation) -> + let ep = Stream.count s in + KEYWORD c, set_loc_pos loc bp ep + | Some (c,Quotation) -> + let txt, loc = parse_quotation loc bp s in + QUOTATION(c, txt), loc let process_sequence loc bp c cs = let rec aux n cs = @@ -599,7 +607,9 @@ let process_chars ~diff_mode loc bp c cs = let ep = Stream.count cs in match t with | Some (t,NoQuotation) -> (KEYWORD t, set_loc_pos loc bp ep) - | Some (c,Quotation) -> (QUOTATION(c, parse_quotation loc cs), set_loc_pos loc bp ep) + | Some (c,Quotation) -> + let txt, loc = parse_quotation loc bp cs in + QUOTATION(c, txt), loc | None -> let ep' = bp + utf8_char_size loc cs c in if diff_mode then begin @@ -623,14 +633,21 @@ let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with Stream.Failure -> raise (Stream.Error "") in let field = get_buff len in - (try find_keyword loc ("."^field) s with Not_found -> FIELD field) + begin try find_keyword loc ("."^field) bp s + with Not_found -> + let ep = Stream.count s in + FIELD field, set_loc_pos loc bp ep end | _ -> match lookup_utf8 loc s with | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in - (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s) + begin try find_keyword loc ("."^field) bp s + with Not_found -> + let ep = Stream.count s in + FIELD field, set_loc_pos loc bp ep end + | AsciiChar | Utf8Token _ | EmptyStream -> + process_chars ~diff_mode loc bp c s (* Parse what follows a question mark *) @@ -664,22 +681,23 @@ let rec next_token ~diff_mode loc s = comm_loc bp; push_char c; next_token ~diff_mode loc s | Some ('.' as c) -> Stream.junk s; - let t = + let t, newloc = try parse_after_dot ~diff_mode loc c bp s with Stream.Failure -> raise (Stream.Error "") in - let ep = Stream.count s in comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) let () = match t with - | KEYWORD ("." | "...") -> - if not (blank_or_eof s) then - err (set_loc_pos loc bp (ep+1)) Undefined_token; - between_commands := true; - | _ -> () + | KEYWORD ("." | "...") -> + if not (blank_or_eof s) then begin + let ep = Stream.count s in + err (set_loc_pos loc bp (ep+1)) Undefined_token + end; + between_commands := true; + | _ -> () in - t, set_loc_pos loc bp ep + t, newloc | Some ('-' | '+' | '*' as c) -> Stream.junk s; let t,new_between_commands = @@ -698,10 +716,12 @@ let rec next_token ~diff_mode loc s = try ident_tail loc (store 0 c) s with Stream.Failure -> raise (Stream.Error "") in - let ep = Stream.count s in let id = get_buff len in comment_stop bp; - (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + begin try find_keyword loc id bp s + with Not_found -> + let ep = Stream.count s in + IDENT id, set_loc_pos loc bp ep end | Some ('0'..'9') -> let n = NumTok.parse s in let ep = Stream.count s in @@ -745,9 +765,11 @@ let rec next_token ~diff_mode loc s = | Utf8Token (st, n) when Unicode.is_valid_ident_initial st -> let len = ident_tail loc (nstore n 0 s) s in let id = get_buff len in - let ep = Stream.count s in comment_stop bp; - (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep + begin try find_keyword loc id bp s + with Not_found -> + let ep = Stream.count s in + IDENT id, set_loc_pos loc bp ep end | AsciiChar | Utf8Token _ -> let t = process_chars ~diff_mode loc bp (Stream.next s) s in comment_stop bp; t diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 72ca5dc8c4..e34150f2b3 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -19,7 +19,8 @@ let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in + let poly = false in + let kind = Decl_kinds.(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 @@ -39,8 +40,8 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in - let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in + let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in + let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end) lemma diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ce3b5a82d6..a904b81d81 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,14 +990,19 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) + let info = Lemmas.Info.make + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) - (mk_equation_id f_id) - Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) - evd - lemma_type + ~name:(mk_equation_id f_id) + ~poly:false + ~info + evd + lemma_type in let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 48eac96ab3..edda2f2eef 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -19,7 +19,6 @@ open Vars open Namegen open Names open Pp -open Entries open Tactics open Context.Rel.Declaration open Indfun_common @@ -310,8 +309,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let hook = DeclareDef.Hook.make (hook new_principle_type) in let lemma = Lemmas.start_lemma - new_princ_name - Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) + ~name:new_princ_name + ~poly:false !evd (EConstr.of_constr new_principle_type) in @@ -325,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - (id,(entry,persistence)), hook + name, entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -371,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (DefinitionEntry ce, + (Declare.DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -380,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook) = + let id,entry,hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -388,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx g_kind + save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -471,7 +470,7 @@ let get_funs_constant mp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -519,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_) = + let _,const,_ = try build_functional_principle evd false first_type @@ -541,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def with Option.IsNone -> (* non recursive definition *) false in - let const = {const with const_entry_opaque = opacity } in + let const = {const with Proof_global.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types then @@ -552,7 +551,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in + let open Proof_global in + let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -576,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def ) ta; - (* If we reach this point, the two principle are not mutually recursive - We fall back to the previous method - *) - let ((_,(const,_)),_) = + (* If we reach this point, the two principle are not mutually recursive + We fall back to the previous method + *) + let _,const,_ = build_functional_principle evd false @@ -596,9 +596,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - const_entry_body = + proof_entry_body = (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - const_entry_type = Some scheme_type + proof_entry_type = Some scheme_type } ) other_fun_princ_types @@ -638,7 +638,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 3f70e870ab..b4f6f92f9c 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -34,7 +34,7 @@ val generate_functional_principle : exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list + (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index ef9d91c7fa..e20d010c71 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl = let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl)))) let classify_funind recsl = match classify_as_Fixpoint recsl with diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 201d953692..bb4e745fe9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1506,7 +1506,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0ecfbacb09..d305a58ccc 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -416,8 +416,10 @@ 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 ComDefinition.do_definition ~program_mode:false - fname - Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl + ~name:fname + ~poly:false + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decl_kinds.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left @@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl; + ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 732a0d818f..254760cb50 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -118,14 +118,13 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) -open Entries -open Decl_kinds open Declare +open DeclareDef let definition_message = Declare.definition_message -let save id const ?hook uctx (locality,_,kind) = - let fix_exn = Future.fix_exn_of const.const_entry_body in +let save id const ?hook uctx locality kind = + let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match locality with | Discharge -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -134,7 +133,7 @@ let save id const ?hook uctx (locality,_,kind) = VarRef id | Global local -> let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id ~local (DefinitionEntry const, k) in + let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in ConstRef kn in DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 8dd990775b..45d332031f 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,10 +44,11 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t - -> Evd.side_effects Entries.definition_entry + -> Evd.side_effects Proof_global.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t - -> Decl_kinds.goal_kind + -> DeclareDef.locality + -> Decl_kinds.goal_object_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e7e523bb32..587e1fc2e8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -786,7 +786,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) + (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) @@ -803,11 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in + let info = Lemmas.Info.make + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in let lemma = Lemmas.start_lemma - lem_id - Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) - !evd - typ in + ~name:lem_id + ~poly:false + ~info + !evd + typ in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma in @@ -865,12 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let lemma = Lemmas.start_lemma lem_id - Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma - (fst lemmas_types_infos.(i)) in + let info = Lemmas.Info.make + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decl_kinds.(Proof Theorem) () in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info + sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by - (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))) lemma) in + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (proving_tac i))) lemma) in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index 8394ac2823..96601785b6 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -15,5 +15,5 @@ val invfun : val derive_correctness : (Evd.evar_map ref -> (Constr.pconstant * Sorts.family) list -> - 'a Entries.definition_entry list) -> + 'a Proof_global.proof_entry list) -> Constr.pconstant list -> Names.inductive list -> unit diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b049e3607c..425e498330 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -17,7 +17,6 @@ open EConstr open Vars open Namegen open Environ -open Entries open Pp open Names open Libnames @@ -1368,10 +1367,13 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type in Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None in + let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma) + () in let lemma = Lemmas.start_lemma - na - Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) - sigma gls_type ~hook:(DeclareDef.Hook.make hook) in + ~name:na + ~poly:false (* FIXME *) ~info + sigma gls_type in let lemma = if Indfun_common.is_strict_tcc () then fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma @@ -1409,9 +1411,13 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let lemma = Lemmas.start_lemma thm_name - (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in + let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in + let lemma = Lemmas.start_lemma ~name:thm_name + ~poly:false (*FIXME*) + ~sign:(Environ.named_context_val env) + ~info + ctx + (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref input_type relation rec_arg_num ))) lemma @@ -1456,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd + let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 49d8ab4e23..1e2b23bf96 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = if poly then ctx else (* This is a global universe context that shouldn't be refreshed at every use of the hint, declare it globally. *) - (Declare.declare_universe_context false ctx; + (Declare.declare_universe_context ~poly:false ctx; Univ.ContextSet.empty) in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4c29d73038..8acb29ba74 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1795,7 +1795,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 atts binders (name,t) fields = - let _id = Classes.new_instance atts.polymorphic + let _id = Classes.new_instance ~poly:atts.polymorphic name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in @@ -1902,7 +1902,7 @@ let declare_projection n instance_id r = Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n - (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1978,8 +1978,8 @@ let add_morphism_as_parameter atts m n : unit = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry + let cst = Declare.declare_constant instance_id + (Declare.ParameterEntry (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in @@ -1994,9 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.t = let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance - in + let poly = atts.polymorphic in + let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function | Globnames.ConstRef cst -> @@ -2007,9 +2006,10 @@ let add_morphism_interactive atts m n : Lemmas.t = | _ -> assert false in let hook = DeclareDef.Hook.make hook in + let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = @@ -2023,7 +2023,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in let _id, lemma = Classes.new_instance_interactive - ~global:atts.global atts.polymorphic + ~global:atts.global ~poly:atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9bbe339770..33798c43c8 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,7 +153,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let () = Declare.declare_universe_context false univs in + let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index edad06777e..f5fffc4c1c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -441,7 +441,7 @@ let coercion_of_reference r = module CoercionPrinting = struct type t = coe_typ - let compare = GlobRef.Ordered.compare + module Set = GlobRef.Set let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2c31aafb70..0daf1ab531 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -182,7 +182,7 @@ module PrintingInductiveMake = end) -> struct type t = inductive - let compare = ind_ord + module Set = Indset let encode = Test.encode let subst subst obj = subst_ind subst obj let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index ed2bb97513..cc9f520583 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -91,7 +91,7 @@ module PrintingInductiveMake : end) -> sig type t = Names.inductive - val compare : t -> t -> int + module Set = Indset val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e8164a14a7..ed60b8274a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -11,7 +11,6 @@ open Pp open Util open Names -open Entries open Environ open Evd @@ -113,21 +112,19 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t (**********************************************************************) (* Shortcut to build a term using tactics *) -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 ImportDefaultBehavior, false, Proof Theorem) typ tac = +let build_constant_by_tactic ~name ctx sign ~poly typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof evd id goal_kind goals in + let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in try let pf, status = by tac pf in let open Proof_global in let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - let univs = UState.demote_seff_univs entry universes in + let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in entry, status, univs | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") @@ -135,13 +132,11 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav let reraise = CErrors.push reraise in iraise reraise -let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = - let id = Id.of_string ("temporary_proof"^string_of_int (next())) in +let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = + let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global ImportDefaultBehavior, poly, Proof Theorem in - let ce, status, univs = - build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let body, eff = Future.force ce.const_entry_body in + let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in + let body, eff = Future.force ce.Proof_global.proof_entry_body in let (cb, ctx) = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 2d3b66ff9f..0626e40047 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -13,7 +13,6 @@ open Names open Constr open Environ -open Decl_kinds (** {6 ... } *) @@ -58,15 +57,23 @@ val use_unification_heuristics : unit -> bool [tac]. The return boolean, if [false] indicates the use of an unsafe tactic. *) -val build_constant_by_tactic : - Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> - EConstr.types -> unit Proofview.tactic -> - Evd.side_effects Entries.definition_entry * bool * - UState.t +val build_constant_by_tactic + : name:Id.t + -> UState.t + -> named_context_val + -> poly:bool + -> EConstr.types + -> unit Proofview.tactic + -> Evd.side_effects Proof_global.proof_entry * bool * UState.t -val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> - EConstr.types -> unit Proofview.tactic -> - constr * bool * UState.t +val build_by_tactic + : ?side_eff:bool + -> env + -> UState.t + -> poly:bool + -> EConstr.types + -> unit Proofview.tactic + -> constr * bool * UState.t val refine_by_tactic : name:Id.t diff --git a/proofs/proof.ml b/proofs/proof.ml index 47502fe402..9f2c90c375 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -118,8 +118,6 @@ type t = (** List of goals that have been shelved. *) ; given_up : Goal.goal list (** List of goals that have been given up *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) ; name : Names.Id.t (** the name of the theorem whose proof is being constructed *) ; poly : bool @@ -290,14 +288,12 @@ let unfocused = is_last_focus end_of_stack_kind let start ~name ~poly sigma goals = let entry, proofview = Proofview.init sigma goals in - let pr = { - proofview; - entry; - focus_stack = [] ; - shelf = [] ; - given_up = []; - initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) + let pr = + { proofview + ; entry + ; focus_stack = [] + ; shelf = [] + ; given_up = [] ; name ; poly } in @@ -305,14 +301,12 @@ let start ~name ~poly sigma goals = let dependent_start ~name ~poly goals = let entry, proofview = Proofview.dependent_init goals in - let pr = { - proofview; - entry; - focus_stack = [] ; - shelf = [] ; - given_up = []; - initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) + let pr = + { proofview + ; entry + ; focus_stack = [] + ; shelf = [] + ; given_up = [] ; name ; poly } in @@ -488,15 +482,13 @@ type data = (** A representation of the shelf *) ; given_up : Evar.t list (** A representation of the given up goals *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) } -let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } = +let data { proofview; focus_stack; entry; shelf; given_up; name; poly } = let goals, sigma = Proofview.proofview proofview in (* spiwack: beware, the bottom of the stack is used by [Proof] internally, and should not be exposed. *) @@ -507,7 +499,7 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; in let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in - { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } + { sigma; goals; entry; stack; shelf; given_up; name; poly } let pr_proof p = let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in diff --git a/proofs/proof.mli b/proofs/proof.mli index 6ef34eed80..7e535a258c 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -47,8 +47,6 @@ type data = (** A representation of the shelf *) ; given_up : Evar.t list (** A representation of the given up goals *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool; diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0b1a7fcc03..ab8d87c100 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -24,28 +24,44 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) -type proof_object = { - id : Names.Id.t; - entries : Evd.side_effects Entries.definition_entry list; - persistence : Decl_kinds.goal_kind; - universes: UState.t; +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; } +type proof_object = + { name : Names.Id.t + ; entries : Evd.side_effects proof_entry list + ; poly : bool + ; universes: UState.t + ; udecl : UState.universe_decl + } + type opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option ; section_vars : Constr.named_context option ; proof : Proof.t - ; universe_decl: UState.universe_decl - ; strength : Decl_kinds.goal_kind + ; udecl: UState.universe_decl + (** Initial universe declarations *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) } (*** Proof Global manipulation ***) let get_proof ps = ps.proof let get_proof_name ps = (Proof.data ps.proof).Proof.name -let get_persistence ps = ps.strength + +let get_initial_euctx ps = ps.initial_euctx let map_proof f p = { p with proof = f p.proof } let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res @@ -56,7 +72,8 @@ let map_fold_proof_endline f ps = | None -> Proofview.tclUNIT () | Some tac -> let open Geninterp in - let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in + let {Proof.poly} = Proof.data ps.proof in + let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in let tac = Geninterp.interp tag ist tac in Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) @@ -71,32 +88,33 @@ let compact_the_proof pf = map_proof Proof.compact pf let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } -(** [start_proof sigma id pl str goals] starts a proof of name - [id] with goals [goals] (a list of pairs of environment and - conclusion); [str] describes what kind of theorem/definition this - is (spiwack: for potential printing, I believe is used only by - closing commands and the xml plugin); [terminator] is used at the - end of the proof to close the proof. The proof is started in the - evar map [sigma] (which can typically contain universe - constraints), and with universe bindings pl. *) -let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals = - { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion). The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +let start_proof ~name ~udecl ~poly sigma goals = + let proof = Proof.start ~name ~poly sigma goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof ; endline_tactic = None ; section_vars = None - ; universe_decl = pl - ; strength = kind + ; udecl + ; initial_euctx } -let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals = - { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals +let start_dependent_proof ~name ~udecl ~poly goals = + let proof = Proof.dependent_start ~name ~poly goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof ; endline_tactic = None ; section_vars = None - ; universe_decl = pl - ; strength = kind + ; udecl + ; initial_euctx } let get_used_variables pf = pf.section_vars -let get_universe_decl pf = pf.universe_decl +let get_universe_decl pf = pf.udecl let set_used_variables ps l = let open Context.Named.Declaration in @@ -147,8 +165,8 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; universe_decl; strength } = ps in - let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in + let { section_vars; proof; udecl; initial_euctx } = ps in + let Proof.{ name; poly; entry } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx @@ -182,13 +200,13 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now 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 = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body universe_decl in + let univs = UState.check_mono_univ_decl ctx_body udecl in (initunivs, typ), ((body, univs), eff) else if poly && opaque && private_poly_univs () then let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let universes = UState.restrict universes used_univs in let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus universe_decl in + let udecl = UState.check_univ_decl ~poly typus udecl in let ubody = Univ.ContextSet.diff (UState.context_set universes) (UState.context_set typus) @@ -202,7 +220,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now TODO: check if restrict is really necessary now. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ~poly ctx universe_decl in + let univs = UState.check_univ_decl ~poly ctx udecl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in fun t p -> Future.split2 (Future.chain p (make_body t)) @@ -224,25 +242,24 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (Vars.universes_of_constr pt) in let univs = UState.restrict univs used_univs in - let univs = UState.check_mono_univ_decl univs universe_decl in + let univs = UState.check_mono_univ_decl univs udecl in (pt,univs),eff) in 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 - {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 = opaque; - const_entry_universes = univs; } + { + proof_entry_body = body; + proof_entry_secctx = section_vars; + proof_entry_feedback = feedback_id; + proof_entry_type = Some typ; + proof_entry_inline_code = false; + proof_entry_opaque = opaque; + proof_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { id = name; entries = entries; persistence = strength; - universes } + { name; entries = entries; poly; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 15685bd9b6..54d5c2087a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -17,12 +17,14 @@ type t (* Should be moved into a proper view *) val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t -val get_persistence : t -> Decl_kinds.goal_kind val get_used_variables : t -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : t -> UState.universe_decl +(** Get initial universe state *) +val get_initial_euctx : t -> UState.t + val compact_the_proof : t -> t (** When a proof is closed, it is reified into a [proof_object], where @@ -31,37 +33,54 @@ val compact_the_proof : t -> t function which takes a [proof_object] together with a [proof_end] (i.e. an proof ending command) and registers the appropriate values. *) -type proof_object = { - id : Names.Id.t; - entries : Evd.side_effects Entries.definition_entry list; - persistence : Decl_kinds.goal_kind; - universes: UState.t; +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; } +(** When a proof is closed, it is reified into a [proof_object] *) +type proof_object = + { name : Names.Id.t + (** name of the proof *) + ; entries : Evd.side_effects proof_entry list + (** list of the proof terms (in a form suitable for definitions). *) + ; poly : bool + (** polymorphic status *) + ; universes: UState.t + (** universe state *) + ; udecl : UState.universe_decl + (** universe declaration *) + } + type opacity_flag = Opaque | Transparent -(** [start_proof id str pl goals] starts a proof of name - [id] with goals [goals] (a list of pairs of environment and - conclusion); [str] describes what kind of theorem/definition this - is; [terminator] is used at the end of the proof to close the proof - (e.g. to declare the built constructions as a coercion or a setoid - morphism). The proof is started in the evar map [sigma] (which can - typically contain universe constraints), and with universe bindings - pl. *) +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion); [poly] determines if the proof is universe + polymorphic. The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) val start_proof - : Evd.evar_map - -> Names.Id.t - -> ?pl:UState.universe_decl - -> Decl_kinds.goal_kind + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof - : Names.Id.t - -> ?pl:UState.universe_decl - -> Decl_kinds.goal_kind + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool -> Proofview.telescope -> t diff --git a/stm/stm.ml b/stm/stm.ml index 89d95d0cc9..28d5447c44 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1537,7 +1537,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, Lemmas.default_info) st + ~proof:(pobject, Lemmas.Info.make ()) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,7 +1677,7 @@ end = struct (* {{{ *) let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm, Lemmas.default_info in + let proof = pterm, Lemmas.Info.make () in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1735,7 +1735,7 @@ end = struct (* {{{ *) | `OK (po,_) -> let con = Nametab.locate_constant - (Libnames.qualid_of_ident po.Proof_global.id) in + (Libnames.qualid_of_ident po.Proof_global.name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with | Declarations.OpaqueDef o -> o diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4e7f6a0ac6..aaba36287a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -87,7 +87,7 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = Some "curly" } (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> + | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) | VernacDefinition (_,({v=i},_),ProveBody _) -> @@ -102,7 +102,7 @@ let classify_vernac e = | VernacFixpoint (discharge,l) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -114,7 +114,7 @@ let classify_vernac e = | VernacCoFixpoint (discharge,l) -> let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 8f66032873..662a2fc22c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -70,26 +70,26 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with + let open Proof_global in + let typ = match const.proof_entry_type with | None -> assert false | Some t -> t in (* The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.const_entry_body) in - let ((body, uctx), eff) = Future.force const.const_entry_body in + let () = assert (Future.is_over const.proof_entry_body) in + let ((body, uctx), eff) = Future.force const.proof_entry_body in let (body, typ, ctx) = decompose (List.length sign) body typ [] in let (body, typ, args) = shrink ctx sign body typ [] in let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; + proof_entry_body = Future.from_val ((body, uctx), eff); + proof_entry_type = Some typ; } in (const, args) -let name_op_to_name ~name_op ~name ~goal_kind suffix = +let name_op_to_name ~name_op ~name suffix = match name_op with - | Some s -> s, goal_kind - | None -> Nameops.add_suffix name suffix, goal_kind + | Some s -> s + | None -> Nameops.add_suffix name suffix let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let open Tacticals.New in @@ -102,10 +102,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let goal_kind, suffix = if opaque - then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof" - else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in - let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in + let suffix = if opaque + then "_subproof" + else "_subterm" in + let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -121,7 +121,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, Environ.empty_named_context_val) in - let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in + let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in let concl = match goal_type with | None -> Proofview.Goal.concl gl | Some ty -> ty in @@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -152,29 +152,29 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl + Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Entries.const_entry_universes with + let inst = match const.Proof_global.proof_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Entries.(snd (Future.force const.const_entry_body)) in + Proof_global.(snd (Future.force const.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index c474a01d1c..e278729f89 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Entries.definition_entry - -> 'c Entries.definition_entry * Constr.t list + -> 'c Proof_global.proof_entry + -> 'c Proof_global.proof_entry * Constr.t list diff --git a/tactics/auto.ml b/tactics/auto.ml index 339d4de2a0..499e7a63d7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -69,7 +69,7 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv poly (c, _, ctx) clenv gl = +let connect_hint_clenv ~poly (c, _, ctx) clenv gl = (* [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) @@ -95,22 +95,22 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c -let unify_resolve poly flags ((c : raw_hint), clenv) = +let unify_resolve ~poly flags ((c : raw_hint), clenv) = Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv poly c clenv gl in + let clenv, c = connect_hint_clenv ~poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine clenv end -let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h +let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h -let unify_resolve_gen poly = function +let unify_resolve_gen ~poly = function | None -> unify_resolve_nodelta poly - | Some flags -> unify_resolve poly flags + | Some flags -> unify_resolve ~poly flags let exact poly (c,clenv) = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly c clenv gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (exact_check c) @@ -378,12 +378,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function - | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) + | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl) | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf")) | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN - (unify_resolve_gen poly flags (c,cl)) + (unify_resolve_gen ~poly flags (c,cl)) (* With "(debug) trivial", we shouldn't end here, and with "debug auto" we don't display the details of inner trivial *) (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db) diff --git a/tactics/auto.mli b/tactics/auto.mli index a834b4b12d..5ae63be539 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -14,7 +14,6 @@ open Names open EConstr open Clenv open Pattern -open Decl_kinds open Hints open Tactypes @@ -24,11 +23,11 @@ val default_search_depth : int ref val auto_flags_of_state : TransparentState.t -> Unification.unify_flags -val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - Proofview.Goal.t -> clausenv * constr +val connect_hint_clenv + : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic +val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b0fb47726a..303ddacb67 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -204,11 +204,11 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = end let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> - let clenv', c = connect_hint_clenv poly c clenv gls in + let clenv', c = connect_hint_clenv ~poly c clenv gls in clenv_unique_resolver_tac true ~flags clenv' end let unify_resolve poly flags = begin fun gls (c,_,clenv) -> - let clenv', _ = connect_hint_clenv poly c clenv gls in + let clenv', _ = connect_hint_clenv ~poly c clenv gls in clenv_unique_resolver_tac false ~flags clenv' end @@ -536,7 +536,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (List.map_append (fun (path,info,c) -> make_resolves env sigma ~name:(PathHints path) - (true,false,not !Flags.quiet) info false + (true,false,not !Flags.quiet) info ~poly:false (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) hints) else [] @@ -544,8 +544,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (hints @ List.map_filter (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) with Failure _ | UserError _ -> None) - [make_exact_entry ~name env sigma pri false; - make_apply_entry ~name env sigma flags pri false]) + [make_exact_entry ~name env sigma pri ~poly:false; + make_apply_entry ~name env sigma flags pri ~poly:false]) else [] let make_hints g (modes,st) only_classes sign = diff --git a/interp/declare.ml b/tactics/declare.ml index 77313a54de..668026500d 100644 --- a/interp/declare.ml +++ b/tactics/declare.ml @@ -27,11 +27,7 @@ open Cooking open Decls open Decl_kinds -(** flag for internal message display *) -type internal_flag = - | UserAutomaticRequest (* kernel action, a message is displayed *) - | InternalTacticRequest (* kernel action, no message is displayed *) - | UserIndividualRequest (* user action, a message is displayed *) +type import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -42,6 +38,11 @@ type constant_obj = { cst_locl : import_status; } +type 'a constant_entry = + | DefinitionEntry of 'a Proof_global.proof_entry + | ParameterEntry of parameter_entry + | PrimitiveEntry of primitive_entry + type constant_declaration = Evd.side_effects constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) @@ -91,7 +92,7 @@ let cache_constant ((sp,kn), obj) = assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in - add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; + add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; add_constant_kind (Constant.make1 kn) obj.cst_kind let discharge_constant ((sp, kn), obj) = @@ -146,13 +147,40 @@ let register_side_effect (c, role) = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - const_entry_secctx = None; - const_entry_type = types; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} + let open Proof_global in + { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); + proof_entry_secctx = None; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = None; + proof_entry_inline_code = inline} + +let cast_proof_entry e = + let open Proof_global in + let (body, ctx), () = Future.force e.proof_entry_body in + { + const_entry_body = (body, ctx); + const_entry_secctx = e.proof_entry_secctx; + const_entry_feedback = e.proof_entry_feedback; + const_entry_type = e.proof_entry_type; + const_entry_universes = e.proof_entry_universes; + const_entry_inline_code = e.proof_entry_inline_code; + } + +let cast_opaque_proof_entry e = + let open Proof_global in + let typ = match e.proof_entry_type with + | None -> assert false + | Some typ -> typ + in + { + opaque_entry_body = e.proof_entry_body; + opaque_entry_secctx = e.proof_entry_secctx; + opaque_entry_feedback = e.proof_entry_feedback; + opaque_entry_type = typ; + opaque_entry_universes = e.proof_entry_universes; + } let get_roles export eff = let map c = @@ -161,9 +189,10 @@ let get_roles export eff = in List.map map export -let define_constant ~side_effect ?(export_seff=false) id cd = +let define_constant ~side_effect id cd = + let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) - let is_poly de = match de.const_entry_universes with + let is_poly de = match de.proof_entry_universes with | Monomorphic_entry _ -> false | Polymorphic_entry _ -> true in @@ -171,35 +200,42 @@ let define_constant ~side_effect ?(export_seff=false) id cd = let export, decl = (* We deal with side effects *) match cd with | DefinitionEntry de when - export_seff || - not de.const_entry_opaque || + not de.proof_entry_opaque || is_poly de -> (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.const_entry_body in + let body, eff = Future.force de.proof_entry_body in let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in let export = get_roles export eff in - let de = { de with const_entry_body = Future.from_val (body, ()) } in - export, ConstantEntry (PureEntry, DefinitionEntry de) + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let cd = match de.proof_entry_opaque with + | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de) + | false -> Entries.DefinitionEntry (cast_proof_entry de) + in + export, ConstantEntry (PureEntry, cd) | DefinitionEntry de -> + let () = assert (de.proof_entry_opaque) in let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.const_entry_body map in - let de = { de with const_entry_body = body } in - [], ConstantEntry (EffectEntry, DefinitionEntry de) - | ParameterEntry _ | PrimitiveEntry _ as cd -> - [], ConstantEntry (PureEntry, cd) + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_opaque_proof_entry de in + [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) + | ParameterEntry e -> + [], ConstantEntry (PureEntry, Entries.ParameterEntry e) + | PrimitiveEntry e -> + [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) in let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export -let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = let () = check_exists id in - let kn, (), export = define_constant ~side_effect:PureEntry ~export_seff id cd in + let kn, (), export = define_constant ~side_effect:PureEntry id cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) = let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in @@ -210,43 +246,44 @@ let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = I let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition ?(internal=UserIndividualRequest) +let declare_definition ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body in - declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + declare_constant ~local id + (DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) type section_variable_entry = - | SectionLocalDef of Evd.side_effects definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(p,d,mk)) -> + | Inr (id,(path,d,kind)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then alreadydeclared (Id.print 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,opaque,poly,univs = match d with (* Fails if not well-typed *) + | SectionLocalAssum {typ;univs;poly;impl} -> + let () = Global.push_named_assum ((id,typ,poly),univs) in let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx + impl, true, poly, univs | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.const_entry_body in + let open Proof_global in + let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in let () = List.iter register_side_effect eff in - let poly, univs = match de.const_entry_universes with + let poly, univs = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in @@ -256,16 +293,16 @@ let cache_variable ((sp,_),o) = let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; - secdef_secctx = de.const_entry_secctx; - secdef_feedback = de.const_entry_feedback; - secdef_type = de.const_entry_type; + secdef_secctx = de.proof_entry_secctx; + secdef_feedback = de.proof_entry_feedback; + secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (id, se) in - Explicit, de.const_entry_opaque, + Explicit, de.proof_entry_opaque, poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; - add_variable_data id (p,opaq,ctx,poly,mk) + add_section_variable ~name:id ~kind:impl ~poly univs; + add_variable_data id {path;opaque;univs;poly;kind} let discharge_variable (_,o) = match o with | Inr (id,_) -> @@ -303,18 +340,18 @@ let inductive_names sp kn mie = let names, _ = List.fold_left (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) ind.mind_entry_consnames in + let sp = Libnames.make_path dp ind.mind_entry_typename + in + ((sp, IndRef ind_p) :: names, n+1)) ([], 0) mie.mind_entry_inds in names @@ -333,7 +370,7 @@ let cache_inductive ((sp,kn),mie) = let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in - add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; + add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names let discharge_inductive ((sp,kn),mie) = @@ -448,15 +485,15 @@ let fixpoint_message indexes l = | [] -> anomaly (Pp.str "no recursive definition.") | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prvect_with_sep pr_comma pr_rank a ++ + str " arguments)" + | None -> mt ())) let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with @@ -484,7 +521,7 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj = ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) ~discharge:(fun (_, x) -> Some x) -let declare_universe_context poly ctx = +let declare_universe_context ~poly ctx = if poly then (Global.push_context_set true ctx; Lib.add_section_context ctx) else @@ -564,7 +601,7 @@ let declare_univ_binders gr pl = in Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) -let do_universe poly l = +let do_universe ~poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then @@ -575,11 +612,11 @@ let do_universe poly l = let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in - let () = declare_universe_context poly ctx in + let () = declare_universe_context ~poly ctx in let src = if poly then BoundUniv else UnqualifiedUniv in Lib.add_anonymous_leaf (input_univ_names (src, l)) -let do_constraint poly l = +let do_constraint ~poly l = let open Univ in let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in @@ -606,4 +643,4 @@ let do_constraint poly l = Constraint.empty l in let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context poly uctx + declare_universe_context ~poly uctx diff --git a/interp/declare.mli b/tactics/declare.mli index 0f64235048..1f72fff30e 100644 --- a/interp/declare.mli +++ b/tactics/declare.mli @@ -23,28 +23,30 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of Evd.side_effects definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) + | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + +type 'a constant_entry = + | DefinitionEntry of 'a Proof_global.proof_entry + | ParameterEntry of parameter_entry + | PrimitiveEntry of primitive_entry type variable_declaration = DirPath.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> Libobject.object_name -(** Declaration of global constructions +(** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) type constant_declaration = Evd.side_effects constant_entry * logical_kind -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - (* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects definition_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry + +type import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -53,13 +55,13 @@ val definition_entry : ?fix_exn:Future.fix_exn -> internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t + ?local:import_status -> Id.t -> constant_declaration -> Constant.t val declare_private_constant : - ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects -val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> +val declare_definition : + ?opaque:bool -> ?kind:definition_object_kind -> ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t @@ -87,7 +89,7 @@ val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit -val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit +val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit -val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit +val do_universe : poly:bool -> lident list -> unit +val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit diff --git a/tactics/eauto.ml b/tactics/eauto.ml index ac6253cf40..cc3e78f3b8 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -113,7 +113,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) let unify_e_resolve poly flags (c,clenv) = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly c clenv gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) @@ -131,7 +131,7 @@ let hintmap_of sigma secvars hdc concl = let e_exact poly flags (c,clenv) = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly c clenv gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (e_give_exact c) @@ -168,7 +168,7 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl = in (b, let tac = function - | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl) | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> diff --git a/tactics/hints.ml b/tactics/hints.ml index e824c4bd64..3a3a6b94dc 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -27,7 +27,6 @@ open Smartlocate open Termops open Inductiveops open Typing -open Decl_kinds open Typeclasses open Pattern open Patternops @@ -142,15 +141,22 @@ type raw_hint = constr * types * Univ.ContextSet.t type hint = (raw_hint * clausenv) hint_ast with_uid -type 'a with_metadata = { - pri : int; (* A number lower is higher priority *) - poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) - pat : constr_pattern option; (* A pattern for the concl of the Goal *) - name : hints_path_atom; (* A potential name to refer to the hint *) - db : string option; (** The database from which the hint comes *) - secvars : Id.Pred.t; (* The set of section variables the hint depends on *) - code : 'a; (* the tactic to apply when the concl matches pat *) -} +type 'a with_metadata = + { pri : int + (** A number lower is higher priority *) + ; poly : bool + (** Is the hint polymorpic and hence should be refreshed at each application *) + ; pat : constr_pattern option + (** A pattern for the concl of the Goal *) + ; name : hints_path_atom + (** A potential name to refer to the hint *) + ; db : string option + (** The database from which the hint comes *) + ; secvars : Id.Pred.t + (** The set of section variables the hint depends on *) + ; code : 'a + (** the tactic to apply when the concl matches pat *) + } type full_hint = hint with_metadata @@ -792,7 +798,7 @@ let secvars_of_constr env sigma c = let secvars_of_global env gr = secvars_of_idset (vars_of_global env gr) -let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = +let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = let secvars = secvars_of_constr env sigma c in let cty = strip_outer_cast sigma cty in match EConstr.kind sigma cty with @@ -813,7 +819,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = db = None; secvars; code = with_uid (Give_exact (c, cty, ctx)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match EConstr.kind sigma cty with | Prod _ -> @@ -887,18 +893,18 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Declare.declare_universe_context false ctx; + Declare.declare_universe_context ~poly:false ctx; (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info poly ?name cr = +let make_resolves env sigma flags info ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply - [make_exact_entry env sigma info poly ?name; - make_apply_entry env sigma flags info poly ?name] + [make_exact_entry env sigma info ~poly ?name; + make_apply_entry env sigma flags info ~poly ?name] in if List.is_empty ents then user_err ~hdr:"Hint" @@ -912,7 +918,7 @@ let make_resolve_hyp env sigma decl = let hname = NamedDecl.get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) empty_hint_info false + [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false ~name:(PathHints [VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with @@ -1178,7 +1184,7 @@ let add_resolves env sigma clist local dbnames = let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> make_resolves env sigma (true,hnf,not !Flags.quiet) - pri poly ~name:path gr) clist) + pri ~poly ~name:path gr) clist) in let hint = make_hint ~local dbname (AddHints r) in Lib.add_anonymous_leaf (inAutoHint hint)) @@ -1238,8 +1244,8 @@ type hnf = bool type nonrec hint_info = hint_info type hints_entry = - | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list - | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list + | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list + | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool @@ -1286,7 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Declare.declare_universe_context false diff; + else (Declare.declare_universe_context ~poly:false diff; IsConstr (c', Univ.ContextSet.empty)) let project_hint ~poly pri l2r r = @@ -1314,11 +1320,11 @@ let project_hint ~poly pri l2r r = in let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let c = Declare.declare_definition id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) -let interp_hints poly = +let interp_hints ~poly = fun h -> let env = Global.env () in let sigma = Evd.from_env env in @@ -1417,7 +1423,7 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems + make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/hints.mli b/tactics/hints.mli index 839ef31189..4c82a068b1 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -12,7 +12,6 @@ open Util open Names open EConstr open Environ -open Decl_kinds open Evd open Tactypes open Clenv @@ -54,15 +53,22 @@ type 'a hints_path_atom_gen = type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string -type 'a with_metadata = private { - pri : int; (** A number between 0 and 4, 4 = lower priority *) - poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) - pat : constr_pattern option; (** A pattern for the concl of the Goal *) - name : hints_path_atom; (** A potential name to refer to the hint *) - db : hint_db_name option; - secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *) - code : 'a; (** the tactic to apply when the concl matches pat *) -} +type 'a with_metadata = private + { pri : int + (** A number lower is higher priority *) + ; poly : bool + (** Is the hint polymorpic and hence should be refreshed at each application *) + ; pat : constr_pattern option + (** A pattern for the concl of the Goal *) + ; name : hints_path_atom + (** A potential name to refer to the hint *) + ; db : string option + (** The database from which the hint comes *) + ; secvars : Id.Pred.t + (** The set of section variables the hint depends on *) + ; code : 'a + (** the tactic to apply when the concl matches pat *) + } type full_hint = hint with_metadata @@ -176,9 +182,8 @@ type hint_term = | IsConstr of constr * Univ.ContextSet.t type hints_entry = - | HintsResolveEntry of - (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list - | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list + | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list + | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool @@ -202,7 +207,7 @@ val current_db_names : unit -> String.Set.t val current_pure_db : unit -> hint_db list -val interp_hints : polymorphic -> hints_expr -> hints_entry +val interp_hints : poly:bool -> hints_expr -> hints_entry val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit @@ -219,7 +224,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> [hint_pattern] is the hint's desired pattern, it is inferred if not specified *) -val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom -> +val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom -> (constr * types * Univ.ContextSet.t) -> hint_entry (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. @@ -237,7 +242,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint *) val make_apply_entry : - env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> + env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom -> (constr * types * Univ.ContextSet.t) -> hint_entry (** A constr which is Hint'ed will be: @@ -248,7 +253,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> + env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 9b8ad8191e..e01f3ab961 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,14 +22,18 @@ open Declarations open Constr open CErrors open Util -open Declare -open Entries open Decl_kinds open Pp (**********************************************************************) (* Registering schemes in the environment *) +(** flag for internal message display *) +type internal_flag = + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) + type mutual_scheme_object_function = internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = @@ -122,20 +126,20 @@ let define internal role id c poly univs = let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in let entry = { - const_entry_body = + Proof_global.proof_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Evd.empty_side_effects); - const_entry_secctx = None; - const_entry_type = None; - const_entry_universes = univs; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; + proof_entry_secctx = None; + proof_entry_type = None; + proof_entry_universes = univs; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None; } in - let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | InternalTacticRequest -> () - | _-> definition_message id + | _-> Declare.definition_message id in kn, eff diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 109fb64b2b..17e9c7ef42 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -10,7 +10,6 @@ open Names open Constr -open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -21,6 +20,11 @@ type mutual type individual type 'a scheme_kind +type internal_flag = + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest + type mutual_scheme_object_function = internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 61608c577c..e242b10d33 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -22,11 +22,9 @@ open Namegen open Evd open Printer open Reductionops -open Entries open Inductiveops open Tacmach.New open Clenv -open Declare open Tacticals.New open Tactics open Decl_kinds @@ -237,8 +235,8 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.univ_entry ~poly sigma in - let entry = definition_entry ~univs invProof in - let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in + let entry = Declare.definition_entry ~univs invProof in + let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in () (* inv_op = Inv (derives de complete inv. lemma) diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 1861c5b99b..6dd749aa0d 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +Declare Dnet Dn Btermdn diff --git a/test-suite/Makefile b/test-suite/Makefile index a48a71c159..c0bdb29fab 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -97,7 +97,7 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed INTERACTIVE := interactive UNIT_TESTS := unit-tests -VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ +VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr arithmetic ltac2 @@ -164,6 +164,7 @@ summary: $(call summary_dir, "Failure tests", failure); \ $(call summary_dir, "Bugs tests", bugs); \ $(call summary_dir, "Output tests", output); \ + $(call summary_dir, "Output tests with coqtop", output-coqtop); \ $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \ $(call summary_dir, "Interactive tests", interactive); \ $(call summary_dir, "Micromega tests", micromega); \ @@ -299,6 +300,11 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test +unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK) + $(SHOW) 'TEST $<' + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \ + -I unit-tests/src $(UNIT_LINK) $< -o $<.test; + $(HIDE)./$<.test ####################################################################### # Other generic tests @@ -420,8 +426,32 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) fi; \ } > "$@" +$(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + $(coqtop) < "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + | grep -v "Welcome to Coq" \ + | grep -v "\[Loading ML file" \ + | grep -v "Skipping rcfile loading" \ + | grep -v "^<W>" \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + rm $$output; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ + fi; \ + } > "$@" + .PHONY: approve-output -approve-output: output +approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ diff --git a/test-suite/README.md b/test-suite/README.md index e81da0830f..a2d5905710 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -76,7 +76,9 @@ The error "(bug seems to be opened, please check)" when running compile. There are also output tests in [`output`](output) which consist of a `.v` file -and a `.out` file with the expected output. +and a `.out` file with the expected output. Output tests in this directory are +run with coqc in -test-mode. Output tests in [`output-coqtop`](output-coqtop) +work the same way, but are run with coqtop. There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as diff --git a/test-suite/bugs/closed/bug_10161.v b/test-suite/bugs/closed/bug_10161.v new file mode 100644 index 0000000000..3d262b89fe --- /dev/null +++ b/test-suite/bugs/closed/bug_10161.v @@ -0,0 +1,8 @@ +Inductive SwitchT (A : Type) : Type := +| switchT : forall T, SwitchT T -> SwitchT A. + +Set Printing Universes. + +Fail Inductive UseSwitchT := +| useSwitchT : SwitchT UseSwitchT -> UseSwitchT. +(* used to stack overflow, should be univ inconsistency cannot satisfy u = u+1 *) diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v index 489fa638e4..9c11d19c27 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -27,6 +27,19 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay). Fail Ltac2 pose1 (v : constr) := ltac1:(pose $v). +(** Variables explicitly crossing the boundary must satisfy typing properties *) +Goal True. +Proof. +(* Wrong type *) +Fail ltac1:(x |- idtac) 0. +(* OK, and runtime has access to variable *) +ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)). + +(* Same for ltac1val *) +Fail Ltac1.run (ltac1val:(x |- idtac) 0). +Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). +Abort. + (** Test calls to Ltac2 from Ltac1 *) Set Default Proof Mode "Classic". diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index adabb7a0a0..8447cf10db 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -11,7 +11,7 @@ let evil t f = let te = Declare.definition_entry ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in - let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry @@ -19,4 +19,4 @@ let evil t f = ~types:(Term.mkArrowR tc tu) (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1)) in - ignore (Declare.declare_constant f (DefinitionEntry fe, k)) + ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k)) diff --git a/test-suite/misc/quotation_token.sh b/test-suite/misc/quotation_token.sh new file mode 100755 index 0000000000..6357e8d7ce --- /dev/null +++ b/test-suite/misc/quotation_token.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/quotation_token/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/quotation_plugin.cma + +TMP=`mktemp` + +if make > $TMP 2>&1; then + echo "should fail" + rm $TMP + exit 1 +fi + +if grep "File.*quotation.v., line 12, characters 6-30" $TMP; then + rm $TMP + exit 0 +else + echo "wong loc: `grep File.*quotation.v $TMP`" + rm $TMP + exit 1 +fi diff --git a/test-suite/misc/quotation_token/.gitignore b/test-suite/misc/quotation_token/.gitignore new file mode 100644 index 0000000000..18da256f3e --- /dev/null +++ b/test-suite/misc/quotation_token/.gitignore @@ -0,0 +1,2 @@ +/Makefile* +/src/quotation.ml diff --git a/test-suite/misc/quotation_token/_CoqProject b/test-suite/misc/quotation_token/_CoqProject new file mode 100644 index 0000000000..1b3e7c6399 --- /dev/null +++ b/test-suite/misc/quotation_token/_CoqProject @@ -0,0 +1,6 @@ +-Q theories Quotation +-I src + +src/quotation.mlg +src/quotation_plugin.mlpack +theories/quotation.v diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg new file mode 100644 index 0000000000..961b170a0d --- /dev/null +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -0,0 +1,12 @@ +{ +open Pcoq.Constr +} +GRAMMAR EXTEND Gram + GLOBAL: operconstr; + + operconstr: LEVEL "0" + [ [ s = QUOTATION "foobar:" -> + { + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + ; +END diff --git a/test-suite/misc/quotation_token/src/quotation_plugin.mlpack b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack new file mode 100644 index 0000000000..b372b94b30 --- /dev/null +++ b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack @@ -0,0 +1 @@ +Quotation diff --git a/test-suite/misc/quotation_token/theories/quotation.v b/test-suite/misc/quotation_token/theories/quotation.v new file mode 100644 index 0000000000..66326e89c1 --- /dev/null +++ b/test-suite/misc/quotation_token/theories/quotation.v @@ -0,0 +1,13 @@ + +Declare ML Module "quotation_plugin". + +Definition x := foobar:{{ hello + there +}}. + +Definition y := foobar:{{ another + multi line + thing +}}. +Check foobar:{{ oops + ips }} y. diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml new file mode 100644 index 0000000000..3082acdf1f --- /dev/null +++ b/test-suite/unit-tests/ide/lex_tests.ml @@ -0,0 +1,50 @@ +open Utest + +let log_out_ch = open_log_out_ch __FILE__ + +let lex s = + let n = + let last = String.length s - 1 in + if s.[last] = '.' then Some last else None in + let stop = ref None in + let f i _ = assert(!stop = None); stop := Some i in + begin try Coq_lex.delimit_sentences f s + with Coq_lex.Unterminated -> () end; + if n <> !stop then begin + let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in + Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop) + end; + n = !stop + +let i2s i = "test at line: " ^ string_of_int i + +let tests = [ + + mk_bool_test (i2s __LINE__) "no quotation" @@ lex + "foo.+1 bar." + ; + mk_bool_test (i2s __LINE__) "quotation" @@ lex + "foo constr:(xxx)." + ; + mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex + "foo constr:(xxx. yyy)." + ; + mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex + "foo constr:((xxx. (foo.+1 ) \")\" yyy))." + ; + mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex + "foo constr:[xxx. (foo.+1 ) \")\" yyy]." + ; + mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex + "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]." + ; + mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex + "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]." + ; + mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex + "bar:{{ foo {{ hello. }} }}." + ; + +] + +let _ = run_tests __FILE__ log_out_ch tests diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 3bed8c1e40..20a8581d46 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -217,8 +217,7 @@ End BASES. Local Notation "v [@ p ]" := (nth v p) (at level 1). Section ITERATORS. -(** * Here are special non dependent useful instantiation of induction -schemes *) +(** * Here are special non dependent useful instantiation of induction schemes *) (** Uniform application on the arguments of the vector *) Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n := diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v new file mode 100755 index 0000000000..d808436e13 --- /dev/null +++ b/user-contrib/Ltac2/Bool.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Ltac2.Init. + +Ltac2 and x y := + match x with + | true => y + | false => false + end. + +Ltac2 or x y := + match x with + | true => true + | false => y + end. + +Ltac2 impl x y := + match x with + | true => y + | false => true + end. + +Ltac2 neg x := + match x with + | true => false + | false => true + end. + +Ltac2 xor x y := + match x with + | true + => match y with + | true => false + | false => true + end + | false + => match y with + | true => true + | false => false + end + end. + +Ltac2 eq x y := + match x with + | true + => match y with + | true => true + | false => false + end + | false + => match y with + | true => false + | false => true + end + end. diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v index 19530b224b..8f35e1a279 100644 --- a/user-contrib/Ltac2/Control.v +++ b/user-contrib/Ltac2/Control.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import Ltac2.Init. +Require Ltac2.Message. (** Panic *) @@ -76,3 +77,28 @@ Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "a Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt". (** For internal use. *) + +(** Assertions throwing exceptions and short form throws *) + +Ltac2 throw_invalid_argument (msg : string) := + Control.throw (Invalid_argument (Some (Message.of_string msg))). + +Ltac2 throw_out_of_bounds (msg : string) := + Control.throw (Out_of_bounds (Some (Message.of_string msg))). + +Ltac2 assert_valid_argument (msg : string) (test : bool) := + match test with + | true => () + | false => throw_invalid_argument msg + end. + +Ltac2 assert_bounds (msg : string) (test : bool) := + match test with + | true => () + | false => throw_out_of_bounds msg + end. + +(** Short form backtracks *) + +Ltac2 backtrack_tactic_failure (msg : string) := + Control.zero (Tactic_failure (Some (Message.of_string msg))). diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 93468f302e..88454ff2fb 100644..100755 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -53,7 +53,7 @@ Ltac2 Type err. Ltac2 Type exn ::= [ Internal (err) ]. (** Wrapper around the errors raised by Coq implementation. *) -Ltac2 Type exn ::= [ Out_of_bounds ]. +Ltac2 Type exn ::= [ Out_of_bounds (message option) ]. (** Used for bound checking, e.g. with String and Array. *) Ltac2 Type exn ::= [ Not_focussed ]. @@ -65,8 +65,14 @@ Ltac2 Type exn ::= [ Not_focussed ]. Ltac2 Type exn ::= [ Not_found ]. (** Used when something is missing. *) +Ltac2 Type exn ::= [ No_value ]. +(** Used for empty lists, None options and the like. *) + Ltac2 Type exn ::= [ Match_failure ]. (** Used to signal a pattern didn't match a term. *) +Ltac2 Type exn ::= [ Invalid_argument (message option) ]. +(** Used to signal that an invalid argument was passed to a tactic. *) + Ltac2 Type exn ::= [ Tactic_failure (message option) ]. (** Generic error for tactic failure. *) diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v index ac48a3328f..60aafcd37d 100644 --- a/user-contrib/Ltac2/Int.v +++ b/user-contrib/Ltac2/Int.v @@ -18,3 +18,18 @@ Ltac2 @ external add : int -> int -> int := "ltac2" "int_add". Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub". Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul". Ltac2 @ external neg : int -> int := "ltac2" "int_neg". + +Ltac2 lt (x : int) (y : int) := equal (compare x y) -1. +Ltac2 gt (x : int) (y : int) := equal (compare x y) 1. +Ltac2 le (x : int) (y : int) := + (* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => lt x y + end. +Ltac2 ge (x : int) (y : int) := + (* we might use [lt (add x 1) y], but that has the wrong behavior on MAX_INT *) + match equal x y with + | true => true + | false => gt x y + end. diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v new file mode 100644 index 0000000000..89e14445ef --- /dev/null +++ b/user-contrib/Ltac2/List.v @@ -0,0 +1,598 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* The interface is an extended version of OCaml stdlib/list.ml. *) + +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +Require Import Ltac2.Init. +Require Ltac2.Int. +Require Ltac2.Control. +Require Ltac2.Bool. +Require Ltac2.Message. + +Ltac2 rec length (ls : 'a list) := + match ls with + | [] => 0 + | _ :: xs => Int.add 1 (length xs) + end. + +Ltac2 rec compare_lengths (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => 0 + | _ :: _ => -1 + end + | _ :: ls1 + => match ls2 with + | [] => 1 + | _ :: ls2 => compare_lengths ls1 ls2 + end + end. + +Ltac2 rec compare_length_with (ls : 'a list) (n : int) := + match Int.lt n 0 with + | true => 1 + | false + => match ls with + | [] => Int.compare 0 n + | _ :: ls => compare_length_with ls (Int.sub n 1) + end + end. + +Ltac2 cons (x : 'a) (xs : 'a list) := + x :: xs. + +(* Since Ltac-2 distinguishes between backtracking and fatal exceptions, + we provide option and default variants of functions which throw in the + OCaml stdlib. *) + +Ltac2 hd_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs => Some x + end. + +Ltac2 hd (ls : 'a list) := + match ls with + | [] => Control.throw_invalid_argument "List.hd" + | x :: xs => x + end. + +Ltac2 tl (ls : 'a list) := + match ls with + | [] => [] + | x :: xs => xs + end. + +Ltac2 rec last_opt (ls : 'a list) := + match ls with + | [] => None + | x :: xs + => match xs with + | [] => Some x + | _ :: _ => last_opt xs + end + end. + +Ltac2 last (ls : 'a list) := + match last_opt ls with + | None => Control.throw_invalid_argument "List.last" + | Some v => v + end. + +Ltac2 rec removelast (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match xs with + | [] => [] + | _ :: _ => x :: removelast xs + end + end. + +Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) := + match ls with + | [] => None + | x :: xs + => match Int.equal n 0 with + | true => Some x + | false => nth_opt_aux xs (Int.sub n 1) + end + end. + +Ltac2 nth_opt (ls : 'a list) (n : int) := + Control.assert_valid_argument "List.nth" (Int.ge n 0); + nth_opt_aux ls n. + +Ltac2 nth (ls : 'a list) (n : int) := + match nth_opt ls n with + | Some v => v + | None => Control.throw_out_of_bounds "List.nth" + end. + +Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) := + match l1 with + | [] => l2 + | a :: l => rev_append l (a :: l2) + end. + +Ltac2 rev l := rev_append l []. + +Ltac2 rec append ls1 ls2 := + match ls1 with + | [] => ls2 + | x :: xs => x :: append xs ls2 + end. + +Ltac2 rec concat (ls : 'a list list) := + match ls with + | [] => [] + | x :: xs => append x (concat xs) + end. + +Ltac2 flatten (ls : 'a list list) := concat ls. + +Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f l; iter f ls + end. + +Ltac2 rec iteri_aux (i : int) (f : int -> 'a -> unit) (ls : 'a list) := + match ls with + | [] => () + | l :: ls => f i l; iteri_aux (Int.add i 1) f ls + end. + +Ltac2 iteri (f : int -> 'a -> unit) (ls : 'a list) := + iteri_aux 0 f ls. + +Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f l :: map f ls + end. + +Ltac2 rec mapi_aux (i : int) (f : int -> 'a -> 'b) (ls : 'a list) := + match ls with + | [] => [] + | l :: ls => f i l :: mapi_aux (Int.add i 1) f ls + end. + +Ltac2 mapi (f : int -> 'a -> 'b) (ls : 'a list) := + mapi_aux 0 f ls. + +Ltac2 rec flat_map (f : 'a -> 'b list) (xs : 'a list) := + match xs with + | [] => [] + | x :: xs => append (f x) (flat_map f xs) + end. + +(* from the OCaml std lib *) +Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) := + let rec rmap_f accu ls := + match ls with + | [] => accu + | a::l => rmap_f (f a :: accu) l + end in + rmap_f [] ls. + +Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) := + match ls with + | [] => a + | l :: ls => f l (fold_right f a ls) + end. + +Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) := + match xs with + | [] => a + | x :: xs => fold_left f xs (f a x) + end. + +Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => () + | _ :: _ => Control.throw_invalid_argument "List.iter2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.iter2" + | l2 :: ls2 + => f l1 l2; iter2 f ls1 ls2 + end + end. + +Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.throw_invalid_argument "List.map2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.map2" + | l2 :: ls2 + => f l1 l2 :: map2 f ls1 ls2 + end + end. + +(* from the OCaml std lib *) +Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) := + let rec rmap2_f accu ls1 ls2 := + match ls1 with + | [] + => match ls2 with + | [] => accu + | _ :: _ => Control.throw_invalid_argument "List.rev_map2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.rev_map2" + | l2 :: ls2 + => rmap2_f (f l1 l2 :: accu) ls1 ls2 + end + end in + rmap2_f [] ls1 ls2. + +Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (a : 'c) (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.throw_invalid_argument "List.fold_right2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.fold_right2" + | l2 :: ls2 + => f l1 l2 (fold_right2 f a ls1 ls2) + end + end. + +Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (ls1 : 'b list) (ls2 : 'c list) (a : 'a) := + match ls1 with + | [] + => match ls2 with + | [] => a + | _ :: _ => Control.throw_invalid_argument "List.fold_left2" + end + | l1 :: ls1 + => match ls2 with + | [] => Control.throw_invalid_argument "List.fold_left2" + | l2 :: ls2 + => fold_left2 f ls1 ls2 (f a l1 l2) + end + end. + +Ltac2 rec for_all f ls := + match ls with + | [] => true + | x :: xs => match f x with + | true => for_all f xs + | false => false + end + end. + +(* we would call this [exists] a la OCaml's [List.exists], but that's a syntax error, so instead we name it exist *) +Ltac2 rec exist f ls := + match ls with + | [] => false + | x :: xs => match f x with + | true => true + | false => exist f xs + end + end. + +Ltac2 rec for_all2 f xs ys := + match xs with + | [] => match ys with + | [] => true + | y :: ys' => Control.throw_invalid_argument "List.for_all2" + end + | x :: xs' + => match ys with + | [] => Control.throw_invalid_argument "List.for_all2" + | y :: ys' + => match f x y with + | true => for_all2 f xs' ys' + | false => false + end + end + end. + +Ltac2 rec exist2 f xs ys := + match xs with + | [] => match ys with + | [] => false + | y :: ys' => Control.throw_invalid_argument "List.exist2" + end + | x :: xs' + => match ys with + | [] => Control.throw_invalid_argument "List.exist2" + | y :: ys' + => match f x y with + | true => true + | false => exist2 f xs' ys' + end + end + end. + +Ltac2 rec find_opt f xs := + match xs with + | [] => None + | x :: xs => match f x with + | true => Some x + | false => find_opt f xs + end + end. + +Ltac2 find f xs := + match find_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + +Ltac2 rec find_rev_opt f xs := + match xs with + | [] => None + | x :: xs => match find_rev_opt f xs with + | Some v => Some v + | None => match f x with + | true => Some x + | false => None + end + end + end. + +Ltac2 find_rev f xs := + match find_rev_opt f xs with + | Some v => v + | None => Control.throw Not_found + end. + +Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) := + exist (eq a) ls. + +Ltac2 rec filter f xs := + match xs with + | [] => [] + | x :: xs + => match f x with + | true => x :: filter f xs + | false => filter f xs + end + end. + +Ltac2 rec filter_out f xs := + filter (fun x => Bool.neg (f x)) xs. + +Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls. + +Ltac2 remove (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + filter_out (eqb x) ls. + +Ltac2 count_occ (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) := + length (filter (eqb x) ls). + +(* from the Coq stdlib *) +Ltac2 rec list_power (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] :: [] + | x :: t + => flat_map (fun f => map (fun y => (x, y) :: f) ls2) + (list_power t ls2) + end. + +Ltac2 rec partition (f : 'a -> bool) (l : 'a list) := + match l with + | [] => ([], []) + | x :: tl + => let (g, d) := partition f tl in + match f x with + | true => ((x::g), d) + | false => (g, (x::d)) + end + end. + +(* from the Coq stdlib *) +(** [list_prod] has the same signature as [combine], but unlike + [combine], it adds every possible pairs, not only those at the + same position. *) + +Ltac2 rec list_prod (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] => [] + | x :: t + => append (map (fun y => (x, y)) ls2) (list_prod t ls2) + end. + +Ltac2 rec firstn (n : int) (ls : 'a list) := + Control.assert_valid_argument "List.firstn" (Int.ge n 0); + match Int.equal n 0 with + | true => [] + | false + => match ls with + | [] => Control.throw_out_of_bounds "List.firstn" + | x :: xs + => x :: firstn (Int.sub n 1) xs + end + end. + +Ltac2 rec skipn (n : int) (ls : 'a list) := + Control.assert_valid_argument "List.skipn" (Int.ge n 0); + match Int.equal n 0 with + | true => ls + | false + => match ls with + | [] => Control.throw_out_of_bounds "List.skipn" + | x :: xs + => skipn (Int.sub n 1) xs + end + end. + +Ltac2 lastn (n : int) (ls : 'a list) := + let l := length ls in + Control.assert_valid_argument "List.lastn" (Int.ge n 0); + Control.assert_bounds "List.lastn" (Int.le n l); + skipn (Int.sub l n). + +Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) := + match ls with + | [] => [] + | x :: xs + => match mem eqb x xs with + | true => nodup eqb xs + | false => x :: nodup eqb xs + end + end. + +(* seq start 1 last = start :: start + 1 :: ... :: (last - 1) *) +Ltac2 rec seq (start : int) (step : int) (last : int) := + match Int.lt (Int.sub last start) step with + | true + => [] + | false + => start :: seq (Int.add start step) step last + end. + +Ltac2 init (len : int) (f : int -> 'a) := + Control.assert_valid_argument "List.init" (Int.ge len 0); + map f (seq 0 1 len). + +Ltac2 repeat (x : 'a) (n : 'int) := + init n (fun _ => x). + +Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + let (_, v) := find eq_key l in + v. + +Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + match find_opt eq_key l with + | Some kv => let (_, v) := kv in Some v + | None => None + end. + +Ltac2 mem_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + exist eq_key l. + +Ltac2 remove_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) := + let eq_key kv := let (k', _) := kv in eqk k k' in + filter_out eq_key l. + +Ltac2 rec split (ls : ('a * 'b) list) := + match ls with + | [] => ([], []) + | xy :: tl + => let (x, y) := xy in + let (left, right) := split tl in + ((x::left), (y::right)) + end. + +Ltac2 rec combine (ls1 : 'a list) (ls2 : 'b list) := + match ls1 with + | [] + => match ls2 with + | [] => [] + | _ :: _ => Control.throw_invalid_argument "List.combine" + end + | x :: xs + => match ls2 with + | y :: ys + => (x, y) :: combine xs ys + | [] => Control.throw_invalid_argument "List.combine" + end + end. + +Ltac2 enumerate (ls : 'a list) := + combine (seq 0 1 (length ls)) ls. + +(* from Coq stdlib *) +Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'b list) := + let rec merge_aux l2 := + match l1 with + | [] => l2 + | a1 :: l1' + => match l2 with + | [] => l1 + | a2 :: l2' + => match Int.le (cmp a1 a2) 0 with + | true => a1 :: merge cmp l1' l2 + | false => a2 :: merge_aux l2' + end + end + end in + merge_aux l2. + +Ltac2 rec merge_list_to_stack cmp stack l := + match stack with + | [] => [Some l] + | l' :: stack' + => match l' with + | None => Some l :: stack' + | Some l' + => None :: merge_list_to_stack cmp stack' (merge cmp l' l) + end + end. + +Ltac2 rec merge_stack cmp stack := + match stack with + | [] => [] + | l :: stack' + => match l with + | None => merge_stack cmp stack' + | Some l => merge cmp l (merge_stack cmp stack') + end + end. + +Ltac2 rec iter_merge cmp stack l := + match l with + | [] => merge_stack cmp stack + | a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l' + end. + +Ltac2 sort cmp l := iter_merge cmp [] l. + +(* TODO: maybe replace this with a faster implementation *) +Ltac2 sort_uniq (cmp : 'a -> 'a -> int) (l : 'a list) := + let rec uniq l := + match l with + | [] => [] + | x1 :: xs + => match xs with + | [] => x1 :: xs + | x2 :: _ + => match Int.equal (cmp x1 x2) 0 with + | true => uniq xs + | false => x1 :: uniq xs + end + end + end in + uniq (sort cmp l). diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v new file mode 100644 index 0000000000..584d84ddb5 --- /dev/null +++ b/user-contrib/Ltac2/Option.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Some of the below functions are inspired by ocaml-extlib *) + +Require Import Ltac2.Init. +Require Import Ltac2.Control. + +Ltac2 may (f : 'a -> unit) (ov : 'a option) := + match ov with + | Some v => f v + | None => () + end. + +Ltac2 map (f : 'a -> 'b) (ov : 'a option) := + match ov with + | Some v => Some (f v) + | None => None + end. + +Ltac2 default (def : 'a) (ov : 'a option) := + match ov with + | Some v => v + | None => def + end. + +Ltac2 map_default (f : 'a -> 'b) (def : 'b) (ov : 'a option) := + match ov with + | Some v => f v + | None => def + end. + +Ltac2 get (ov : 'a option) := + match ov with + | Some v => v + | None => Control.throw No_value + end. + +Ltac2 get_bt (ov : 'a option) := + match ov with + | Some v => v + | None => Control.zero No_value + end. + +Ltac2 bind (x : 'a option) (f : 'a -> 'b option) := + match x with + | Some x => f x + | None => None + end. + +Ltac2 ret (x : 'a) := Some x. + +Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index e348396aad..23b5f4daef 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -37,6 +37,8 @@ let (<+>) (lk1 : lookahead) lk2 n strm = match lk1 n strm with | None -> lk2 n strm | Some n -> Some n +let lk_empty n strm = Some n + let lk_kw kw n strm = match stream_nth n strm with | KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None | _ -> None @@ -51,6 +53,9 @@ let lk_int n strm = match stream_nth n strm with let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident) +let rec lk_ident_list n strm = + ((lk_ident >> lk_ident_list) <+> lk_empty) n strm + (* lookahead for (x:=t), (?x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = entry_of_lookahead "test_lpar_idnum_coloneq" begin @@ -85,6 +90,11 @@ let test_dollar_ident = lk_kw "$" >> lk_ident end +let test_ltac1_env = + entry_of_lookahead "test_ltac1_env" begin + lk_ident_list >> lk_kw "|-" + end + let tac2expr = Tac2entries.Pltac.tac2expr let tac2type = Entry.create "tactic:tac2type" let tac2def_val = Entry.create "tactic:tac2def_val" @@ -225,8 +235,13 @@ GRAMMAR EXTEND Gram | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c } | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c } | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c } - | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1 loc qid } - | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1val loc qid } + | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid } + | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid } + ] ] + ; + ltac1_expr_in_env: + [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e } + | e = ltac1_expr -> { [], e } ] ] ; let_clause: diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 2eb199633d..a05612c1b1 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1118,26 +1118,47 @@ let () = define_ml_object Tac2quote.wit_reference obj let () = - let intern self ist tac = + let intern self ist (ids, tac) = + let map { CAst.v = id } = id in + let ids = List.map map ids in (* Prevent inner calls to Ltac2 values *) let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in - let ist = { ist with Genintern.extra } in + let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in + let ist = { ist with Genintern.extra; ltacvars } in let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in - GlbVal tac, gtypref t_unit + let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in + let ty = List.fold_left fold (gtypref t_unit) ids in + GlbVal (ids, tac), ty in - let interp ist tac = - let ist = { env_ist = Id.Map.empty } in - let lfun = Tac2interp.set_env ist Id.Map.empty in - let ist = Ltac_plugin.Tacinterp.default_ist () in - let ist = { ist with Geninterp.lfun = lfun } in - let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in - let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in - Proofview.tclOR tac wrap >>= fun () -> - return v_unit + let interp _ (ids, tac) = + let clos args = + let add lfun id v = + let v = Tac2ffi.to_ext val_ltac1 v in + Id.Map.add id v lfun + in + let lfun = List.fold_left2 add Id.Map.empty ids args in + let ist = { env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist lfun in + let ist = Ltac_plugin.Tacinterp.default_ist () in + let ist = { ist with Geninterp.lfun = lfun } in + let tac = (Ltac_plugin.Tacinterp.eval_tactic_ist ist tac : unit Proofview.tactic) in + let wrap (e, info) = set_bt info >>= fun info -> Proofview.tclZERO ~info e in + Proofview.tclOR tac wrap >>= fun () -> + return v_unit + in + let len = List.length ids in + if Int.equal len 0 then + clos [] + else + return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in - let subst s tac = Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac in - let print env tac = - str "ltac1:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" + let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in + let print env (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc () + in + str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" in let obj = { ml_intern = intern; @@ -1149,23 +1170,44 @@ let () = let () = let open Ltac_plugin in - let intern self ist tac = + let intern self ist (ids, tac) = + let map { CAst.v = id } = id in + let ids = List.map map ids in (* Prevent inner calls to Ltac2 values *) let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in - let ist = { ist with Genintern.extra } in + let ltacvars = List.fold_right Id.Set.add ids ist.Genintern.ltacvars in + let ist = { ist with Genintern.extra; ltacvars } in let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in - GlbVal tac, gtypref t_ltac1 + let fold ty _ = GTypArrow (gtypref t_ltac1, ty) in + let ty = List.fold_left fold (gtypref t_ltac1) ids in + GlbVal (ids, tac), ty in - let interp ist tac = - let ist = { env_ist = Id.Map.empty } in - let lfun = Tac2interp.set_env ist Id.Map.empty in - let ist = Ltac_plugin.Tacinterp.default_ist () in - let ist = { ist with Geninterp.lfun = lfun } in - return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac)) + let interp _ (ids, tac) = + let clos args = + let add lfun id v = + let v = Tac2ffi.to_ext val_ltac1 v in + Id.Map.add id v lfun + in + let lfun = List.fold_left2 add Id.Map.empty ids args in + let ist = { env_ist = Id.Map.empty } in + let lfun = Tac2interp.set_env ist lfun in + let ist = Ltac_plugin.Tacinterp.default_ist () in + let ist = { ist with Geninterp.lfun = lfun } in + return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac)) + in + let len = List.length ids in + if Int.equal len 0 then + clos [] + else + return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in - let subst s tac = Genintern.substitute Tacarg.wit_tactic s tac in - let print env tac = - str "ltac1val:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" + let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in + let print env (ids, tac) = + let ids = + if List.is_empty ids then mt () + else pr_sequence Id.print ids ++ str " |- " + in + str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")" in let obj = { ml_intern = intern; diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index 0cef0e3a2b..da28e04df0 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -97,8 +97,8 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag -val wit_ltac1 : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag +val wit_ltac1 : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag (** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *) -val wit_ltac1val : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag +val wit_ltac1val : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag (** Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t. *) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 38852992e4..9b96fbf68a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -676,9 +676,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") let side_effect_of_mode = function - | Declare.UserAutomaticRequest -> false - | Declare.InternalTacticRequest -> true - | Declare.UserIndividualRequest -> false + | UserAutomaticRequest -> false + | InternalTacticRequest -> true + | UserIndividualRequest -> false let make_bl_scheme mode mind = let mib = Global.lookup_mind mind in @@ -694,7 +694,7 @@ let make_bl_scheme mode mind = let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -824,7 +824,7 @@ let make_lb_scheme mode mind = let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -1001,7 +1001,7 @@ let make_eq_decidability mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/vernac/class.ml b/vernac/class.ml index 420baf7966..febe8e34e4 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -17,7 +17,6 @@ open Constr open Context open Vars open Termops -open Entries open Environ open Classops open Declare @@ -339,42 +338,44 @@ let try_add_new_coercion_core ref ~local c d e f = user_err ~hdr:"try_add_new_coercion_core" (explain_coercion_error ref e ++ str ".") -let try_add_new_coercion ref ~local poly = +let try_add_new_coercion ref ~local ~poly = try_add_new_coercion_core ref ~local poly None None false -let try_add_new_coercion_subclass cl ~local poly = +let try_add_new_coercion_subclass cl ~local ~poly = let coe_ref = build_id_coercion None cl poly in try_add_new_coercion_core coe_ref ~local poly (Some cl) None true -let try_add_new_coercion_with_target ref ~local poly ~source ~target = +let try_add_new_coercion_with_target ref ~local ~poly ~source ~target = try_add_new_coercion_core ref ~local poly (Some source) (Some target) false -let try_add_new_identity_coercion id ~local poly ~source ~target = +let try_add_new_identity_coercion id ~local ~poly ~source ~target = let ref = build_id_coercion (Some id) source poly in try_add_new_coercion_core ref ~local poly (Some source) (Some target) true -let try_add_new_coercion_with_source ref ~local poly ~source = +let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false let add_coercion_hook poly _uctx _trans local ref = + let open DeclareDef in let local = match local with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in - let () = try_add_new_coercion ref ~local poly in + let () = try_add_new_coercion ref ~local ~poly in let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly) +let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) -let add_subclass_hook poly _uctx _trans local ref = +let add_subclass_hook ~poly _uctx _trans local ref = + let open DeclareDef in let stre = match local with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true | Global ImportDefaultBehavior -> false in let cl = class_of_global ref in - try_add_new_coercion_subclass cl ~local:stre poly + try_add_new_coercion_subclass cl ~local:stre ~poly -let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly) +let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/class.mli b/vernac/class.mli index d530d218d4..3254d5d981 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -15,35 +15,39 @@ open Classops (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : GlobRef.t -> local:bool -> - Decl_kinds.polymorphic -> - source:cl_typ -> target:cl_typ -> unit +val try_add_new_coercion_with_target + : GlobRef.t + -> local:bool + -> poly:bool + -> source:cl_typ + -> target:cl_typ + -> unit (** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : GlobRef.t -> local:bool -> - Decl_kinds.polymorphic -> unit +val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> unit (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a transparent constant which unfolds to some class [tg]; it declares an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) -val try_add_new_coercion_subclass : cl_typ -> local:bool -> - Decl_kinds.polymorphic -> unit +val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> unit (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> - Decl_kinds.polymorphic -> source:cl_typ -> unit + poly:bool -> source:cl_typ -> unit (** [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an identity coercion from [src] to [tg] *) -val try_add_new_identity_coercion : Id.t -> local:bool -> - Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit +val try_add_new_identity_coercion + : Id.t + -> local:bool + -> poly:bool -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t +val add_coercion_hook : poly:bool -> DeclareDef.Hook.t -val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t +val add_subclass_hook : poly:bool -> DeclareDef.Hook.t val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/classes.ml b/vernac/classes.ml index 442f139827..35108744cd 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -29,7 +29,6 @@ module NamedDecl = Context.Named.Declaration (*i*) open Decl_kinds -open Entries let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] @@ -324,7 +323,7 @@ let declare_instance_constant info global imps ?hook id decl poly sigma term ter in let uctx = Evd.check_univ_decl ~poly sigma decl in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in - let cdecl = (DefinitionEntry entry, kind) in + let cdecl = (Declare.DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); @@ -338,8 +337,8 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + let cst = Declare.declare_constant id + (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (ConstRef cst) @@ -363,21 +362,21 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt in let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls) + ignore(Obligations.add_definition ~name:id ?term:constr + ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls) - -let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in - let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype) - ~hook:(DeclareDef.Hook.make - (fun _ _ _ -> instance_hook pri global imps ?hook)) in + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in + let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in + let info = Lemmas.Info.make ~hook ~scope ~kind () in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = if not (Option.is_empty term) then @@ -568,7 +567,7 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl = id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl let new_instance_interactive ?(global=false) - poly instid ctx cl + ~poly instid ctx cl ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = @@ -577,7 +576,7 @@ let new_instance_interactive ?(global=false) cty k u ctx ctx' pri decl imps subst id let new_instance_program ?(global=false) - poly instid ctx cl opt_props + ~poly instid ctx cl opt_props ?(generalize=true) ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = @@ -587,7 +586,7 @@ let new_instance_program ?(global=false) id let new_instance ?(global=false) - poly instid ctx cl props + ~poly instid ctx cl props ?(generalize=true) ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = @@ -596,7 +595,7 @@ let new_instance ?(global=false) cty k u ctx ctx' pri decl imps subst id props; id -let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = +let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = diff --git a/vernac/classes.mli b/vernac/classes.mli index 472690cdd4..1247fdc8c1 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -27,7 +27,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit val new_instance_interactive : ?global:bool (** Not global by default. *) - -> Decl_kinds.polymorphic + -> poly:bool -> name_decl -> local_binder_expr list -> constr_expr @@ -39,7 +39,7 @@ val new_instance_interactive val new_instance : ?global:bool (** Not global by default. *) - -> Decl_kinds.polymorphic + -> poly:bool -> name_decl -> local_binder_expr list -> constr_expr @@ -51,7 +51,7 @@ val new_instance val new_instance_program : ?global:bool (** Not global by default. *) - -> Decl_kinds.polymorphic + -> poly:bool -> name_decl -> local_binder_expr list -> constr_expr @@ -64,7 +64,7 @@ val new_instance_program val declare_new_instance : ?global:bool (** Not global by default. *) -> program_mode:bool - -> Decl_kinds.polymorphic + -> poly:bool -> ident_decl -> local_binder_expr list -> constr_expr diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 3eb5eacd46..e91d8b9d3e 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -43,14 +43,15 @@ let should_axiom_into_instance = function true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = -match local with +let declare_assumption is_coe ~poly ~scope ~kind typ univs pl imps impl nl {CAst.v=ident} = +let open DeclareDef in +match scope with | Discharge -> - let ctx = match ctx with - | Monomorphic_entry ctx -> ctx - | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx + let univs = match univs with + | Monomorphic_entry univs -> univs + | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs in - let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in + let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in let r = VarRef ident in @@ -58,7 +59,7 @@ match local with let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true false in + let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in (r,Univ.Instance.empty,true) | Global local -> @@ -68,7 +69,7 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in + let decl = (Declare.ParameterEntry (None,(typ,univs),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 @@ -78,9 +79,9 @@ match local with let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = match ctx with - | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx + let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in + let inst = match univs with + | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs | Monomorphic_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -96,11 +97,11 @@ let next_uctx = | Polymorphic_entry _ as uctx -> uctx | Monomorphic_entry _ -> empty_uctx -let declare_assumptions idl is_coe k (c,uctx) pl imps nl = +let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = let refs, status, _ = List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,uctx) pl imps false nl id in + declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in (ref',u')::refs, status' && status, next_uctx uctx) ([],true,uctx) idl in @@ -115,7 +116,7 @@ let maybe_error_many_udecls = function str "(which will be shared by the whole block).") | (_, None) -> () -let process_assumptions_udecls kind l = +let process_assumptions_udecls ~scope l = let udecl, first_id = match l with | (coe, ((id, udecl)::rest, c))::rest' -> List.iter maybe_error_many_udecls rest; @@ -123,8 +124,9 @@ let process_assumptions_udecls kind l = udecl, id | (_, ([], _))::_ | [] -> assert false in - let () = match kind, udecl with - | (Discharge, _, _), Some _ -> + let open DeclareDef in + let () = match scope, udecl with + | Discharge, Some _ -> let loc = first_id.CAst.loc in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg @@ -132,13 +134,13 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions ~program_mode kind nl l = +let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let open Context.Named.Declaration in let env = Global.env () in - let udecl, l = process_assumptions_udecls kind l in + let udecl, l = process_assumptions_udecls ~scope l in let sigma, udecl = interp_univ_decl_opt env udecl in let l = - if pi2 kind (* poly *) then + if poly 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 -> @@ -174,11 +176,11 @@ let do_assumptions ~program_mode kind nl l = IMO, thus I think we should adapt `prepare_parameter` to handle this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in - let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in + let uctx = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in - pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> - let t = replace_vars subst t in - let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in + pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) -> + let typ = replace_vars subst typ in + let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs @@ -226,7 +228,7 @@ let named_of_rel_context l = l ([], []) in ctx -let context poly l = +let context ~poly l = let env = Global.env() in let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in @@ -251,7 +253,7 @@ let context poly l = separately. *) begin let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; + Declare.declare_universe_context ~poly uctx; if poly then Polymorphic_entry ([||], Univ.UContext.empty) else Monomorphic_entry Univ.ContextSet.empty end @@ -263,7 +265,7 @@ let context poly l = to avoid redeclaring them. *) begin let uctx = Evd.universe_context_set sigma in - Declare.declare_universe_context poly uctx; + Declare.declare_universe_context ~poly uctx; Monomorphic_entry Univ.ContextSet.empty end in @@ -273,12 +275,12 @@ let context poly l = (* Declare the universe context once *) let decl = match b with | None -> - (ParameterEntry (None,(t,univs),None), IsAssumption Logical) + (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in - (DefinitionEntry entry, IsAssumption Logical) + (Declare.DefinitionEntry entry, IsAssumption Logical) in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in + let cst = Declare.declare_constant id decl in let env = Global.env () in Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); status @@ -288,17 +290,17 @@ let context poly l = | _ -> false in let impl = List.exists test impls in - let persistence = - if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in - let decl = (persistence, poly, Context) in + let scope = + if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in let nstatus = match b with | None -> - pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl + pi3 (declare_assumption false ~scope ~poly ~kind:Context t univs UnivNames.empty_binders [] impl Declaremods.NoInline (CAst.make id)) | Some b -> - let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in + let _gr = DeclareDef.declare_definition + ~name:id ~scope:DeclareDef.Discharge + ~kind:Definition UnivNames.empty_binders entry [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 07e96d87a2..57b4aea9e3 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -16,8 +16,10 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions - : program_mode:bool - -> locality * polymorphic * assumption_object_kind + : program_mode:bool + -> poly:bool + -> scope:DeclareDef.locality + -> kind:assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool @@ -26,8 +28,11 @@ val do_assumptions nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag - -> assumption_kind - -> Constr.types Entries.in_universes_entry + -> poly:bool + -> scope:DeclareDef.locality + -> kind:assumption_object_kind + -> Constr.types + -> Entries.universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) @@ -40,7 +45,7 @@ val declare_assumption (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) val context - : Decl_kinds.polymorphic + : poly:bool -> local_binder_expr list -> bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 853f2c9aa3..57de719cb4 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -10,7 +10,6 @@ open Pp open Util -open Entries open Redexpr open Constrintern open Pretyping @@ -41,7 +40,7 @@ let check_imps ~impsty ~impsbody = | [], [] -> () in aux impsty impsbody -let interp_definition ~program_mode pl bl poly red_option c ctypopt = +let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let env = Global.env() in (* Explicitly bound universes and constraints *) let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in @@ -80,29 +79,29 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = +let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt + interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.const_entry_body in + let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.const_entry_type with + let typ = match ce.Proof_global.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in let obls, _, c, cty = - Obligations.eterm_obligations env ident evd 0 c typ + Obligations.eterm_obligations env name evd 0 c typ in let ctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls) + ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) else let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index af09a83f02..71926a9d23 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Decl_kinds open Redexpr open Constrexpr @@ -17,10 +16,12 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool + : program_mode:bool -> ?hook:DeclareDef.Hook.t - -> Id.t - -> definition_kind + -> name:Id.t + -> scope:DeclareDef.locality + -> poly:bool + -> kind:definition_object_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option @@ -37,9 +38,9 @@ val interp_definition : program_mode:bool -> universe_decl_expr option -> local_binder_expr list - -> polymorphic + -> poly:bool -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects definition_entry * + -> Evd.side_effects Proof_global.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a88413cf7f..e3428d6afc 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,80 +255,59 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint_notations ntns = - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns - -let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = - (* Some bodies to define by proof *) +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = + let fix_kind, cofix, indexes = match indexes with + | Some indexes -> Fixpoint, false, indexes + | None -> CoFixpoint, true, [] + in let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in + List.map3 (fun name t (ctx,impargs,_) -> + { Lemmas.Recthm.name; typ = EConstr.of_constr t + ; args = List.map RelDecl.get_name ctx; impargs}) + fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) - fixdefs) in + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None in - declare_fixpoint_notations ntns; + let lemma = + Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl + evd (Some(cofix,indexes,init_tac)) thms None in + (* Declare notations *) + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + let indexes, cofix, fix_kind = + match indexes with + | Some indexes -> indexes, false, Fixpoint + | None -> [], true, CoFixpoint + in (* We shortcut the proof process *) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let env = Global.env() in - let indexes = search_guard env indexes fixdecls in + let vars, fixdecls, gidx = + if not cofix then + let env = Global.env() in + let indexes = search_guard env indexes fixdecls in + let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + vars, fixdecls, Some indexes + else (* cofix *) + let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in - let fixdecls = - 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 ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - fixpoint_message (Some indexes) fixnames; - declare_fixpoint_notations ntns - -let declare_cofixpoint_notations = declare_fixpoint_notations - -let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr 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 - let lemma = Lemmas.start_lemma_with_initialization - (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None in - declare_cofixpoint_notations ntns; - lemma - -let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in - let fixdecls = List.map mk_pure fixdecls in - 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 ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) + ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - cofixpoint_message fixnames; - declare_cofixpoint_notations ntns + recursive_message (not cofix) gidx fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; + () let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with | CStructRec na -> na @@ -372,28 +351,28 @@ let do_fixpoint_common l = let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in fixl, ntns, fix, List.map compute_possible_guardness_evidences info -let do_fixpoint_interactive local poly l = +let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - let pstate = declare_fixpoint_interactive local poly fix possible_indexes ntns in + let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); - pstate + lemma -let do_fixpoint local poly l = +let do_fixpoint ~scope ~poly l = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint local poly fix possible_indexes ntns; + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint_common l = let fixl,ntns = extract_cofixpoint_components l in ntns, interp_fixpoint ~cofix:true fixl ntns -let do_cofixpoint_interactive local poly l = +let do_cofixpoint_interactive ~scope ~poly l = let ntns, cofix = do_cofixpoint_common l in - let pstate = declare_cofixpoint_interactive local poly cofix ntns in + let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); - pstate + lemma -let do_cofixpoint local poly l = +let do_cofixpoint ~scope ~poly l = let ntns, cofix = do_cofixpoint_common l in - declare_cofixpoint local poly cofix ntns; + declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b42e877d41..982d316605 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Decl_kinds open Constrexpr open Vernacexpr @@ -19,16 +18,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t val do_fixpoint : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint_interactive : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t val do_cofixpoint : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit (************************************************************************) (** Internal API *) @@ -81,22 +80,6 @@ val interp_fixpoint : recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list -(** Registering fixpoints and cofixpoints in the environment *) - -(** [Not used so far] *) -val declare_fixpoint : - locality -> polymorphic -> - recursive_preentry * UState.universe_decl * UState.t * - (Constr.rel_context * Impargs.manual_implicits * int option) list -> - Lemmas.lemma_possible_guards -> decl_notation list -> - unit - -val declare_cofixpoint : - locality -> polymorphic -> - recursive_preentry * UState.universe_decl * UState.t * - (Constr.rel_context * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit - (** Very private function, do not use *) val compute_possible_guardness_evidences : ('a, 'b) Context.Rel.pt * 'c * int option -> int list diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 363ba5beff..f530dad4fd 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -349,7 +349,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum ~poly prv finite = check_all_names_different indl; List.iter check_param paramsl; if not (List.is_empty uparamsl) && not (List.is_empty notations) @@ -469,8 +469,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite +let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum ~poly prv finite = + interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum ~poly prv finite (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -564,16 +564,16 @@ type uniform_inductive_flag = | UniformParameters | NonUniformParameters -let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = +let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in - let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum ~poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 2d6ecf48ef..a77cd66a33 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -26,7 +26,7 @@ type uniform_inductive_flag = val do_mutual_inductive : template:bool option -> universe_decl_expr option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + poly:bool -> private_flag -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit (************************************************************************) @@ -75,5 +75,5 @@ val extract_mutual_inductive_declaration_components : val interp_mutual_inductive : template:bool option -> universe_decl_expr option -> structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> + poly:bool -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 23c98c97f9..d804957917 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -13,7 +13,6 @@ open CErrors open Util open Constr open Context -open Entries open Vars open Declare open Names @@ -235,8 +234,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~hook) + ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl + ~poly evars_typ ctx evars ~hook) let out_def = function | Some def -> def @@ -247,7 +246,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive local poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl ntns = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl ntns @@ -289,12 +288,12 @@ let do_program_recursive local poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint) - | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint) + | DeclareObl.IsFixpoint _ -> Fixpoint + | DeclareObl.IsCoFixpoint -> CoFixpoint in - Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind + Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind -let do_program_fixpoint local poly l = +let do_program_fixpoint ~scope ~poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> @@ -317,7 +316,7 @@ let do_program_fixpoint local poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let fixl,ntns = extract_fixpoint_components ~structonly:true l in let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive local poly fixkind fixl ntns + do_program_recursive ~scope ~poly fixkind fixl ntns | _, _ -> user_err ~hdr:"do_program_fixpoint" @@ -335,11 +334,11 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint local poly l = - do_program_fixpoint local poly l; +let do_fixpoint ~scope ~poly l = + do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint local poly l = +let do_cofixpoint ~scope ~poly l = let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns; + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 943cb8efe6..f25abb95c3 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,12 +1,11 @@ -open Decl_kinds open Vernacexpr (** Special Fixpoint handling when command is activated. *) val do_fixpoint : (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 42327d6bdd..d74fdcab2c 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -10,16 +10,17 @@ open Decl_kinds open Declare -open Entries open Globnames open Impargs +type locality = Discharge | Global of Declare.import_status + (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct module S = struct type t = UState.t -> (Names.Id.t * Constr.t) list - -> Decl_kinds.locality + -> locality -> Names.GlobRef.t -> unit end @@ -37,31 +38,31 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ident (local, p, k) ?hook_data ce pl imps = - let fix_exn = Future.fix_exn_of ce.const_entry_body in - let gr = match local with +let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = + let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in + let gr = match scope with | Discharge -> - let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in - VarRef ident + let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in + VarRef name | Global local -> - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in let gr = ConstRef kn in - let () = Declare.declare_univ_binders gr pl in + let () = Declare.declare_univ_binders gr udecl in gr in let () = maybe_declare_manual_implicits false gr imps in - let () = definition_message ident in + let () = definition_message name in begin match hook_data with | None -> () | Some (hook, uctx, extra_defs) -> - Hook.call ~fix_exn ~hook uctx extra_defs local gr + Hook.call ~fix_exn ~hook uctx extra_defs scope gr end; gr -let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ?hook_data ce pl imps + declare_definition ~name ~scope ~kind ?hook_data udecl ce imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 6f9608f04a..3934a29413 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -11,6 +11,8 @@ open Names open Decl_kinds +type locality = Discharge | Global of Declare.import_status + (** Declaration hooks *) module Hook : sig type t @@ -28,10 +30,10 @@ module Hook : sig (** [(n1,t1),...(nm,tm)]: association list between obligation name and the corresponding defined term (might be a constant, but also an arbitrary term in the Expand case of obligations) *) - -> Decl_kinds.locality + -> locality (** [locality]: Locality of the original declaration *) -> GlobRef.t - (** [ref]: identifier of the origianl declaration *) + (** [ref]: identifier of the original declaration *) -> unit end @@ -40,21 +42,23 @@ module Hook : sig end val declare_definition - : Id.t - -> definition_kind + : name:Id.t + -> scope:locality + -> kind:definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> Evd.side_effects Entries.definition_entry -> UnivNames.universe_binders + -> Evd.side_effects Proof_global.proof_entry -> Impargs.manual_implicits -> GlobRef.t val declare_fix - : ?opaque:bool + : ?opaque:bool -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> definition_kind + -> name:Id.t + -> scope:locality + -> kind:definition_object_kind -> UnivNames.universe_binders -> Entries.universes_entry - -> Id.t -> Evd.side_effects Entries.proof_output -> Constr.types -> Impargs.manual_implicits @@ -64,7 +68,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Entries.definition_entry + Evd.evar_map * Evd.side_effects Proof_global.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 30aa347692..81cde786c2 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -48,7 +48,9 @@ type program_info = ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits ; prg_notations : notations - ; prg_kind : definition_kind + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool @@ -146,7 +148,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_poly in let ctx, body, ty, args = if get_shrink_obligations () && not poly then shrink_body body ty else ([], body, ty, [||]) @@ -155,18 +157,18 @@ let declare_obligation prg obl body ty uctx = ((body, Univ.ContextSet.empty), Evd.empty_side_effects) in let ce = - { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body - ; const_entry_secctx = None - ; const_entry_type = ty - ; const_entry_universes = uctx - ; const_entry_opaque = opaque - ; const_entry_inline_code = false - ; const_entry_feedback = None } + Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body + ; proof_entry_secctx = None + ; proof_entry_type = ty + ; proof_entry_universes = uctx + ; proof_entry_opaque = opaque + ; proof_entry_inline_code = false + ; proof_entry_feedback = None } in (* ppedrot: seems legit to have obligations as local *) let constant = - Declare.declare_constant obl.obl_name ~local:ImportNeedQualified - (DefinitionEntry ce, IsProof Property) + Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified + (Declare.DefinitionEntry ce, IsProof Property) in if not opaque then add_hint (Locality.make_section_locality None) prg constant; @@ -355,13 +357,14 @@ let declare_definition prg = in let uctx = UState.restrict prg.prg_ctx uvars in let univs = - UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl + UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl in let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders + DeclareDef.declare_definition + ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce prg.prg_implicits ?hook_data let rec lam_index n t acc = @@ -418,7 +421,6 @@ let declare_mutual_definition l = let rvec = Array.of_list fixrs in let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in let fixdecls = (Array.map2 make_annot namevec rvec, 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 @@ -438,12 +440,14 @@ let declare_mutual_definition l = (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) in (* Declare the recursive definitions *) + let poly = first.prg_poly in + let scope = first.prg_scope in let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 - (DeclareDef.declare_fix ~opaque (local, poly, kind) - UnivNames.empty_binders univs) + (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind + UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -452,7 +456,7 @@ let declare_mutual_definition l = first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls scope gr; List.iter progmap_remove l; gr @@ -498,8 +502,8 @@ let obligation_terminator opq entries uctx { name; num; auto } = match entries with | [entry] -> let env = Global.env () in - let ty = entry.Entries.const_entry_type in - let body, eff = Future.force entry.const_entry_body in + let ty = entry.proof_entry_type in + let body, eff = Future.force entry.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in @@ -523,15 +527,15 @@ let obligation_terminator opq entries uctx { name; num; auto } = in let obl = { obl with obl_status = false, status } in let ctx = - if pi2 prg.prg_kind then ctx + if prg.prg_poly then ctx else UState.union prg.prg_ctx ctx in - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let () = obls.(num) <- obl in let prg_ctx = - if pi2 (prg.prg_kind) then (* Polymorphic *) + if prg.prg_poly then (* Polymorphic *) (* We merge the new universes and constraints of the polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 70a4601ac6..2d275b5ed8 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -42,7 +42,9 @@ type program_info = ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits ; prg_notations : notations - ; prg_kind : Decl_kinds.definition_kind + ; prg_poly : bool + ; prg_scope : DeclareDef.locality + ; prg_kind : Decl_kinds.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool @@ -78,7 +80,7 @@ type obligation_qed_info = val obligation_terminator : Proof_global.opacity_flag - -> Evd.side_effects Entries.definition_entry list + -> Evd.side_effects Proof_global.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 80b3df84db..9559edbea0 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -21,7 +21,6 @@ open CErrors open Util open Names open Declarations -open Entries open Term open Constr open Inductive @@ -101,18 +100,19 @@ let () = (* Util *) -let define ~poly id internal sigma c t = - let f = declare_constant ~internal in +let define ~poly id sigma c t = + let f = declare_constant in let univs = Evd.univ_entry ~poly sigma in + let open Proof_global in let kn = f id (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = t; - const_entry_universes = univs; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; + { proof_entry_body = c; + proof_entry_secctx = None; + proof_entry_type = t; + proof_entry_universes = univs; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None; }, Decl_kinds.IsDefinition Scheme) in definition_message id; @@ -415,7 +415,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma proof_output (Some decltype) in ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -544,7 +544,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in - ignore (define ~poly name.v UserIndividualRequest sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma proof_output (Some typ)); fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 400e0dfa3e..173a83f1d1 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -56,13 +56,43 @@ module Proof_ending = struct end +module Recthm = struct + type t = + { name : Id.t + ; typ : EConstr.t + ; args : Name.t list + ; impargs : Impargs.manual_implicits + } +end + +module Info = struct + + type t = + { hook : DeclareDef.Hook.t option + ; compute_guard : lemma_possible_guards + ; impargs : Impargs.manual_implicits + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) + ; other_thms : Recthm.t list + ; scope : DeclareDef.locality + ; kind : Decl_kinds.goal_object_kind + } + + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () = + { hook + ; compute_guard = [] + ; impargs = [] + ; proof_ending = CEphemeron.create proof_ending + ; other_thms = [] + ; scope + ; kind + } +end + (* Proofs with a save constant function *) type t = { proof : Proof_global.t - ; hook : DeclareDef.Hook.t option - ; compute_guard : lemma_possible_guards - ; proof_ending : Proof_ending.t CEphemeron.key - (* This could be improved and the CEphemeron removed *) + ; info : Info.t } let pf_map f pf = { pf with proof = f pf.proof } @@ -73,12 +103,11 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) (* To be removed *) module Internal = struct -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending + (** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) + let get_info ps = ps.info end -(* Internal *) let by tac pf = let proof, res = Pfedit.by tac pf.proof in @@ -107,21 +136,22 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with const_entry_body = - Future.chain const.const_entry_body + let open Proof_global in + { const with proof_entry_body = + Future.chain const.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> (* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in + List.map2 (fun i c -> match i with Some i -> i | None -> + List.interval 0 (List.length ((lam_assum c)))) + lemma_guard (Array.to_list fixdefs) in *) let env = Safe_typing.push_private_constants env eff.Evd.seff_private in let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff + (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } let find_mutually_recursive_statements sigma thms = @@ -159,23 +189,23 @@ let find_mutually_recursive_statements sigma thms = (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] ind_ccls in + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] ind_ccls in let ordered_same_indccl = List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in (* Check if some hypotheses are inductive in the same type *) let common_same_indhyp = List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] inds_hyps in + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] inds_hyps in let ordered_inds,finite,guard = match ordered_same_indccl, common_same_indhyp with | indccl::rest, _ -> - assert (List.is_empty rest); + assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) - if not (List.is_empty common_same_indhyp) then - Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); - flush_all (); + if not (List.is_empty common_same_indhyp) then + Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); + flush_all (); indccl, true, [] | [], _::_ -> let () = match same_indccl with @@ -190,10 +220,10 @@ let find_mutually_recursive_statements sigma thms = | _ -> () in let possible_guards = List.map (List.map pi3) inds_hyps in - (* assume the largest indices as possible *) - List.last common_same_indhyp, false, possible_guards + (* assume the largest indices as possible *) + List.last common_same_indhyp, false, possible_guards | _, [] -> - user_err Pp.(str + user_err Pp.(str ("Cannot find common (mutual) inductive premises or coinductive" ^ " conclusions in the statements.")) in @@ -216,16 +246,18 @@ let default_thm_id = Id.of_string "Unnamed_thm" let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = - let t_i = norm t_i in +let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i + { Recthm.name; typ; impargs } = + let t_i = norm typ in let k = IsAssumption Conjectural in match body with | None -> - (match locality with + let open DeclareDef in + (match scope with | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with @@ -234,17 +266,16 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i Univ.ContextSet.of_context univs | Monomorphic_entry univs -> univs in - let c = SectionLocalAssum ((t_i, univs),p,impl) in - let _ = declare_variable id (Lib.cwd(),c,k) in - (VarRef id,imps) + let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in + let _ = declare_variable name (Lib.cwd(),c,k) in + (VarRef name,impargs) | Global local -> let k = IsAssumption Conjectural in let decl = (ParameterEntry (None,(t_i,univs),None), k) in - let kn = declare_constant id ~local decl in - (ConstRef kn,imps)) + let kn = declare_constant name ~local decl in + (ConstRef kn,impargs)) | Some body -> let body = norm body in - let k = Kindops.logical_kind_of_goal_kind kind in let rec body_i t = match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) @@ -254,18 +285,19 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in - match locality with + let open DeclareDef in + match scope with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (VarRef id,imps) + let c = SectionLocalDef const in + let _ = declare_variable name (Lib.cwd(), c, k) in + (VarRef name,impargs) | Global local -> let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i - in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (ConstRef kn,imps) + in + let kn = declare_constant name ~local (DefinitionEntry const, k) in + (ConstRef kn,impargs) let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -311,34 +343,38 @@ module Stack = struct end (* Starting a goal *) -let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular) - ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = +let start_lemma ~name ~poly + ?(udecl=UState.default_univ_decl) + ?(sign=initialize_named_context_for_proof()) + ?(info=Info.make ()) + sigma c = let goals = [ Global.env_of_context sign , c ] in - let proof = Proof_global.start_proof sigma id ?pl kind goals in - { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } + let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in + { proof ; info } -let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular) - ?(compute_guard=[]) ?hook telescope = - let proof = Proof_global.start_dependent_proof id ?pl kind telescope in - { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } +let start_dependent_lemma ~name ~poly + ?(udecl=UState.default_univ_decl) + ?(info=Info.make ()) telescope = + let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly telescope in + { proof; info } let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with + match List.map (fun { Recthm.name; typ } -> name,typ) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) - let nl = match snl with + 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, t)) thms nl with + in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = - let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in - let init_tac,guard = match recguard with +let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = + let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in + let init_tac, compute_guard = match recguard with | Some (finite,guard,init_tac) -> let rec_tac = rec_tac_initializer finite guard thms snl in Some (match init_tac with @@ -353,33 +389,26 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = Some (intro_tac (List.hd thms)), [] in match thms with | [] -> anomaly (Pp.str "No proof to start.") - | (id,(t,(_,imps)))::other_thms -> - let hook ctx _ strength ref = - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ctx ref in - let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in - let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in - let env = Global.env () in - List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in - let thms_data = (ref,imps)::other_thms_data in - List.iter (fun (ref,imps) -> - maybe_declare_manual_implicits false ref imps; - DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in - let hook = DeclareDef.Hook.make hook in - let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let lemma = pf_map (Proof_global.map_proof (fun p -> - match init_tac with - | None -> p - | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in - lemma - -let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = + | { Recthm.name; typ; impargs; _}::other_thms -> + let info = + Info.{ hook + ; impargs + ; compute_guard + ; other_thms + ; proof_ending = CEphemeron.create Proof_ending.Regular + ; scope + ; kind + } in + let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in + pf_map (Proof_global.map_proof (fun p -> + match init_tac with + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma + +let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms = let env0 = Global.env () in let decl = fst (List.hd thms) in - let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in @@ -387,7 +416,7 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = let hook = inference_hook in let evd = solve_remaining_evars ?hook flags env evd in let ids = List.map RelDecl.get_name ctx in - check_name_freshness (pi1 kind) id; + check_name_freshness scope id; (* XXX: The nf_evar is critical !! *) evd, (id.CAst.v, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), @@ -397,18 +426,19 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = let evd = Evd.minimize_universes evd in (* XXX: This nf_evar is critical too!! We are normalizing twice if you look at the previous lines... *) - let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in + let thms = List.map (fun (name, (typ, (args, impargs))) -> + { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in let () = let open UState in - if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) + if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly evd udecl) in let evd = - if pi2 kind then evd + if poly then evd else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_lemma_with_initialization ?hook kind evd decl recguard thms snl + start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) (* Admitting a lemma-like constant *) @@ -424,16 +454,21 @@ let warn_let_as_axiom = (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let finish_admitted id k pe ctx hook = - let local = match k with - | Global local, _, _ -> local - | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified - in - let kn = declare_constant id ~local (ParameterEntry pe, IsAssumption Conjectural) in - let () = assumption_message id in - Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); - DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn); - Feedback.feedback Feedback.AddedAxiom +(* This declares implicits and calls the hooks for all the theorems, + including the main one *) +let process_recthms ?fix_exn ?hook env sigma ctx ~udecl ~poly ~scope ref imps other_thms = + let other_thms_data = + if List.is_empty other_thms then [] else + (* there are several theorems defined mutually *) + let body,opaq = retrieve_first_recthm ctx ref in + let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in + let body = Option.map EConstr.of_constr body in + let uctx = UState.check_univ_decl ~poly ctx udecl in + List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in + let thms_data = (ref,imps)::other_thms_data in + List.iter (fun (ref,imps) -> + maybe_declare_manual_implicits false ref imps; + DeclareDef.Hook.call ?fix_exn ?hook ctx [] scope ref) thms_data let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref @@ -442,22 +477,40 @@ let get_keep_admitted_vars = ~key:["Keep"; "Admitted"; "Variables"] ~value:true +let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms = + let open DeclareDef in + let local = match scope with + | Global local -> local + | Discharge -> warn_let_as_axiom name; ImportNeedQualified + in + let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in + let () = assumption_message name in + Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); + (* This takes care of the implicits and hook for the current constant*) + process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms; + Feedback.feedback Feedback.AddedAxiom + let save_lemma_admitted ?proof ~(lemma : t) = let open Proof_global in + let env = Global.env () in match proof with - | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) -> + | Some ({ name; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then + let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + if proof_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); - let typ = Option.get const_entry_type in - let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in - finish_admitted id k (sec_vars, (typ, ctx), None) universes hook + let poly = match proof_entry_universes with + | Entries.Monomorphic_entry _ -> false + | Entries.Polymorphic_entry (_, _) -> true in + let typ = Option.get proof_entry_type in + let ctx = UState.univ_entry ~poly universes in + let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in + let sigma = Evd.from_env env in + finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms | None -> let pftree = Proof_global.get_proof lemma.proof in - let gk = Proof_global.get_persistence lemma.proof in + let scope = lemma.info.Info.scope in let Proof.{ name; poly; entry } = Proof.data pftree in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ @@ -466,7 +519,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") in let typ = EConstr.Unsafe.to_constr typ in - let universes = Proof.((data pftree).initial_euctx) in + let universes = Proof_global.get_initial_euctx lemma.proof in (* This will warn if the proof is complete *) let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in @@ -480,46 +533,46 @@ let save_lemma_admitted ?proof ~(lemma : t) = let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in - let decl = Proof_global.get_universe_decl lemma.proof in - let ctx = UState.check_univ_decl ~poly universes decl in - finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook + let udecl = Proof_global.get_universe_decl lemma.proof in + let { Info.hook; impargs; other_thms } = lemma.info in + let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in + let ctx = UState.check_univ_decl ~poly universes udecl in + finish_admitted env sigma ~name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms (************************************************************************) (* Saving a lemma-like constant *) (************************************************************************) -type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key - -let default_info = None, [], CEphemeron.create Proof_ending.Regular - -let finish_proved opaque idopt po hook compute_guard = +let finish_proved env sigma opaque idopt po info = let open Proof_global in + let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in match po with - | { id; entries=[const]; persistence=locality,poly,kind; universes } -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false + | { name; entries=[const]; universes; udecl; poly } -> + let is_opaque = match opaque with + | Transparent -> false + | Opaque -> true in - assert (is_opaque == const.const_entry_opaque); - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + assert (is_opaque == const.proof_entry_opaque); + let name = match idopt with + | None -> name + | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in + let fix_exn = Future.fix_exn_of const.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in let k = Kindops.logical_kind_of_goal_kind kind in - let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in - let r = match locality with + let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let open DeclareDef in + let r = match scope with | Discharge -> let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in + let _ = declare_variable name (Lib.cwd(), c, k) in let () = if should_suggest - then Proof_using.suggest_variable (Global.env ()) id + then Proof_using.suggest_variable (Global.env ()) name in - VarRef id + VarRef name | Global local -> let kn = - declare_constant ~export_seff id ~local (DefinitionEntry const, k) in + declare_constant name ~local (DefinitionEntry const, k) in let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in @@ -527,8 +580,9 @@ let finish_proved opaque idopt po hook compute_guard = Declare.declare_univ_binders gr (UState.universe_binders universes); gr in - definition_message id; - DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r + definition_message name; + (* This takes care of the implicits and hook for the current constant*) + process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -550,8 +604,8 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in (* In the type and body of the proof of [suchthat] there can be @@ -561,31 +615,31 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with + match Proof_global.(lemma_def.proof_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Entries in + let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = let open Proof_global in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } + proof_entry_body = lemma_body ; + proof_entry_type = Some lemma_type ; + proof_entry_opaque = opaque ; } in let lemma_def = - Entries.DefinitionEntry lemma_def , + Declare.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in ignore (Declare.declare_constant name lemma_def) -let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = +let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 = let open Decl_kinds in let obls = ref 1 in - let kind = match pi3 proof_obj.Proof_global.persistence with + let kind = match kind with | DefinitionBody d -> IsDefinition d | Proof p -> IsProof p in @@ -597,7 +651,7 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Abstract.shrink_entry local_context entry in - let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in + let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in let sigma, app = Evarutil.new_global sigma (ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 @@ -609,25 +663,28 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) if Option.is_empty lemma && Option.is_empty proof then user_err (str "No focused proof (No proof-editing in progress)."); - let proof_obj, proof_info = + (* Env and sigma are just used for error printing in save_remaining_recthms *) + let env = Global.env () in + let sigma, proof_obj, proof_info = match proof with | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let { proof; hook; compute_guard; proof_ending } = Option.get lemma in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending) + let { proof; info } = Option.get lemma in + let { Proof.sigma } = Proof.data (Proof_global.get_proof proof) in + sigma, + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info | Some (proof, info) -> - proof, info + Evd.from_env env, proof, info in - let hook, compute_guard, proof_ending = proof_info in let open Proof_global in let open Proof_ending in - match CEphemeron.default proof_ending Regular with + match CEphemeron.default proof_info.Info.proof_ending Regular with | Regular -> - finish_proved opaque idopt proof_obj hook compute_guard + finish_proved env sigma opaque idopt proof_obj proof_info | End_obligation oinfo -> DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> - finish_proved_equations opaque idopt proof_obj hook i types wits sigma + finish_proved_equations opaque idopt proof_info.Info.kind proof_obj hook i types wits sigma diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 70c8b511a1..88f26a04b7 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -11,9 +11,11 @@ open Names open Decl_kinds -(* Proofs that define a constant *) +(** {4 Proofs attached to a constant} *) + type t -type lemma_possible_guards = int list list +(** [Lemmas.t] represents a constant that is being proved, usually + interactively *) module Stack : sig @@ -40,11 +42,12 @@ end val set_endline_tactic : Genarg.glob_generic_argument -> t -> t val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t val pf_fold : (Proof_global.t -> 'a) -> t -> 'a +(** [pf_fold f l] fold over the underlying proof object *) val by : unit Proofview.tactic -> t -> t * bool +(** [by tac l] apply a tactic to [l] *) -(* Start of high-level proofs with an associated constant *) - +(** Creating high-level proofs with an associated constant *) module Proof_ending : sig type t = @@ -60,71 +63,112 @@ module Proof_ending : sig end +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : EConstr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +module Info : sig + + type t + + val make + : ?hook: DeclareDef.Hook.t + (** Callback to be executed at the end of the proof *) + -> ?proof_ending : Proof_ending.t + (** Info for special constants *) + -> ?scope : DeclareDef.locality + (** locality *) + -> ?kind:goal_object_kind + (** Theorem, etc... *) + -> unit + -> t + +end + +(** Starts the proof of a constant *) val start_lemma - : Id.t - -> ?pl:UState.universe_decl - -> goal_kind - -> Evd.evar_map - -> ?proof_ending:Proof_ending.t + : name:Id.t + -> poly:bool + -> ?udecl:UState.universe_decl -> ?sign:Environ.named_context_val - -> ?compute_guard:lemma_possible_guards - -> ?hook:DeclareDef.Hook.t + -> ?info:Info.t + -> Evd.evar_map -> EConstr.types -> t val start_dependent_lemma - : Id.t - -> ?pl:UState.universe_decl - -> goal_kind - -> ?proof_ending:Proof_ending.t - -> ?compute_guard:lemma_possible_guards - -> ?hook:DeclareDef.Hook.t + : name:Id.t + -> poly:bool + -> ?udecl:UState.universe_decl + -> ?info:Info.t -> Proofview.telescope -> t -val start_lemma_com - : program_mode:bool - -> ?inference_hook:Pretyping.inference_hook - -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list - -> t +type lemma_possible_guards = int list list +(** Pretty much internal, only used in ComFixpoint *) val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t - -> goal_kind -> Evd.evar_map -> UState.universe_decl + -> poly:bool + -> scope:DeclareDef.locality + -> kind:goal_object_kind + -> udecl:UState.universe_decl + -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option - -> (Id.t (* name of thm *) * - (EConstr.types (* type of thm *) * - (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list + -> Recthm.t list -> int list option -> t val default_thm_id : Names.Id.t +(** Main [Lemma foo args : type.] command *) +val start_lemma_com + : program_mode:bool + -> poly:bool + -> scope:DeclareDef.locality + -> kind:goal_object_kind + -> ?inference_hook:Pretyping.inference_hook + -> ?hook:DeclareDef.Hook.t + -> Vernacexpr.proof_expr list + -> t + (* Prepare global named context for proof session: remove proofs of opaque section definitions and remove vm-compiled code *) val initialize_named_context_for_proof : unit -> Environ.named_context_val -(** {6 Saving proofs } *) +(** {4 Saving proofs} *) -type proof_info +(** The extra [?proof] parameter here is due to problems with the + lower-level [Proof_global.close_proof] API; we cannot inject closed + proofs properly in the proof state so we must leave this backdoor open. -val default_info : proof_info + The regular user can ignore it. +*) val save_lemma_admitted - : ?proof:(Proof_global.proof_object * proof_info) + : ?proof:(Proof_global.proof_object * Info.t) -> lemma:t -> unit val save_lemma_proved - : ?proof:(Proof_global.proof_object * proof_info) + : ?proof:(Proof_global.proof_object * Info.t) -> ?lemma:t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option -> unit -(* To be removed *) +(** To be removed, don't use! *) module Internal : sig + val get_info : t -> Info.t (** Only needed due to the Proof_global compatibility layer. *) - val get_info : t -> proof_info end diff --git a/vernac/locality.ml b/vernac/locality.ml index bc33d53594..f033d32874 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -8,13 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds - (** * Managing locality *) let importability_of_bool = function - | true -> ImportNeedQualified - | false -> ImportDefaultBehavior + | true -> Declare.ImportNeedQualified + | false -> Declare.ImportDefaultBehavior (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -36,13 +34,15 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = + let open DeclareDef in + let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) - | None, NoDischarge -> Global ImportDefaultBehavior + | None, NoDischarge -> Global Declare.ImportDefaultBehavior | None, DoDischarge when not (Lib.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); - Global ImportNeedQualified + Global Declare.ImportNeedQualified | None, DoDischarge -> Discharge | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") diff --git a/vernac/locality.mli b/vernac/locality.mli index be7e0cbe76..eda754324a 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -20,7 +20,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index cd8d22ac9a..b7392a28ca 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,7 +9,6 @@ (************************************************************************) open Printf -open Entries open Decl_kinds (** @@ -301,7 +300,7 @@ let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind - notations obls impls kind reduce = + notations obls impls ~scope ~poly ~kind reduce = let obls', b = match b with | None -> @@ -321,13 +320,23 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind obls, b in let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n ; prg_body = b; prg_type = reduce t; - 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; - prg_hook = hook; prg_opaque = opaque; - prg_sign = sign } + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; 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_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque + ; prg_sign = sign } let map_cardinal m = let i = ref 0 in @@ -389,16 +398,14 @@ let deps_remaining obls deps = deps [] -let goal_kind poly = - Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition) +let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition) +let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma) -let goal_proof_kind poly = - Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma) - -let kind_of_obligation poly o = +let kind_of_obligation o = match o with - | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly - | _ -> goal_proof_kind poly + | Evar_kinds.Define false + | Evar_kinds.Expand -> goal_kind + | _ -> goal_proof_kind let rec string_of_list sep f = function [] -> "" @@ -411,18 +418,17 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego str "This will become an error in the future"]) let solve_by_tac ?loc name evi t poly ctx = - let id = name in (* spiwack: the status is dropped. *) try let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.const_entry_body in + let (body, eff) = Future.force entry.Proof_global.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in @@ -446,7 +452,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = | _ -> () in let inst, ctx' = - if not (pi2 prg.prg_kind) (* Not polymorphic *) then + if not prg.prg_poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) let ctx = UState.make (Global.universes ()) in @@ -487,13 +493,15 @@ 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 scope, kind = kind_of_obligation (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 oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook in + let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in + let poly = prg.prg_poly in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma @@ -528,14 +536,14 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + prg.prg_poly (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:prg.prg_poly 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_poly 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 @@ -629,12 +637,12 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic +let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) + ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in - let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in + let info = Id.print name ++ str " has type-checked" in + let prg = init_prog_info sign ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~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 "."); @@ -643,21 +651,21 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) else ( let len = Array.length obls in let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in - progmap_add n (CEphemeron.create prg); - let res = auto_solve_obligations (Some n) tactic in + progmap_add name (CEphemeron.create prg); + let res = auto_solve_obligations (Some name) tactic in match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res | _ -> res) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic - ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce) + ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.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 univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps kind reduce ?hook + notations obls imps ~poly ~scope ~kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> @@ -681,8 +689,8 @@ let admit_prog prg = | None -> let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in - let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified - (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified + (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/obligations.mli b/vernac/obligations.mli index a0010a5026..233739ee46 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -43,12 +43,14 @@ type obligation_info = val default_tactic : unit Proofview.tactic ref val add_definition - : Names.Id.t + : name:Names.Id.t -> ?term:constr -> types -> UState.t -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) -> ?implicits:Impargs.manual_implicits - -> ?kind:Decl_kinds.definition_kind + -> poly:bool + -> ?scope:DeclareDef.locality + -> ?kind:Decl_kinds.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t @@ -56,16 +58,19 @@ val add_definition -> obligation_info -> DeclareObl.progress -val add_mutual_definitions : - (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list -> - UState.t -> - ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) - ?tactic:unit Proofview.tactic -> - ?kind:Decl_kinds.definition_kind -> - ?reduce:(constr -> constr) -> - ?hook:DeclareDef.Hook.t -> ?opaque:bool -> - DeclareObl.notations -> - DeclareObl.fixpoint_kind -> unit +val add_mutual_definitions + : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list + -> UState.t + -> ?univdecl:UState.universe_decl + (** Universe binders and constraints *) + -> ?tactic:unit Proofview.tactic + -> poly:bool + -> ?scope:DeclareDef.locality + -> ?kind:Decl_kinds.definition_object_kind + -> ?reduce:(constr -> constr) + -> ?hook:DeclareDef.Hook.t -> ?opaque:bool + -> DeclareObl.notations + -> DeclareObl.fixpoint_kind -> unit val obligation : int * Names.Id.t option * Constrexpr.constr_expr option diff --git a/vernac/record.ml b/vernac/record.ml index 7cc8d9e9b9..cc4f02349d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -342,17 +342,18 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try + let open Proof_global in let entry = { - const_entry_body = + proof_entry_body = Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); - const_entry_secctx = None; - const_entry_type = Some projtyp; - const_entry_universes = ctx; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None } in - let k = (DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:InternalTacticRequest fid k in + proof_entry_secctx = None; + proof_entry_type = Some projtyp; + proof_entry_universes = ctx; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None } in + let k = (Declare.DefinitionEntry entry,IsDefinition kind) in + let kn = declare_constant fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) @@ -366,7 +367,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f Impargs.maybe_declare_manual_implicits false refi impls; if flags.pf_subclass then begin let cl = Class.class_of_global (IndRef indsp) in - Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl + Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) @@ -469,7 +470,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in - let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in + let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in rsp in @@ -679,7 +680,7 @@ let extract_record_data records = (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure udecl kind ~template cum poly finite records = +let definition_structure udecl kind ~template cum ~poly finite records = let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in diff --git a/vernac/record.mli b/vernac/record.mli index 11d9a833e2..d0164572f3 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -31,15 +31,18 @@ val declare_projections : val declare_structure_entry : Recordops.struc_tuple -> unit -val definition_structure : - universe_decl_expr option -> inductive_kind -> template:bool option -> - Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Declarations.recursivity_kind -> - (coercion_flag * - Names.lident * - local_binder_expr list * - (local_decl_expr * record_field_attr) list * - Id.t * constr_expr option) list -> - GlobRef.t list +val definition_structure + : universe_decl_expr option + -> inductive_kind + -> template:bool option + -> Decl_kinds.cumulative_inductive_flag + -> poly:bool + -> Declarations.recursivity_kind + -> (coercion_flag * + Names.lident * + local_binder_expr list * + (local_decl_expr * record_field_attr) list * + Id.t * constr_expr option) list + -> GlobRef.t list val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/search.ml b/vernac/search.ml index d9ab76b11b..a7f1dd33c2 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -200,12 +200,10 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter_aux () = - let l = SearchBlacklist.elements () in - fun ref env typ -> +let blacklist_filter ref env typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in - List.for_all is_not_bl l + CString.Set.for_all is_not_bl (SearchBlacklist.v ()) let module_filter (mods, outside) ref env typ = let sp = Nametab.path_of_global ref in @@ -227,7 +225,6 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) let search_pattern ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -251,7 +248,6 @@ let rewrite_pat2 pat = let search_rewrite ?pstate gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || @@ -266,7 +262,6 @@ let search_rewrite ?pstate gopt pat mods pr_search = (** Search *) let search_by_head ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -280,7 +275,6 @@ let search_by_head ?pstate gopt pat mods pr_search = (** SearchAbout *) let search_about ?pstate gopt items mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && @@ -324,7 +318,6 @@ let interface_search ?pstate = let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in - let blacklist_filter = blacklist_filter_aux () in let filter_function ref env constr = let id = Names.Id.to_string (Nametab.basename_of_global ref) in let path = Libnames.dirpath (Nametab.path_of_global ref) in @@ -378,6 +371,3 @@ let interface_search ?pstate = in let () = generic_search ?pstate glnum iter in !ans - -let blacklist_filter ref env typ = - blacklist_filter_aux () ref env typ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 222f727f8e..dc46aad8af 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -560,7 +560,7 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ?hook k l = +let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = let inference_hook = if program_mode then let hook env sigma ev = @@ -574,7 +574,7 @@ let start_proof_and_print ~program_mode ?hook k l = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac + Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> user_err Pp.(str "The statement obligations could not be resolved \ @@ -582,15 +582,15 @@ let start_proof_and_print ~program_mode ?hook k l = in Some hook else None in - start_lemma_com ~program_mode ?inference_hook ?hook k l + start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l -let vernac_definition_hook p = function +let vernac_definition_hook ~poly = function | Coercion -> - Some (Class.add_coercion_hook p) + Some (Class.add_coercion_hook ~poly) | CanonicalStructure -> Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure)) | SubClass -> - Some (Class.add_subclass_hook p) + Some (Class.add_subclass_hook ~poly) | _ -> None let fresh_name_for_anonymous_theorem () = @@ -603,6 +603,7 @@ let vernac_definition_name lid local = CAst.make ?loc (fresh_name_for_anonymous_theorem ()) | { v = Name.Name n; loc } -> CAst.make ?loc n in let () = + let open DeclareDef in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Global _ -> Dumpglob.dump_definition lid false "def" @@ -612,33 +613,34 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook atts.polymorphic kind in + let hook = vernac_definition_hook ~poly:atts.polymorphic kind in let program_mode = atts.program in + let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)] + start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(DefinitionBody kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in - let hook = vernac_definition_hook atts.polymorphic kind in + let scope = enforce_locality_exp atts.locality discharge in + let hook = vernac_definition_hook ~poly:atts.polymorphic kind in let program_mode = atts.program in - let name = vernac_definition_name lid local in + let name = vernac_definition_name lid scope in let red_option = match red_option with | None -> None | Some r -> let env = Global.env () in let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~program_mode name.v - (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook + ComDefinition.do_definition ~program_mode ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook (* NB: pstate argument to use combinators easily *) let vernac_start_proof ~atts kind l = let open DefAttributes in - let local = enforce_locality_exp atts.locality NoDischarge in + let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l + start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l let vernac_end_proof ?stack ?proof = let open Vernacexpr in function | Admitted -> @@ -665,15 +667,14 @@ let vernac_exact_proof ~lemma c = let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in - let kind = local, atts.polymorphic, kind in + let scope = enforce_locality_exp atts.locality discharge in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> - match local with - | Global _ -> Dumpglob.dump_definition lid false "ax" - | Discharge -> Dumpglob.dump_definition lid true "var") idl) l; - let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in + match scope with + | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax" + | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; + let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let is_polymorphic_inductive_cumulativity = @@ -725,7 +726,7 @@ let vernac_record ~template udecl cum k poly finite records = coe, id, binders, cfs, const, sort in let records = List.map map records in - ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records) + ignore(Record.definition_structure ~template udecl k is_cumulative ~poly finite records) let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) = match indl with @@ -825,7 +826,7 @@ let vernac_inductive ~atts cum lo finite indl = let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum poly in let uniform = should_treat_as_uniform () in - ComInductive.do_mutual_inductive ~template udecl indl is_cumulative poly lo ~uniform finite + ComInductive.do_mutual_inductive ~template udecl indl is_cumulative ~poly lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -846,19 +847,19 @@ let vernac_fixpoint_common ~atts discharge l = let vernac_fixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = vernac_fixpoint_common ~atts discharge l in + let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program Fixpoint requires a body"); - ComFixpoint.do_fixpoint_interactive local atts.polymorphic l + ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l let vernac_fixpoint ~atts discharge l = let open DefAttributes in - let local = vernac_fixpoint_common ~atts discharge l in + let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then (* XXX: Switch to the attribute system and match on ~atts *) - ComProgramFixpoint.do_fixpoint local atts.polymorphic l + ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_fixpoint local atts.polymorphic l + ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then @@ -867,18 +868,18 @@ let vernac_cofixpoint_common ~atts discharge l = let vernac_cofixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = vernac_cofixpoint_common ~atts discharge l in + let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); - ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l + ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l let vernac_cofixpoint ~atts discharge l = let open DefAttributes in - let local = vernac_cofixpoint_common ~atts discharge l in + let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then - ComProgramFixpoint.do_cofixpoint local atts.polymorphic l + ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_cofixpoint local atts.polymorphic l + ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then @@ -901,14 +902,14 @@ let vernac_universe ~poly l = user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - Declare.do_universe poly l + Declare.do_universe ~poly l let vernac_constraint ~poly l = if poly && not (Lib.sections_are_opened ()) then user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - Declare.do_constraint poly l + Declare.do_constraint ~poly l (**********************) (* Modules *) @@ -1088,62 +1089,62 @@ let vernac_canonical r = Canonical.declare_canonical_structure (smart_global r) let vernac_coercion ~atts ref qids qidt = - let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in + let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' ~local polymorphic ~source ~target; + Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion ~atts id qids qidt = - let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in + let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_locality local in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id ~local polymorphic ~source ~target + Class.try_add_new_identity_coercion id ~local ~poly ~source ~target (* Type classes *) let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), polymorphic = + let (program, locality), poly = Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in - let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in + let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in () let vernac_instance_interactive ~atts name bl t info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), polymorphic = + let (program, locality), poly = Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id, pstate = - Classes.new_instance_interactive ~global polymorphic name bl t info in + Classes.new_instance_interactive ~global ~poly name bl t info in pstate let vernac_instance ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), polymorphic = + let (program, locality), poly = Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = - Classes.new_instance ~global polymorphic name bl t props info in + Classes.new_instance ~global ~poly name bl t props info in () let vernac_declare_instance ~atts id bl inst pri = Dumpglob.dump_definition (fst id) false "inst"; - let (program, locality), polymorphic = + let (program, locality), poly = Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in - Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri + Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri let vernac_context ~poly l = - if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom + if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom let vernac_existing_instance ~section_local insts = let glob = not section_local in @@ -1266,7 +1267,7 @@ let vernac_hints ~atts dbnames h = in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local dbnames (Hints.interp_hints poly h) + Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x compat = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e46212ca1c..ad3e9f93d9 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -22,7 +22,7 @@ val vernac_require : (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> - ?proof:(Proof_global.proof_object * Lemmas.proof_info) -> + ?proof:(Proof_global.proof_object * Lemmas.Info.t) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 6a67a49d0a..dc5df5904e 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -256,6 +256,8 @@ type extend_name = is given an offset, starting from zero. *) int +type discharge = DoDischarge | NoDischarge + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -274,15 +276,15 @@ type nonrec vernac_expr = | VernacDeclareCustomEntry of string (* Gallina *) - | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 2bc20a747d..f9b4aec45e 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -131,7 +131,7 @@ module Proof_global = struct s_lemmas := Some stack; res - type closed_proof = Proof_global.proof_object * Lemmas.proof_info + type closed_proof = Proof_global.proof_object * Lemmas.Info.t let return_proof ?allow_partial () = cc (return_proof ?allow_partial) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7e4d5d0315..5234ef7a73 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -51,7 +51,7 @@ module Proof_global : sig val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output - type closed_proof = Proof_global.proof_object * Lemmas.proof_info + type closed_proof = Proof_global.proof_object * Lemmas.Info.t val close_future_proof : opaque:Proof_global.opacity_flag -> |