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

Concrete syntax for modules and module types

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Constrexpr/index.html

Module `Constrexpr`

Concrete syntax for terms

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Constrexpr/index.html

Module Constrexpr

Concrete syntax for terms

Module `Constrexpr`