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

- ctor (val : ConstructorVal) (args : Array Arg) : CtorInfo
- natVal (n : Nat) : CtorInfo

  Natural numbers are morally constructor applications

Instances For

source
def Lean.Compiler.LCNF.Simp.CtorInfo.getName :
CtorInfo → Name
Equations

- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getName = val.name
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal 0).getName = `Nat.zero
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getName = `Nat.succ

Instances For

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

- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getNumParams = val.numParams
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getNumParams = 0

Instances For

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

- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getNumFields = val.numFields
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal 0).getNumFields = 0
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getNumFields = 1

Instances For

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.

Instances For

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

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

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

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

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

Instances For

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.

Instances For