diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
tree | f69105ad9813738abd10ae824756947940a7dc6d /intf | |
parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'intf')
-rw-r--r-- | intf/constrexpr.ml | 4 | ||||
-rw-r--r-- | intf/misctypes.ml | 7 | ||||
-rw-r--r-- | intf/vernacexpr.ml | 27 |
3 files changed, 24 insertions, 14 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 413cd9704..8eadafe66 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -132,10 +132,6 @@ and constr_notation_substitution = constr_expr list list * (** for recursive notations *) local_binder_expr list list (** for binders subexpressions *) -type typeclass_constraint = (Name.t Loc.located * Id.t Loc.located list option) * binding_kind * constr_expr - -and typeclass_context = typeclass_constraint list - type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 807882b42..8b7073143 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -53,6 +53,7 @@ type level_info = Name.t Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen +type glob_constraint = glob_level * Univ.constraint_type * glob_level (** A synonym of [Evar.t], also defined in Term *) @@ -136,3 +137,9 @@ type inversion_kind = | SimpleInversion | FullInversion | FullInversionClear + +type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index fb713d352..cfc3343b6 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -166,8 +166,11 @@ type option_ref_value = | StringRefValue of string | QualidRefValue of reference -(** Identifier and optional list of bound universes. *) -type plident = lident * lident list option +(** 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 @@ -177,10 +180,10 @@ type definition_expr = * constr_expr option type fixpoint_expr = - plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = - plident * local_binder_expr list * constr_expr * constr_expr option + ident_decl * local_binder_expr list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -199,14 +202,18 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - plident * local_binder_expr list * constr_expr option * constructor_expr list + 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 + +and typeclass_context = typeclass_constraint list type proof_expr = - plident option * (local_binder_expr list * constr_expr) + ident_decl option * (local_binder_expr list * constr_expr) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -333,12 +340,12 @@ type vernac_expr = (* Gallina *) | VernacDefinition of - (locality option * definition_object_kind) * plident * definition_expr + (locality option * 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) * - inline * (plident list * constr_expr) with_coercion list + 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 @@ -347,7 +354,7 @@ type vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list + | VernacConstraint of glob_constraint list (* Gallina extensions *) | VernacBeginSection of lident |