diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 60 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 10 | ||||
| -rw-r--r-- | intf/evar_kinds.ml | 10 | ||||
| -rw-r--r-- | intf/extend.ml | 59 | ||||
| -rw-r--r-- | intf/genredexpr.ml | 14 | ||||
| -rw-r--r-- | intf/glob_term.ml | 13 | ||||
| -rw-r--r-- | intf/intf.mllib | 2 | ||||
| -rw-r--r-- | intf/locus.ml | 10 | ||||
| -rw-r--r-- | intf/misctypes.ml | 24 | ||||
| -rw-r--r-- | intf/notation_term.ml | 35 | ||||
| -rw-r--r-- | intf/pattern.ml | 12 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 102 |
12 files changed, 207 insertions, 144 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8bcdbcc0ef..31f811bc8a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -15,6 +17,11 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) +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 + type notation = string type explicitation = @@ -46,10 +53,10 @@ 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 *) + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of reference option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution @@ -68,14 +75,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 +91,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 @@ -97,40 +104,39 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr + | CProj of reference * constr_expr 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 | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) -(** Anonymous defs allowed ?? *) +(* 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 @@ -138,7 +144,7 @@ type constr_pattern_expr = constr_expr type with_declaration_ast = | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * constr_expr + | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index b9a3f0c212..0d32853116 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Informal mathematical status of declarations *) diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index 428d6b6785..c5de383b21 100644 --- a/intf/evar_kinds.ml +++ b/intf/evar_kinds.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/intf/extend.ml b/intf/extend.ml index 5552bed559..10c9b3dc14 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Entry keys for constr notations *) @@ -29,29 +31,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..80697461a6 100644 --- a/intf/genredexpr.ml +++ b/intf/genredexpr.ml @@ -1,15 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Reduction expressions *) -open Names - (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -52,7 +52,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 f311d33b8a..39a7b956ab 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Untyped intermediate terms *) @@ -55,6 +57,7 @@ type 'a glob_constr_r = | GSort of glob_sort | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type + | GProj of Projection.t * 'a glob_constr_g and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g @@ -104,7 +107,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/locus.ml b/intf/locus.ml index 81fa704d88..95a2e495be 100644 --- a/intf/locus.ml +++ b/intf/locus.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 33e961419d..54a4861d09 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -1,14 +1,22 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) 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 +109,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 +142,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 7823d3febb..a9c2e2a532 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -25,11 +27,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 * @@ -43,6 +45,7 @@ type notation_constr = notation_constr array * notation_constr array | NSort of glob_sort | NCast of notation_constr * notation_constr cast_type + | NProj of Projection.t * notation_constr (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted @@ -59,21 +62,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; @@ -94,7 +107,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/pattern.ml b/intf/pattern.ml index 20636accfa..af2347674f 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -26,7 +28,7 @@ type constr_pattern = | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of patvar * constr_pattern list - | PProj of projection * constr_pattern + | PProj of Projection.t * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index a90e5501a5..0a6e5b3b31 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -1,24 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -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 +35,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 +52,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 +68,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,10 +160,6 @@ 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 ident_decl = lident * universe_decl_expr option - type sort_expr = Sorts.family type definition_expr = @@ -176,7 +168,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 @@ -204,22 +196,23 @@ type inductive_expr = type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = (Name.t Loc.located * universe_decl_expr option) * binding_kind * constr_expr +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = - ident_decl option * (local_binder_expr list * constr_expr) + ident_decl * (local_binder_expr list * constr_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 @@ -314,7 +307,16 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) -type vernac_expr = +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string CAst.t option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = | VernacLoad of verbose_flag * string (* Syntax *) @@ -330,15 +332,15 @@ type vernac_expr = | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of (discharge * definition_object_kind) * ident_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 @@ -405,7 +407,7 @@ type 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 @@ -440,7 +442,6 @@ type vernac_expr = | VernacComments of comment list (* Proof management *) - | VernacGoal of constr_expr | VernacAbort of lident option | VernacAbortAll | VernacRestart @@ -451,7 +452,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard @@ -463,25 +464,17 @@ type vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list - (* Flags *) - | VernacProgram of vernac_expr - | VernacPolymorphic of bool * vernac_expr - | VernacLocal of bool * vernac_expr - -and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -and vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string Loc.located option; - implicit_status : vernac_implicit_status; -} +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool type vernac_control = - | VernacExpr of vernac_expr - (* Control *) - | VernacTime of vernac_control located - | VernacRedirect of string * vernac_control located + | 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 CAst.t + | VernacRedirect of string * vernac_control CAst.t | VernacTimeout of int * vernac_control | VernacFail of vernac_control @@ -538,3 +531,14 @@ type vernac_when = | VtNow | VtLater type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] |