diff options
-rw-r--r-- | intf/tacexpr.mli | 160 | ||||
-rw-r--r-- | printing/pptactic.ml | 13 |
2 files changed, 118 insertions, 55 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 55d6e53a5..3501917f2 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -119,7 +119,7 @@ type intro_pattern_naming = intro_pattern_naming_expr located (** Generic expressions for atomic tactics *) -type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr = +type 'a gen_atomic_tactic_expr = (* Basic tactics *) | TacIntroPattern of 'trm intro_pattern_expr located list | TacIntroMove of Id.t option * 'nam move_location @@ -133,7 +133,7 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - bool * ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option * + bool * 'a gen_tactic_expr option * 'trm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list | TacGeneralizeDep of 'trm @@ -168,12 +168,21 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr = (* Equality and inversion *) | TacRewrite of evars_flag * (bool * multi * 'trm with_bindings_arg) list * 'nam clause_expr * - ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr option + 'a gen_tactic_expr option | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis +constraint 'a = < + term:'trm; + pattern:'pat; + constant:'cst; + reference:'ref; + name:'nam; + level:'lev +> + (** Possible arguments of a tactic definition *) -and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg = +and 'a gen_tactic_arg = | TacDynamic of Loc.t * Dyn.t | TacGeneric of 'lev generic_argument | MetaIdArg of Loc.t * bool * string @@ -184,77 +193,104 @@ and ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg = is not a variant of [tactic_expr]. *) | Reference of 'ref | TacCall of Loc.t * 'ref * - ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_arg list + 'a gen_tactic_arg list | TacFreshId of string or_var list - | Tacexp of ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr + | Tacexp of 'a gen_tactic_expr | TacPretype of 'trm | TacNumgoals +constraint 'a = < + term:'trm; + pattern:'pat; + constant:'cst; + reference:'ref; + name:'nam; + level:'lev +> + (** Generic ltac expressions. 't : terms, 'p : patterns, 'c : constants, 'i : inductive, 'r : ltac refs, 'n : idents, 'l : levels *) -and ('t,'p,'c,'r,'n,'l) gen_tactic_expr = - | TacAtom of Loc.t * ('t,'p,'c,'r,'n,'l) gen_atomic_tactic_expr +and 'a gen_tactic_expr = + | TacAtom of Loc.t * 'a gen_atomic_tactic_expr | TacThen of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr + 'a gen_tactic_expr * + 'a gen_tactic_expr | TacDispatch of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr list + 'a gen_tactic_expr list | TacExtendTac of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr array * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr array + 'a gen_tactic_expr array * + 'a gen_tactic_expr * + 'a gen_tactic_expr array | TacThens of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr list + 'a gen_tactic_expr * + 'a gen_tactic_expr list | TacThens3parts of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr array * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr array - | TacFirst of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list - | TacComplete of ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacSolve of ('t,'p,'c,'r,'n,'l) gen_tactic_expr list - | TacTry of ('t,'p,'c,'r,'n,'l) gen_tactic_expr + '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 - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr + 'a gen_tactic_expr * + 'a gen_tactic_expr | TacOnce of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr + 'a gen_tactic_expr | TacExactlyOnce of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr + 'a gen_tactic_expr | TacOrelse of - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacDo of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacTimeout of int or_var * ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacTime of string option * ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacRepeat of ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacProgress of ('t,'p,'c,'r,'n,'l) gen_tactic_expr - | TacShowHyps of ('t,'p,'c,'r,'n,'l) gen_tactic_expr + '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 - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * Id.t option + 'a gen_tactic_expr * Id.t option | TacId of 'n message_token list | TacFail of int or_var * 'n message_token list - | TacInfo of ('t,'p,'c,'r,'n,'l) gen_tactic_expr + | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Id.t located * ('t,'p,'c,'r,'n,'l) gen_tactic_arg) list * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr + (Id.t located * 'a gen_tactic_arg) list * + 'a gen_tactic_expr | TacMatch of lazy_flag * - ('t,'p,'c,'r,'n,'l) gen_tactic_expr * - ('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list + 'a gen_tactic_expr * + ('p,'a gen_tactic_expr) match_rule list | TacMatchGoal of lazy_flag * direction_flag * - ('p,('t,'p,'c,'r,'n,'l) gen_tactic_expr) match_rule list - | TacFun of ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast - | TacArg of ('t,'p,'c,'r,'n,'l) gen_tactic_arg located + ('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 -and ('t,'p,'c,'r,'n,'l) gen_tactic_fun_ast = - Id.t option list * ('t,'p,'c,'r,'n,'l) gen_tactic_expr +constraint 'a = < + term:'t; + pattern:'p; + constant:'c; + reference:'r; + name:'n; + level:'l +> + +and 'a gen_tactic_fun_ast = + Id.t option list * 'a gen_tactic_expr + +constraint 'a = < + term:'t; + pattern:'p; + constant:'c; + reference:'r; + name:'n; + level:'l +> (** Globalized tactics *) @@ -264,14 +300,23 @@ 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; + pattern:g_pat; + constant:g_cst; + reference:g_ref; + name:g_nam; + level:glevel +> + type glob_tactic_expr = - (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_expr + g_dispatch gen_tactic_expr type glob_atomic_tactic_expr = - (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_atomic_tactic_expr + g_dispatch gen_atomic_tactic_expr type glob_tactic_arg = - (g_trm, g_pat, g_cst, g_ref, g_nam, glevel) gen_tactic_arg + g_dispatch gen_tactic_arg (** Raw tactics *) @@ -282,14 +327,23 @@ type r_ref = reference type r_nam = Id.t located type r_lev = rlevel +type r_dispatch = < + term:r_trm; + pattern:r_pat; + constant:r_cst; + reference:r_ref; + name:r_nam; + level:rlevel +> + type raw_atomic_tactic_expr = - (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_atomic_tactic_expr + r_dispatch gen_atomic_tactic_expr type raw_tactic_expr = - (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_expr + r_dispatch gen_tactic_expr type raw_tactic_arg = - (r_trm, r_pat, r_cst, r_ref, r_nam, rlevel) gen_tactic_arg + r_dispatch gen_tactic_arg (** Misc *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b6b8c9c2e..647d5702e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -608,8 +608,8 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) -type ('trm,'pat,'cst,'ref,'nam,'lev) printer = { - pr_tactic : tolerability -> ('trm,'pat,'cst,'ref,'nam,'lev) gen_tactic_expr -> std_ppcmds; +type 'a printer = { + pr_tactic : tolerability -> 'a gen_tactic_expr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -622,6 +622,15 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) printer = { pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; } +constraint 'a = < + term:'trm; + pattern:'pat; + constant:'cst; + reference:'ref; + name:'nam; + level:'lev +> + let make_pr_tac pr (strip_prod_binders) = |