diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 139 | ||||
| -rw-r--r-- | intf/decl_kinds.mli | 76 | ||||
| -rw-r--r-- | intf/evar_kinds.mli | 31 | ||||
| -rw-r--r-- | intf/extend.mli | 52 | ||||
| -rw-r--r-- | intf/genredexpr.mli | 50 | ||||
| -rw-r--r-- | intf/glob_term.mli | 86 | ||||
| -rw-r--r-- | intf/locus.mli | 94 | ||||
| -rw-r--r-- | intf/misctypes.mli | 106 | ||||
| -rw-r--r-- | intf/notation_term.mli | 81 | ||||
| -rw-r--r-- | intf/pattern.mli | 81 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 415 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 482 |
12 files changed, 1693 insertions, 0 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli new file mode 100644 index 00000000..79f4e99e --- /dev/null +++ b/intf/constrexpr.mli @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +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 notation = string + +type explicitation = + | ExplByPos of int * Id.t option + | 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 *) + +type prim_token = Numeral of Bigint.bigint | String of string + +type raw_cases_pattern_expr = + | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t + | RCPatCstr of Loc.t * Globnames.global_reference + * raw_cases_pattern_expr list * raw_cases_pattern_expr list + (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + | RCPatAtom of Loc.t * Id.t option + | RCPatOr of Loc.t * raw_cases_pattern_expr list + +type cases_pattern_expr = + | CPatAlias of Loc.t * cases_pattern_expr * Id.t + | CPatCstr of Loc.t * reference + * cases_pattern_expr list * cases_pattern_expr list + (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *) + | CPatAtom of Loc.t * reference option + | CPatOr of Loc.t * cases_pattern_expr list + | CPatNotation of Loc.t * 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 Loc.t * prim_token + | CPatRecord of Loc.t * (reference * cases_pattern_expr) list + | CPatDelimiters of Loc.t * string * cases_pattern_expr + +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + +type instance_expr = Misctypes.glob_level list + +type constr_expr = + | CRef of reference * instance_expr option + | CFix of Loc.t * Id.t located * fix_expr list + | CCoFix of Loc.t * Id.t located * cofix_expr list + | CProdN of Loc.t * binder_expr list * constr_expr + | CLambdaN of Loc.t * binder_expr list * constr_expr + | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr + | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list + | CApp of Loc.t * (proj_flag * constr_expr) * + (constr_expr * explicitation located option) list + | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list + | CCases of Loc.t * case_style * constr_expr option * + case_expr list * branch_expr list + | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * + constr_expr * constr_expr + | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) + * constr_expr * constr_expr + | CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of Loc.t * patvar + | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of Loc.t * glob_sort + | CCast of Loc.t * constr_expr * constr_expr cast_type + | CNotation of Loc.t * notation * constr_notation_substitution + | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr + | CPrim of Loc.t * prim_token + | CDelimiters of Loc.t * string * constr_expr + +and case_expr = + constr_expr * (Name.t located option * cases_pattern_expr option) + +and branch_expr = + Loc.t * cases_pattern_expr list located list * constr_expr + +and binder_expr = + Name.t located list * binder_kind * constr_expr + +and fix_expr = + Id.t located * (Id.t located option * recursion_order_expr) * + local_binder list * constr_expr * constr_expr + +and cofix_expr = + Id.t located * local_binder 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 = + | LocalRawDef of Name.t located * constr_expr + | LocalRawAssum of Name.t located list * binder_kind * constr_expr + +and constr_notation_substitution = + constr_expr list * (** for constr subterms *) + constr_expr list list * (** for recursive notations *) + local_binder list list (** for binders subexpressions *) + +type typeclass_constraint = Name.t located * binding_kind * constr_expr + +and typeclass_context = typeclass_constraint list + +type constr_pattern_expr = constr_expr + +(** Concrete syntax for modules and module types *) + +type with_declaration_ast = + | CWith_Module of Id.t list located * qualid located + | CWith_Definition of Id.t list located * constr_expr + +type module_ast = + | CMident of qualid located + | CMapply of Loc.t * module_ast * module_ast + | CMwith of Loc.t * module_ast * with_declaration_ast diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli new file mode 100644 index 00000000..6886083c --- /dev/null +++ b/intf/decl_kinds.mli @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Informal mathematical status of declarations *) + +type locality = Discharge | Local | Global + +type binding_kind = Explicit | Implicit + +type polymorphic = bool + +type private_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 + +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 = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli new file mode 100644 index 00000000..38a3e81f --- /dev/null +++ b/intf/evar_kinds.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Globnames + +(** 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 t = + | ImplicitArg of global_reference * (int * Id.t option) + * bool (** Force inference *) + | BinderType of Name.t + | QuestionMark of obligation_definition_status + | CasesType of bool (* true = a subterm of the type *) + | InternalHole + | TomatchTypeParameter of inductive * int + | GoalEvar + | ImpossibleCase + | MatchingVar of bool * Id.t + | VarInstance of Id.t + | SubEvar of Constr.existential_key diff --git a/intf/extend.mli b/intf/extend.mli new file mode 100644 index 00000000..ad9706f3 --- /dev/null +++ b/intf/extend.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Entry keys for constr notations *) + +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 ('lev,'pos) constr_entry_key_gen = + | ETName | ETReference | ETBigint + | ETBinder of bool + | ETConstr of ('lev * 'pos) + | ETPattern + | ETOther of string * string + | ETConstrList of ('lev * 'pos) * Tok.t list + | ETBinderList of bool * Tok.t list + +(** Entries level (left-hand-side of grammar rules) *) + +type constr_entry_key = + (int,unit) constr_entry_key_gen + +(** Entries used in productions (in right-hand-side of grammar rules) *) + +type constr_prod_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,unit) constr_entry_key_gen diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli new file mode 100644 index 00000000..61340914 --- /dev/null +++ b/intf/genredexpr.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Reduction expressions *) + +(** The parsing produces initially a list of [red_atom] *) + +type 'a red_atom = + | FBeta + | FIota + | 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; + rIota : 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 (Loc.t * Names.Id.t) * 'a + | ConstrTypeOf of 'a diff --git a/intf/glob_term.mli b/intf/glob_term.mli new file mode 100644 index 00000000..32cf9eaf --- /dev/null +++ b/intf/glob_term.mli @@ -0,0 +1,86 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** 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 cases_pattern = + | PatVar of Loc.t * Name.t + | PatCstr of Loc.t * constructor * cases_pattern list * Name.t + (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) + +type glob_constr = + | GRef of (Loc.t * global_reference * glob_level list option) + | GVar of (Loc.t * Id.t) + | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list + | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) + | GApp of Loc.t * glob_constr * glob_constr list + | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLetIn of Loc.t * Name.t * glob_constr * glob_constr + | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses + (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in + [MatchStyle]) *) + | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * + glob_constr * glob_constr + | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr + | GRec of Loc.t * fix_kind * Id.t array * glob_decl list array * + glob_constr array * glob_constr array + | GSort of Loc.t * glob_sort + | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option) + | GCast of Loc.t * glob_constr * glob_constr cast_type + +and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr + +and fix_recursion_order = + | GStructRec + | GWfRec of glob_constr + | GMeasureRec of glob_constr * glob_constr option + +and fix_kind = + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int + +and predicate_pattern = + Name.t * (Loc.t * inductive * Name.t list) option + (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) + +and tomatch_tuple = (glob_constr * predicate_pattern) + +and tomatch_tuples = tomatch_tuple list + +and cases_clause = (Loc.t * Id.t list * cases_pattern list * glob_constr) +(** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables + of [t] are members of [il]. *) +and cases_clauses = cases_clause list + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: Pattern.constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } diff --git a/intf/locus.mli b/intf/locus.mli new file mode 100644 index 00000000..80857794 --- /dev/null +++ b/intf/locus.mli @@ -0,0 +1,94 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +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.mli b/intf/misctypes.mli new file mode 100644 index 00000000..74e13690 --- /dev/null +++ b/intf/misctypes.mli @@ -0,0 +1,106 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names + +(** Basic types used both in [constr_expr] and in [glob_constr] *) + +(** 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 (Loc.t * 'constr intro_pattern_expr) list + | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + (Loc.t * 'constr intro_pattern_expr) list 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 | GSet | GType of 'a +type sort_info = string list +type level_info = string option + +type glob_sort = sort_info glob_sort_gen +type glob_level = level_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 = Term.case_style = + | LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) + +(** 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 = (Loc.t * quantified_hypothesis * 'a) 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 Names.Id.t Loc.located + +type 'a and_short_name = 'a * Id.t Loc.located option + +type 'a or_by_notation = + | AN of 'a + | ByNotation of (Loc.t * string * string option) + +(* 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 diff --git a/intf/notation_term.mli b/intf/notation_term.mli new file mode 100644 index 00000000..5a563bf9 --- /dev/null +++ b/intf/notation_term.mli @@ -0,0 +1,81 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +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 * 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 + | NLetIn of Name.t * notation_constr * notation_constr + | NCases of 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 + | NPatVar of patvar + | 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_var_instance_type = + | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList + +(** Type of variables when interpreting a constr_expr as an 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 = + | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + +(** This characterizes to what a notation is interpreted to *) +type interpretation = + (Id.t * (subscopes * notation_var_instance_type)) list * + notation_constr + +type notation_interp_env = { + ninterp_var_type : notation_var_internalization_type Id.Map.t; + ninterp_rec_vars : Id.t Id.Map.t; + mutable ninterp_only_parse : bool; +} diff --git a/intf/pattern.mli b/intf/pattern.mli new file mode 100644 index 00000000..18cd2df0 --- /dev/null +++ b/intf/pattern.mli @@ -0,0 +1,81 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Globnames +open Term +open Misctypes + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** {5 Patterns} *) + +type case_info_pattern = + { cip_style : 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 * 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 + | 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/tacexpr.mli b/intf/tacexpr.mli new file mode 100644 index 00000000..7b9ad313 --- /dev/null +++ b/intf/tacexpr.mli @@ -0,0 +1,415 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +open Names +open Constrexpr +open Libnames +open Globnames +open Nametab +open Genredexpr +open Genarg +open Pattern +open Decl_kinds +open Misctypes +open Locus + +type direction_flag = bool (* true = Left-to-right false = right-to-right *) +type lazy_flag = + | General (* returns all possible successes *) + | Select (* returns all successes of the first matching branch *) + | Once (* returns the first success in a maching branch + (not necessarily the first) *) +type global_flag = (* [gfail] or [fail] *) + | TacGlobal + | TacLocal +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 debug = Debug | Info | Off (* for trivial / auto / eauto ... *) + +type 'a core_induction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of Id.t located + | ElimOnAnonHyp of int + +type 'a induction_arg = + clear_flag * 'a core_induction_arg + +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + +type ('c,'d,'id) inversion_strength = + | NonDepInversion of + inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option + | DepInversion of + inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option + | InversionUsing of 'c * 'id list + +type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b + +type 'id message_token = + | MsgString of string + | MsgInt of int + | MsgIdent of 'id + +type ('dconstr,'id) induction_clause = + 'dconstr with_bindings induction_arg * + (intro_pattern_naming_expr located option (* eqn:... *) + * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *) + * 'id clause_expr option (* in ... *) + +type ('constr,'dconstr,'id) induction_clause_list = + ('dconstr,'id) induction_clause list + * 'constr with_bindings option (* using ... *) + +type 'a with_bindings_arg = clear_flag * 'a with_bindings + +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + +(* Type of patterns *) +type 'a match_pattern = + | Term of 'a + | Subterm of bool * Id.t option * 'a + +(* Type of hypotheses for a Match Context rule *) +type 'a match_context_hyps = + | Hyp of Name.t located * 'a match_pattern + | Def of Name.t located * 'a match_pattern * 'a match_pattern + +(* Type of a Match rule for Match Context and Match *) +type ('a,'t) match_rule = + | Pat of 'a match_context_hyps list * 'a match_pattern * 't + | All of 't + +type ml_tactic_name = { + mltac_plugin : string; + mltac_tactic : string; +} + +(** Composite types *) + +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option + +type open_constr_expr = unit * constr_expr +type open_glob_constr = unit * glob_constr_and_expr + +type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern + +type delayed_open_constr_with_bindings = + Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr with_bindings + +type delayed_open_constr = + Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr + +type intro_pattern = delayed_open_constr intro_pattern_expr located +type intro_patterns = delayed_open_constr intro_pattern_expr located list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located +type intro_pattern_naming = intro_pattern_naming_expr located + +(** Generic expressions for atomic tactics *) + +type 'a gen_atomic_tactic_expr = + (* Basic tactics *) + | TacIntroPattern of 'dtrm intro_pattern_expr located list + | TacIntroMove of Id.t option * 'nam move_location + | TacExact of 'trm + | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * + (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option + | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option + | TacCase of evars_flag * 'trm with_bindings_arg + | TacFix of Id.t option * int + | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list + | TacCofix of Id.t option + | TacMutualCofix of Id.t * (Id.t * 'trm) list + | TacAssert of + bool * 'tacexpr option * + 'dtrm intro_pattern_expr located option * 'trm + | TacGeneralize of ('trm with_occurrences * Name.t) list + | TacGeneralizeDep of 'trm + | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * + intro_pattern_naming_expr located option + + (* Derived basic tactics *) + | TacInductionDestruct of + rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list + | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis + + (* Automation tactics *) + | TacTrivial of debug * 'trm list * string list option + | TacAuto of debug * int or_var option * 'trm list * string list option + + (* Context management *) + | TacClear of bool * 'nam list + | TacClearBody of 'nam list + | TacMove of 'nam * 'nam move_location + | TacRename of ('nam *'nam) list + + (* Trmuctors *) + | TacSplit of evars_flag * 'trm bindings list + + (* Conversion *) + | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr + | TacChange of 'pat option * 'dtrm * 'nam clause_expr + + (* Equivalence relations *) + | TacSymmetry of 'nam clause_expr + + (* Equality and inversion *) + | TacRewrite of evars_flag * + (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * + (* spiwack: using ['dtrm] here is a small hack, may not be + stable by a change in the representation of delayed + terms. Because, in fact, it is the whole "with_bindings" + which is delayed. But because the "t" level for ['dtrm] is + uninterpreted, it works fine here too, and avoid more + disruption of this file. *) + 'tacexpr option + | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis + +constraint 'a = < + term:'trm; + utrm: 'utrm; + dterm: 'dtrm; + pattern:'pat; + constant:'cst; + reference:'ref; + name:'nam; + tacexpr:'tacexpr; + level:'lev +> + +(** Possible arguments of a tactic definition *) + +and 'a gen_tactic_arg = + | TacDynamic of Loc.t * Dyn.t + | TacGeneric of 'lev generic_argument + | MetaIdArg of Loc.t * bool * string + | ConstrMayEval of ('trm,'cst,'pat) may_eval + | UConstr of 'utrm + | Reference of 'ref + | TacCall of Loc.t * 'ref * + 'a gen_tactic_arg list + | TacFreshId of string or_var list + | Tacexp of 'tacexpr + | TacPretype of 'trm + | TacNumgoals + +constraint 'a = < + term:'trm; + utrm: 'utrm; + dterm: 'dtrm; + pattern:'pat; + constant:'cst; + reference:'ref; + name:'nam; + tacexpr:'tacexpr; + level:'lev +> + +(** Generic ltac expressions. + 't : terms, 'p : patterns, 'c : constants, 'i : inductive, + 'r : ltac refs, 'n : idents, 'l : levels *) + +and 'a gen_tactic_expr = + | TacAtom of Loc.t * 'a gen_atomic_tactic_expr + | TacThen of + 'a gen_tactic_expr * + 'a gen_tactic_expr + | TacDispatch of + 'a gen_tactic_expr list + | TacExtendTac of + 'a gen_tactic_expr array * + 'a gen_tactic_expr * + 'a gen_tactic_expr array + | TacThens of + 'a gen_tactic_expr * + 'a gen_tactic_expr list + | TacThens3parts of + 'a gen_tactic_expr * + 'a gen_tactic_expr array * + 'a gen_tactic_expr * + 'a gen_tactic_expr array + | TacFirst of 'a gen_tactic_expr list + | TacComplete of 'a gen_tactic_expr + | TacSolve of 'a gen_tactic_expr list + | TacTry of 'a gen_tactic_expr + | TacOr of + 'a gen_tactic_expr * + 'a gen_tactic_expr + | TacOnce of + 'a gen_tactic_expr + | TacExactlyOnce of + 'a gen_tactic_expr + | TacIfThenCatch of + 'a gen_tactic_expr * + 'a gen_tactic_expr * + 'a gen_tactic_expr + | TacOrelse of + 'a gen_tactic_expr * + 'a gen_tactic_expr + | TacDo of int or_var * 'a gen_tactic_expr + | TacTimeout of int or_var * 'a gen_tactic_expr + | TacTime of string option * 'a gen_tactic_expr + | TacRepeat of 'a gen_tactic_expr + | TacProgress of 'a gen_tactic_expr + | TacShowHyps of 'a gen_tactic_expr + | TacAbstract of + 'a gen_tactic_expr * Id.t option + | TacId of 'n message_token list + | TacFail of global_flag * int or_var * 'n message_token list + | TacInfo of 'a gen_tactic_expr + | TacLetIn of rec_flag * + (Id.t located * 'a gen_tactic_arg) list * + 'a gen_tactic_expr + | TacMatch of lazy_flag * + 'a gen_tactic_expr * + ('p,'a gen_tactic_expr) match_rule list + | TacMatchGoal of lazy_flag * direction_flag * + ('p,'a gen_tactic_expr) match_rule list + | TacFun of 'a gen_tactic_fun_ast + | TacArg of 'a gen_tactic_arg located + (* For ML extensions *) + | TacML of Loc.t * ml_tactic_name * 'l generic_argument list + (* For syntax extensions *) + | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list + +constraint 'a = < + term:'t; + utrm: 'utrm; + dterm: 'dtrm; + pattern:'p; + constant:'c; + reference:'r; + name:'n; + tacexpr:'tacexpr; + level:'l +> + +and 'a gen_tactic_fun_ast = + Id.t option list * 'a gen_tactic_expr + +constraint 'a = < + term:'t; + utrm: 'utrm; + dterm: 'dtrm; + pattern:'p; + constant:'c; + reference:'r; + name:'n; + tacexpr:'te; + level:'l +> + +(** Globalized tactics *) + +type g_trm = glob_constr_and_expr +type g_utrm = g_trm +type g_pat = glob_constr_and_expr * constr_pattern +type g_cst = evaluable_global_reference and_short_name or_var +type g_ref = ltac_constant located or_var +type g_nam = Id.t located + +type g_dispatch = < + term:g_trm; + utrm:g_utrm; + dterm:g_trm; + pattern:g_pat; + constant:g_cst; + reference:g_ref; + name:g_nam; + tacexpr:glob_tactic_expr; + level:glevel +> + +and glob_tactic_expr = + g_dispatch gen_tactic_expr + +type glob_atomic_tactic_expr = + g_dispatch gen_atomic_tactic_expr + +type glob_tactic_arg = + g_dispatch gen_tactic_arg + +(** Raw tactics *) + +type r_trm = constr_expr +type r_utrm = r_trm +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation +type r_ref = reference +type r_nam = Id.t located +type r_lev = rlevel + +type r_dispatch = < + term:r_trm; + utrm:r_utrm; + dterm:r_trm; + pattern:r_pat; + constant:r_cst; + reference:r_ref; + name:r_nam; + tacexpr:raw_tactic_expr; + level:rlevel +> + +and raw_tactic_expr = + r_dispatch gen_tactic_expr + +type raw_atomic_tactic_expr = + r_dispatch gen_atomic_tactic_expr + +type raw_tactic_arg = + r_dispatch gen_tactic_arg + +(** Interpreted tactics *) + +type t_trm = Term.constr +type t_utrm = Glob_term.closed_glob_constr +type t_pat = glob_constr_and_expr * constr_pattern +type t_cst = evaluable_global_reference and_short_name +type t_ref = ltac_constant located +type t_nam = Id.t + +type t_dispatch = < + term:t_trm; + utrm:t_utrm; + dterm:g_trm; + pattern:t_pat; + constant:t_cst; + reference:t_ref; + name:t_nam; + tacexpr:glob_tactic_expr; + level:tlevel +> + +type tactic_expr = + t_dispatch gen_tactic_expr + +type atomic_tactic_expr = + t_dispatch gen_atomic_tactic_expr + +type tactic_arg = + t_dispatch gen_tactic_arg + +(** Misc *) + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen +type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli new file mode 100644 index 00000000..3f2d002c --- /dev/null +++ b/intf/vernacexpr.mli @@ -0,0 +1,482 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +open Names +open Tacexpr +open Misctypes +open Constrexpr +open Decl_kinds +open Libnames + +(** Vernac expressions, produced by the parser *) + +type lident = Id.t located +type lname = Name.t located +type lstring = string located +type lreference = reference + +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 + | SelectId of Id.t + | SelectAll + | SelectAllParallel + +type goal_identifier = string +type scope_name = string + +type goal_reference = + | OpenSubgoals + | NthGoal of int + | GoalId of goal_identifier + +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 + | PrintGraph + | PrintClasses + | PrintTypeClasses + | PrintInstances of reference or_by_notation + | PrintLtac of reference + | PrintCoercions + | PrintCoercionPaths of class_rawexpr * class_rawexpr + | PrintCanonicalConversions + | PrintUniverses of bool * string option + | PrintHint of reference or_by_notation + | PrintHintGoal + | PrintHintDbName of string + | PrintRewriteHintDbName of string + | PrintHintDb + | PrintScopes + | PrintScope of string + | PrintVisibility of string option + | PrintAbout of reference or_by_notation*int 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 + | LocateTactic of reference + | LocateFile of string + +type showable = + | ShowGoal of goal_reference + | ShowGoalImplicitly of int option + | ShowProof + | ShowNode + | ShowScript + | ShowExistentials + | ShowUniverses + | ShowTree + | ShowProofNames + | ShowIntros of bool + | ShowMatch of lident + | ShowThesis + +type comment = + | CommentConstr of constr_expr + | CommentString of string + | CommentInt of int + +type reference_or_constr = + | HintsReference of reference + | HintsConstr of constr_expr + +type hints_expr = + | HintsResolve of (int option * bool * reference_or_constr) list + | HintsImmediate of reference_or_constr list + | HintsUnfold of reference list + | HintsTransparency of reference list * bool + | HintsMode of reference * bool list + | HintsConstructors of reference list + | HintsExtern of int * constr_expr option * raw_tactic_expr + +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 = bool (* true = Opaque; false = 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 = Decl_kinds.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 obsolete_locality = bool +(* Some grammar entries use obsolete_locality. This bool is to be backward + * compatible. If the grammar is fixed removing deprecated syntax, this + * bool should go away too *) + +type option_value = Goptions.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +type option_ref_value = + | StringRefValue of string + | QualidRefValue of reference + +type sort_expr = glob_sort + +type definition_expr = + | ProveBody of local_binder list * constr_expr + | DefineBody of local_binder list * raw_red_expr option * constr_expr + * constr_expr option + +type fixpoint_expr = + Id.t located * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + +type cofixpoint_expr = + Id.t located * local_binder 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 = + lident with_coercion * local_binder list * constr_expr option * inductive_kind * + constructor_list_or_record_decl_expr + +type one_inductive_expr = + lident * local_binder list * constr_expr option * constructor_expr list + +type grammar_tactic_prod_item_expr = + | TacTerm of string + | TacNonTerm of Loc.t * string * (Names.Id.t * string) option + +type syntax_modifier = + | SetItemLevel of string list * Extend.production_level + | SetLevel of int + | SetAssoc of Extend.gram_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing of Flags.compat_version + | SetFormat of string * string located + +type proof_end = + | Admitted + | Proved of opacity_flag * (lident * theorem_kind option) 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 = + | SsSet of lident list + | SsCompl of section_subset_expr + | SsUnion of section_subset_expr * section_subset_expr + | SsSubstr of section_subset_expr * section_subset_expr + +type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + +type extend_name = string * 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 Stm} *) +type 'a stm_vernac = + | JoinDocument + | Finish + | Wait + | PrintDag + | Observe of Stateid.t + | Command of 'a (* An out of flow command not to be recorded by Stm *) + | PGLast of 'a (* To ease the life of PG *) + +(** {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 + +(** {6 The type of vernacular expressions} *) + +type vernac_expr = + (* Control *) + | VernacLoad of verbose_flag * string + | VernacTime of vernac_list + | VernacTimeout of int * vernac_expr + | VernacFail of vernac_expr + | VernacError of exn (* always fails *) + + (* Syntax *) + | VernacTacticNotation of + int * grammar_tactic_prod_item_expr list * raw_tactic_expr + | VernacSyntaxExtension of + obsolete_locality * (lstring * syntax_modifier list) + | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacDelimiters of scope_name * string + | VernacBindScope of scope_name * reference or_by_notation list + | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + constr_expr * scope_name option + | VernacNotation of + obsolete_locality * constr_expr * (lstring * syntax_modifier list) * + scope_name option + | VernacNotationAddFormat of string * string * string + + (* Gallina *) + | VernacDefinition of + (locality option * definition_object_kind) * lident * definition_expr + | VernacStartTheoremProof of theorem_kind * + (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * + bool + | VernacEndProof of proof_end + | VernacExactProof of constr_expr + | VernacAssumption of (locality option * assumption_object_kind) * + inline * simple_binder with_coercion list + | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of + locality option * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of + locality option * (cofixpoint_expr * decl_notation list) list + | VernacScheme of (lident option * scheme) list + | VernacCombinedScheme of lident * lident list + | VernacUniverse of lident list + | VernacConstraint of (lident * Univ.constraint_type * lident) list + + (* Gallina extensions *) + | VernacBeginSection of lident + | VernacEndSegment of lident + | VernacRequire of + export_flag option * lreference list + | VernacImport of export_flag * lreference list + | VernacCanonical of reference or_by_notation + | VernacCoercion of obsolete_locality * reference or_by_notation * + class_rawexpr * class_rawexpr + | VernacIdentityCoercion of obsolete_locality * lident * + class_rawexpr * class_rawexpr + | VernacNameSectionHypSet of lident * section_subset_descr + + (* Type classes *) + | VernacInstance of + bool * (* abstract instance *) + local_binder list * (* super *) + typeclass_constraint * (* instance name, class name, params *) + (bool * constr_expr) option * (* props *) + int option (* Priority *) + + | VernacContext of local_binder list + + | VernacDeclareInstances of + reference list * int option (* instance names, priority *) + + | 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 *) + + | VernacSolve of goal_selector * int option * raw_tactic_expr * bool + | 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 *) + | VernacDeclareTacticDefinition of + (rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacCreateHintDb of string * bool + | VernacRemoveHints of string list * reference list + | VernacHints of obsolete_locality * string list * hints_expr + | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * + obsolete_locality * onlyparsing_flag + | VernacDeclareImplicits of reference or_by_notation * + (explicitation * bool * bool) list list + | VernacArguments of reference or_by_notation * + ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list * + int * [ `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 Goptions.option_name + | VernacSetOption of 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 raw_red_expr option * int option * constr_expr + | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of string * raw_red_expr + | VernacPrint of printable + | VernacSearch of searchable * int option * search_restriction + | VernacLocate of locatable + | VernacRegister of lident * register_kind + | VernacComments of comment list + | VernacNop + + (* Stm backdoor *) + | VernacStm of vernac_expr stm_vernac + + (* Proof management *) + | VernacGoal of constr_expr + | 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 int option + | VernacEndSubproof + | VernacShow of showable + | VernacCheckGuard + | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProofMode of string + (* Toplevel control *) + | VernacToplevelControl of exn + + (* For extension *) + | VernacExtend of extend_name * Genarg.raw_generic_argument list + + (* Flags *) + | VernacProgram of vernac_expr + | VernacPolymorphic of bool * vernac_expr + | VernacLocal of bool * vernac_expr + +and vernac_list = located_vernac_expr list + +and located_vernac_expr = Loc.t * vernac_expr + +(* A vernac classifier has to tell if a command: + vernac_when: has to be executed now (alters the parser) or later + 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 *) +type vernac_type = + | VtStartProof of vernac_start + | VtSideff of vernac_sideff_type + | VtQed of vernac_qed_type + | VtProofStep of bool (* parallelize *) + | VtProofMode of string + | VtQuery of vernac_part_of_script * report_with + | VtStm of vernac_control * vernac_part_of_script + | VtUnknown +and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) +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_is_alias = bool +and vernac_part_of_script = bool +and vernac_control = + | VtFinish + | VtWait + | VtJoinDocument + | VtPrintDag + | VtObserve of Stateid.t + | VtBack of Stateid.t + | VtPG +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when |