Module ast

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.
• ModelType
  A model of an SMT-LIB type.
• ModelValue
  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.
• SpecExpr
  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.
• TypeValue
  The actual type-value: a primitive or an enum with variants.