diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-19 16:54:01 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-23 13:23:29 +0200 |
commit | b4b515c2e61bc6ea662b48e84eb319ec8252b07d (patch) | |
tree | e2b501a4cfe8915ce7c179672b1eae3aa5f7e205 /parsing | |
parent | e87288450d4d9e49ac91d179714a73bd0147c0d7 (diff) |
[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.
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/extend.ml | 134 | ||||
-rw-r--r-- | parsing/parsing.mllib | 2 | ||||
-rw-r--r-- | parsing/vernacexpr.ml | 530 |
3 files changed, 666 insertions, 0 deletions
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 *) +(* <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) *) +(************************************************************************) + +(** Entry keys for constr notations *) + +type 'a entry = 'a Grammar.GMake(CLexer).Entry.e + +type side = Left | Right + +type gram_assoc = NonA | RightA | LeftA + +type gram_position = + | First + | Last + | Before of string + | After of string + | Level of string + +type production_position = + | BorderProd of side * gram_assoc option + | InternalProd + +type production_level = + | NextLevel + | NumLevel of int + +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + +(** User-level types used to tell how to parse or interpret of the non-terminal *) + +type 'a constr_entry_key_gen = + | ETName + | ETReference + | ETBigint + | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) + | ETConstr of 'a + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) + | ETOther of string * string + +(** Entries level (left-hand side of grammar rules) *) + +type constr_entry_key = + (production_level * production_position) constr_entry_key_gen + +(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) + +type simple_constr_prod_entry_key = + production_level option constr_entry_key_gen + +(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) + +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + +type binder_target = ForBinder | ForTerm + +type constr_prod_entry_key = + | ETProdName (* Parsed as a name (ident or _) *) + | ETProdReference (* Parsed as a global reference *) + | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) + | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) + | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) + | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) + +(** {5 AST for user-provided entries} *) + +type 'a user_symbol = +| Ulist1 of 'a user_symbol +| Ulist1sep of 'a user_symbol * string +| Ulist0 of 'a user_symbol +| Ulist0sep of 'a user_symbol * string +| Uopt of 'a user_symbol +| Uentry of 'a +| Uentryl of 'a * int + +type ('a,'b,'c) ty_user_symbol = +| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('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 *) +(* <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) *) +(************************************************************************) + +open Names +open Misctypes +open Constrexpr +open Libnames + +(** Vernac expressions, produced by the parser *) +type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + +type goal_selector = Goal_select.t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll +[@@ocaml.deprecated "Use Goal_select.t"] + +type goal_identifier = string +type scope_name = string + +type goal_reference = + | OpenSubgoals + | NthGoal of int + | GoalId of Id.t + +type univ_name_list = UnivNames.univ_name_list +[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] + +type printable = + | PrintTables + | PrintFullContext + | PrintSectionContext of reference + | PrintInspect of int + | PrintGrammar of string + | PrintLoadPath of DirPath.t option + | PrintModules + | PrintModule of reference + | PrintModuleType of reference + | PrintNamespace of DirPath.t + | PrintMLLoadPath + | PrintMLModules + | PrintDebugGC + | PrintName of reference or_by_notation * UnivNames.univ_name_list option + | PrintGraph + | PrintClasses + | PrintTypeClasses + | PrintInstances of reference or_by_notation + | PrintCoercions + | PrintCoercionPaths of class_rawexpr * class_rawexpr + | PrintCanonicalConversions + | PrintUniverses of bool * string option + | PrintHint of reference or_by_notation + | PrintHintGoal + | PrintHintDbName of string + | PrintHintDb + | PrintScopes + | PrintScope of string + | PrintVisibility of string option + | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option + | PrintImplicit of reference or_by_notation + | PrintAssumptions of bool * bool * reference or_by_notation + | PrintStrategy of reference or_by_notation option + +type search_about_item = + | SearchSubPattern of constr_pattern_expr + | SearchString of string * scope_name option + +type searchable = + | SearchPattern of constr_pattern_expr + | SearchRewrite of constr_pattern_expr + | SearchHead of constr_pattern_expr + | SearchAbout of (bool * search_about_item) list + +type locatable = + | LocateAny of reference or_by_notation + | LocateTerm of reference or_by_notation + | LocateLibrary of reference + | LocateModule of reference + | LocateOther of string * reference + | LocateFile of string + +type showable = + | ShowGoal of goal_reference + | ShowProof + | ShowScript + | ShowExistentials + | ShowUniverses + | ShowProofNames + | ShowIntros of bool + | ShowMatch of reference + +type comment = + | CommentConstr of constr_expr + | CommentString of string + | CommentInt of int + +type reference_or_constr = + | HintsReference of reference + | HintsConstr of constr_expr + +type hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) + +type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = + { hint_priority : int option; + hint_pattern : 'a option } +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] + +type hint_info_expr = Typeclasses.hint_info_expr +[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"] + +type hints_expr = + | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list + | HintsImmediate of reference_or_constr list + | HintsUnfold of reference list + | HintsTransparency of reference list * bool + | HintsMode of reference * hint_mode list + | HintsConstructors of reference list + | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument + +type search_restriction = + | SearchInside of reference list + | SearchOutside of reference list + +type rec_flag = bool (* true = Rec; false = NoRec *) +type verbose_flag = bool (* true = Verbose; false = Silent *) +type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent + [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] +type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) +type instance_flag = bool option + (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) +type export_flag = bool (* true = Export; false = Import *) +type inductive_flag = Declarations.recursivity_kind +type onlyparsing_flag = Flags.compat_version option + (* Some v = Parse only; None = Print also. + If v<>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"] |