Alpha equivalence for LCNF Code

@[inline, reducible]

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₁ : Lean.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 := Option.getD (Lean.RBMap.find? __do_lift fvarId₂) fvarId₂ pure (fvarId₁ == fvarId₂)

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

def Lean.Compiler.LCNF.AlphaEqv.eqvTypes (es₁ : Array Lean.Expr) (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₁ : Lean.Compiler.LCNF.Arg) (a₂ : 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.eqvArgs (as₁ : Array Lean.Compiler.LCNF.Arg) (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₁ : Lean.Compiler.LCNF.LetValue) (e₂ : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool

Equations

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

@[inline]

def Lean.Compiler.LCNF.AlphaEqv.withFVar {α : Type} (fvarId₁ : Lean.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) => Lean.FVarIdMap.insert x fvarId₂ fvarId₁) x

@[inline]

def Lean.Compiler.LCNF.AlphaEqv.withParams (params₁ : Array Lean.Compiler.LCNF.Param) (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 : Array.size params₂ = Array.size params₁ then Lean.Compiler.LCNF.AlphaEqv.withParams.go params₁ params₂ x h 0 else pure false

@[specialize #[]]

def Lean.Compiler.LCNF.AlphaEqv.withParams.go (params₁ : Array Lean.Compiler.LCNF.Param) (params₂ : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool) (h : Array.size params₂ = Array.size params₁) (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₁ : Array Lean.Compiler.LCNF.Alt) (alts₂ : Array Lean.Compiler.LCNF.Alt) : Lean.Compiler.LCNF.AlphaEqv.EqvM Bool

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

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

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

Equations

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