Expand description
Abstract syntax tree (AST) created from parsed ISLE.
Structs§
- 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
- One field of an enum variant.
- 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)
- Rule
- Signature
- Spec
- A specification of the semantics of a term.
- Type
- A declaration of a type.
- Variant
- One variant of an enum type.
Enums§
- 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.
- 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.