From dfac5aa2285de5b89f08ada3c30c0a1594737440 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Sep 2016 18:02:52 +0200 Subject: Making Vernacexpr independent from Tacexpr. --- intf/genredexpr.mli | 14 +++++++++++++- intf/tacexpr.mli | 6 +++++- intf/vernacexpr.mli | 17 ++++++----------- 3 files changed, 24 insertions(+), 13 deletions(-) (limited to 'intf') diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 2df79673ad..16f0c0c92a 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -8,6 +8,8 @@ (** Reduction expressions *) +open Names + (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -50,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/tacexpr.mli b/intf/tacexpr.mli index 5b5957bef5..946d124a45 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -34,7 +34,7 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) -type goal_selector = +type goal_selector = Vernacexpr.goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -401,3 +401,7 @@ type ltac_call_kind = | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map type ltac_trace = (Loc.t * ltac_call_kind) list + +type tacdef_body = + | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ed44704df4..5713b2ee6e 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -8,7 +8,6 @@ open Loc open Names -open Tacexpr open Misctypes open Constrexpr open Decl_kinds @@ -27,7 +26,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation 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 = Tacexpr.goal_selector = +type goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t @@ -130,7 +129,7 @@ type hints_expr = | HintsTransparency of reference list * bool | 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 @@ -171,7 +170,7 @@ 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 = @@ -432,9 +431,9 @@ type vernac_expr = | 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 @@ -460,7 +459,7 @@ type vernac_expr = | VernacEndSubproof | VernacShow of showable | VernacCheckGuard - | VernacProof of raw_tactic_expr option * section_subset_expr option + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option | VernacProofMode of string (* Toplevel control *) | VernacToplevelControl of exn @@ -473,10 +472,6 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) - (* 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 -- cgit v1.2.3 From ae9f6d13b63f30168d2eaa2289108a117ad840f7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 7 Sep 2016 18:51:52 +0200 Subject: Unplugging Tacexpr in several interface files. --- intf/misctypes.mli | 9 +++++++++ intf/tacexpr.mli | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 1452bbc347..c6c4b01e4e 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -108,3 +108,12 @@ 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 *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 946d124a45..cf33d79733 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -125,7 +125,7 @@ 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 binding_bound_vars = Id.Set.t +type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern type 'a delayed_open = 'a Pretyping.delayed_open = -- cgit v1.2.3 From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Sep 2016 18:11:54 +0200 Subject: Untangling Tacexpr from lower strata. --- intf/misctypes.mli | 19 +++++++++++++++++++ intf/tacexpr.mli | 19 ++++--------------- intf/tactypes.mli | 35 +++++++++++++++++++++++++++++++++++ 3 files changed, 58 insertions(+), 15 deletions(-) create mode 100644 intf/tactypes.mli (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index c6c4b01e4e..e4f595ac4a 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -117,3 +117,22 @@ 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/tacexpr.mli b/intf/tacexpr.mli index cf33d79733..9c25a16457 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -32,15 +32,13 @@ 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 goal_selector = Vernacexpr.goal_selector = | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t | SelectAll -type 'a core_destruction_arg = +type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of Id.t located | ElimOnAnonHyp of int @@ -48,7 +46,7 @@ type 'a core_destruction_arg = type 'a destruction_arg = clear_flag * 'a core_destruction_arg -type inversion_kind = +type inversion_kind = Misctypes.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear @@ -79,12 +77,6 @@ type ('constr,'dconstr,'id) induction_clause_list = 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 @@ -117,10 +109,7 @@ type ml_tactic_entry = { (** 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 glob_constr_and_expr = Tactypes.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr @@ -128,7 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = 'a Pretyping.delayed_open = +type 'a delayed_open = 'a Tactypes.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open 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 *) +(* '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 -- cgit v1.2.3 From 108fbe13e3c07c283e2cb972ac96679632bcd84a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Sep 2016 19:36:13 +0200 Subject: Moving Tacexpr to ltac/ folder. --- intf/tacexpr.mli | 396 ------------------------------------------------------- 1 file changed, 396 deletions(-) delete mode 100644 intf/tacexpr.mli (limited to 'intf') diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli deleted file mode 100644 index 9c25a16457..0000000000 --- a/intf/tacexpr.mli +++ /dev/null @@ -1,396 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'r Sigma.t -> ('a, 'r) Sigma.sigma } - -type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open - -type delayed_open_constr = Term.constr 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 - -(** Generic expressions for atomic tactics *) - -type 'a gen_atomic_tactic_expr = - (* Basic tactics *) - | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list - | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * - ('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 - | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list - | TacMutualCofix of Id.t * (Id.t * 'trm) list - | TacAssert of - bool * 'tacexpr option option * - 'dtrm intro_pattern_expr located option * 'trm - | TacGeneralize of ('trm with_occurrences * Name.t) list - | 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 - - (* Conversion *) - | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr - | TacChange of 'pat option * 'dtrm * '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; - dterm: 'dtrm; - pattern:'pat; - constant:'cst; - reference:'ref; - name:'nam; - tacexpr:'tacexpr; - level:'lev -> - -(** Possible arguments of a tactic definition *) - -type 'a gen_tactic_arg = - | TacGeneric of 'lev generic_argument - | ConstrMayEval of ('trm,'cst,'pat) may_eval - | 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; - 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 - | TacSelect of goal_selector * 'a gen_tactic_expr - (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list - (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list - -constraint 'a = < - term:'t; - 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; - 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_pat = glob_constr_pattern_and_expr -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; - 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_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; - 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_pat = constr_pattern -type t_cst = evaluable_global_reference -type t_ref = ltac_constant located -type t_nam = Id.t - -type t_dispatch = < - term:t_trm; - dterm:g_trm; - pattern:t_pat; - constant:t_cst; - reference:t_ref; - name:t_nam; - tacexpr:unit; - level:tlevel -> - -type atomic_tactic_expr = - t_dispatch gen_atomic_tactic_expr - -(** 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 - -(** Traces *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -type tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) -- cgit v1.2.3