diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 34 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 20 |
2 files changed, 47 insertions, 7 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index ad9706f3a5..975f194b07 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -50,3 +50,37 @@ type constr_prod_entry_key = type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen + +(** {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 * string -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Amodifiers : ('self, 'a) symbol -> ('self, 'a list) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a Entry.t -> ('self, 'a) symbol +| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol + +type ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +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/tacexpr.mli b/intf/tacexpr.mli index eb4e5ae7d3..124d4c0fef 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -104,6 +104,11 @@ type ml_tactic_name = { 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 @@ -117,11 +122,12 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t 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 'a 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 -type delayed_open_constr = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr +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 @@ -291,7 +297,7 @@ and 'a gen_tactic_expr = | 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 + | 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 @@ -387,8 +393,8 @@ type raw_tactic_arg = type t_trm = Term.constr type t_utrm = Glob_term.closed_glob_constr -type t_pat = glob_constr_pattern_and_expr -type t_cst = evaluable_global_reference and_short_name +type t_pat = constr_pattern +type t_cst = evaluable_global_reference type t_ref = ltac_constant located type t_nam = Id.t |