Module ast 

The core abstract syntax tree (AST) representation for hax.

This module defines the primary data structures used to represent typed syntax.

The design of this AST is designed under the following constraints:

1. Valid (cargo check) pretty-printed Rust can be produced out of it.
2. The Rust THIR AST from the frontend can be imported into this AST.
3. The AST defined in the OCaml engine can be imported into this AST.
4. This AST can be exported to the OCaml engine.
5. This AST should be suitable for AST transformations.

Re-exports

pub use identifiers::*;

pub use traits::*;

Modules

diagnostics

Diagnostic types used to represent and propagate errors (or warnings, notes, etc.) within the AST.

fragment

Enumeration types of any possible fragment of AST (Fragment / FragmentRef).

identifiers

Identifier types used throughout the AST.

literals

Literal and numeric type kinds used in constant expressions.

resugared

This module defines resugared fragments for the Hax Rust engine’s AST.

span

Source positions.

traits

Traits for utilities on AST data types

utils

This module provides a collection of utilities to work on AST.

visitors

Syntax tree traversals to walk a shared or mutable borrow of the syntax tree of Hax. The visitors are generated using the derive_generic_visitor library.

Structs

Arm

A pattern matching arm with metadata.

Attribute

Represents a single attribute.

DynTraitGoal

A dyn trait. The generic arguments are known but the actual type implementing the trait is known dynamically.

ErrorNode

Represent a node of the AST where an error occurred.

Expr

A typed expression with metadata.

GenericParam

A generic parameter (lifetime, type parameter or const parameter)

Generics

Generic parameters and constraints (contained between <> in function declarations)

Guard

A pattern matching arm guard with metadata.

ImplExpr

An ImplExpr describes the full data of a trait implementation. Because of generics, this may need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the concrete implementations for u8 and &str, represented as a tree.

ImplIdent

Represents a trait bound in a generic constraint

ImplItem

Represents an impl item (associated type or function)

Item

A top-level item with metadata.

ItemQuoteOrigin

The origin of a quote item.

LoopState

Represent explicit mutation context for a loop. This is useful to make loops pure.

Metadata

Extra information attached to syntax nodes.

Module

A “flat” module: this contains only non-module items.

Param

A function or closure parameter.

Pat

A typed pattern with metadata.

ProjectionPredicate

A projection predicate expresses a constraint over an associated type:

Quote

Represents an inlined piece of backend code

Region

Represent a Rust lifetime region.

SpannedTy

A type with its associated span.

TraitGoal

Represents an instantiated trait that needs to be implemented.

TraitItem

Represents a trait item (associated type, fn, or default)

Ty

A indirection for the representation of types.

Variant

A variant of an enum or struct. In our representation structs always have one variant with an argument for each field.

Enums

AttributeKind

Represents the kind of an attribute.

BindingMode

Binding modes used in patterns.

BorrowKind

Represents different levels of borrowing.

ControlFlowKind

This is a marker to describe what control flow is present in a loop. It is added by phase DropReturnBreakContinue and the information is used in FunctionalizeLoops. We need it to replace the control flow nodes of the AST by an encoding in the ControlFlow enum.

DocCommentKind

Represents the kind of a doc comment.

ExprKind

Describes the shape of an expression.

GenericConstraint

A generic constraint (lifetime, type-class or equality)

GenericParamKind

Represents the kinds of generic parameters

GenericValue

Represents a generic value used in type applications (e.g., T in Vec<T>).

GuardKind

Represents the various kinds of pattern guards.

ImplExprKind

Represents all the kinds of impl expr.

ImplItemKind

Represents the kinds of impl items

ItemKind

A top-level item in the module.

ItemQuoteOriginKind

The kind of a quote item’s origin

ItemQuoteOriginPosition

The position of a quote item relative to its origin

Lhs

The left-hand side of an assignment.

LoopKind

The kind of a loop (resugared by respective Reconstruct...Loops phases). Useful for FunctionalizeLoops.

PatKind

Represents the various kinds of patterns.

PrimitiveTy

Built-in primitive types.

QuoteContent

A QuoteContent is a component of a quote: it can be a verbatim string, a Rust expression to embed in the quote, a pattern etc.

SafetyKind

Safety level of a function.

TraitItemKind

Represents the kinds of trait items

TyKind

Describes any Rust type (e.g., i32, Vec<T>, fn(i32) -> bool).

Type Aliases

Attributes

A list of attributes.