diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 6 | ||||
| -rw-r--r-- | intf/extend.mli | 39 | ||||
| -rw-r--r-- | intf/notation_term.mli | 2 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 50 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 13 |
5 files changed, 49 insertions, 61 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 40812a3d87..efd5129b66 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -40,15 +40,15 @@ 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 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 diff --git a/intf/extend.mli b/intf/extend.mli index 57abdc38fb..381d47dd18 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -53,18 +53,28 @@ type simple_constr_prod_entry_key = (** {5 AST for user-provided entries} *) -type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Umodifiers : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +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} *) +(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *) +type (_, _, _) adj = +| Adj0 : ('r, unit, 'r) adj +| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj + +type _ index = +| I0 : 'a -> ('a * 'r) index +| IS : 'a index -> ('b * 'a) index + +(** This type should be marshallable, this is why we use a convoluted + representation in the [Arules] constructor instead of putting a function. *) type ('self, 'a) symbol = | Atoken : Tok.t -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol @@ -72,16 +82,23 @@ type ('self, 'a) 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 +| Arules : 'a rules -> ('self, 'a index) symbol -type ('self, _, 'r) rule = +and ('self, _, 'r) rule = | Stop : ('self, 'r, 'r) rule | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule +and 'a rules = +| Rule0 : unit rules +| RuleS : + ('any, 'act, Loc.t -> Loc.t * 'a) rule * + ('act, 'a, Loc.t -> Loc.t * 'a) adj * + 'b rules -> ((Loc.t * 'a) * 'b) rules + type 'a production_rule = | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 3a643b99b2..39a36310d1 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -61,7 +61,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 diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 57c61874a5..e06436d8a3 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -120,9 +120,9 @@ type open_constr_expr = unit * constr_expr 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 glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = +type 'a delayed_open = 'a Pretyping.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 @@ -145,15 +145,12 @@ type 'a gen_atomic_tactic_expr = ('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 @@ -163,21 +160,12 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* 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 * @@ -192,7 +180,6 @@ type 'a gen_atomic_tactic_expr = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -204,11 +191,9 @@ constraint 'a = < (** Possible arguments of a tactic definition *) -and 'a gen_tactic_arg = +type 'a gen_tactic_arg = | 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 @@ -219,7 +204,6 @@ and 'a gen_tactic_arg = constraint 'a = < term:'trm; - utrm: 'utrm; dterm: 'dtrm; pattern:'pat; constant:'cst; @@ -298,7 +282,6 @@ and 'a gen_tactic_expr = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -313,7 +296,6 @@ and 'a gen_tactic_fun_ast = constraint 'a = < term:'t; - utrm: 'utrm; dterm: 'dtrm; pattern:'p; constant:'c; @@ -326,7 +308,6 @@ constraint 'a = < (** Globalized tactics *) type g_trm = glob_constr_and_expr -type g_utrm = g_trm 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 @@ -334,7 +315,6 @@ type g_nam = Id.t located type g_dispatch = < term:g_trm; - utrm:g_utrm; dterm:g_trm; pattern:g_pat; constant:g_cst; @@ -356,7 +336,6 @@ type glob_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 @@ -365,7 +344,6 @@ type r_lev = rlevel type r_dispatch = < term:r_trm; - utrm:r_utrm; dterm:r_trm; pattern:r_pat; constant:r_cst; @@ -387,7 +365,6 @@ type raw_tactic_arg = (** Interpreted tactics *) type t_trm = Term.constr -type t_utrm = Glob_term.closed_glob_constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located @@ -395,26 +372,31 @@ 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; + tacexpr:unit; 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 + +(** 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 diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 7273b92b9a..ae9328fcc0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -31,7 +31,6 @@ type goal_selector = | SelectNth of int | SelectId of Id.t | SelectAll - | SelectAllParallel type goal_identifier = string type scope_name = string @@ -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 @@ -203,10 +200,6 @@ type one_inductive_expr = type proof_expr = plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) -type grammar_tactic_prod_item_expr = - | TacTerm of string - | TacNonTerm of Loc.t * string * (Names.Id.t * string) - type syntax_modifier = | SetItemLevel of string list * Extend.production_level | SetLevel of int @@ -293,13 +286,11 @@ type 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 option - | VernacBindScope of scope_name * reference or_by_notation list + | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of @@ -364,7 +355,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 *) @@ -385,7 +375,6 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr |