diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 152 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 87 | ||||
| -rw-r--r-- | intf/evar_kinds.ml | 37 | ||||
| -rw-r--r-- | intf/extend.ml | 134 | ||||
| -rw-r--r-- | intf/genredexpr.ml | 66 | ||||
| -rw-r--r-- | intf/glob_term.ml | 112 | ||||
| -rw-r--r-- | intf/intf.mllib | 11 | ||||
| -rw-r--r-- | intf/locus.ml | 96 | ||||
| -rw-r--r-- | intf/misctypes.ml | 162 | ||||
| -rw-r--r-- | intf/notation_term.ml | 123 | ||||
| -rw-r--r-- | intf/pattern.ml | 44 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 543 |
12 files changed, 0 insertions, 1567 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml deleted file mode 100644 index 542eb38a..00000000 --- a/intf/constrexpr.ml +++ /dev/null @@ -1,152 +0,0 @@ -(************************************************************************) -(* * 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 Libnames -open Misctypes -open Decl_kinds - -(** {6 Concrete syntax for terms } *) - -(** [constr_expr] is the abstract syntax tree produced by the parser *) - -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl - -type ident_decl = lident * universe_decl_expr option -type name_decl = lname * universe_decl_expr option - -type notation = string - -type explicitation = - | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) - | ExplByName of Id.t - -type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool - (** Inner binding, outer bindings, typeclass-specific flag - for implicit generalization of superclasses *) - -type abstraction_kind = AbsLambda | AbsPi - -type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) - -(** Representation of integer literals that appear in Coq scripts. - We now use raw strings of digits in base 10 (big-endian), and a separate - sign flag. Note that this representation is not unique, due to possible - multiple leading zeros, and -0 = +0 *) - -type sign = bool -type raw_natural_number = string - -type prim_token = - | Numeral of raw_natural_number * sign - | String of string - -type instance_expr = Misctypes.glob_level list - -type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * lname - | CPatCstr of reference - * cases_pattern_expr list option * cases_pattern_expr list - (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) - | CPatAtom of reference option - | CPatOr of cases_pattern_expr list - | CPatNotation of notation * cases_pattern_notation_substitution - * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents - (notation n applied with substitution l1) - applied to arguments l2 *) - | CPatPrim of prim_token - | CPatRecord of (reference * cases_pattern_expr) list - | CPatDelimiters of string * cases_pattern_expr - | CPatCast of cases_pattern_expr * constr_expr -and cases_pattern_expr = cases_pattern_expr_r CAst.t - -and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) - -and constr_expr_r = - | CRef of reference * instance_expr option - | CFix of lident * fix_expr list - | CCoFix of lident * cofix_expr list - | CProdN of local_binder_expr list * constr_expr - | CLambdaN of local_binder_expr list * constr_expr - | CLetIn of lname * constr_expr * constr_expr option * constr_expr - | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list - | CApp of (proj_flag * constr_expr) * - (constr_expr * explicitation CAst.t option) list - | CRecord of (reference * constr_expr) list - - (* representation of the "let" and "match" constructs *) - | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) - * constr_expr option (* return-clause *) - * case_expr list - * branch_expr list (* branches *) - - | CLetTuple of lname list * (lname option * constr_expr option) * - constr_expr * constr_expr - | CIf of constr_expr * (lname option * constr_expr option) - * constr_expr * constr_expr - | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option - | CPatVar of patvar - | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list - | CSort of glob_sort - | CCast of constr_expr * constr_expr cast_type - | CNotation of notation * constr_notation_substitution - | CGeneralization of binding_kind * abstraction_kind option * constr_expr - | CPrim of prim_token - | CDelimiters of string * constr_expr -and constr_expr = constr_expr_r CAst.t - -and case_expr = constr_expr (* expression that is being matched *) - * lname option (* as-clause *) - * cases_pattern_expr option (* in-clause *) - -and branch_expr = - (cases_pattern_expr list list * constr_expr) CAst.t - -and fix_expr = - lident * (lident option * recursion_order_expr) * - local_binder_expr list * constr_expr * constr_expr - -and cofix_expr = - lident * local_binder_expr list * constr_expr * constr_expr - -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) - -(* Anonymous defs allowed ?? *) -and local_binder_expr = - | CLocalAssum of lname list * binder_kind * constr_expr - | CLocalDef of lname * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t - -and constr_notation_substitution = - constr_expr list * (** for constr subterms *) - constr_expr list list * (** for recursive notations *) - cases_pattern_expr list * (** for binders *) - local_binder_expr list list (** for binder lists (recursive notations) *) - -type constr_pattern_expr = constr_expr - -(** Concrete syntax for modules and module types *) - -type with_declaration_ast = - | CWith_Module of Id.t list CAst.t * qualid CAst.t - | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr - -type module_ast_r = - | CMident of qualid - | CMapply of module_ast * module_ast - | CMwith of module_ast * with_declaration_ast -and module_ast = module_ast_r CAst.t diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml deleted file mode 100644 index 0d328531..00000000 --- a/intf/decl_kinds.ml +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -(** Informal mathematical status of declarations *) - -type discharge = DoDischarge | NoDischarge - -type locality = Discharge | Local | Global - -type binding_kind = Explicit | Implicit - -type polymorphic = bool - -type private_flag = bool - -type cumulative_inductive_flag = bool - -type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - -type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - -type assumption_object_kind = Definitional | Logical | Conjectural - -(* [assumption_kind] - - | Local | Global - ------------------------------------ - Definitional | Variable | Parameter - Logical | Hypothesis | Axiom - -*) -type assumption_kind = locality * polymorphic * assumption_object_kind - -type definition_kind = locality * polymorphic * definition_object_kind - -(** Kinds used in proofs *) - -type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - -type goal_kind = locality * polymorphic * goal_object_kind - -(** Kinds used in library *) - -type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - -(** Recursive power of type declarations *) - -type recursivity_kind = Declarations.recursivity_kind = - | Finite (** = inductive *) - [@ocaml.deprecated "Please use [Declarations.Finite"] - | CoFinite (** = coinductive *) - [@ocaml.deprecated "Please use [Declarations.CoFinite"] - | BiFinite (** = non-recursive, like in "Record" definitions *) - [@ocaml.deprecated "Please use [Declarations.BiFinite"] -[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml deleted file mode 100644 index c5de383b..00000000 --- a/intf/evar_kinds.ml +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* * 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 Globnames -open Misctypes - -(** The kinds of existential variable *) - -(** Should the obligation be defined (opaque or transparent (default)) or - defined transparent and expanded in the term? *) - -type obligation_definition_status = Define of bool | Expand - -type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar - -type t = - | ImplicitArg of global_reference * (int * Id.t option) - * bool (** Force inference *) - | BinderType of Name.t - | NamedHole of Id.t (* coming from some ?[id] syntax *) - | QuestionMark of obligation_definition_status * Name.t - | CasesType of bool (* true = a subterm of the type *) - | InternalHole - | TomatchTypeParameter of inductive * int - | GoalEvar - | ImpossibleCase - | MatchingVar of matching_var_kind - | VarInstance of Id.t - | SubEvar of Evar.t diff --git a/intf/extend.ml b/intf/extend.ml deleted file mode 100644 index 734b859f..00000000 --- a/intf/extend.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* * 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/intf/genredexpr.ml b/intf/genredexpr.ml deleted file mode 100644 index 80697461..00000000 --- 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 *) -(* <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) *) -(************************************************************************) - -(** Reduction expressions *) - -(** The parsing produces initially a list of [red_atom] *) - -type 'a red_atom = - | FBeta - | FMatch - | FFix - | FCofix - | FZeta - | FConst of 'a list - | FDeltaBut of 'a list - -(** This list of atoms is immediately converted to a [glob_red_flag] *) - -type 'a glob_red_flag = { - rBeta : bool; - rMatch : bool; - rFix : bool; - rCofix : bool; - rZeta : bool; - rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) - rConst : 'a list -} - -(** Generic kinds of reductions *) - -type ('a,'b,'c) red_expr_gen = - | Red of bool - | Hnf - | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option - | Cbv of 'b glob_red_flag - | Cbn of 'b glob_red_flag - | Lazy of 'b glob_red_flag - | Unfold of 'b Locus.with_occurrences list - | Fold of 'a list - | Pattern of 'a Locus.with_occurrences list - | ExtraRedExpr of string - | CbvVm of ('b,'c) Util.union Locus.with_occurrences option - | CbvNative of ('b,'c) Util.union Locus.with_occurrences option - -type ('a,'b,'c) may_eval = - | ConstrTerm of 'a - | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Misctypes.lident * 'a - | ConstrTypeOf of 'a - -open Libnames -open Constrexpr -open Misctypes - -type r_trm = constr_expr -type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation - -type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/intf/glob_term.ml b/intf/glob_term.ml deleted file mode 100644 index 655dd20c..00000000 --- a/intf/glob_term.ml +++ /dev/null @@ -1,112 +0,0 @@ -(************************************************************************) -(* * 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) *) -(************************************************************************) - -(** Untyped intermediate terms *) - -(** [glob_constr] comes after [constr_expr] and before [constr]. - - Resolution of names, insertion of implicit arguments placeholder, - and notations are done, but coercions, inference of implicit - arguments and pattern-matching compilation are not. *) - -open Names -open Globnames -open Decl_kinds -open Misctypes - -type existential_name = Id.t - -(** The kind of patterns that occurs in "match ... with ... end" - - locs here refers to the ident's location, not whole pat *) -type 'a cases_pattern_r = - | PatVar of Name.t - | PatCstr of constructor * 'a cases_pattern_g list * Name.t - (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) -and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t - -type cases_pattern = [ `any ] cases_pattern_g - -(** Representation of an internalized (or in other words globalized) term. *) -type 'a glob_constr_r = - | GRef of global_reference * glob_level list option - (** An identifier that represents a reference to an object defined - either in the (global) environment or in the (local) context. *) - | GVar of Id.t - (** An identifier that cannot be regarded as "GRef". - Bound variables are typically represented this way. *) - | GEvar of existential_name * (Id.t * 'a glob_constr_g) list - | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *) - | GApp of 'a glob_constr_g * 'a glob_constr_g list - | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g - | GProd of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g - | GLetIn of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g - | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g - (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) - | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * - 'a glob_constr_g array * 'a glob_constr_g array - | GSort of glob_sort - | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type -and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t - -and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g - -and 'a fix_recursion_order_g = - | GStructRec - | GWfRec of 'a glob_constr_g - | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - -and 'a fix_kind_g = - | GFix of ((int option * 'a fix_recursion_order_g) array * int) - | GCoFix of int - -and 'a predicate_pattern_g = - Name.t * (inductive * Name.t list) CAst.t option - (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) - -and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) - -and 'a tomatch_tuples_g = 'a tomatch_tuple_g list - -and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t -(** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables - of [t] are members of [il]. *) -and 'a cases_clauses_g = 'a cases_clause_g list - -type glob_constr = [ `any ] glob_constr_g -type tomatch_tuple = [ `any ] tomatch_tuple_g -type tomatch_tuples = [ `any ] tomatch_tuples_g -type cases_clause = [ `any ] cases_clause_g -type cases_clauses = [ `any ] cases_clauses_g -type glob_decl = [ `any ] glob_decl_g -type fix_kind = [ `any ] fix_kind_g -type predicate_pattern = [ `any ] predicate_pattern_g -type fix_recursion_order = [ `any ] fix_recursion_order_g - -type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> 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 2b8960d3..00000000 --- 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 95a2e495..00000000 --- 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 *) -(* <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 - -(** Locus : positions in hypotheses and goals *) - -(** {6 Occurrences} *) - -type 'a occurrences_gen = - | AllOccurrences - | AllOccurrencesBut of 'a list (** non-empty *) - | NoOccurrences - | OnlyOccurrences of 'a list (** non-empty *) - -type occurrences_expr = (int or_var) occurrences_gen -type 'a with_occurrences = occurrences_expr * 'a - -type occurrences = int occurrences_gen - - -(** {6 Locations} - - Selecting the occurrences in body (if any), in type, or in both *) - -type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly - - -(** {6 Abstract clauses expressions} - - A [clause_expr] (and its instance [clause]) denotes occurrences and - hypotheses in a goal in an abstract way; in particular, it can refer - to the set of all hypotheses independently of the effective contents - of the current goal - - Concerning the field [onhyps]: - - [None] means *on every hypothesis* - - [Some l] means on hypothesis belonging to l *) - -type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag - -type 'id clause_expr = - { onhyps : 'id hyp_location_expr list option; - concl_occs : occurrences_expr } - -type clause = Id.t clause_expr - - -(** {6 Concrete view of occurrence clauses} *) - -(** [clause_atom] refers either to an hypothesis location (i.e. an - hypothesis with occurrences and a position, in body if any, in type - or in both) or to some occurrences of the conclusion *) - -type clause_atom = - | OnHyp of Id.t * occurrences_expr * hyp_location_flag - | OnConcl of occurrences_expr - -(** A [concrete_clause] is an effective collection of occurrences - in the hypotheses and the conclusion *) - -type concrete_clause = clause_atom list - - -(** {6 A weaker form of clause with no mention of occurrences} *) - -(** A [hyp_location] is an hypothesis together with a location *) - -type hyp_location = Id.t * hyp_location_flag - -(** A [goal_location] is either an hypothesis (together with a location) - or the conclusion (represented by None) *) - -type goal_location = hyp_location option - - -(** {6 Simple clauses, without occurrences nor location} *) - -(** A [simple_clause] is a set of hypotheses, possibly extended with - the conclusion (conclusion is represented by None) *) - -type simple_clause = Id.t option list - -(** {6 A notion of occurrences allowing to express "all occurrences - convertible to the first which matches"} *) - -type 'a or_like_first = AtOccs of 'a | LikeFirst - diff --git a/intf/misctypes.ml b/intf/misctypes.ml deleted file mode 100644 index 9eb6f62c..00000000 --- a/intf/misctypes.ml +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* * 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 - -(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) - -(** Located identifiers and objects with syntax. *) - -type lident = Id.t CAst.t -type lname = Name.t CAst.t -type lstring = string CAst.t - -(** Cases pattern variables *) - -type patvar = Id.t - -(** Introduction patterns *) - -type 'constr intro_pattern_expr = - | IntroForthcoming of bool - | IntroNaming of intro_pattern_naming_expr - | IntroAction of 'constr intro_pattern_action_expr -and intro_pattern_naming_expr = - | IntroIdentifier of Id.t - | IntroFresh of Id.t - | IntroAnonymous -and 'constr intro_pattern_action_expr = - | IntroWildcard - | IntroOrAndPattern of 'constr or_and_intro_pattern_expr - | IntroInjection of ('constr intro_pattern_expr) CAst.t list - | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t - | IntroRewrite of bool -and 'constr or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list - | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list - -(** Move destination for hypothesis *) - -type 'id move_location = - | MoveAfter of 'id - | MoveBefore of 'id - | MoveFirst - | MoveLast (** can be seen as "no move" when doing intro *) - -(** Sorts *) - -type 'a glob_sort_gen = - | GProp (** representation of [Prop] literal *) - | GSet (** representation of [Set] literal *) - | GType of 'a (** representation of [Type] literal *) - -type 'a universe_kind = - | UAnonymous - | UUnknown - | UNamed of 'a - -type level_info = Libnames.reference universe_kind -type glob_level = level_info glob_sort_gen -type glob_constraint = glob_level * Univ.constraint_type * glob_level - -type sort_info = (Libnames.reference * int) option list -type glob_sort = sort_info glob_sort_gen - -(** A synonym of [Evar.t], also defined in Term *) - -type existential_key = Evar.t - -(** Case style, shared with Term *) - -type case_style = Constr.case_style = - | LetStyle - | IfStyle - | LetPatternStyle - | MatchStyle - | RegularStyle (** infer printing form from number of constructor *) -[@@ocaml.deprecated "Alias for Constr.case_style"] - -(** Casts *) - -type 'a cast_type = - | CastConv of 'a - | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) - | CastNative of 'a - -(** Bindings *) - -type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t - -type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list - -type 'a bindings = - | ImplicitBindings of 'a list - | ExplicitBindings of 'a explicit_bindings - | NoBindings - -type 'a with_bindings = 'a * 'a bindings - - -(** Some utility types for parsing *) - -type 'a or_var = - | ArgArg of 'a - | ArgVar of lident - -type 'a and_short_name = 'a * lident option - -type 'a or_by_notation_r = - | AN of 'a - | ByNotation of (string * string option) - -type 'a or_by_notation = 'a or_by_notation_r CAst.t - -(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], - but this formulation avoids a useless dependency. *) - - -(** Kinds of modules *) - -type module_kind = Module | ModType | ModAny - -(** Various flags *) - -type direction_flag = bool (* true = Left-to-right false = right-to-right *) -type evars_flag = bool (* true = pose evars false = fail on evars *) -type rec_flag = bool (* true = recursive false = not recursive *) -type advanced_flag = bool (* true = advanced false = basic *) -type letin_flag = bool (* true = use local def false = use Leibniz *) -type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) - -type multi = - | Precisely of int - | UpTo of int - | RepeatStar - | RepeatPlus - -type 'a core_destruction_arg = - | ElimOnConstr of 'a - | ElimOnIdent of lident - | ElimOnAnonHyp of int - -type 'a destruction_arg = - clear_flag * 'a core_destruction_arg - -type inversion_kind = - | SimpleInversion - | FullInversion - | FullInversionClear - -type ('a, 'b) gen_universe_decl = { - univdecl_instance : 'a; (* Declared universes *) - univdecl_extensible_instance : bool; (* Can new universes be added *) - univdecl_constraints : 'b; (* Declared constraints *) - univdecl_extensible_constraints : bool (* Can new constraints be added *) } diff --git a/intf/notation_term.ml b/intf/notation_term.ml deleted file mode 100644 index af9d6918..00000000 --- a/intf/notation_term.ml +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* * 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 Globnames -open Misctypes -open Glob_term - -(** [notation_constr] *) - -(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic - extensions (i.e. notations). - No location since intended to be substituted at any place of a text. - Complex expressions such as fixpoints and cofixpoints are excluded, - as well as non global expressions such as existential variables. *) - -type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) - | NRef of global_reference - | NVar of Id.t - | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) - | NLambda of Name.t * notation_constr * notation_constr - | NProd of Name.t * notation_constr * notation_constr - | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr - | NCases of Constr.case_style * notation_constr option * - (notation_constr * (Name.t * (inductive * Name.t list) option)) list * - (cases_pattern list * notation_constr) list - | NLetTuple of Name.t list * (Name.t * notation_constr option) * - notation_constr * notation_constr - | NIf of notation_constr * (Name.t * notation_constr option) * - notation_constr * notation_constr - | NRec of fix_kind * Id.t array * - (Name.t * notation_constr option * notation_constr) list array * - notation_constr array * notation_constr array - | NSort of glob_sort - | NCast of notation_constr * notation_constr cast_type - -(** Note concerning NList: first constr is iterator, second is terminator; - first id is where each argument of the list has to be substituted - in iterator and snd id is alternative name just for printing; - boolean is associativity *) - -(** Types concerning notations *) - -type scope_name = string - -type tmp_scope_name = scope_name - -type subscopes = tmp_scope_name option * scope_name list - -(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, - x carries the sequence of objects bound to the list x..y *) - -type notation_binder_source = - (* This accepts only pattern *) - (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) - | NtnParsedAsPattern of bool - (* This accepts only ident *) - | NtnParsedAsIdent - (* This accepts ident, or pattern, or both *) - | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind - -type notation_var_instance_type = - | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList - -(** Type of variables when interpreting a constr_expr as a notation_constr: - in a recursive pattern x..y, both x and y carry the individual type - of each element of the list x..y *) -type notation_var_internalization_type = - | NtnInternTypeAny | NtnInternTypeOnlyBinder - -(** This characterizes to what a notation is interpreted to *) -type interpretation = - (Id.t * (subscopes * notation_var_instance_type)) list * - notation_constr - -type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list - -type notation_interp_env = { - ninterp_var_type : notation_var_internalization_type Id.Map.t; - ninterp_rec_vars : Id.t Id.Map.t; -} - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool * int - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list when true; additionally release - the p last items as if they were parsed autonomously *) - -(** Dealing with precedences *) - -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = precedence * tolerability list * Extend.constr_entry_key list - -(** Grammar rules for a notation *) - -type one_notation_grammar = { - notgram_level : level; - notgram_assoc : Extend.gram_assoc option; - notgram_notation : Constrexpr.notation; - notgram_prods : grammar_constr_prod_item list list; -} - -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} diff --git a/intf/pattern.ml b/intf/pattern.ml deleted file mode 100644 index af234767..00000000 --- a/intf/pattern.ml +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* * 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 Globnames -open Constr -open Misctypes - -(** {5 Patterns} *) - -type case_info_pattern = - { cip_style : Constr.case_style; - cip_ind : inductive option; - cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) - cip_extensible : bool (** does this match end with _ => _ ? *) } - -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 fixpoint - | PCoFix of cofixpoint - -(** 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 df061bfb..00000000 --- a/intf/vernacexpr.ml +++ /dev/null @@ -1,543 +0,0 @@ -(************************************************************************) -(* * 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 - -(* spiwack: I'm choosing, for now, to have [goal_selector] be a - different type than [goal_reference] mostly because if it makes sense - to print a goal that is out of focus (or already solved) it doesn't - make sense to apply a tactic to it. Hence it the types may look very - similar, they do not seem to mean the same thing. *) -type goal_selector = - | SelectNth of int - | SelectList of (int * int) list - | SelectId of Id.t - | SelectAll - -type goal_identifier = string -type scope_name = string - -type goal_reference = - | OpenSubgoals - | NthGoal of int - | GoalId of Id.t - -type univ_name_list = Universes.univ_name_list -[@@ocaml.deprecated "Use [Universes.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 * Universes.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 * Universes.univ_name_list option * goal_selector 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 = - { hint_priority : int option; - hint_pattern : 'a option } - -type hint_info_expr = constr_pattern_expr hint_info_gen - -type hints_expr = - | HintsResolve of (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 = Opaque | Transparent -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 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 = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = - | NoInline - | DefaultInline - | InlineAt of int - -type module_ast_inl = module_ast * inline -type module_binder = bool option * lident list * module_ast_inl - -(** Cumulativity can be set globally, locally or unset locally and it - can not enabled at all. *) -type cumulative_inductive_parsing_flag = - | GlobalCumulativity - | GlobalNonCumulativity - | LocalCumulativity - | LocalNonCumulativity - -(** {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) * - inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * 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 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 - | VernacDeclareImplicits of reference or_by_notation * - (explicitation * bool * bool) list list - | 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 - | VernacArgumentsScope of reference or_by_notation * - scope_name option 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 - | VernacBacktrack of int*int*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 - (* Toplevel control *) - | VernacToplevelControl of exn - - (* 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 of vernac_part_of_script * Feedback.route_id - (* 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 vernac_part_of_script = bool -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"] |