source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.PP.M (α : Type) :
Type
Equations

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

Instances For

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

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

Instances For

source
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 })

Instances For

source
def Lean.Compiler.LCNF.PP.ppArg (e : Arg) :
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

Instances For

source
def Lean.Compiler.LCNF.PP.ppArgs (args : Array Arg) :
M Format
Equations

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

Instances For

source
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))

Instances For

source
def Lean.Compiler.LCNF.PP.ppLetValue (e : LetValue) :
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

Instances For

source
def Lean.Compiler.LCNF.PP.ppParam (param : Param) :
M Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.PP.ppParams (params : Array Param) :
M Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.PP.ppLetDecl (letDecl : LetDecl) :
M Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.PP.getFunType (ps : Array Param) (type : Expr) :
CoreM Expr
Equations

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

Instances For

source
partial def Lean.Compiler.LCNF.PP.ppFunDecl (funDecl : FunDecl) :
M Format
source
partial def Lean.Compiler.LCNF.PP.ppAlt (alt : Alt) :
M Format
source
partial def Lean.Compiler.LCNF.PP.ppCode (c : Code) :
M Format
source
def Lean.Compiler.LCNF.PP.ppDeclValue (b : DeclValue) :
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")

Instances For

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

- Lean.Compiler.LCNF.PP.run x = Lean.withOptions (fun (x : Lean.Options) => Lean.Option.set x Lean.pp.sanitizeNames false) do let __do_lift ← get ReaderT.run x __do_lift.lctx.toLocalContext

Instances For

source
def Lean.Compiler.LCNF.ppCode (code : Code) :
CompilerM Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.ppLetValue (e : LetValue) :
CompilerM Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.ppDecl (decl : Decl) :
CompilerM Format
Equations

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

Instances For

source
def Lean.Compiler.LCNF.ppFunDecl (decl : FunDecl) :
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)

Instances For

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

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

Equations

- Lean.Compiler.LCNF.runCompilerWithoutModifyingState x = do let s ← get tryFinally x.run (set s)

Instances For

source
def Lean.Compiler.LCNF.ppDecl' (decl : Decl) :
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 = Lean.Compiler.LCNF.runCompilerWithoutModifyingState do let __do_lift ← decl.internalize Lean.Compiler.LCNF.ppDecl __do_lift

Instances For

source
def Lean.Compiler.LCNF.ppCode' (code : Code) :
CoreM Format

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

Equations

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

Instances For