Documentation

Lean.Compiler.LCNF.Simp.DiscrM

source
inductive Lean.Compiler.LCNF.Simp.CtorInfo :
Type
source
def Lean.Compiler.LCNF.Simp.CtorInfo.getName :
CtorInfo → Name
Equations
source
def Lean.Compiler.LCNF.Simp.CtorInfo.getNumParams :
CtorInfo → Nat
Equations
source
def Lean.Compiler.LCNF.Simp.CtorInfo.getNumFields :
CtorInfo → Nat
Equations
source
structure Lean.Compiler.LCNF.Simp.DiscrM.Context :
Type
  • discrCtorMap : FVarIdMap CtorInfo

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

  • ctorDiscrMap : PersistentExprMap FVarId

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

source
@[reducible, inline]
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
source
def Lean.Compiler.LCNF.Simp.findCtor? (fvarId : FVarId) :
DiscrM (Option 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.
source
def Lean.Compiler.LCNF.Simp.findCtorName? (fvarId : FVarId) :
DiscrM (Option Name)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.Simp.getIndInfo? (type : Expr) :
CoreM (Option (List Level × Array 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.
source
@[inline]
def Lean.Compiler.LCNF.Simp.withDiscrCtorImp {α : Type} (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) (x : DiscrM α) :
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.
source
def Lean.Compiler.LCNF.Simp.withDiscrCtorImp.updateCtx (discr : FVarId) (ctorName : Name) (ctorFields : Array Param) :
DiscrM DiscrM.Context
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Compiler.LCNF.Simp.withDiscrCtor {m : Type → Type u_1} {α : Type} [MonadFunctorT DiscrM m] (discr : FVarId) (ctorName : Name) (ctorFields : Array 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
source
def Lean.Compiler.LCNF.Simp.simpCtorDiscrCore? (e : Expr) :
DiscrM (Option FVarId)
Equations
  • One or more equations did not get rendered due to their size.