diff options
Diffstat (limited to 'intf/constrexpr.mli')
| -rw-r--r-- | intf/constrexpr.mli | 115 |
1 files changed, 58 insertions, 57 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 77f052ddbd..d54ad8bee3 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Libnames open Misctypes @@ -38,75 +37,76 @@ type prim_token = type instance_expr = Misctypes.glob_level list -type cases_pattern_expr = - | CPatAlias of Loc.t * cases_pattern_expr * Id.t - | CPatCstr of Loc.t * reference +type cases_pattern_expr_r = + | CPatAlias of cases_pattern_expr * Id.t + | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) - | CPatAtom of Loc.t * reference option - | CPatOr of Loc.t * cases_pattern_expr list - | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution + | CPatAtom of reference option + | CPatOr of cases_pattern_expr list + | CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) - | CPatPrim of Loc.t * prim_token - | CPatRecord of Loc.t * (reference * cases_pattern_expr) list - | CPatDelimiters of Loc.t * string * cases_pattern_expr - | CPatCast of Loc.t * cases_pattern_expr * constr_expr + | CPatPrim of prim_token + | CPatRecord of (reference * cases_pattern_expr) list + | CPatDelimiters of string * cases_pattern_expr + | CPatCast of cases_pattern_expr * constr_expr +and cases_pattern_expr = cases_pattern_expr_r CAst.ast and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) cases_pattern_expr list list (** for recursive notations *) -and constr_expr = - | CRef of reference * instance_expr option - | CFix of Loc.t * Id.t located * fix_expr list - | CCoFix of Loc.t * Id.t located * cofix_expr list - | CProdN of Loc.t * binder_expr list * constr_expr - | CLambdaN of Loc.t * binder_expr list * constr_expr - | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr - | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list - | CApp of Loc.t * (proj_flag * constr_expr) * - (constr_expr * explicitation located option) list - | CRecord of Loc.t * (reference * constr_expr) list +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 + | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation Loc.located option) list + | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) - | CCases of Loc.t (* position of the "match" keyword *) - * case_style (* determines whether this value represents "let" or "match" construct *) - * constr_expr option (* return-clause *) - * case_expr list - * branch_expr list (* branches *) - - | CLetTuple of Loc.t * Name.t located list * (Name.t located option * constr_expr option) * - constr_expr * constr_expr - | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option) - * constr_expr * constr_expr - | CHole of Loc.t * Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option - | CPatVar of Loc.t * patvar - | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list - | CSort of Loc.t * glob_sort - | CCast of Loc.t * constr_expr * constr_expr cast_type - | CNotation of Loc.t * notation * constr_notation_substitution - | CGeneralization of Loc.t * binding_kind * abstraction_kind option * constr_expr - | CPrim of Loc.t * prim_token - | CDelimiters of Loc.t * string * constr_expr + | CCases of case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + + | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) * + constr_expr * constr_expr + | CIf of constr_expr * (Name.t Loc.located 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 + | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of glob_sort + | CCast of constr_expr * constr_expr cast_type + | CNotation of notation * constr_notation_substitution + | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CPrim of prim_token + | CDelimiters of string * constr_expr +and constr_expr = constr_expr_r CAst.ast and case_expr = constr_expr (* expression that is being matched *) - * Name.t located option (* as-clause *) + * Name.t Loc.located option (* as-clause *) * cases_pattern_expr option (* in-clause *) and branch_expr = - Loc.t * cases_pattern_expr list located list * constr_expr + (cases_pattern_expr list Loc.located list * constr_expr) Loc.located and binder_expr = - Name.t located list * binder_kind * constr_expr + Name.t Loc.located list * binder_kind * constr_expr and fix_expr = - Id.t located * (Id.t located option * recursion_order_expr) * + Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t located * local_binder_expr list * constr_expr * constr_expr + Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -115,16 +115,16 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | CLocalAssum of Name.t located list * binder_kind * constr_expr - | CLocalDef of Name.t located * constr_expr * constr_expr option - | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option + | 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 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 *) -type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr +type typeclass_constraint = (Name.t Loc.located * Id.t Loc.located list option) * binding_kind * constr_expr and typeclass_context = typeclass_constraint list @@ -133,10 +133,11 @@ type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) type with_declaration_ast = - | CWith_Module of Id.t list located * qualid located - | CWith_Definition of Id.t list located * constr_expr - -type module_ast = - | CMident of qualid located - | CMapply of Loc.t * module_ast * module_ast - | CMwith of Loc.t * module_ast * with_declaration_ast + | CWith_Module of Id.t list Loc.located * qualid Loc.located + | CWith_Definition of Id.t list Loc.located * constr_expr + +type module_ast_r = + | CMident of qualid + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast +and module_ast = module_ast_r CAst.ast |