Module Constrexpr

Concrete syntax for terms
type sort_name_expr =
| CSProp
| CProp
| CSet
| CType of Libnames.qualid
| CRawType of Univ.Level.t

Universes like "foo.1" have no qualid form

Universes

type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen
type qvar_expr =
| CQVar of Libnames.qualid
| CQAnon of Loc.t option
| CRawQVar of Sorts.QVar.t
type quality_expr =
| CQConstant of Sorts.Quality.constant
| CQualVar of qvar_expr
type sort_expr = (qvar_expr option * (sort_name_expr * int) list) Glob_term.glob_sort_gen
type instance_expr = quality_expr list * univ_level_expr list
type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr

Constraints don't have anonymous universes

type universe_decl_expr = (Names.lident list, Names.lident list, univ_constraint_expr list) UState.gen_universe_decl
type cumul_univ_decl_expr = (Names.lident list, (Names.lident * UVars.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
type ident_decl = Names.lident * universe_decl_expr option
type cumul_ident_decl = Names.lident * cumul_univ_decl_expr option
type name_decl = Names.lname * universe_decl_expr option
type notation_with_optional_scope =
| LastLonelyNotation
| NotationInScope of string
type side =
| Left
| Right
type entry_level = int
type entry_relative_level =
| LevelLt of entry_level
| LevelLe of entry_level
| LevelSome
type notation_entry =
| InConstrEntry
| InCustomEntry of string
type notation_entry_level = {
notation_entry : notation_entry;
notation_level : entry_level;
}
type notation_entry_relative_level = {
notation_subentry : notation_entry;
notation_relative_level : entry_relative_level;
notation_position : side option;
}
type notation_key = string
type notation = notation_entry * notation_key
type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
type 'a or_by_notation_r =
| AN of 'a
| ByNotation of string * string option
type 'a or_by_notation = 'a or_by_notation_r CAst.t
type explicitation =
| ExplByName of Names.Id.t
| ExplByPos of int
type binder_kind =
| Default of Glob_term.binding_kind
| Generalized of Glob_term.binding_kind * bool

(Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses

type explicit_flag = bool

true = with "@"

type delimiter_depth =
| DelimOnlyTmpScope
| DelimUnboundedScope

shallow (%_) vs. deep (%) scope opening

type prim_token =
| Number of NumTok.Signed.t
| String of string
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * Names.lname
| CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list

CPatCstr (_, c, Some l1, l2) represents (@ c l1) l2

| CPatAtom of Libnames.qualid option
| CPatOr of cases_pattern_expr list
| CPatNotation of notation_with_optional_scope option * 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 prim_token
| CPatRecord of (Libnames.qualid * cases_pattern_expr) list
| CPatDelimiters of delimiter_depth * string * cases_pattern_expr
| CPatCast of cases_pattern_expr * constr_expr

constr_expr is the abstract syntax tree produced by the parser

and cases_pattern_expr = cases_pattern_expr_r CAst.t
and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
and cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list * kinded_cases_pattern_expr list
and constr_expr_r =
| CRef of Libnames.qualid * instance_expr option
| CFix of Names.lident * fix_expr list
| CCoFix of Names.lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
| CAppExpl of Libnames.qualid * instance_expr option * constr_expr list
| CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
| CProj of explicit_flag * Libnames.qualid * instance_expr option * (constr_expr * explicitation CAst.t option) list * constr_expr
| CRecord of (Libnames.qualid * constr_expr) list
| CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
| CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
| CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
| CHole of Evar_kinds.glob_evar_kind option
| CGenarg of Genarg.raw_generic_argument
| CGenargGlob of Genarg.glob_generic_argument
| CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name CAst.t * (Names.lident * constr_expr) list
| CSort of sort_expr
| CCast of constr_expr * Constr.cast_kind option * constr_expr
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * constr_expr
| CPrim of prim_token
| CDelimiters of delimiter_depth * string * constr_expr
| CArray of instance_expr option * constr_expr array * constr_expr * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr * Names.lname option * cases_pattern_expr option
and branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr = Names.lident * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr
and cofix_expr = Names.lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr_r =
| CStructRec of Names.lident
| CWfRec of Names.lident * constr_expr
| CMeasureRec of Names.lident option * constr_expr * constr_expr option

argument, measure, relation

and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
| CLocalAssum of Names.lname list * binder_kind * constr_expr
| CLocalDef of Names.lname * constr_expr * constr_expr option
| CLocalPattern of cases_pattern_expr
and constr_notation_substitution = constr_expr list * constr_expr list list * kinded_cases_pattern_expr list * local_binder_expr list list
type constr_pattern_expr = constr_expr
type with_declaration_ast =
| CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
| CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
| CMident of Libnames.qualid
| CMapply of module_ast * Libnames.qualid
| CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t