charon_lib::ast

Module types

source

Modules§

  • vars 🔒
    Type-level variables. There are 4 kinds of variables at the type-level: regions, types, const generics and trait clauses. The relevant definitions are in this module.

Structs§

  • A value of type T bound by generic parameters. Used in any context where we’re adding generic parameters that aren’t on the top-level item, e.g. for<'a> clauses (uses RegionBinder for now), trait methods, GATs (TODO).
  • A stack of values corresponding to nested binders. Each binder introduces an entry in this stack, with the entry as index 0 being the innermost binder. This is indexed by DeBruijnIds. Most methods assume that the stack is non-empty and panic if not.
  • Additional information for closures. We mostly use it in micro-passes like [crate::update_closure_signature].
  • A const generic variable in a signature or binder.
  • The index of a binder, counting from the innermost. See DeBruijnVar for details.
  • A predicate of the form exists<T> where T: Trait.
  • A function signature.
  • A set of generic arguments.
  • Generic parameters for a declaration. We group the generics which come from the Rust compiler substitutions (the regions, types and const generics) as well as the trait clauses. The reason is that we consider that those are parameters that need to be filled. We group in a different place the predicates which are not trait clauses, because those enforce constraints but do not need to be filled with witnesses/instances.
  • .0 outlives .1
  • A value of type T bound by regions. We should use binder instead but this causes name clash issues in the derived ocaml visitors. TODO: merge with binder
  • A region variable in a signature or binder.
  • A trait predicate in a signature, of the form Type: Trait<Args>. This functions like a variable binder, to which variables of the form TraitRefKind::Clause can refer to.
  • A predicate of the form Type: Trait<Args>.
  • A reference to a tait impl, using the provided arguments.
  • A reference to a trait
  • A constraint over a trait associated type.
  • A type.
  • A type declaration.
  • A type variable in a signature or binder.

Enums§

Type Aliases§