diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 2 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 6 | ||||
| -rw-r--r-- | intf/glob_term.ml | 8 | ||||
| -rw-r--r-- | intf/misctypes.ml | 12 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 64 |
5 files changed, 61 insertions, 31 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index e0d2d7bf48..8bcdbcc0ef 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -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 a977588332..b0c1f66613 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/glob_term.ml b/intf/glob_term.ml index 72c91db6a0..f311d33b8a 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -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/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/vernacexpr.ml b/intf/vernacexpr.ml index 96bcba5e8b..c7a9db1cbc 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 @@ -327,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 @@ -364,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 *) @@ -418,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 * @@ -491,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 *) |