inductive Lean.Compiler.LCNF.Simp.CtorInfo : Type

• ctor: Lean.ConstructorVal → Array Lean.Compiler.LCNF.Arg → Lean.Compiler.LCNF.Simp.CtorInfo
• natVal: Nat → Lean.Compiler.LCNF.Simp.CtorInfo

  Natural numbers are morally constructor applications

def Lean.Compiler.LCNF.Simp.CtorInfo.getName : Lean.Compiler.LCNF.Simp.CtorInfo → Lake.Name

Equations

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

def Lean.Compiler.LCNF.Simp.CtorInfo.getNumParams : Lean.Compiler.LCNF.Simp.CtorInfo → Nat

Equations

• Lean.Compiler.LCNF.Simp.CtorInfo.getNumParams x = match x with | Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args => val.numParams | Lean.Compiler.LCNF.Simp.CtorInfo.natVal n => 0

def Lean.Compiler.LCNF.Simp.CtorInfo.getNumFields : Lean.Compiler.LCNF.Simp.CtorInfo → Nat

Equations

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

structure Lean.Compiler.LCNF.Simp.DiscrM.Context : Type

• discrCtorMap : Lean.FVarIdMap Lean.Compiler.LCNF.Simp.CtorInfo

  A mapping from discriminant to constructor application it is equal to in the current context.

• ctorDiscrMap : Lean.PersistentExprMap Lean.FVarId

  A mapping from constructor application to discriminant it is equal to in the current context.

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Simp.DiscrM (α : Type) : Type

Helper monad for tracking mappings from discriminant to constructor applications and back. The combinator withDiscrCtor should be used when visiting cases alternatives.

Equations

• Lean.Compiler.LCNF.Simp.DiscrM = ReaderT Lean.Compiler.LCNF.Simp.DiscrM.Context Lean.Compiler.LCNF.CompilerM

def Lean.Compiler.LCNF.Simp.findCtor? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.DiscrM (Option Lean.Compiler.LCNF.Simp.CtorInfo)

If fvarId is a constructor application, returns constructor information. Remark: we use the map discrCtorMap. Remark: We use this method when simplifying projections and cases-constructor.

Equations

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

def Lean.Compiler.LCNF.Simp.findCtorName? (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.Simp.DiscrM (Option Lake.Name)

Equations

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

def Lean.Compiler.LCNF.Simp.getIndInfo? (type : Lean.Expr) : Lean.CoreM (Option (List Lean.Level × Array Lean.Compiler.LCNF.Arg))

If type is an inductive datatype, return its universe levels and parameters.

Equations

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

@[inline]

def Lean.Compiler.LCNF.Simp.withDiscrCtorImp {α : Type} (discr : Lean.FVarId) (ctorName : Lake.Name) (ctorFields : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.Simp.DiscrM α) : Lean.Compiler.LCNF.Simp.DiscrM α

Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

Equations

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

def Lean.Compiler.LCNF.Simp.withDiscrCtorImp.updateCtx (discr : Lean.FVarId) (ctorName : Lake.Name) (ctorFields : Array Lean.Compiler.LCNF.Param) : Lean.Compiler.LCNF.Simp.DiscrM Lean.Compiler.LCNF.Simp.DiscrM.Context

Equations

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

@[inline]

def Lean.Compiler.LCNF.Simp.withDiscrCtor {m : Type → Type u_1} {α : Type} [MonadFunctorT Lean.Compiler.LCNF.Simp.DiscrM m] (discr : Lean.FVarId) (ctorName : Lake.Name) (ctorFields : Array Lean.Compiler.LCNF.Param) : m α → m α

Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

Equations

• Lean.Compiler.LCNF.Simp.withDiscrCtor discr ctorName ctorFields = monadMap fun {β : Type} => Lean.Compiler.LCNF.Simp.withDiscrCtorImp discr ctorName ctorFields

def Lean.Compiler.LCNF.Simp.simpCtorDiscrCore? (e : Lean.Expr) : Lean.Compiler.LCNF.Simp.DiscrM (Option Lean.FVarId)

Equations

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