Expand description
Abstract syntax tree (AST) created from parsed ISLE.
Structs§
- Arm
- Arm of a spec match expression.
- Attr
- An attribute applied to a declaration.
- Converter
- An implicit converter: the given term, which must have type (inner_ty) -> outer_ty, is used either in extractor or constructor position as appropriate when a type mismatch with the given pair of types would otherwise occur.
- Decl
- A declaration of a term with its argument and return types.
- Extractor
- An extractor macro: (A x y) becomes (B x _ y …). Expanded during ast-to-sema pass.
- Field
Init - Field initializer in a struct constructor.
- Form
- Ident
- An identifier – a variable, term symbol, or type.
- IfLet
- Instantiation
- LetDef
- One variable locally bound in a
(let ...)expression. - Model
- A model of a construct into SMT-LIB (currently, types or enums)
- Model
Field - Modifies
- State modification clause.
- Rule
- Signature
- Spec
- A specification of the semantics of a term.
- Spec
Macro - State
- Declare an element of global state accessible by verification specs.
- Struct
Field - One named field of a struct or enum variant.
- Struct
Fields - A List of named fields of a struct.
- Tuple
Field - One unnamed field of a tuple.
- Tuple
Fields - A List of unnamed fields of a tuple.
- Type
- A declaration of a type.
- Variant
- One variant of an enum type.
Enums§
- Attr
Kind - A kind of attribute that can be applied to a term declaration or rule.
- Attr
Target - Object an attribute applies to.
- Def
- One toplevel form in an ISLE file.
- Expr
- An expression: the right-hand side of a rule.
- Extern
- An external binding: an extractor or constructor function attached to a term.
- Fields
- The fields of a struct or enum variant, formatted as a struct or tuple.
- Model
Type - A model of an SMT-LIB type.
- Model
Value - A construct’s value in SMT-LIB
- Pattern
- A pattern: the left-hand side of a rule.
- Pragma
- Pragmas parsed with the
(pragma <ident>)syntax. - Spec
Expr - An expression used to specify term semantics, similar to SMT-LIB syntax.
- SpecOp
- An operation used to specify term semantics, similar to SMT-LIB syntax.
- Type
Value - The actual type-value: a primitive or an enum with variants.