diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 15 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 9 | ||||
| -rw-r--r-- | intf/extend.ml | 49 | ||||
| -rw-r--r-- | intf/glob_term.ml | 11 | ||||
| -rw-r--r-- | intf/intf.mllib | 2 | ||||
| -rw-r--r-- | intf/misctypes.ml | 12 | ||||
| -rw-r--r-- | intf/notation_term.ml | 25 | ||||
| -rw-r--r-- | intf/pattern.ml | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 113 |
9 files changed, 153 insertions, 85 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index e0d2d7bf48..c598287943 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 * Name.t Loc.located | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -70,8 +70,8 @@ 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 + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * @@ -97,6 +97,7 @@ 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 *) @@ -104,10 +105,7 @@ and case_expr = constr_expr (* expression that is being matched * cases_pattern_expr option (* in-clause *) and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located - -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr + (cases_pattern_expr list list * constr_expr) Loc.located and fix_expr = Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * @@ -130,7 +128,8 @@ and local_binder_expr = 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/decl_kinds.ml b/intf/decl_kinds.ml index a977588332..b9a3f0c212 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -8,6 +8,8 @@ (** Informal mathematical status of declarations *) +type discharge = DoDischarge | NoDischarge + type locality = Discharge | Local | Global type binding_kind = Explicit | Implicit @@ -40,6 +42,7 @@ type definition_object_kind = | IdentityCoercion | Instance | Method + | Let type assumption_object_kind = Definitional | Logical | Conjectural @@ -72,7 +75,11 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) + [@ocaml.deprecated "Please use [Declarations.Finite"] | CoFinite (** = coinductive *) + [@ocaml.deprecated "Please use [Declarations.CoFinite"] | BiFinite (** = non-recursive, like in "Record" definitions *) + [@ocaml.deprecated "Please use [Declarations.BiFinite"] +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] 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/glob_term.ml b/intf/glob_term.ml index 72c91db6a0..3f48fa5479 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -55,6 +55,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 @@ -93,10 +94,18 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +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 87484ccd50..33e961419d 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -48,13 +48,19 @@ 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 = Name.t Loc.located list -type level_info = Name.t Loc.located option -type glob_sort = sort_info glob_sort_gen +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 7823d3febb..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 * @@ -43,6 +43,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 +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; @@ -94,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/pattern.ml b/intf/pattern.ml index 20636accfa..64873a0394 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -26,7 +26,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 96bcba5e8b..d16c9bb802 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -145,16 +145,12 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Decl_kinds.recursivity_kind +type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) -type obsolete_locality = bool -(* Some grammar entries use obsolete_locality. This bool is to be backward - * compatible. If the grammar is fixed removing deprecated syntax, this - * bool should go away too *) type option_value = Goptions.option_value = | BoolValue of bool @@ -171,6 +167,7 @@ type option_ref_value = type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option type sort_expr = Sorts.family @@ -208,15 +205,16 @@ 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 * 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 @@ -318,40 +316,40 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) -type vernac_expr = - (* Control *) - | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr located - | VernacRedirect of string * vernac_expr located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string Loc.located option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = + + | VernacLoad of verbose_flag * string (* Syntax *) - | VernacSyntaxExtension of - bool * obsolete_locality * (lstring * syntax_modifier list) - | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + | VernacInfix of (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of - obsolete_locality * constr_expr * (lstring * syntax_modifier list) * + constr_expr * (lstring * syntax_modifier list) * scope_name option | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of - (locality option * definition_object_kind) * ident_decl * definition_expr + | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr | VernacStartTheoremProof of theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (locality option * assumption_object_kind) * + | VernacAssumption of (discharge * 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 - locality option * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of - locality option * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -364,10 +362,9 @@ type vernac_expr = 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 - | VernacIdentityCoercion of obsolete_locality * lident * + | VernacCoercion of reference or_by_notation * class_rawexpr * class_rawexpr + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) @@ -418,9 +415,9 @@ type vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list - | VernacHints of obsolete_locality * string list * hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * - obsolete_locality * onlyparsing_flag + onlyparsing_flag | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * @@ -454,7 +451,6 @@ type vernac_expr = | VernacComments of comment list (* Proof management *) - | VernacGoal of constr_expr | VernacAbort of lident option | VernacAbortAll | VernacRestart @@ -465,7 +461,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard @@ -477,32 +473,53 @@ 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 +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool -and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit +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 + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control -and vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string Loc.located option; - implicit_status : vernac_implicit_status; -} +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. -(* A vernac classifier has to tell if a command: - vernac_when: has to be executed now (alters the parser) or later - vernac_type: if it is starts, ends, continues a proof or + - vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is - a query like Check *) + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) type vernac_type = + (* Start of a proof *) | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) | VtSideff of vernac_sideff_type + (* End of a proof *) | VtQed of vernac_qed_type + (* A proof step *) | VtProofStep of proof_step + (* To be removed *) | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) | VtQuery of vernac_part_of_script * Feedback.route_id + (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) |