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 sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
type instance_expr = 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, univ_constraint_expr list) UState.gen_universe_decl
type cumul_univ_decl_expr = ((Names.lident * Univ.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 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 =
| InConstrEntrySomeLevel
| InCustomEntryLevel of string * entry_level
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 =
| ExplByPos of int * Names.Id.t option
| ExplByName of Names.Id.t
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 abstraction_kind =
| AbsLambda
| AbsPi
type proj_flag = int option

Some n = proj of the n-th visible argument

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 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
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 proj_flag * Libnames.qualid * instance_expr option * constr_expr list
| CApp of proj_flag * constr_expr * (constr_expr * explicitation CAst.t option) list
| 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.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| 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_expr Glob_term.cast_type
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of 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 * module_ast
| CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t