diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 38 | ||||
| -rw-r--r-- | intf/extend.ml | 49 | ||||
| -rw-r--r-- | intf/genredexpr.ml | 4 | ||||
| -rw-r--r-- | intf/glob_term.ml | 2 | ||||
| -rw-r--r-- | intf/intf.mllib | 2 | ||||
| -rw-r--r-- | intf/misctypes.ml | 14 | ||||
| -rw-r--r-- | intf/notation_term.ml | 24 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 43 |
8 files changed, 101 insertions, 75 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index fbf9e248ab..5b51953bbe 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -46,7 +46,7 @@ type prim_token = type instance_expr = Misctypes.glob_level list type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Id.t + | CPatAlias of cases_pattern_expr * lname | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -68,14 +68,14 @@ and cases_pattern_notation_substitution = and constr_expr_r = | CRef of reference * instance_expr option - | CFix of Id.t Loc.located * fix_expr list - | CCoFix of Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr - | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * - (constr_expr * explicitation Loc.located option) list + (constr_expr * explicitation CAst.t option) list | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) @@ -84,9 +84,9 @@ and constr_expr_r = * case_expr list * branch_expr list (* branches *) - | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) * + | CLetTuple of lname list * (lname option * constr_expr option) * constr_expr * constr_expr - | CIf of constr_expr * (Name.t Loc.located option * constr_expr option) + | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of patvar @@ -101,21 +101,18 @@ and constr_expr_r = and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) - * Name.t Loc.located option (* as-clause *) + * lname option (* as-clause *) * cases_pattern_expr option (* in-clause *) and branch_expr = - (cases_pattern_expr list list * constr_expr) Loc.located - -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr + (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * + lident * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr + lident * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -124,14 +121,15 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | CLocalAssum of Name.t Loc.located list * binder_kind * constr_expr - | CLocalDef of Name.t Loc.located * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder_expr list list (** for binders subexpressions *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/intf/extend.ml b/intf/extend.ml index 5552bed559..78f0aa1178 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,29 +29,48 @@ type production_level = | NextLevel | NumLevel of int -type ('lev,'pos) constr_entry_key_gen = - | ETName | ETReference | ETBigint - | ETBinder of bool - | ETConstr of ('lev * 'pos) - | ETPattern +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + +(** User-level types used to tell how to parse or interpret of the non-terminal *) + +type 'a constr_entry_key_gen = + | ETName + | ETReference + | ETBigint + | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) + | ETConstr of 'a + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string - | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of bool * Tok.t list -(** Entries level (left-hand-side of grammar rules) *) +(** Entries level (left-hand side of grammar rules) *) type constr_entry_key = - (int,unit) constr_entry_key_gen - -(** Entries used in productions (in right-hand-side of grammar rules) *) - -type constr_prod_entry_key = - (production_level,production_position) constr_entry_key_gen + (production_level * production_position) constr_entry_key_gen (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = - (production_level,unit) constr_entry_key_gen + production_level option constr_entry_key_gen + +(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) + +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + +type binder_target = ForBinder | ForTerm + +type constr_prod_entry_key = + | ETProdName (* Parsed as a name (ident or _) *) + | ETProdReference (* Parsed as a global reference *) + | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) + | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) + | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) + | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) (** {5 AST for user-provided entries} *) diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml index a8c37c6207..bdf3242ca3 100644 --- a/intf/genredexpr.ml +++ b/intf/genredexpr.ml @@ -8,8 +8,6 @@ (** Reduction expressions *) -open Names - (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -52,7 +50,7 @@ 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 Id.t Loc.located * 'a + | ConstrContext of Misctypes.lident * 'a | ConstrTypeOf of 'a open Libnames diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 61bbe2c264..3f48fa5479 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -105,7 +105,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option - | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g + | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g diff --git a/intf/intf.mllib b/intf/intf.mllib index 38a2a71cc0..2b8960d3f2 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -2,9 +2,9 @@ Constrexpr Evar_kinds Genredexpr Locus +Extend Notation_term Decl_kinds -Extend Glob_term Misctypes Pattern diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 33e961419d..aafd61b3c2 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -8,7 +8,13 @@ open Names -(** Basic types used both in [constr_expr] and in [glob_constr] *) +(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t (** Cases pattern variables *) @@ -101,9 +107,9 @@ type 'a with_bindings = 'a * 'a bindings type 'a or_var = | ArgArg of 'a - | ArgVar of Names.Id.t Loc.located + | ArgVar of lident -type 'a and_short_name = 'a * Id.t Loc.located option +type 'a and_short_name = 'a * lident option type 'a or_by_notation = | AN of 'a @@ -134,7 +140,7 @@ type multi = type 'a core_destruction_arg = | ElimOnConstr of 'a - | ElimOnIdent of Id.t Loc.located + | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cad6f4b821..86f5adbd78 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -25,11 +25,11 @@ type notation_constr = | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Id.t * Id.t * notation_constr * notation_constr * bool + | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr - | NBinderList of Id.t * Id.t * notation_constr * notation_constr + | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * @@ -60,21 +60,31 @@ 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_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind + type notation_var_instance_type = - | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList -(** Type of variables when interpreting a constr_expr as an notation_constr: +(** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + | NtnInternTypeAny | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr -type reversibility_flag = bool +type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; @@ -95,7 +105,7 @@ type precedence = int type parenRelation = L | E | Any | Prec of precedence type tolerability = precedence * parenRelation -type level = precedence * tolerability list * notation_var_internalization_type list +type level = precedence * tolerability list * Extend.constr_entry_key list (** Grammar rules for a notation *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8e0fe54c55..ba28eaceaa 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -6,19 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Misctypes open Constrexpr -open Decl_kinds open Libnames (** Vernac expressions, produced by the parser *) - -type lident = Id.t located -type lname = Name.t located -type lstring = string located - type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation (* spiwack: I'm choosing, for now, to have [goal_selector] be a @@ -40,7 +33,8 @@ type goal_reference = | NthGoal of int | GoalId of Id.t -type univ_name_list = Name.t Loc.located list +type univ_name_list = Universes.univ_name_list +[@@ocaml.deprecated "Use [Universes.univ_name_list]"] type printable = | PrintTables @@ -56,7 +50,7 @@ type printable = | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation * univ_name_list option + | PrintName of reference or_by_notation * Universes.univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses @@ -72,7 +66,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option + | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -164,7 +158,7 @@ type option_ref_value = (** Identifier and optional list of bound universes and constraints. *) -type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option @@ -177,7 +171,7 @@ type definition_expr = * constr_expr option type fixpoint_expr = - ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = ident_decl * local_binder_expr list * constr_expr * constr_expr option @@ -205,7 +199,7 @@ type inductive_expr = type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = name_decl * binding_kind * constr_expr +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr and typeclass_context = typeclass_constraint list @@ -214,13 +208,14 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key | SetOnlyParsing | SetOnlyPrinting | SetCompatVersion of Flags.compat_version - | SetFormat of string * string located + | SetFormat of string * lstring type proof_end = | Admitted @@ -320,7 +315,7 @@ type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit type vernac_argument_status = { name : Name.t; recarg_like : bool; - notation_scope : string Loc.located option; + notation_scope : string CAst.t option; implicit_status : vernac_implicit_status; } @@ -340,15 +335,15 @@ type nonrec vernac_expr = | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of theorem_kind * proof_expr list + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (discharge * assumption_object_kind) * + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -415,7 +410,7 @@ type nonrec vernac_expr = | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of string list * hints_expr - | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * + | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list @@ -481,8 +476,8 @@ type vernac_control = | VernacExpr of vernac_flag list * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control located - | VernacRedirect of string * vernac_control located + | VernacTime of bool * vernac_control CAst.t + | VernacRedirect of string * vernac_control CAst.t | VernacTimeout of int * vernac_control | VernacFail of vernac_control |