diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 21 | ||||
| -rw-r--r-- | intf/extend.mli | 34 | ||||
| -rw-r--r-- | intf/glob_term.mli | 8 | ||||
| -rw-r--r-- | intf/misctypes.mli | 5 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 27 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 21 |
6 files changed, 82 insertions, 34 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 79f4e99e1f..34dc1c6691 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -32,7 +32,9 @@ 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 @@ -73,9 +75,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 +98,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 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/glob_term.mli b/intf/glob_term.mli index 32cf9eaf13..dfcd4a67d3 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -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/misctypes.mli b/intf/misctypes.mli index 5c11119ed8..65c7dccf2a 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -43,7 +43,10 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a +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 diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 8c55a57051..05e7ea1a3b 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 = - Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr +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 @@ -156,10 +162,6 @@ type 'a gen_atomic_tactic_expr = 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 @@ -203,7 +205,6 @@ constraint 'a = < (** 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 @@ -291,9 +292,9 @@ 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 * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list + | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list constraint 'a = < term:'t; @@ -387,8 +388,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 diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 99264dbe0a..f763ba6cf8 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -19,7 +19,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 @@ -206,7 +205,7 @@ type proof_expr = type grammar_tactic_prod_item_expr = | TacTerm of string - | TacNonTerm of Loc.t * string * (Names.Id.t * string) option + | TacNonTerm of Loc.t * string * (Names.Id.t * string) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -287,8 +286,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of vernac_list - | VernacRedirect of string * 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 *) @@ -330,8 +329,8 @@ type vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - lreference option * 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 @@ -386,8 +385,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of - (rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacDeclareTacticDefinition of tacdef_body list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -421,7 +419,6 @@ type vernac_expr = | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacNop (* Stm backdoor *) | VernacStm of vernac_expr stm_vernac @@ -455,9 +452,9 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and vernac_list = located_vernac_expr list - -and located_vernac_expr = Loc.t * 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 |