diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 4 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 6 | ||||
| -rw-r--r-- | intf/evar_kinds.ml | 2 | ||||
| -rw-r--r-- | intf/glob_term.ml | 10 | ||||
| -rw-r--r-- | intf/intf.mllib | 1 | ||||
| -rw-r--r-- | intf/misctypes.ml | 15 | ||||
| -rw-r--r-- | intf/notation_term.ml | 2 | ||||
| -rw-r--r-- | intf/pattern.ml | 4 | ||||
| -rw-r--r-- | intf/tactypes.ml | 33 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 70 |
10 files changed, 73 insertions, 74 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 8eadafe66..8bcdbcc0e 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 *) @@ -104,7 +104,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 a97758833..b0c1f6661 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,8 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) | BiFinite (** = non-recursive, like in "Record" definitions *) +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml index 36c421c6c..428d6b678 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 508990a58..f311d33b8 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 @@ -93,6 +93,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 523e4b265..38a2a71cc 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 8b7073143..33e961419 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 c342da3dc..7823d3feb 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) * diff --git a/intf/pattern.ml b/intf/pattern.ml index 16c480735..20636accf 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 _ => _ ? *) } diff --git a/intf/tactypes.ml b/intf/tactypes.ml deleted file mode 100644 index 2c42e1311..000000000 --- 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 9aef4b131..c7a9db1cb 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 @@ -325,31 +323,27 @@ type vernac_expr = | VernacFail of vernac_expr (* 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) * ident_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 +356,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 +409,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 * @@ -489,18 +482,39 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } -(* 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 +(* 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. + + - 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 *) |