max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: split up the compiler SCC after lambda lifting (#12003)

Browse source 
This PR splits up the SCC that the compiler manages into (potentially)
multiple ones after
performing lambda lifting. This aids both the closed term extractor and
the elimDeadBranches pass as
they are both negatively influenced when more declarations than required
are within one SCC.
This commit is contained in:
Henrik Böving 2026-01-14 19:36:25 +01:00 • committed by GitHub
parent b994cb4497
commit dc70d0cc43
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
17 changed files with 358 additions and 303 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Compiler/LCNF.lean
View file

@ -45,3 +45,4 @@ public import Lean.Compiler.LCNF.LambdaLifting
public import Lean.Compiler.LCNF.ReduceArity
public import Lean.Compiler.LCNF.Probing
public import Lean.Compiler.LCNF.Irrelevant
public import Lean.Compiler.LCNF.SplitSCC

41
src/Lean/Compiler/LCNF/Check.lean
View file

@ -258,45 +258,4 @@ end Check
def Decl.check (decl : Decl) : CompilerM Unit := do
Check.run do decl.value.forCodeM (Check.checkFunDeclCore decl.name decl.params decl.type)
/--
Check whether every local declaration in the local context is used in one of given `decls`.
-/
partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
let (_, s) := visitDecls decls |>.run {}
let usesFVar (binderName : Name) (fvarId : FVarId) :=
unless s.contains fvarId do
throwError "LCNF local context contains unused local variable declaration `{binderName}`"
let lctx := (← get).lctx
lctx.params.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.letDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
lctx.funDecls.forM fun fvarId decl => usesFVar decl.binderName fvarId
where
visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
modify (·.insert fvarId)
visitParam (param : Param) : StateM FVarIdHashSet Unit := do
visitFVar param.fvarId
visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
params.forM visitParam
visitCode (code : Code) : StateM FVarIdHashSet Unit := do
match code with
| .jmp .. | .return .. | .unreach .. => return ()
| .let decl k => visitFVar decl.fvarId; visitCode k
| .fun decl k | .jp decl k =>
visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
visitCode k
| .cases c => c.alts.forM fun alt => do
match alt with
| .default k => visitCode k
| .alt _ ps k => visitParams ps; visitCode k
visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
visitParams decl.params
decl.value.forCodeM visitCode
visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
decls.forM visitDecl
end Lean.Compiler.LCNF

51
src/Lean/Compiler/LCNF/Main.lean
View file

@ -11,6 +11,7 @@ public import Lean.Compiler.LCNF.Passes
public import Lean.Compiler.LCNF.ToDecl
public import Lean.Compiler.LCNF.Check
import Lean.Meta.Match.MatcherInfo
import Lean.Compiler.LCNF.SplitSCC
public section
namespace Lean.Compiler.LCNF
/--
@ -56,8 +57,6 @@ def checkpoint (stepName : Name) (decls : Array Decl) (shouldCheck : Bool) : Com
Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl' decl}"
if shouldCheck then
decl.check
if shouldCheck then
checkDeadLocalDecls decls
def isValidMainType (type : Expr) : Bool :=
let isValidResultName (name : Name) : Bool :=
@ -74,7 +73,7 @@ def isValidMainType (type : Expr) : Bool :=
namespace PassManager
def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRecDepth 8192 do
def run (declNames : Array Name) : CompilerM (Array (Array IR.Decl)) := withAtLeastMaxRecDepth 8192 do
/-
Note: we need to increase the recursion depth because we currently do to save phase1
declarations in .olean files. Then, we have to recursively compile all dependencies,
@ -100,31 +99,33 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
let decls := markRecDecls decls
let manager ← getPassManager
let isCheckEnabled := compiler.check.get (← getOptions)
let decls ← profileitM Exception "compilation (LCNF base)" (← getOptions) do
let mut decls := decls
for pass in manager.basePasses do
decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
let decls ← profileitM Exception "compilation (LCNF mono)" (← getOptions) do
let mut decls := decls
for pass in manager.monoPasses do
decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
if (← Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
let decl ← normalizeFVarIds decl
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
profileitM Exception "compilation (IR)" (← getOptions) do
let irDecls ← IR.toIR decls
IR.compile irDecls
let decls ← runPassManagerPart "compilation (LCNF base)" manager.basePasses decls isCheckEnabled
let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPasses decls isCheckEnabled
let sccs ← withTraceNode `Compiler.splitSCC (fun _ => return m!"Splitting up SCC") do
splitScc decls
sccs.mapM fun decls => do
let decls ← runPassManagerPart "compilation (LCNF mono)" manager.monoPassesNoLambda decls isCheckEnabled
if (← Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
let decl ← normalizeFVarIds decl
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
profileitM Exception "compilation (IR)" (← getOptions) do
let irDecls ← IR.toIR decls
IR.compile irDecls
where
runPassManagerPart (profilerName : String) (passes : Array Pass) (decls : Array Decl)
(isCheckEnabled : Bool) : CompilerM (Array Decl) := do
profileitM Exception profilerName (← getOptions) do
let mut decls := decls
for pass in passes do
decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
return decls
end PassManager
def compile (declNames : Array Name) : CoreM (Array IR.Decl) :=
def compile (declNames : Array Name) : CoreM (Array (Array IR.Decl)) :=
CompilerM.run <| PassManager.run declNames
def showDecl (phase : Phase) (declName : Name) : CoreM Format := do

2
src/Lean/Compiler/LCNF/PassManager.lean
View file

@ -87,6 +87,7 @@ pipeline.
structure PassManager where
basePasses : Array Pass
monoPasses : Array Pass
monoPassesNoLambda : Array Pass
deriving Inhabited
instance : ToString Phase where
@ -114,6 +115,7 @@ private def validatePasses (phase : Phase) (passes : Array Pass) : CoreM Unit :=
def validate (manager : PassManager) : CoreM Unit := do
validatePasses .base manager.basePasses
validatePasses .mono manager.monoPasses
validatePasses .mono manager.monoPassesNoLambda
def findOccurrenceBounds (targetName : Name) (passes : Array Pass) : CoreM (Nat × Nat) := do
let mut lowest := none

2
src/Lean/Compiler/LCNF/Passes.lean
View file

@ -115,6 +115,8 @@ def builtinPassManager : PassManager := {
simp (occurrence := 4) (phase := .mono),
floatLetIn (phase := .mono) (occurrence := 2),
lambdaLifting,
]
monoPassesNoLambda := #[
extendJoinPointContext (phase := .mono) (occurrence := 1),
simp (occurrence := 5) (phase := .mono),
elimDeadBranches,

50
src/Lean/Compiler/LCNF/SplitSCC.lean Normal file
View file

@ -0,0 +1,50 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
module
prelude
public import Lean.Compiler.LCNF.CompilerM
import Lean.Util.SCC
namespace Lean.Compiler.LCNF
namespace SplitScc
partial def findSccCalls (scc : Std.HashMap Name Decl) (decl : Decl) : BaseIO (Std.HashSet Name) := do
match decl.value with
| .code code =>
let (_, calls) ← goCode code |>.run {}
return calls
| .extern .. => return {}
where
goCode (c : Code) : StateRefT (Std.HashSet Name) BaseIO Unit := do
match c with
| .let decl k =>
if let .const name .. := decl.value then
if scc.contains name then
modify fun s => s.insert name
goCode k
| .fun decl k | .jp decl k =>
goCode decl.value
goCode k
| .cases cases => cases.alts.forM (·.forCodeM goCode)
| .jmp .. | .return .. | .unreach .. => return ()
end SplitScc
public def splitScc (scc : Array Decl) : CompilerM (Array (Array Decl)) := do
let declMap := Std.HashMap.ofArray <| scc.map fun decl => (decl.name, decl)
let callers := Std.HashMap.ofArray <| ← scc.mapM fun decl => do
let calls ← SplitScc.findSccCalls declMap decl
return (decl.name, calls.toList)
let newSccs := Lean.SCC.scc (scc.toList.map (·.name)) (callers.getD · [])
trace[Compiler.splitSCC] m!"Split SCC into {newSccs}"
return newSccs.toArray.map (fun scc => scc.toArray.map declMap.get!)
builtin_initialize
registerTraceClass `Compiler.splitSCC (inherited := true)
end Lean.Compiler.LCNF

7
tests/lean/4089.lean.expected.out
View file

@ -8,9 +8,6 @@
let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_3 x_2;
ret x_4
[Compiler.IR] [reset_reuse]
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) (x_3 : obj) : obj :=
let x_4 : obj := Sigma.toProd._redArg x_3;
ret x_4
def Sigma.toProd._redArg (x_1 : obj) : obj :=
case x_1 : obj of
Sigma.mk →
@ -19,6 +16,10 @@
let x_5 : tobj := reset[2] x_1;
let x_4 : obj := reuse x_5 in ctor_0[Prod.mk] x_2 x_3;
ret x_4
[Compiler.IR] [reset_reuse]
def Sigma.toProd (x_1 : ◾) (x_2 : ◾) (x_3 : obj) : obj :=
let x_4 : obj := Sigma.toProd._redArg x_3;
ret x_4
[Compiler.IR] [reset_reuse]
def foo (x_1 : tobj) : tobj :=
case x_1 : tobj of

23
tests/lean/4240.lean.expected.out
View file

@ -1,10 +1,4 @@
[Compiler.IR] [result]
def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
let x_2 : usize := 0;
let x_3 : tobj := Array.uget ◾ x_1 x_2 ◾;
let x_4 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_3;
dec x_3;
ret x_4
def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 (x_1 : @& tobj) : u8 :=
case x_1 : tobj of
MyOption.none →
@ -13,13 +7,20 @@
MyOption.some →
let x_3 : u8 := 1;
ret x_3
def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
let x_2 : u8 := isSomeWithInstanceNat x_1;
dec x_1;
let x_3 : tagged := box x_2;
ret x_3
def MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0._boxed (x_1 : tobj) : tagged :=
let x_2 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_1;
dec x_1;
let x_3 : tagged := box x_2;
ret x_3
[Compiler.IR] [result]
def isSomeWithInstanceNat (x_1 : @& obj) : u8 :=
let x_2 : usize := 0;
let x_3 : tobj := Array.uget ◾ x_1 x_2 ◾;
let x_4 : u8 := MyOption.isSomeWithInstance._at_.isSomeWithInstanceNat.spec_0 x_3;
dec x_3;
ret x_4
def isSomeWithInstanceNat._boxed (x_1 : obj) : tagged :=
let x_2 : u8 := isSomeWithInstanceNat x_1;
dec x_1;
let x_3 : tagged := box x_2;
ret x_3

196
tests/lean/computedFieldsCode.lean.expected.out
View file

@ -27,9 +27,6 @@
dec x_1;
ret x_2
[Compiler.IR] [result]
def Exp.ctorElim (x_1 : ◾) (x_2 : @& tobj) (x_3 : tobj) (x_4 : ◾) (x_5 : tobj) : tobj :=
let x_6 : tobj := Exp.ctorElim._redArg x_3 x_5;
ret x_6
def Exp.ctorElim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
case x_1 : tobj of
Exp.var →
@ -49,59 +46,122 @@
default →
dec x_1;
ret x_2
[Compiler.IR] [result]
def Exp.ctorElim (x_1 : ◾) (x_2 : @& tobj) (x_3 : tobj) (x_4 : ◾) (x_5 : tobj) : tobj :=
let x_6 : tobj := Exp.ctorElim._redArg x_3 x_5;
ret x_6
def Exp.ctorElim._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) : tobj :=
let x_6 : tobj := Exp.ctorElim x_1 x_2 x_3 x_4 x_5;
dec x_2;
ret x_6
[Compiler.IR] [result]
def Exp.var.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.var.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.var.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.app.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.app.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.app.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.a1.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.a1.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.a1.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.a2.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.a2.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.a2.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.a3.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.a3.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.a3.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.a4.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.a4.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.a4.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
[Compiler.IR] [result]
def Exp.a5.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.a5.elim (x_1 : ◾) (x_2 : tobj) (x_3 : ◾) (x_4 : tobj) : tobj :=
let x_5 : tobj := Exp.ctorElim._redArg x_2 x_4;
ret x_5
def Exp.a5.elim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : tobj := Exp.ctorElim._redArg x_1 x_2;
ret x_3
[Compiler.IR] [result]
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
case x_1 : tobj of
Exp.var._impl →
dec x_3;
let x_9 : u32 := sproj[0, 8] x_1;
dec x_1;
let x_10 : tobj := box x_9;
let x_11 : tobj := app x_2 x_10;
ret x_11
Exp.app._impl →
dec x_2;
let x_12 : tobj := proj[0] x_1;
inc x_12;
let x_13 : tobj := proj[1] x_1;
inc x_13;
dec x_1;
let x_14 : tobj := app x_3 x_12 x_13;
ret x_14
Exp.a1._impl →
dec x_3;
dec x_2;
inc x_4;
ret x_4
Exp.a2._impl →
dec x_3;
dec x_2;
inc x_5;
ret x_5
Exp.a3._impl →
dec x_3;
dec x_2;
inc x_6;
ret x_6
Exp.a4._impl →
dec x_3;
dec x_2;
inc x_7;
ret x_7
Exp.a5._impl →
dec x_3;
dec x_2;
inc x_8;
ret x_8
def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
dec x_8;
dec x_7;
dec x_6;
dec x_5;
dec x_4;
ret x_9
[Compiler.IR] [result]
def Exp.casesOn._override (x_1 : ◾) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) (x_9 : @& tobj) : tobj :=
case x_2 : tobj of
@ -146,49 +206,6 @@
dec x_3;
inc x_9;
ret x_9
def Exp.casesOn._override._redArg (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : @& tobj) (x_5 : @& tobj) (x_6 : @& tobj) (x_7 : @& tobj) (x_8 : @& tobj) : tobj :=
case x_1 : tobj of
Exp.var._impl →
dec x_3;
let x_9 : u32 := sproj[0, 8] x_1;
dec x_1;
let x_10 : tobj := box x_9;
let x_11 : tobj := app x_2 x_10;
ret x_11
Exp.app._impl →
dec x_2;
let x_12 : tobj := proj[0] x_1;
inc x_12;
let x_13 : tobj := proj[1] x_1;
inc x_13;
dec x_1;
let x_14 : tobj := app x_3 x_12 x_13;
ret x_14
Exp.a1._impl →
dec x_3;
dec x_2;
inc x_4;
ret x_4
Exp.a2._impl →
dec x_3;
dec x_2;
inc x_5;
ret x_5
Exp.a3._impl →
dec x_3;
dec x_2;
inc x_6;
ret x_6
Exp.a4._impl →
dec x_3;
dec x_2;
inc x_7;
ret x_7
Exp.a5._impl →
dec x_3;
dec x_2;
inc x_8;
ret x_8
def Exp.casesOn._override._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) (x_9 : tobj) : tobj :=
let x_10 : tobj := Exp.casesOn._override x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9;
dec x_9;
@ -197,37 +214,7 @@
dec x_6;
dec x_5;
ret x_10
def Exp.casesOn._override._redArg._boxed (x_1 : tobj) (x_2 : tobj) (x_3 : tobj) (x_4 : tobj) (x_5 : tobj) (x_6 : tobj) (x_7 : tobj) (x_8 : tobj) : tobj :=
let x_9 : tobj := Exp.casesOn._override._redArg x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8;
dec x_8;
dec x_7;
dec x_6;
dec x_5;
dec x_4;
ret x_9
[Compiler.IR] [result]
def Exp.a1._override : tobj :=
let x_1 : tagged := ctor_2[Exp.a1._impl];
ret x_1
def Exp.a2._override : tobj :=
let x_1 : tagged := ctor_3[Exp.a2._impl];
ret x_1
def Exp.a3._override : tobj :=
let x_1 : tagged := ctor_4[Exp.a3._impl];
ret x_1
def Exp.a4._override : tobj :=
let x_1 : tagged := ctor_5[Exp.a4._impl];
ret x_1
def Exp.a5._override : tobj :=
let x_1 : tagged := ctor_6[Exp.a5._impl];
ret x_1
def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : u64 := Exp.hash._override x_1;
let x_4 : u64 := Exp.hash._override x_2;
let x_5 : u64 := mixHash x_3 x_4;
let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
sset x_6[2, 0] : u64 := x_5;
ret x_6
def Exp.var._override (x_1 : u32) : tobj :=
let x_2 : u64 := UInt32.toUInt64 x_1;
let x_3 : u64 := 1000;
@ -236,6 +223,12 @@
sset x_5[0, 0] : u64 := x_4;
sset x_5[0, 8] : u32 := x_1;
ret x_5
def Exp.var._override._boxed (x_1 : tobj) : tobj :=
let x_2 : u32 := unbox x_1;
dec x_1;
let x_3 : tobj := Exp.var._override x_2;
ret x_3
[Compiler.IR] [result]
def Exp.hash._override (x_1 : @& tobj) : u64 :=
case x_1 : tobj of
Exp.var._impl →
@ -247,16 +240,39 @@
default →
let x_4 : u64 := 42;
ret x_4
def Exp.var._override._boxed (x_1 : tobj) : tobj :=
let x_2 : u32 := unbox x_1;
dec x_1;
let x_3 : tobj := Exp.var._override x_2;
ret x_3
def Exp.hash._override._boxed (x_1 : tobj) : tobj :=
let x_2 : u64 := Exp.hash._override x_1;
dec x_1;
let x_3 : tobj := box x_2;
ret x_3
[Compiler.IR] [result]
def Exp.app._override (x_1 : tobj) (x_2 : tobj) : tobj :=
let x_3 : u64 := Exp.hash._override x_1;
let x_4 : u64 := Exp.hash._override x_2;
let x_5 : u64 := mixHash x_3 x_4;
let x_6 : obj := ctor_1.0.8[Exp.app._impl] x_1 x_2;
sset x_6[2, 0] : u64 := x_5;
ret x_6
[Compiler.IR] [result]
def Exp.a1._override : tobj :=
let x_1 : tagged := ctor_2[Exp.a1._impl];
ret x_1
[Compiler.IR] [result]
def Exp.a2._override : tobj :=
let x_1 : tagged := ctor_3[Exp.a2._impl];
ret x_1
[Compiler.IR] [result]
def Exp.a3._override : tobj :=
let x_1 : tagged := ctor_4[Exp.a3._impl];
ret x_1
[Compiler.IR] [result]
def Exp.a4._override : tobj :=
let x_1 : tagged := ctor_5[Exp.a4._impl];
ret x_1
[Compiler.IR] [result]
def Exp.a5._override : tobj :=
let x_1 : tagged := ctor_6[Exp.a5._impl];
ret x_1
[Compiler.IR] [result]
def f._closed_0 : tobj :=
let x_1 : u32 := 10;

25
tests/lean/doubleReset.lean.expected.out
View file

@ -1,15 +1,4 @@
[Compiler.IR] [reset_reuse]
def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : tobj) (x_5 : usize) (x_6 : usize) (x_7 : obj) : obj :=
let x_8 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_4 x_5 x_6 x_7;
ret x_8
def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : tobj) : obj :=
let x_6 : obj := applyProjectionRules._redArg x_4 x_5;
ret x_6
def applyProjectionRules._redArg (x_1 : obj) (x_2 : tobj) : obj :=
let x_3 : usize := Array.usize ◾ x_1;
let x_4 : usize := 0;
let x_5 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_2 x_3 x_4 x_1;
ret x_5
def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg (x_1 : tobj) (x_2 : usize) (x_3 : usize) (x_4 : obj) : obj :=
let x_5 : u8 := USize.decLt x_3 x_2;
case x_5 : u8 of
@ -35,3 +24,17 @@
let x_16 : obj := Array.uset ◾ x_11 x_3 x_13 ◾;
let x_17 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_1 x_2 x_15 x_16;
ret x_17
[Compiler.IR] [reset_reuse]
def applyProjectionRules._redArg (x_1 : obj) (x_2 : tobj) : obj :=
let x_3 : usize := Array.usize ◾ x_1;
let x_4 : usize := 0;
let x_5 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_2 x_3 x_4 x_1;
ret x_5
[Compiler.IR] [reset_reuse]
def applyProjectionRules (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : obj) (x_5 : tobj) : obj :=
let x_6 : obj := applyProjectionRules._redArg x_4 x_5;
ret x_6
[Compiler.IR] [reset_reuse]
def _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0 (x_1 : ◾) (x_2 : ◾) (x_3 : ◾) (x_4 : tobj) (x_5 : usize) (x_6 : usize) (x_7 : obj) : obj :=
let x_8 : obj := _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map._at_.applyProjectionRules.spec_0._redArg x_4 x_5 x_6 x_7;
ret x_8

8
tests/lean/reduceArity.lean.expected.out
View file

@ -1,7 +1,3 @@
[Compiler.result] size: 1
def g (α : ◾) (n : Nat) (a : lcAny) (b : lcAny) (f : lcAny → lcAny) : lcAny :=
let _x.1 := g._redArg n a f;
return _x.1
[Compiler.result] size: 9
def g._redArg (n : Nat) (a : lcAny) (f : lcAny → lcAny) : lcAny :=
let zero := 0;
@ -15,6 +11,10 @@
let _x.2 := g._redArg n.1 a f;
let _x.3 := f _x.2;
return _x.3
[Compiler.result] size: 1
def g (α : ◾) (n : Nat) (a : lcAny) (b : lcAny) (f : lcAny → lcAny) : lcAny :=
let _x.1 := g._redArg n a f;
return _x.1
[Compiler.result] size: 1
def h._closed_0 : Nat → Nat :=
let _x.1 := double;

1
tests/lean/run/async_sleep.lean
View file

@ -13,7 +13,6 @@ def assertDuration (should : Nat) (eps : Nat) (x : IO α) : IO α := do
assertElapsed t1 t2 should eps
return res
def BASE_DURATION : Nat := 1000
-- generous tolerance for slow CI systems

10
tests/lean/run/boxing_bug.lean
View file

@ -6,9 +6,6 @@ class Semiring (α : Type u) where
/--
trace: [Compiler.IR] [result]
def instSemiringUInt8 : obj :=
let x_1 : obj := pap instSemiringUInt8._lam_0._boxed;
ret x_1
def instSemiringUInt8._lam_0 (x_1 : @& tobj) (x_2 : u8) : u8 :=
let x_3 : u8 := UInt8.ofNat x_1;
let x_4 : u8 := UInt8.mul x_3 x_2;
@ -19,6 +16,13 @@ trace: [Compiler.IR] [result]
dec x_1;
let x_5 : tagged := box x_4;
ret x_5
[Compiler.IR] [result]
def instSemiringUInt8._closed_0 : obj :=
let x_1 : obj := pap instSemiringUInt8._lam_0._boxed;
ret x_1
def instSemiringUInt8 : obj :=
let x_1 : obj := instSemiringUInt8._closed_0;
ret x_1
-/
#guard_msgs in
set_option trace.compiler.ir.result true in

120
tests/lean/run/do_for_loop_compiler_test.lean
View file

@ -18,17 +18,6 @@ trace: [Compiler.saveMono] size: 7
let x := Nat.add _x.6 head.4;
let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
return _x.7
[Compiler.saveMono] size: 7
def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
cases l : Nat
| List.nil =>
let _x.1 := kcontinue b;
return _x.1
| List.cons head.2 tail.3 =>
let _x.4 := Nat.add b i;
let x := Nat.add _x.4 head.2;
let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
return _x.5
[Compiler.saveMono] size: 7
def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.2 i l b : Nat :=
cases l : Nat
@ -40,18 +29,6 @@ trace: [Compiler.saveMono] size: 7
let x := Nat.add _x.6 head.4;
let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
return _x.7
[Compiler.saveMono] size: 9
def testing : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
return _x.8
[Compiler.saveMono] size: 12
def List.newForIn._at_.testing.spec_1 _x.1 l b : Nat :=
cases l : Nat
@ -68,6 +45,29 @@ trace: [Compiler.saveMono] size: 7
let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.3 head.2 _x.11 b;
return _x.12
[Compiler.saveMono] size: 9
def testing : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
return _x.8
[Compiler.saveMono] size: 7
def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
cases l : Nat
| List.nil =>
let _x.1 := kcontinue b;
return _x.1
| List.cons head.2 tail.3 =>
let _x.4 := Nat.add b i;
let x := Nat.add _x.4 head.2;
let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
return _x.5
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in
@ -100,18 +100,6 @@ trace: [Compiler.saveMono] size: 7
let x := Nat.add _x.6 head.4;
let _x.7 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i tail.5 x;
return _x.7
[Compiler.saveMono] size: 9
def testing2 : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
return _x.8
[Compiler.saveMono] size: 14
def List.newForIn._at_.testing2.spec_0 _x.1 l b : Nat :=
cases l : Nat
@ -130,6 +118,18 @@ trace: [Compiler.saveMono] size: 7
let _x.12 := List.range'TR.go _x.1 _x.9 _x.10 _x.11;
let _x.13 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.3 head.2 _x.12 x;
return _x.13
[Compiler.saveMono] size: 9
def testing2 : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
return _x.8
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in
@ -164,19 +164,6 @@ trace: [Compiler.saveMono] size: 9
let x := Nat.add _x.7 head.4;
let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
return _x.8
[Compiler.saveMono] size: 9
def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
cases l : Nat
| List.nil =>
let _x.1 := kcontinue b;
return _x.1
| List.cons head.2 tail.3 =>
let _x.4 := Nat.add b b;
let x := Nat.add _x.4 s;
let _x.5 := Nat.add x i;
let x := Nat.add _x.5 head.2;
let _x.6 := List.newForIn._at_.testing3.spec_0 s i kcontinue tail.3 x;
return _x.6
[Compiler.saveMono] size: 9
def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.2 s i l b : Nat :=
cases l : Nat
@ -190,18 +177,6 @@ trace: [Compiler.saveMono] size: 9
let x := Nat.add _x.7 head.4;
let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
return _x.8
[Compiler.saveMono] size: 9
def testing3 : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
return _x.8
[Compiler.saveMono] size: 12
def List.newForIn._at_.testing3.spec_1 _x.1 l b : Nat :=
cases l : Nat
@ -218,6 +193,31 @@ trace: [Compiler.saveMono] size: 9
let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
let _x.12 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.3 b head.2 _x.11 b;
return _x.12
[Compiler.saveMono] size: 9
def testing3 : Nat :=
let x := 42;
let _x.1 := 1;
let _x.2 := 2;
let _x.3 := 3;
let _x.4 := [] ◾;
let _x.5 := List.cons ◾ _x.3 _x.4;
let _x.6 := List.cons ◾ _x.2 _x.5;
let _x.7 := List.cons ◾ _x.1 _x.6;
let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
return _x.8
[Compiler.saveMono] size: 9
def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
cases l : Nat
| List.nil =>
let _x.1 := kcontinue b;
return _x.1
| List.cons head.2 tail.3 =>
let _x.4 := Nat.add b b;
let x := Nat.add _x.4 s;
let _x.5 := Nat.add x i;
let x := Nat.add _x.5 head.2;
let _x.6 := List.newForIn._at_.testing3.spec_0 s i kcontinue tail.3 x;
return _x.6
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in

102
tests/lean/run/do_for_loop_levenstein_compiler_test.lean
View file

@ -21,39 +21,7 @@
loop range.start (by simp) (by simp) init
/--
trace: [Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 _x.2 as sz _x.3 range this i hs hl a.4 : Array
String :=
let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4;
return _x.5
[Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 _x.2 kcontinue range this i hs hl a.3 : Array
String :=
let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3;
return _x.4
[Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 _x.3 range this i hs hl a.4 : Array
String :=
let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4;
return _x.5
[Compiler.saveMono] size: 12
def Array.contains._at_.deletions.spec_0 as a : Bool :=
let _x.1 := 0;
let _x.2 := Array.size ◾ as;
let _x.3 := Nat.decLt _x.1 _x.2;
cases _x.3 : Bool
| Bool.false =>
return _x.3
| Bool.true =>
cases _x.3 : Bool
| Bool.false =>
return _x.3
| Bool.true =>
let _x.4 := 0;
let _x.5 := USize.ofNat _x.2;
let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.4 _x.5;
return _x.6
[Compiler.saveMono] size: 13
trace: [Compiler.saveMono] size: 13
def _private.Init.Data.Array.Basic.0.Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0 a as i stop : Bool :=
let _x.1 := USize.decEq i stop;
cases _x.1 : Bool
@ -71,25 +39,23 @@ trace: [Compiler.saveMono] size: 1
| Bool.true =>
let _x.7 := false;
return _x.7
[Compiler.saveMono] size: 15
def deletions n s : Array String :=
let zero := 0;
let isZero := Nat.decEq n zero;
cases isZero : Array String
| Bool.true =>
let _x.1 := 1;
let _x.2 := Array.mkEmpty ◾ _x.1;
let _x.3 := Array.push ◾ _x.2 s;
return _x.3
[Compiler.saveMono] size: 12
def Array.contains._at_.deletions.spec_0 as a : Bool :=
let _x.1 := 0;
let _x.2 := Array.size ◾ as;
let _x.3 := Nat.decLt _x.1 _x.2;
cases _x.3 : Bool
| Bool.false =>
let one := 1;
let n.4 := Nat.sub n one;
let out := Array.mkEmpty ◾ zero;
let _x.5 := deletions n.4 s;
let sz := Array.usize ◾ _x.5;
let _x.6 := 0;
let _x.7 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 _x.5 sz _x.6 out;
return _x.7
return _x.3
| Bool.true =>
cases _x.3 : Bool
| Bool.false =>
return _x.3
| Bool.true =>
let _x.4 := 0;
let _x.5 := USize.ofNat _x.2;
let _x.6 := Array.anyMUnsafe.any._at_.Array.contains._at_.deletions.spec_0.spec_0.2 a as _x.4 _x.5;
return _x.6
[Compiler.saveMono] size: 19
def Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz i s : Array String :=
let _x.1 := USize.decLt i sz;
@ -186,6 +152,25 @@ trace: [Compiler.saveMono] size: 1
return _x.19
| Bool.true =>
goto _jp.16
[Compiler.saveMono] size: 15
def deletions n s : Array String :=
let zero := 0;
let isZero := Nat.decEq n zero;
cases isZero : Array String
| Bool.true =>
let _x.1 := 1;
let _x.2 := Array.mkEmpty ◾ _x.1;
let _x.3 := Array.push ◾ _x.2 s;
return _x.3
| Bool.false =>
let one := 1;
let n.4 := Nat.sub n one;
let out := Array.mkEmpty ◾ zero;
let _x.5 := deletions n.4 s;
let sz := Array.usize ◾ _x.5;
let _x.6 := 0;
let _x.7 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 _x.5 sz _x.6 out;
return _x.7
[Compiler.saveMono] size: 29
def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3 : Array
String :=
@ -222,6 +207,21 @@ trace: [Compiler.saveMono] size: 1
return _x.18
| Bool.true =>
goto _jp.15
[Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 _x.2 kcontinue range this i hs hl a.3 : Array
String :=
let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3;
return _x.4
[Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 _x.3 range this i hs hl a.4 : Array
String :=
let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4;
return _x.5
[Compiler.saveMono] size: 1
def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 _x.2 as sz _x.3 range this i hs hl a.4 : Array
String :=
let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4;
return _x.5
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in

9
tests/lean/run/emptyLcnf.lean
View file

@ -41,6 +41,13 @@ trace: [Compiler.result] size: 5
let _x.2 := _eval._closed_2.2;
let _x.3 := Array.push ◾ _x.2 _x.1;
return _x.3
[Compiler.result] size: 3
def _private.lean.run.emptyLcnf.0._eval._closed_4 : Lean.Elab.Term.Context →
lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
let _x.1 := PUnit.unit;
let _x.2 := _eval._closed_3.2;
let _f.3 := _eval._lam_0.2 _x.2 _x.1;
return _f.3
[Compiler.result] size: 8
def _private.lean.run.emptyLcnf.0._eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
let _x.4 := _eval._closed_0.2;
@ -49,7 +56,7 @@ trace: [Compiler.result] size: 5
let _x.7 := _eval._closed_2.2;
let _x.8 := _eval._closed_3.2;
let _x.9 := PUnit.unit;
let _f.10 := _eval._lam_0.2 _x.8 _x.9;
let _f.10 := _eval._closed_4.2;
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
return _x.11
-/

13
tests/lean/run/erased.lean
View file

@ -61,6 +61,16 @@ trace: [Compiler.result] size: 5
let _x.2 : Array Lean.Name := _eval._closed_3.2;
let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
return _x.3
[Compiler.result] size: 3
def _private.lean.run.erased.0._eval._closed_5 : Lean.Elab.Term.Context →
lcAny → Lean.Meta.Context → lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit :=
let _x.1 : PUnit := PUnit.unit;
let _x.2 : Array Lean.Name := _eval._closed_4.2;
let _f.3 : Lean.Elab.Term.Context →
lcAny →
Lean.Meta.Context →
lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.2 _x.1;
return _f.3
[Compiler.result] size: 9
def _private.lean.run.erased.0._eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out
Lean.Exception lcAny PUnit :=
@ -74,8 +84,7 @@ trace: [Compiler.result] size: 5
let _f.11 : Lean.Elab.Term.Context →
lcAny →
Lean.Meta.Context →
lcAny →
Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0.2 _x.9 _x.10;
lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._closed_5.2;
let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
return _x.12
-/