diff options
Diffstat (limited to 'intf/constrexpr.ml')
| -rw-r--r-- | intf/constrexpr.ml | 60 |
1 files changed, 33 insertions, 27 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index e0d2d7bf48..31f811bc8a 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -15,6 +17,11 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + type notation = string type explicitation = @@ -46,10 +53,10 @@ 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 * lname | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list - (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of reference option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution @@ -68,14 +75,14 @@ and cases_pattern_notation_substitution = 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 - | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * - (constr_expr * explicitation Loc.located option) list + (constr_expr * explicitation CAst.t option) list | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) @@ -84,9 +91,9 @@ and constr_expr_r = * case_expr list * branch_expr list (* branches *) - | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) * + | CLetTuple of lname list * (lname option * constr_expr option) * constr_expr * constr_expr - | CIf of constr_expr * (Name.t Loc.located option * constr_expr option) + | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of patvar @@ -97,40 +104,39 @@ 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 *) - * Name.t Loc.located option (* as-clause *) + * lname option (* as-clause *) * 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) CAst.t and fix_expr = - Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * + lident * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr + lident * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) -(** Anonymous defs allowed ?? *) +(* Anonymous defs allowed ?? *) and local_binder_expr = - | CLocalAssum of Name.t Loc.located list * binder_kind * constr_expr - | CLocalDef of Name.t Loc.located * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t 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 @@ -138,7 +144,7 @@ type constr_pattern_expr = constr_expr type with_declaration_ast = | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * constr_expr + | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid |