@[reducible, inline]

abbrev Lean.Compiler.LCNF.PP.M (α : Type) : Type

Equations

• Lean.Compiler.LCNF.PP.M = ReaderT Lean.LocalContext Lean.Compiler.LCNF.CompilerM

def Lean.Compiler.LCNF.PP.ppFVar (fvarId : FVarId) : M Format

Equations

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

def Lean.Compiler.LCNF.PP.ppExpr (e : Expr) : M Format

Equations

• Lean.Compiler.LCNF.PP.ppExpr e = do let __do_lift ← read liftM ((Lean.Meta.ppExpr e).run' { lctx := __do_lift })

def Lean.Compiler.LCNF.PP.ppArg {pu : Purity} (e : Arg pu) : M Format

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PP.ppArg Lean.Compiler.LCNF.Arg.erased = pure (Std.Format.text "◾")
• Lean.Compiler.LCNF.PP.ppArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.PP.ppFVar fvarId

def Lean.Compiler.LCNF.PP.ppArgs {pu : Purity} (args : Array (Arg pu)) : M Format

Equations

• Lean.Compiler.LCNF.PP.ppArgs args = Lean.Compiler.LCNF.PP.prefixJoin✝ (Std.Format.text " ") args Lean.Compiler.LCNF.PP.ppArg

def Lean.Compiler.LCNF.PP.ppLitValue (lit : LitValue) : M Format

Equations

• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.nat v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.uint8 v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.uint16 v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.uint32 v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.uint64 v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.usize v) = pure (Std.format v)
• Lean.Compiler.LCNF.PP.ppLitValue (Lean.Compiler.LCNF.LitValue.str v) = pure (Std.format (repr v))

@[instance_reducible]

instance Lean.Compiler.LCNF.PP.instToFormatCtorInfo : ToFormat CtorInfo

Equations

• Lean.Compiler.LCNF.PP.instToFormatCtorInfo = { format := Lean.Compiler.LCNF.PP.instToFormatCtorInfo._private_1 }

def Lean.Compiler.LCNF.PP.ppLetValue {pu : Purity} (e : LetValue pu) : M Format

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PP.ppLetValue Lean.Compiler.LCNF.LetValue.erased = pure (Std.Format.text "◾")
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.lit v) = Lean.Compiler.LCNF.PP.ppLitValue v
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.ctor i args h) = do let __do_lift ← Lean.Compiler.LCNF.PP.ppArgs args pure (Std.format i ++ Std.format " " ++ Std.format __do_lift)
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.fap declName args h) = do let __do_lift ← Lean.Compiler.LCNF.PP.ppArgs args pure (Std.format declName ++ Std.format __do_lift)
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.box ty fvarId h) = do let __do_lift ← Lean.Compiler.LCNF.PP.ppFVar fvarId pure (Std.format "box " ++ Std.format __do_lift)
• Lean.Compiler.LCNF.PP.ppLetValue (Lean.Compiler.LCNF.LetValue.unbox fvarId h) = do let __do_lift ← Lean.Compiler.LCNF.PP.ppFVar fvarId pure (Std.format "unbox " ++ Std.format __do_lift)

def Lean.Compiler.LCNF.PP.ppParam {pu : Purity} (param : Param pu) : M Format

Equations

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

def Lean.Compiler.LCNF.PP.ppParams {pu : Purity} (params : Array (Param pu)) : M Format

Equations

• Lean.Compiler.LCNF.PP.ppParams params = Lean.Compiler.LCNF.PP.prefixJoin✝ (Std.Format.text " ") params Lean.Compiler.LCNF.PP.ppParam

def Lean.Compiler.LCNF.PP.ppLetDecl {pu : Purity} (letDecl : LetDecl pu) : M Format

Equations

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

def Lean.Compiler.LCNF.PP.getFunType {pu : Purity} (ps : Array (Param pu)) (type : Expr) : CoreM Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.PP.getFunType ps_2 type = if type.isErased = true then pure type else pure type

partial def Lean.Compiler.LCNF.PP.ppFunDecl {pu : Purity} (funDecl : FunDecl pu) : M Format

partial def Lean.Compiler.LCNF.PP.ppAlt {pu : Purity} (alt : Alt pu) : M Format

partial def Lean.Compiler.LCNF.PP.ppCode {pu : Purity} (c : Code pu) : M Format

def Lean.Compiler.LCNF.PP.ppDeclValue {pu : Purity} (b : DeclValue pu) : M Format

Equations

• Lean.Compiler.LCNF.PP.ppDeclValue (Lean.Compiler.LCNF.DeclValue.code c) = Lean.Compiler.LCNF.PP.ppCode c
• Lean.Compiler.LCNF.PP.ppDeclValue (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure (Std.Format.text "extern")

def Lean.Compiler.LCNF.PP.run {α : Type} (x : M α) : CompilerM α

Equations

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

def Lean.Compiler.LCNF.ppCode {pu : Purity} (code : Code pu) : CompilerM Format

Equations

• Lean.Compiler.LCNF.ppCode code = Lean.Compiler.LCNF.PP.run (Lean.Compiler.LCNF.PP.ppCode code)

def Lean.Compiler.LCNF.ppLetValue {pu : Purity} (e : LetValue pu) : CompilerM Format

Equations

• Lean.Compiler.LCNF.ppLetValue e = Lean.Compiler.LCNF.PP.run (Lean.Compiler.LCNF.PP.ppLetValue e)

def Lean.Compiler.LCNF.ppDecl {pu : Purity} (decl : Decl pu) : CompilerM Format

Equations

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

def Lean.Compiler.LCNF.ppFunDecl {pu : Purity} (decl : FunDecl pu) : CompilerM Format

Equations

• Lean.Compiler.LCNF.ppFunDecl decl = Lean.Compiler.LCNF.PP.run do let __do_lift ← Lean.Compiler.LCNF.PP.ppFunDecl decl pure (Std.format "fun " ++ Std.format __do_lift)

def Lean.Compiler.LCNF.runCompilerWithoutModifyingState {α : Type} (phase : Phase) (x : CompilerM α) : CoreM α

Execute x in CoreM without modifying Cores state. This is useful if we want make sure we do not affect the next free variable id.

Equations

• Lean.Compiler.LCNF.runCompilerWithoutModifyingState phase x = do let s ← get tryFinally (x.run { } phase) (set s)

def Lean.Compiler.LCNF.ppDecl' {pu : Purity} (decl : Decl pu) (phase : Phase) : CoreM Format

Similar to ppDecl, but in CoreM, and it does not assume decl has already been internalized. This function is used for debugging purposes.

Equations

• Lean.Compiler.LCNF.ppDecl' decl phase = Lean.Compiler.LCNF.runCompilerWithoutModifyingState phase do let __do_lift ← decl.internalize Lean.Compiler.LCNF.ppDecl __do_lift

def Lean.Compiler.LCNF.ppCode' {pu : Purity} (code : Code pu) (phase : Phase) : CoreM Format

Similar to ppCode, but in CoreM, and it does not assume code has already been internalized.

Equations

• Lean.Compiler.LCNF.ppCode' code phase = Lean.Compiler.LCNF.runCompilerWithoutModifyingState phase do let __do_lift ← code.internalize Lean.Compiler.LCNF.ppCode __do_lift