From 7dfac786626f8f6775dadc0df85360759584c976 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 28 Dec 2017 00:16:46 +0100 Subject: [api] Relocate `intf` modules according to dependency-order. In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc... --- .github/CODEOWNERS | 5 - .merlin | 2 - META.coq | 13 - Makefile.common | 4 +- configure.ml | 2 +- dev/base_include | 1 - dev/core.dbg | 1 - dev/doc/coq-src-description.txt | 6 - dev/ocamldebug-coq.run | 2 +- engine/engine.mllib | 1 + engine/evar_kinds.ml | 39 +++ interp/interp.mllib | 1 + interp/notation_term.ml | 124 ++++++++++ intf/constrexpr.ml | 153 ------------ intf/decl_kinds.ml | 87 ------- intf/evar_kinds.ml | 39 --- intf/extend.ml | 134 ---------- intf/genredexpr.ml | 66 ----- intf/glob_term.ml | 113 --------- intf/intf.mllib | 11 - intf/locus.ml | 96 -------- intf/misctypes.ml | 149 ----------- intf/notation_term.ml | 124 ---------- intf/pattern.ml | 43 ---- intf/vernacexpr.ml | 533 ---------------------------------------- library/decl_kinds.ml | 87 +++++++ library/library.mllib | 2 + library/misctypes.ml | 149 +++++++++++ pretyping/constrexpr.ml | 153 ++++++++++++ pretyping/extend.ml | 134 ++++++++++ pretyping/genredexpr.ml | 66 +++++ pretyping/glob_term.ml | 113 +++++++++ pretyping/locus.ml | 96 ++++++++ pretyping/pattern.ml | 43 ++++ pretyping/pretyping.mllib | 9 +- pretyping/vernacexpr.ml | 533 ++++++++++++++++++++++++++++++++++++++++ 36 files changed, 1553 insertions(+), 1581 deletions(-) create mode 100644 engine/evar_kinds.ml create mode 100644 interp/notation_term.ml delete mode 100644 intf/constrexpr.ml delete mode 100644 intf/decl_kinds.ml delete mode 100644 intf/evar_kinds.ml delete mode 100644 intf/extend.ml delete mode 100644 intf/genredexpr.ml delete mode 100644 intf/glob_term.ml delete mode 100644 intf/intf.mllib delete mode 100644 intf/locus.ml delete mode 100644 intf/misctypes.ml delete mode 100644 intf/notation_term.ml delete mode 100644 intf/pattern.ml delete mode 100644 intf/vernacexpr.ml create mode 100644 library/decl_kinds.ml create mode 100644 library/misctypes.ml create mode 100644 pretyping/constrexpr.ml create mode 100644 pretyping/extend.ml create mode 100644 pretyping/genredexpr.ml create mode 100644 pretyping/glob_term.ml create mode 100644 pretyping/locus.ml create mode 100644 pretyping/pattern.ml create mode 100644 pretyping/vernacexpr.ml diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 029b55b9a..7f3ee5c37 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -86,11 +86,6 @@ /interp/ @herbelin # Secondary maintainer @ejgallego -########## Interfaces ########## - -/intf/ @letouzey -# Secondary maintainer @ppedrot - ########## Kernel ########## /kernel/ @maximedenes diff --git a/.merlin b/.merlin index d60f5037b..40db60950 100644 --- a/.merlin +++ b/.merlin @@ -10,8 +10,6 @@ S kernel B kernel S kernel/byterun B kernel/byterun -S intf -B intf S library B library S engine diff --git a/META.coq b/META.coq index 30bfdd67a..3414ccbd4 100644 --- a/META.coq +++ b/META.coq @@ -90,19 +90,6 @@ package "library" ( ) -package "intf" ( - - description = "Coq Public Data Types" - version = "8.8" - - requires = "coq.library" - - directory = "intf" - - archive(byte) = "intf.cma" - archive(native) = "intf.cmxa" -) - package "engine" ( description = "Coq Tactic Engine" diff --git a/Makefile.common b/Makefile.common index 9a30e2a4c..eed41fbe7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -75,7 +75,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config clib lib kernel intf kernel/byterun library \ + config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel @@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \ +CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma diff --git a/configure.ml b/configure.ml index 6c052b63b..2ac705ad2 100644 --- a/configure.ml +++ b/configure.ml @@ -1212,7 +1212,7 @@ let write_configml f = let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; "intf"; + "tactics"; "toplevel"; "printing"; "grammar"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" diff --git a/dev/base_include b/dev/base_include index e76044f41..2f7183dd6 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; diff --git a/dev/core.dbg b/dev/core.dbg index 57c136900..edf67020a 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,4 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer intf.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e5..764d48295 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea..8f1c165dd 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -18,7 +18,7 @@ exec $OCAMLDEBUG \ -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml new file mode 100644 index 000000000..c964ecf1f --- /dev/null +++ b/engine/evar_kinds.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * 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/intf/genredexpr.ml b/intf/genredexpr.ml deleted file mode 100644 index 80697461a..000000000 --- a/intf/genredexpr.ml +++ /dev/null @@ -1,66 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* any_glob_constr - -type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t -type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list -type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list - -type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g -type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g -type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g - -type 'a extended_glob_local_binder_r = - | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g - | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option - | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g -and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t - -type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g diff --git a/intf/intf.mllib b/intf/intf.mllib deleted file mode 100644 index 2b8960d3f..000000000 --- a/intf/intf.mllib +++ /dev/null @@ -1,11 +0,0 @@ -Constrexpr -Evar_kinds -Genredexpr -Locus -Extend -Notation_term -Decl_kinds -Glob_term -Misctypes -Pattern -Vernacexpr diff --git a/intf/locus.ml b/intf/locus.ml deleted file mode 100644 index 95a2e495b..000000000 --- a/intf/locus.ml +++ /dev/null @@ -1,96 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* _ ? *) } - -type constr_pattern = - | PRef of global_reference - | PVar of Id.t - | PEvar of existential_key * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of patvar * constr_pattern list - | PProj of Projection.t * constr_pattern - | PLambda of Name.t * constr_pattern * constr_pattern - | PProd of Name.t * constr_pattern * constr_pattern - | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of glob_sort - | PMeta of patvar option - | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * bool list * constr_pattern) list (** index of constructor, nb of args *) - | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) - | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) - -(** Nota : in a [PCase], the array of branches might be shorter than - expected, denoting the use of a final "_ => _" branch *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml deleted file mode 100644 index 4e1c986f1..000000000 --- a/intf/vernacexpr.ml +++ /dev/null @@ -1,533 +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 = - | Dash of int - | Star of int - | Plus of int - -(** {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_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 *) - hint_info_expr - - | VernacContext of local_binder_expr list - - | VernacDeclareInstances of - (reference * 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_selector option * constr_expr - | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * Genredexpr.raw_red_expr - | VernacPrint of printable - | VernacSearch of searchable * goal_selector 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 bullet - | VernacSubproof of goal_selector 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/library/decl_kinds.ml b/library/decl_kinds.ml new file mode 100644 index 000000000..0d3285311 --- /dev/null +++ b/library/decl_kinds.ml @@ -0,0 +1,87 @@ +(************************************************************************) +(* * 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/genredexpr.ml b/pretyping/genredexpr.ml new file mode 100644 index 000000000..80697461a --- /dev/null +++ b/pretyping/genredexpr.ml @@ -0,0 +1,66 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* any_glob_constr + +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g + +type 'a extended_glob_local_binder_r = + | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g + | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g +and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t + +type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g diff --git a/pretyping/locus.ml b/pretyping/locus.ml new file mode 100644 index 000000000..95a2e495b --- /dev/null +++ b/pretyping/locus.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* _ ? *) } + +type constr_pattern = + | PRef of global_reference + | PVar of Id.t + | PEvar of existential_key * constr_pattern array + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of patvar * constr_pattern list + | PProj of Projection.t * constr_pattern + | PLambda of Name.t * constr_pattern * constr_pattern + | PProd of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern + | PSort of glob_sort + | PMeta of patvar option + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) + | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) + +(** Nota : in a [PCase], the array of branches might be shorter than + expected, denoting the use of a final "_ => _" branch *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ae4ad0be7..d98026bc6 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,5 +1,5 @@ Geninterp -Ltac_pretype +Locus Locusops Pretype_errors Reductionops @@ -16,12 +16,19 @@ Evarsolve Recordops Evarconv Typing +Constrexpr +Genredexpr Miscops +Glob_term +Ltac_pretype Glob_ops Redops +Pattern Patternops Constr_matching Tacred +Extend +Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml new file mode 100644 index 000000000..4e1c986f1 --- /dev/null +++ b/pretyping/vernacexpr.ml @@ -0,0 +1,533 @@ +(************************************************************************) +(* * 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 = + | Dash of int + | Star of int + | Plus of int + +(** {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_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 *) + hint_info_expr + + | VernacContext of local_binder_expr list + + | VernacDeclareInstances of + (reference * 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_selector option * constr_expr + | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr + | VernacPrint of printable + | VernacSearch of searchable * goal_selector 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 bullet + | VernacSubproof of goal_selector 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"] -- cgit v1.2.3