diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 5 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 9 | ||||
| -rw-r--r-- | intf/evar_kinds.ml | 2 | ||||
| -rw-r--r-- | intf/glob_term.ml | 11 | ||||
| -rw-r--r-- | intf/intf.mllib | 1 | ||||
| -rw-r--r-- | intf/misctypes.ml | 15 | ||||
| -rw-r--r-- | intf/notation_term.ml | 3 | ||||
| -rw-r--r-- | intf/pattern.ml | 6 | ||||
| -rw-r--r-- | intf/tactypes.ml | 33 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 118 |
10 files changed, 106 insertions, 97 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8eadafe667..fbf9e248ab 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -79,7 +79,7 @@ and constr_expr_r = | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) - | CCases of case_style (* determines whether this value represents "let" or "match" construct *) + | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) * constr_expr option (* return-clause *) * case_expr list * branch_expr list (* branches *) @@ -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,7 +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 + (cases_pattern_expr list list * constr_expr) Loc.located and binder_expr = Name.t Loc.located list * binder_kind * 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/evar_kinds.ml b/intf/evar_kinds.ml index 36c421c6ca..428d6b6785 100644 --- a/intf/evar_kinds.ml +++ b/intf/evar_kinds.ml @@ -32,4 +32,4 @@ type t = | ImpossibleCase | MatchingVar of matching_var_kind | VarInstance of Id.t - | SubEvar of Constr.existential_key + | SubEvar of Evar.t diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 508990a580..61bbe2c264 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -46,7 +46,7 @@ type 'a glob_constr_r = | GLambda of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g | GProd of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g | GLetIn of Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g - | GCases of case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GCases of Constr.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g @@ -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,6 +94,14 @@ 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 diff --git a/intf/intf.mllib b/intf/intf.mllib index 523e4b2650..38a2a71cc0 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -3,7 +3,6 @@ Evar_kinds Genredexpr Locus Notation_term -Tactypes Decl_kinds Extend Glob_term diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 8b70731432..33e961419d 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -48,25 +48,32 @@ 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 (** Case style, shared with Term *) -type case_style = Term.case_style = +type case_style = Constr.case_style = | LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) +[@@ocaml.deprecated "Alias for Constr.case_style"] (** Casts *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index c342da3dca..cad6f4b821 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -31,7 +31,7 @@ type notation_constr = | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr - | NCases of case_style * notation_constr option * + | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list | NLetTuple of Name.t list * (Name.t * notation_constr option) * @@ -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 diff --git a/intf/pattern.ml b/intf/pattern.ml index 16c4807355..64873a0394 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -8,13 +8,13 @@ open Names open Globnames -open Term +open Constr open Misctypes (** {5 Patterns} *) type case_info_pattern = - { cip_style : case_style; + { cip_style : Constr.case_style; cip_ind : inductive option; cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } @@ -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/tactypes.ml b/intf/tactypes.ml deleted file mode 100644 index 2c42e13110..0000000000 --- a/intf/tactypes.ml +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Tactic-related types that are not totally Ltac specific and still used in - lower API. It's not clear whether this is a temporary API or if this is - meant to stay. *) - -open Loc -open Names -open Constrexpr -open Pattern -open Misctypes - -(** In globalize tactics, we need to keep the initial [constr_expr] to recompute - in the environment by the effective calls to Intro, Inversion, etc - The [constr_expr] field is [None] in TacDef though *) -type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option -type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr located -type intro_patterns = delayed_open_constr intro_pattern_expr located list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located -type intro_pattern_naming = intro_pattern_naming_expr located diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 9aef4b1312..8e0fe54c55 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -40,6 +40,8 @@ type goal_reference = | NthGoal of int | GoalId of Id.t +type univ_name_list = Name.t Loc.located list + type printable = | PrintTables | PrintFullContext @@ -54,7 +56,7 @@ type printable = | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation + | PrintName of reference or_by_notation * univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses @@ -70,7 +72,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * goal_selector option + | PrintAbout of reference or_by_notation * 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 @@ -143,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 @@ -169,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 @@ -206,12 +205,12 @@ 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 @@ -316,40 +315,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 @@ -362,10 +361,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 *) @@ -416,9 +414,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 * @@ -452,7 +450,6 @@ type vernac_expr = | VernacComments of comment list (* Proof management *) - | VernacGoal of constr_expr | VernacAbort of lident option | VernacAbortAll | VernacRestart @@ -463,7 +460,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard @@ -475,32 +472,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 *) |