diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 39 | ||||
| -rw-r--r-- | intf/decl_kinds.mli | 4 | ||||
| -rw-r--r-- | intf/evar_kinds.mli | 2 | ||||
| -rw-r--r-- | intf/extend.mli | 54 | ||||
| -rw-r--r-- | intf/genredexpr.mli | 24 | ||||
| -rw-r--r-- | intf/glob_term.mli | 10 | ||||
| -rw-r--r-- | intf/locus.mli | 2 | ||||
| -rw-r--r-- | intf/misctypes.mli | 42 | ||||
| -rw-r--r-- | intf/notation_term.mli | 24 | ||||
| -rw-r--r-- | intf/pattern.mli | 2 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 420 | ||||
| -rw-r--r-- | intf/tactypes.mli | 35 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 161 |
13 files changed, 309 insertions, 510 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 79f4e99e1f..0cbb29575d 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,21 +32,25 @@ 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 prim_token = + | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *) + | 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 *) + (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list +type instance_expr = Misctypes.glob_level 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 *) + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some 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 @@ -56,14 +60,13 @@ type cases_pattern_expr = | CPatPrim of Loc.t * prim_token | CPatRecord of Loc.t * (reference * cases_pattern_expr) list | CPatDelimiters of Loc.t * string * cases_pattern_expr + | CPatCast of Loc.t * cases_pattern_expr * constr_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 = +and 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 @@ -73,9 +76,15 @@ type 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 + | CRecord of Loc.t * (reference * constr_expr) list + + (* representation of the "let" and "match" constructs *) + | CCases of Loc.t (* position of the "match" keyword *) + * 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 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) @@ -90,8 +99,9 @@ type 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 case_expr = constr_expr (* expression that is being matched *) + * Name.t located option (* as-clause *) + * cases_pattern_expr option (* in-clause *) and branch_expr = Loc.t * cases_pattern_expr list located list * constr_expr @@ -115,13 +125,14 @@ and recursion_order_expr = and local_binder = | LocalRawDef of Name.t located * constr_expr | LocalRawAssum of Name.t located list * binder_kind * constr_expr + | LocalPattern of Loc.t * cases_pattern_expr * constr_expr option 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 +type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr and typeclass_context = typeclass_constraint list diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 6886083c87..8254b1b802 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,7 +41,7 @@ type definition_object_kind = type assumption_object_kind = Definitional | Logical | Conjectural -(** [assumption_kind] +(* [assumption_kind] | Local | Global ------------------------------------ diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index 38a3e81f44..afc5e3bab9 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/extend.mli b/intf/extend.mli index ad9706f3a5..7ba332f709 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,6 +8,8 @@ (** Entry keys for constr notations *) +type 'a entry = 'a Compat.GrammarMake(CLexer).entry + type side = Left | Right type gram_assoc = NonA | RightA | LeftA @@ -50,3 +52,53 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen + +(** {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 + +(** {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.mli b/intf/genredexpr.mli index 6134091457..16f0c0c92a 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,11 +8,15 @@ (** Reduction expressions *) +open Names + (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = | FBeta - | FIota + | FMatch + | FFix + | FCofix | FZeta | FConst of 'a list | FDeltaBut of 'a list @@ -21,7 +25,9 @@ type 'a red_atom = type 'a glob_red_flag = { rBeta : bool; - rIota : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; rZeta : bool; rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) rConst : 'a list @@ -46,5 +52,15 @@ type ('a,'b,'c) red_expr_gen = 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 + | ConstrContext of (Loc.t * Id.t) * '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.mli b/intf/glob_term.mli index 32cf9eaf13..b3159c860c 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,9 +29,14 @@ type cases_pattern = | PatCstr of Loc.t * constructor * cases_pattern list * Name.t (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) +(** Representation of an internalized (or in other words globalized) term. *) type glob_constr = | GRef of (Loc.t * 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 (Loc.t * Id.t) + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) | 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 @@ -39,8 +44,7 @@ type 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]) *) + (** [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 diff --git a/intf/locus.mli b/intf/locus.mli index 808577943e..57b398ab46 100644 --- a/intf/locus.mli +++ b/intf/locus.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 74e136904d..e4f595ac4a 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -31,7 +31,8 @@ and 'constr intro_pattern_action_expr = | 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 + | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list + | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list (** Move destination for hypothesis *) @@ -43,9 +44,12 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a -type sort_info = string list -type level_info = string option +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) +type sort_info = string Loc.located list +type level_info = string Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen @@ -104,3 +108,31 @@ type 'a or_by_notation = (** 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 Id.t Loc.located + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 5a563bf953..1ab9980a5c 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -42,7 +42,6 @@ type notation_constr = (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; @@ -61,7 +60,7 @@ 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 + | NtnTypeConstr | NtnTypeOnlyBinder | 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 @@ -74,8 +73,25 @@ type interpretation = (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr +type reversibility_flag = bool + 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; +} + +type grammar_constr_prod_item = + | GramConstrTerminal of Tok.t + | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option + | GramConstrListMark of int * bool + (* tells action rule to make a list of the n previous parsed items; + concat with last parsed list if true *) + +type notation_grammar = { + notgram_level : int; + notgram_assoc : Extend.gram_assoc option; + notgram_notation : Constrexpr.notation; + notgram_prods : grammar_constr_prod_item list list; + notgram_typs : notation_var_internalization_type list; + notgram_onlyprinting : bool; } diff --git a/intf/pattern.mli b/intf/pattern.mli index 18cd2df0c4..329ae837e1 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli deleted file mode 100644 index f0377cff97..0000000000 --- a/intf/tacexpr.mli +++ /dev/null @@ -1,420 +0,0 @@ -(************************************************************************) -(* 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; -} - -type ml_tactic_entry = { - mltac_name : ml_tactic_name; - mltac_index : int; -} - -(** 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_entry * '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/tactypes.mli b/intf/tactypes.mli new file mode 100644 index 0000000000..b96cb67df8 --- /dev/null +++ b/intf/tactypes.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Tactic-related types that are not totally Ltac specific and still used in + lower API. It's not clear whether this is a temporary API or if this is + meant to stay. *) + +open Loc +open Names +open Constrexpr +open Glob_term +open Pattern +open Misctypes + +(** 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 glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern + +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } + +type delayed_open_constr = Term.constr delayed_open +type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open + +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 diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3f2d002c77..8827bc132e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ open Loc open Names -open Tacexpr open Misctypes open Constrexpr open Decl_kinds @@ -19,7 +18,6 @@ open Libnames 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 @@ -30,9 +28,9 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation 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 - | SelectAllParallel type goal_identifier = string type scope_name = string @@ -40,7 +38,8 @@ type scope_name = string type goal_reference = | OpenSubgoals | NthGoal of int - | GoalId of goal_identifier + | GoalId of Id.t + | GoalUid of goal_identifier type printable = | PrintTables @@ -61,7 +60,6 @@ type printable = | PrintClasses | PrintTypeClasses | PrintInstances of reference or_by_notation - | PrintLtac of reference | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions @@ -69,7 +67,6 @@ type printable = | PrintHint of reference or_by_notation | PrintHintGoal | PrintHintDbName of string - | PrintRewriteHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string @@ -108,7 +105,7 @@ type showable = | ShowTree | ShowProofNames | ShowIntros of bool - | ShowMatch of lident + | ShowMatch of reference | ShowThesis type comment = @@ -120,14 +117,25 @@ 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 (int option * bool * reference_or_constr) list + | 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 * bool list + | HintsMode of reference * hint_mode list | HintsConstructors of reference list - | HintsExtern of int * constr_expr option * raw_tactic_expr + | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument type search_restriction = | SearchInside of reference list @@ -135,7 +143,7 @@ type search_restriction = 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 opacity_flag = Opaque of lident list option | Transparent type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) @@ -155,23 +163,27 @@ 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. *) +type plident = lident * lident list option + 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 + | DefineBody of local_binder list * Genredexpr.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 + plident * (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 + plident * local_binder list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -190,22 +202,23 @@ 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 * + plident 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 + plident * 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 proof_expr = + plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) 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 + | SetOnlyParsing + | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version | SetFormat of string * string located type proof_end = @@ -218,14 +231,46 @@ type scheme = | EqualityScheme of reference or_by_notation type section_subset_expr = - | SsSet of lident list + | SsEmpty + | 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. -type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr + {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. -type extend_name = string * int + {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 *) @@ -272,19 +317,18 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of vernac_list + | VernacTime of vernac_expr located + | VernacRedirect of string * vernac_expr located | 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 + | VernacDelimiters of scope_name * string option + | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of @@ -294,14 +338,12 @@ type vernac_expr = (* 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 + (locality option * definition_object_kind) * plident * definition_expr + | VernacStartTheoremProof of theorem_kind * proof_expr list * bool | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * - inline * simple_binder with_coercion list + inline * (plident list * constr_expr) 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 @@ -310,20 +352,20 @@ type vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of (lident * Univ.constraint_type * lident) list + | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list (* Gallina extensions *) | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - export_flag option * lreference list - | VernacImport of export_flag * lreference list + reference option * export_flag option * reference list + | VernacImport of export_flag * reference 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 + | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) | VernacInstance of @@ -331,12 +373,12 @@ type vernac_expr = local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) - int option (* Priority *) + hint_info_expr | VernacContext of local_binder list | VernacDeclareInstances of - reference list * int option (* instance names, priority *) + (reference * hint_info_expr) list (* instances names, priorities and patterns *) | VernacDeclareClass of reference (* inductive or definition name *) @@ -351,7 +393,6 @@ type vernac_expr = (* Solving *) - | VernacSolve of goal_selector * int option * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) @@ -372,8 +413,6 @@ type vernac_expr = | 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 @@ -382,10 +421,12 @@ type vernac_expr = | 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 + 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 @@ -395,19 +436,19 @@ type vernac_expr = (Conv_oracle.level * reference or_by_notation list) list | VernacUnsetOption of Goptions.option_name | VernacSetOption of Goptions.option_name * option_value + | VernacSetAppendOption of Goptions.option_name * string | 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 + | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * raw_red_expr + | VernacDeclareReduction of string * Genredexpr.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 @@ -428,7 +469,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_descr option + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -441,9 +482,14 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and vernac_list = located_vernac_expr list +and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit -and located_vernac_expr = Loc.t * vernac_expr +and vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : (Loc.t * string) option; + implicit_status : vernac_implicit_status; +} (* A vernac classifier has to tell if a command: vernac_when: has to be executed now (alters the parser) or later @@ -454,7 +500,7 @@ type vernac_type = | VtStartProof of vernac_start | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type - | VtProofStep of bool (* parallelize *) + | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * report_with | VtStm of vernac_control * vernac_part_of_script @@ -476,6 +522,13 @@ and vernac_control = 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 |