From b4b515c2e61bc6ea662b48e84eb319ec8252b07d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:54:01 +0200 Subject: [api] Move `Vernacexpr` to parsing. There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more. --- META.coq | 4 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 4 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- parsing/extend.ml | 134 ++++++++++ parsing/parsing.mllib | 2 + parsing/vernacexpr.ml | 530 ++++++++++++++++++++++++++++++++++++++++ pretyping/extend.ml | 134 ---------- pretyping/pretyping.mllib | 2 - pretyping/vernacexpr.ml | 530 ---------------------------------------- vernac/vernacentries.ml | 4 +- 12 files changed, 675 insertions(+), 675 deletions(-) create mode 100644 parsing/extend.ml create mode 100644 parsing/vernacexpr.ml delete mode 100644 pretyping/extend.ml delete mode 100644 pretyping/vernacexpr.ml diff --git a/META.coq b/META.coq index 3414ccbd4..12d7666cb 100644 --- a/META.coq +++ b/META.coq @@ -131,10 +131,10 @@ package "interp" ( package "grammar" ( - description = "Coq Base Grammar" + description = "Coq Camlp5 Grammar Extensions for Plugins" version = "8.8" - requires = "coq.interp" + requires = "camlp5.gramlib" directory = "grammar" archive(byte) = "grammar.cma" diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3a..74618a290 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = +let dump_constraint { CAst.loc; v = n } sec ty = match n with | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 8dfb4f8f7..bf83d2df4 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : - Vernacexpr.typeclass_constraint -> bool -> string -> unit + +val dump_constraint : Misctypes.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 58df9abc4..289890544 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5f4129ae0..39d0174f9 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t diff --git a/parsing/extend.ml b/parsing/extend.ml new file mode 100644 index 000000000..734b859f6 --- /dev/null +++ b/parsing/extend.ml @@ -0,0 +1,134 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ('a list,'b list,'c list) ty_user_symbol +| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol +| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol +| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol + +(** {5 Type-safe grammar extension} *) + +type ('self, 'a) symbol = +| Atoken : Tok.t -> ('self, string) symbol +| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a entry -> ('self, 'a) symbol +| Aentryl : 'a entry * int -> ('self, 'a) symbol +| Arules : 'a rules list -> ('self, 'a) symbol + +and ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } + +and 'a rules = +| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules + +type 'a production_rule = +| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +type 'a single_extend_statment = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + +type 'a extend_statment = + gram_position option * + 'a single_extend_statment list diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 1f29636b2..103e1188a 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,5 +1,7 @@ Tok CLexer +Extend +Vernacexpr Pcoq Egramml Egramcoq diff --git a/parsing/vernacexpr.ml b/parsing/vernacexpr.ml new file mode 100644 index 000000000..6ebf66349 --- /dev/null +++ b/parsing/vernacexpr.ml @@ -0,0 +1,530 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Current, it contains the name of the coq version + which this notation is trying to be compatible with *) +type locality_flag = bool (* true = Local *) + +type option_value = Goptions.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | StringOptValue of string option + +type option_ref_value = + | StringRefValue of string + | QualidRefValue of reference + +(** Identifier and optional list of bound universes and constraints. *) + +type sort_expr = Sorts.family + +type definition_expr = + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr + * constr_expr option + +type fixpoint_expr = + ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + +type cofixpoint_expr = + ident_decl * local_binder_expr list * constr_expr * constr_expr option + +type local_decl_expr = + | AssumExpr of lname * constr_expr + | DefExpr of lname * constr_expr * constr_expr option + +type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) +type decl_notation = lstring * constr_expr * scope_name option +type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list +type 'a with_coercion = coercion_flag * 'a +type 'a with_instance = instance_flag * 'a +type 'a with_notation = 'a * decl_notation list +type 'a with_priority = 'a * int option +type constructor_expr = (lident * constr_expr) with_coercion +type constructor_list_or_record_decl_expr = + | Constructors of constructor_expr list + | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list +type inductive_expr = + ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + constructor_list_or_record_decl_expr + +type one_inductive_expr = + ident_decl * local_binder_expr list * constr_expr option * constructor_expr list + +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +and typeclass_context = typeclass_constraint list + +type proof_expr = + ident_decl * (local_binder_expr list * constr_expr) + +type syntax_modifier = + | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option + | SetLevel of int + | SetAssoc of Extend.gram_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing + | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version + | SetFormat of string * lstring + +type proof_end = + | Admitted + (* name in `Save ident` when closing goal *) + | Proved of Proof_global.opacity_flag * lident option + +type scheme = + | InductionScheme of bool * reference or_by_notation * sort_expr + | CaseScheme of bool * reference or_by_notation * sort_expr + | EqualityScheme of reference or_by_notation + +type section_subset_expr = + | SsEmpty + | SsType + | SsSingl of lident + | SsCompl of section_subset_expr + | SsUnion of section_subset_expr * section_subset_expr + | SsSubstr of section_subset_expr * section_subset_expr + | SsFwdClose of section_subset_expr + +(** Extension identifiers for the VERNAC EXTEND mechanism. + + {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. + + {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. + + {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. + + {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. + + {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. + + {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. + + {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. + + {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. + + {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. + + {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. + *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int + +(* This type allows registering the inlining of constants in native compiler. + It will be extended with primitive inductive types and operators *) +type register_kind = + | RegisterInline + +type bullet = Proof_bullet.t +[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] + +(** {6 Types concerning the module layer} *) + +(** Rigid / flexible module signature *) + +type 'a module_signature = 'a Declaremods.module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) +[@@ocaml.deprecated "please use [Declaremods.module_signature]."] + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = Declaremods.inline = + | NoInline + | DefaultInline + | InlineAt of int +[@@ocaml.deprecated "please use [Declaremods.inline]."] + +type module_ast_inl = module_ast * Declaremods.inline +type module_binder = bool option * lident list * module_ast_inl + +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type vernac_cumulative = VernacCumulative | VernacNonCumulative + +(** {6 The type of vernacular expressions} *) + +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string CAst.t option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = + + | VernacLoad of verbose_flag * string + (* Syntax *) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name + | VernacDelimiters of scope_name * string option + | VernacBindScope of scope_name * class_rawexpr list + | VernacInfix of (lstring * syntax_modifier list) * + constr_expr * scope_name option + | VernacNotation of + constr_expr * (lstring * syntax_modifier list) * + scope_name option + | VernacNotationAddFormat of string * string * string + + (* Gallina *) + | VernacDefinition of (Decl_kinds.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) * + 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 + | VernacScheme of (lident option * scheme) list + | VernacCombinedScheme of lident * lident list + | VernacUniverse of lident list + | VernacConstraint of Glob_term.glob_constraint list + + (* Gallina extensions *) + | VernacBeginSection of lident + | VernacEndSegment of lident + | VernacRequire of + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list + | VernacCanonical of reference or_by_notation + | VernacCoercion of reference or_by_notation * + class_rawexpr * class_rawexpr + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr + | VernacNameSectionHypSet of lident * section_subset_expr + + (* Type classes *) + | VernacInstance of + bool * (* abstract instance *) + local_binder_expr list * (* super *) + typeclass_constraint * (* instance name, class name, params *) + (bool * constr_expr) option * (* props *) + Typeclasses.hint_info_expr + + | VernacContext of local_binder_expr list + + | VernacDeclareInstances of + (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) + + | VernacDeclareClass of reference (* inductive or definition name *) + + (* Modules and Module Types *) + | VernacDeclareModule of bool option * lident * + module_binder list * module_ast_inl + | VernacDefineModule of bool option * lident * module_binder list * + module_ast_inl Declaremods.module_signature * module_ast_inl list + | VernacDeclareModuleType of lident * + module_binder list * module_ast_inl list * module_ast_inl list + | VernacInclude of module_ast_inl list + + (* Solving *) + + | VernacSolveExistential of int * constr_expr + + (* Auxiliary file and library management *) + | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacRemoveLoadPath of string + | VernacAddMLPath of rec_flag * string + | VernacDeclareMLModule of string list + | VernacChdir of string option + + (* State management *) + | VernacWriteState of string + | VernacRestoreState of string + + (* Resetting *) + | VernacResetName of lident + | VernacResetInitial + | VernacBack of int + | VernacBackTo of int + + (* Commands *) + | VernacCreateHintDb of string * bool + | VernacRemoveHints of string list * reference list + | VernacHints of string list * hints_expr + | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + onlyparsing_flag + | VernacArguments of reference or_by_notation * + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list + | VernacReserve of simple_binder list + | VernacGeneralizable of (lident list) option + | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetStrategy of + (Conv_oracle.level * reference or_by_notation list) list + | VernacUnsetOption of export_flag * Goptions.option_name + | VernacSetOption of export_flag * Goptions.option_name * option_value + | VernacAddOption of Goptions.option_name * option_ref_value list + | VernacRemoveOption of Goptions.option_name * option_ref_value list + | VernacMemOption of Goptions.option_name * option_ref_value list + | VernacPrintOption of Goptions.option_name + | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr + | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr + | VernacPrint of printable + | VernacSearch of searchable * Goal_select.t option * search_restriction + | VernacLocate of locatable + | VernacRegister of lident * register_kind + | VernacComments of comment list + + (* Proof management *) + | VernacAbort of lident option + | VernacAbortAll + | VernacRestart + | VernacUndo of int + | VernacUndoTo of int + | VernacFocus of int option + | VernacUnfocus + | VernacUnfocused + | VernacBullet of Proof_bullet.t + | VernacSubproof of Goal_select.t option + | VernacEndSubproof + | VernacShow of showable + | VernacCheckGuard + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option + | VernacProofMode of string + + (* For extension *) + | VernacExtend of extend_name * Genarg.raw_generic_argument list + +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool + +type vernac_control = + | VernacExpr of vernac_flag list * vernac_expr + (* boolean is true when the `-time` batch-mode command line flag was set. + the flag is used to print differently in `-time` vs `Time foo` *) + | VernacTime of bool * vernac_control CAst.t + | VernacRedirect of string * vernac_control CAst.t + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or + alters the global state or is a control command like BackTo or is + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of proof_step + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Id.t list +and vernac_sideff_type = Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option +} +and solving_tac = bool (* a terminator *) +and anon_abstracting_tac = bool (* abstracting anonymously its result *) +and proof_block_name = string (* open type of delimiters *) +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/pretyping/extend.ml b/pretyping/extend.ml deleted file mode 100644 index 734b859f6..000000000 --- a/pretyping/extend.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* ('a list,'b list,'c list) ty_user_symbol -| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol -| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol -| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol - -(** {5 Type-safe grammar extension} *) - -type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, string) symbol -| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol -| Aself : ('self, 'self) symbol -| Anext : ('self, 'self) symbol -| Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * int -> ('self, 'a) symbol -| Arules : 'a rules list -> ('self, 'a) symbol - -and ('self, _, 'r) rule = -| Stop : ('self, 'r, 'r) rule -| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - -and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } - -and 'a rules = -| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - -type 'a production_rule = -| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statment = - string option * - (** Level *) - gram_assoc option * - (** Associativity *) - 'a production_rule list - (** Symbol list with the interpretation function *) - -type 'a extend_statment = - gram_position option * - 'a single_extend_statment list diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d98026bc6..c48decdb0 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -27,8 +27,6 @@ Pattern Patternops Constr_matching Tacred -Extend -Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml deleted file mode 100644 index 71a2e8cb8..000000000 --- a/pretyping/vernacexpr.ml +++ /dev/null @@ -1,530 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Current, it contains the name of the coq version - which this notation is trying to be compatible with *) -type locality_flag = bool (* true = Local *) - -type option_value = Goptions.option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option - -type option_ref_value = - | StringRefValue of string - | QualidRefValue of reference - -(** Identifier and optional list of bound universes and constraints. *) - -type sort_expr = Sorts.family - -type definition_expr = - | ProveBody of local_binder_expr list * constr_expr - | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr - * constr_expr option - -type fixpoint_expr = - ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option - -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option - -type local_decl_expr = - | AssumExpr of lname * constr_expr - | DefExpr of lname * constr_expr * constr_expr option - -type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option -type simple_binder = lident list * constr_expr -type class_binder = lident * constr_expr list -type 'a with_coercion = coercion_flag * 'a -type 'a with_instance = instance_flag * 'a -type 'a with_notation = 'a * decl_notation list -type 'a with_priority = 'a * int option -type constructor_expr = (lident * constr_expr) with_coercion -type constructor_list_or_record_decl_expr = - | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list -type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * - constructor_list_or_record_decl_expr - -type one_inductive_expr = - ident_decl * local_binder_expr list * constr_expr option * constructor_expr list - -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr -and typeclass_context = typeclass_constraint list - -type proof_expr = - ident_decl * (local_binder_expr list * constr_expr) - -type syntax_modifier = - | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option - | SetLevel of int - | SetAssoc of Extend.gram_assoc - | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing - | SetOnlyPrinting - | SetCompatVersion of Flags.compat_version - | SetFormat of string * lstring - -type proof_end = - | Admitted - (* name in `Save ident` when closing goal *) - | Proved of opacity_flag * lident option - -type scheme = - | InductionScheme of bool * reference or_by_notation * sort_expr - | CaseScheme of bool * reference or_by_notation * sort_expr - | EqualityScheme of reference or_by_notation - -type section_subset_expr = - | SsEmpty - | SsType - | SsSingl of lident - | SsCompl of section_subset_expr - | SsUnion of section_subset_expr * section_subset_expr - | SsSubstr of section_subset_expr * section_subset_expr - | SsFwdClose of section_subset_expr - -(** Extension identifiers for the VERNAC EXTEND mechanism. - - {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. - - {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. - - {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. - - {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. - - {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. - - {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. - - {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. - - {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. - - {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. - - {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. - *) -type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) - string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) - int - -(* This type allows registering the inlining of constants in native compiler. - It will be extended with primitive inductive types and operators *) -type register_kind = - | RegisterInline - -type bullet = Proof_bullet.t -[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] - -(** {6 Types concerning the module layer} *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = 'a Declaremods.module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) -[@@ocaml.deprecated "please use [Declaremods.module_signature]."] - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = Declaremods.inline = - | NoInline - | DefaultInline - | InlineAt of int -[@@ocaml.deprecated "please use [Declaremods.inline]."] - -type module_ast_inl = module_ast * Declaremods.inline -type module_binder = bool option * lident list * module_ast_inl - -(** [Some b] if locally enabled/disabled according to [b], [None] if - we should use the global flag. *) -type vernac_cumulative = VernacCumulative | VernacNonCumulative - -(** {6 The type of vernacular expressions} *) - -type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -type vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string CAst.t option; - implicit_status : vernac_implicit_status; -} - -type nonrec vernac_expr = - - | VernacLoad of verbose_flag * string - (* Syntax *) - | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) - | VernacOpenCloseScope of bool * scope_name - | VernacDelimiters of scope_name * string option - | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of (lstring * syntax_modifier list) * - constr_expr * scope_name option - | VernacNotation of - constr_expr * (lstring * syntax_modifier list) * - scope_name option - | VernacNotationAddFormat of string * string * string - - (* Gallina *) - | VernacDefinition of (Decl_kinds.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) * - 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 - | VernacScheme of (lident option * scheme) list - | VernacCombinedScheme of lident * lident list - | VernacUniverse of lident list - | VernacConstraint of Glob_term.glob_constraint list - - (* Gallina extensions *) - | VernacBeginSection of lident - | VernacEndSegment of lident - | VernacRequire of - reference option * export_flag option * reference list - | VernacImport of export_flag * reference list - | VernacCanonical of reference or_by_notation - | VernacCoercion of reference or_by_notation * - class_rawexpr * class_rawexpr - | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_expr - - (* Type classes *) - | VernacInstance of - bool * (* abstract instance *) - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Typeclasses.hint_info_expr - - | VernacContext of local_binder_expr list - - | VernacDeclareInstances of - (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) - - | VernacDeclareClass of reference (* inductive or definition name *) - - (* Modules and Module Types *) - | VernacDeclareModule of bool option * lident * - module_binder list * module_ast_inl - | VernacDefineModule of bool option * lident * module_binder list * - module_ast_inl Declaremods.module_signature * module_ast_inl list - | VernacDeclareModuleType of lident * - module_binder list * module_ast_inl list * module_ast_inl list - | VernacInclude of module_ast_inl list - - (* Solving *) - - | VernacSolveExistential of int * constr_expr - - (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option - | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string - | VernacDeclareMLModule of string list - | VernacChdir of string option - - (* State management *) - | VernacWriteState of string - | VernacRestoreState of string - - (* Resetting *) - | VernacResetName of lident - | VernacResetInitial - | VernacBack of int - | VernacBackTo of int - - (* Commands *) - | VernacCreateHintDb of string * bool - | VernacRemoveHints of string list * reference list - | VernacHints of string list * hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * - onlyparsing_flag - | VernacArguments of reference or_by_notation * - vernac_argument_status list (* Main arguments status list *) * - (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list - | VernacReserve of simple_binder list - | VernacGeneralizable of (lident list) option - | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) - | VernacSetStrategy of - (Conv_oracle.level * reference or_by_notation list) list - | VernacUnsetOption of export_flag * Goptions.option_name - | VernacSetOption of export_flag * Goptions.option_name * option_value - | VernacAddOption of Goptions.option_name * option_ref_value list - | VernacRemoveOption of Goptions.option_name * option_ref_value list - | VernacMemOption of Goptions.option_name * option_ref_value list - | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr - | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * Genredexpr.raw_red_expr - | VernacPrint of printable - | VernacSearch of searchable * Goal_select.t option * search_restriction - | VernacLocate of locatable - | VernacRegister of lident * register_kind - | VernacComments of comment list - - (* Proof management *) - | VernacAbort of lident option - | VernacAbortAll - | VernacRestart - | VernacUndo of int - | VernacUndoTo of int - | VernacFocus of int option - | VernacUnfocus - | VernacUnfocused - | VernacBullet of Proof_bullet.t - | VernacSubproof of Goal_select.t option - | VernacEndSubproof - | VernacShow of showable - | VernacCheckGuard - | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option - | VernacProofMode of string - - (* For extension *) - | VernacExtend of extend_name * Genarg.raw_generic_argument list - -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool - -type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr - (* boolean is true when the `-time` batch-mode command line flag was set. - the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control CAst.t - | VernacRedirect of string * vernac_control CAst.t - | VernacTimeout of int * vernac_control - | VernacFail of vernac_control - -(* A vernac classifier provides information about the exectuion of a - command: - - - vernac_when: encodes if the vernac may alter the parser [thus - forcing immediate execution], or if indeed it is pure and parsing - can continue without its execution. - - - vernac_type: if it is starts, ends, continues a proof or - alters the global state or is a control command like BackTo or is - a query like Check. - - The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof - state. For example, commands that only alter the proof state are - considered safe to delegate to a worker. - -*) -type vernac_type = - (* Start of a proof *) - | VtStartProof of vernac_start - (* Command altering the global state, bad for parallel - processing. *) - | VtSideff of vernac_sideff_type - (* End of a proof *) - | VtQed of vernac_qed_type - (* A proof step *) - | VtProofStep of proof_step - (* To be removed *) - | VtProofMode of string - (* Queries are commands assumed to be "pure", that is to say, they - don't modify the interpretation state. *) - | VtQuery - (* To be removed *) - | VtMeta - | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list -and vernac_sideff_type = Id.t list -and opacity_guarantee = - | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) - | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option -} -and solving_tac = bool (* a terminator *) -and anon_abstracting_tac = bool (* abstracting anonymously its result *) -and proof_block_name = string (* open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - - -(** Deprecated stuff *) -type universe_decl_expr = Constrexpr.universe_decl_expr -[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] - -type ident_decl = Constrexpr.ident_decl -[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] - -type name_decl = Constrexpr.name_decl -[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 48deea97f..e1ce4e194 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint inst false "inst"; + Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) @@ -1268,7 +1268,7 @@ let vernac_reserve bl = let vernac_generalizable ~atts = let local = make_non_locality atts.locality in - Implicit_quantifiers.declare_generalizable local + Implicit_quantifiers.declare_generalizable ~local let _ = declare_bool_option -- cgit v1.2.3