package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.interp/Constrexpr/index.html

Module Constrexpr

Concrete syntax for terms
type sort_name_expr =
  1. | CSProp
  2. | CProp
  3. | CSet
  4. | CType of Libnames.qualid
  5. | CRawType of Univ.Level.t
    (*

    Universes like "foo.1" have no qualid form

    *)

Universes

type qvar_expr =
  1. | CQVar of Libnames.qualid
  2. | CQAnon of Loc.t option
  3. | CRawQVar of Sorts.QVar.t
type quality_expr =
  1. | CQConstant of Sorts.Quality.constant
  2. | CQualVar of qvar_expr
type relevance_expr =
  1. | CRelevant
  2. | CIrrelevant
  3. | CRelevanceVar of qvar_expr
type relevance_info_expr = relevance_expr option
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 =
  1. | LastLonelyNotation
  2. | NotationInScope of string
type side =
  1. | Left
  2. | Right
type entry_level = int
type entry_relative_level =
  1. | LevelLt of entry_level
  2. | LevelLe of entry_level
  3. | LevelSome
type notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
type notation_entry_level = {
  1. notation_entry : notation_entry;
  2. notation_level : entry_level;
}
type notation_entry_relative_level = {
  1. notation_subentry : notation_entry;
  2. notation_relative_level : entry_relative_level;
  3. notation_position : side option;
}
type notation_key = string
type notation = notation_entry * notation_key
type 'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
type 'a or_by_notation = 'a or_by_notation_r CAst.t
type explicitation =
  1. | ExplByName of Names.Id.t
  2. | ExplByPos of int
type binder_kind =
  1. | Default of Glob_term.binding_kind
  2. | 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 =
  1. | DelimOnlyTmpScope
  2. | DelimUnboundedScope
    (*

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

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

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

    *)
  3. | CPatAtom of Libnames.qualid option
  4. | CPatOr of cases_pattern_expr list
  5. | 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

    *)
  6. | CPatPrim of prim_token
  7. | CPatRecord of (Libnames.qualid * cases_pattern_expr) list
  8. | CPatDelimiters of delimiter_depth * string * cases_pattern_expr
  9. | 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 =
  1. | CRef of Libnames.qualid * instance_expr option
  2. | CFix of Names.lident * fix_expr list
  3. | CCoFix of Names.lident * cofix_expr list
  4. | CProdN of local_binder_expr list * constr_expr
  5. | CLambdaN of local_binder_expr list * constr_expr
  6. | CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
  7. | CAppExpl of Libnames.qualid * instance_expr option * constr_expr list
  8. | CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
  9. | CProj of explicit_flag * Libnames.qualid * instance_expr option * (constr_expr * explicitation CAst.t option) list * constr_expr
  10. | CRecord of (Libnames.qualid * constr_expr) list
  11. | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
  12. | CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
  13. | CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
  14. | CHole of Evar_kinds.glob_evar_kind option
  15. | CGenarg of Genarg.raw_generic_argument
  16. | CGenargGlob of Genarg.glob_generic_argument
  17. | CPatVar of Pattern.patvar
  18. | CEvar of Glob_term.existential_name CAst.t * (Names.lident * constr_expr) list
  19. | CSort of sort_expr
  20. | CCast of constr_expr * Constr.cast_kind option * constr_expr
  21. | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
  22. | CGeneralization of Glob_term.binding_kind * constr_expr
  23. | CPrim of prim_token
  24. | CDelimiters of delimiter_depth * string * constr_expr
  25. | 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 fixpoint_order_expr_r =
  1. | CStructRec of Names.lident
  2. | CWfRec of Names.lident * constr_expr
  3. | CMeasureRec of Names.lident option * constr_expr * constr_expr option
    (*

    argument, measure, relation

    *)
and fixpoint_order_expr = fixpoint_order_expr_r CAst.t
and local_binder_expr =
  1. | CLocalAssum of Names.lname list * relevance_info_expr * binder_kind * constr_expr
  2. | CLocalDef of Names.lname * relevance_info_expr * constr_expr * constr_expr option
  3. | 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 =
  1. | CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
  2. | CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
type module_ast_r =
  1. | CMident of Libnames.qualid
  2. | CMapply of module_ast * Libnames.qualid
  3. | CMwith of module_ast * with_declaration_ast
and module_ast = module_ast_r CAst.t