Struct ProductEtaExpander 

struct ProductEtaExpander<'a> {
    current_path: Expr,
    expr_to_eta_expansion: &'a mut UnordMap<Expr, Expr>,
}

Fields

current_path: Expr

expr_to_eta_expansion: &'a mut UnordMap<Expr, Expr>

Implementations

impl<'a> ProductEtaExpander<'a>

Recursively “unpacks” a product by eta-expanding each part of it. Maps each part of the product to its eta-expanded path.

e.g.

in = {
  current_path: self,
  expr: TwoFields { 0: (a0.0, a0.1), 1: 42 })
}

out =
  a0.0 => self.0.0
  a0.1 => self.0.1
  42 => self.1

fn eta_expand_products( current_path: Expr, expr: Expr, expr_to_eta_expansion: &'a mut UnordMap<Expr, Expr>, )

Trait Implementations

impl TypeVisitor for ProductEtaExpander<'_>

fn visit_expr(&mut self, expr: &Expr) -> ControlFlow<Self::BreakTy>

type BreakTy = !

fn enter_binder(&mut self, _vars: &Interned<[BoundVariableKind]>)

fn exit_binder(&mut self)

fn visit_sort(&mut self, sort: &Sort) -> ControlFlow<Self::BreakTy>

fn visit_ty(&mut self, ty: &Ty) -> ControlFlow<Self::BreakTy>

fn visit_bty(&mut self, bty: &BaseTy) -> ControlFlow<Self::BreakTy>