Alpha equivalence for LCNF Code

@[reducible, inline]

abbrev Lean.Compiler.LCNF.AlphaEqv.EqvM (α : Type) : Type

Equations

• Lean.Compiler.LCNF.AlphaEqv.EqvM = ReaderM (Lean.FVarIdMap Lean.FVarId)

def Lean.Compiler.LCNF.AlphaEqv.eqvFVar (fvarId₁ fvarId₂ : FVarId) : EqvM Bool

Equations

• Lean.Compiler.LCNF.AlphaEqv.eqvFVar fvarId₁ fvarId₂ = do let __do_lift ← read have fvarId₂ : Lean.FVarId := (Std.TreeMap.get? __do_lift fvarId₂).getD fvarId₂ pure (fvarId₁ == fvarId₂)

def Lean.Compiler.LCNF.AlphaEqv.eqvType (e₁ e₂ : Expr) : EqvM Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.AlphaEqv.eqvType (f₁.app a₁) (f₂.app a₂) = (Lean.Compiler.LCNF.AlphaEqv.eqvType a₁ a₂ <&&> Lean.Compiler.LCNF.AlphaEqv.eqvType f₁ f₂)
• Lean.Compiler.LCNF.AlphaEqv.eqvType (Lean.Expr.fvar fvarId₁) (Lean.Expr.fvar fvarId₂) = Lean.Compiler.LCNF.AlphaEqv.eqvFVar fvarId₁ fvarId₂
• Lean.Compiler.LCNF.AlphaEqv.eqvType e₁ e₂ = pure (e₁ == e₂)

def Lean.Compiler.LCNF.AlphaEqv.eqvTypes (es₁ es₂ : Array Expr) : EqvM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.AlphaEqv.eqvArg {pu : Purity} (a₁ a₂ : Arg pu) : EqvM Bool

Equations

• Lean.Compiler.LCNF.AlphaEqv.eqvArg (Lean.Compiler.LCNF.Arg.type e₁ h) (Lean.Compiler.LCNF.Arg.type e₂ h_1) = Lean.Compiler.LCNF.AlphaEqv.eqvType e₁ e₂
• Lean.Compiler.LCNF.AlphaEqv.eqvArg (Lean.Compiler.LCNF.Arg.fvar x₁) (Lean.Compiler.LCNF.Arg.fvar x₂) = Lean.Compiler.LCNF.AlphaEqv.eqvFVar x₁ x₂
• Lean.Compiler.LCNF.AlphaEqv.eqvArg Lean.Compiler.LCNF.Arg.erased Lean.Compiler.LCNF.Arg.erased = pure true
• Lean.Compiler.LCNF.AlphaEqv.eqvArg a₁ a₂ = pure false

def Lean.Compiler.LCNF.AlphaEqv.eqvArgs {pu : Purity} (as₁ as₂ : Array (Arg pu)) : EqvM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.AlphaEqv.eqvLetValue {pu : Purity} (e₁ e₂ : LetValue pu) : EqvM Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.AlphaEqv.eqvLetValue (Lean.Compiler.LCNF.LetValue.lit v₁) (Lean.Compiler.LCNF.LetValue.lit v₂) = pure (v₁ == v₂)
• Lean.Compiler.LCNF.AlphaEqv.eqvLetValue Lean.Compiler.LCNF.LetValue.erased Lean.Compiler.LCNF.LetValue.erased = pure true
• Lean.Compiler.LCNF.AlphaEqv.eqvLetValue (Lean.Compiler.LCNF.LetValue.unbox v₁ h) (Lean.Compiler.LCNF.LetValue.unbox v₂ h_1) = Lean.Compiler.LCNF.AlphaEqv.eqvFVar v₁ v₂
• Lean.Compiler.LCNF.AlphaEqv.eqvLetValue e₁ e₂ = pure false

@[inline]

def Lean.Compiler.LCNF.AlphaEqv.withFVar {α : Type} (fvarId₁ fvarId₂ : FVarId) (x : EqvM α) : EqvM α

Equations

• Lean.Compiler.LCNF.AlphaEqv.withFVar fvarId₁ fvarId₂ x = withReader (fun (x : Lean.FVarIdMap Lean.FVarId) => x.insert fvarId₂ fvarId₁) x

@[inline]

def Lean.Compiler.LCNF.AlphaEqv.withParams {pu : Purity} (params₁ params₂ : Array (Param pu)) (x : EqvM Bool) : EqvM Bool

Equations

• Lean.Compiler.LCNF.AlphaEqv.withParams params₁ params₂ x = if h : params₂.size = params₁.size then Lean.Compiler.LCNF.AlphaEqv.withParams.go✝ params₁ params₂ x h 0 else pure false

def Lean.Compiler.LCNF.AlphaEqv.sortAlts {pu : Purity} (alts : Array (Alt pu)) : Array (Alt pu)

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Compiler.LCNF.AlphaEqv.eqvAlts {pu : Purity} (alts₁ alts₂ : Array (Alt pu)) : EqvM Bool

partial def Lean.Compiler.LCNF.AlphaEqv.eqv {pu : Purity} (code₁ code₂ : Code pu) : EqvM Bool

def Lean.Compiler.LCNF.Code.alphaEqv {pu : Purity} (c₁ c₂ : Code pu) : Bool

Return true if c₁ and c₂ are alpha equivalent.

Equations

• c₁.alphaEqv c₂ = ReaderT.run (Lean.Compiler.LCNF.AlphaEqv.eqv c₁ c₂) ∅