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 let fvarId₂ : Lean.FVarId := (Lean.RBMap.find? __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 (a₁ a₂ : Arg) : EqvM Bool

Equations

• Lean.Compiler.LCNF.AlphaEqv.eqvArg (Lean.Compiler.LCNF.Arg.type e₁) (Lean.Compiler.LCNF.Arg.type e₂) = 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 (as₁ as₂ : Array Arg) : EqvM Bool

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.AlphaEqv.eqvLetValue (Lean.Compiler.LCNF.LetValue.value v₁) (Lean.Compiler.LCNF.LetValue.value 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 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 (params₁ params₂ : Array Param) (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

@[irreducible, specialize #[]]

def Lean.Compiler.LCNF.AlphaEqv.withParams.go (params₁ params₂ : Array Param) (x : EqvM Bool) (h : params₂.size = params₁.size) (i : Nat) : EqvM Bool

Equations

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

def Lean.Compiler.LCNF.AlphaEqv.sortAlts (alts : Array Alt) : Array Alt

Equations

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

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

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

def Lean.Compiler.LCNF.Code.alphaEqv (c₁ c₂ : Code) : Bool

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

Equations

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