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₂ : Lean.FVarId) : Lean.Compiler.LCNF.AlphaEqv.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₂ : Lean.Expr) : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool

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

Equations

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

def Lean.Compiler.LCNF.AlphaEqv.eqvArg (a₁ a₂ : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.AlphaEqv.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 Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool

Equations

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

def Lean.Compiler.LCNF.AlphaEqv.eqvLetValue (e₁ e₂ : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.AlphaEqv.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₂ : Lean.FVarId) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM α) : Lean.Compiler.LCNF.AlphaEqv.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 Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool) : Lean.Compiler.LCNF.AlphaEqv.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 Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool) (h : params₂.size = params₁.size) (i : Nat) : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool

Equations

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

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

Equations

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

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

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

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

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

Equations

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