mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
353 lines
10 KiB
Plaintext
353 lines
10 KiB
Plaintext
[Compiler.IR] [result]
|
|
def Exp.ctorIdx (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var →
|
|
let x_2 : tagged := 0;
|
|
ret x_2
|
|
Exp.app →
|
|
let x_3 : tagged := 1;
|
|
ret x_3
|
|
Exp.a1 →
|
|
let x_4 : tagged := 2;
|
|
ret x_4
|
|
Exp.a2 →
|
|
let x_5 : tagged := 3;
|
|
ret x_5
|
|
Exp.a3 →
|
|
let x_6 : tagged := 4;
|
|
ret x_6
|
|
Exp.a4 →
|
|
let x_7 : tagged := 5;
|
|
ret x_7
|
|
Exp.a5 →
|
|
let x_8 : tagged := 6;
|
|
ret x_8
|
|
def Exp.ctorIdx._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := Exp.ctorIdx x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def Exp.ctorElim._redArg (x_1 : tobj) (x_2 : tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var →
|
|
let x_3 : u32 := sproj[0, 0] x_1;
|
|
dec x_1;
|
|
let x_4 : tobj := box x_3;
|
|
let x_5 : tobj := app x_2 x_4;
|
|
ret x_5
|
|
Exp.app →
|
|
let x_6 : tobj := proj[0] x_1;
|
|
inc x_6;
|
|
let x_7 : tobj := proj[1] x_1;
|
|
inc x_7;
|
|
dec x_1;
|
|
let x_8 : tobj := app x_2 x_6 x_7;
|
|
ret x_8
|
|
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
|
|
[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
|
|
[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
|
|
[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
|
|
[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
|
|
[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
|
|
[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
|
|
[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
|
|
Exp.var._impl →
|
|
dec x_4;
|
|
let x_10 : u32 := sproj[0, 8] x_2;
|
|
dec x_2;
|
|
let x_11 : tobj := box x_10;
|
|
let x_12 : tobj := app x_3 x_11;
|
|
ret x_12
|
|
Exp.app._impl →
|
|
dec x_3;
|
|
let x_13 : tobj := proj[0] x_2;
|
|
inc x_13;
|
|
let x_14 : tobj := proj[1] x_2;
|
|
inc x_14;
|
|
dec x_2;
|
|
let x_15 : tobj := app x_4 x_13 x_14;
|
|
ret x_15
|
|
Exp.a1._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_5;
|
|
ret x_5
|
|
Exp.a2._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_6;
|
|
ret x_6
|
|
Exp.a3._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_7;
|
|
ret x_7
|
|
Exp.a4._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_8;
|
|
ret x_8
|
|
Exp.a5._impl →
|
|
dec x_4;
|
|
dec x_3;
|
|
inc x_9;
|
|
ret x_9
|
|
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;
|
|
dec x_8;
|
|
dec x_7;
|
|
dec x_6;
|
|
dec x_5;
|
|
ret x_10
|
|
[Compiler.IR] [result]
|
|
def Exp.var._override (x_1 : u32) : tobj :=
|
|
let x_2 : u64 := UInt32.toUInt64 x_1;
|
|
let x_3 : u64 := 1000;
|
|
let x_4 : u64 := UInt64.add x_2 x_3;
|
|
let x_5 : obj := ctor_0.0.12[Exp.var._impl];
|
|
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 →
|
|
let x_2 : u64 := sproj[0, 0] x_1;
|
|
ret x_2
|
|
Exp.app._impl →
|
|
let x_3 : u64 := sproj[2, 0] x_1;
|
|
ret x_3
|
|
default →
|
|
let x_4 : u64 := 42;
|
|
ret x_4
|
|
def Exp.hash._override._boxed (x_1 : tobj) : obj :=
|
|
let x_2 : u64 := Exp.hash._override x_1;
|
|
dec x_1;
|
|
let x_3 : obj := 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;
|
|
let x_2 : tobj := Exp.var._override x_1;
|
|
ret x_2
|
|
def f._closed_1 : tobj :=
|
|
let x_1 : tagged := ctor_5[Exp.a4._impl];
|
|
let x_2 : tobj := f._closed_0;
|
|
let x_3 : tobj := Exp.app._override x_2 x_1;
|
|
ret x_3
|
|
def f._closed_2 : u64 :=
|
|
let x_1 : tobj := f._closed_1;
|
|
let x_2 : u64 := Exp.hash._override x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
def f : u64 :=
|
|
let x_1 : u64 := f._closed_2;
|
|
ret x_1
|
|
[Compiler.IR] [result]
|
|
def g (x_1 : @& tobj) : u8 :=
|
|
case x_1 : tobj of
|
|
Exp.a3._impl →
|
|
let x_2 : u8 := 1;
|
|
ret x_2
|
|
default →
|
|
let x_3 : u8 := 0;
|
|
ret x_3
|
|
def g._boxed (x_1 : tobj) : tagged :=
|
|
let x_2 : u8 := g x_1;
|
|
dec x_1;
|
|
let x_3 : tagged := box x_2;
|
|
ret x_3
|
|
[Compiler.IR] [result]
|
|
def hash' (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.var._impl →
|
|
let x_2 : u32 := sproj[0, 8] x_1;
|
|
let x_3 : tobj := UInt32.toNat x_2;
|
|
ret x_3
|
|
Exp.app._impl →
|
|
let x_4 : tobj := proj[0] x_1;
|
|
let x_5 : tobj := proj[1] x_1;
|
|
let x_6 : tobj := hash' x_4;
|
|
let x_7 : tobj := hash' x_5;
|
|
let x_8 : tobj := Nat.add x_6 x_7;
|
|
dec x_7;
|
|
dec x_6;
|
|
ret x_8
|
|
default →
|
|
let x_9 : tagged := 42;
|
|
ret x_9
|
|
def hash'._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := hash' x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def getAppFn (x_1 : @& tobj) : tobj :=
|
|
case x_1 : tobj of
|
|
Exp.app._impl →
|
|
let x_2 : tobj := proj[0] x_1;
|
|
let x_3 : tobj := getAppFn x_2;
|
|
ret x_3
|
|
default →
|
|
inc x_1;
|
|
ret x_1
|
|
def getAppFn._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := getAppFn x_1;
|
|
dec x_1;
|
|
ret x_2
|
|
[Compiler.IR] [result]
|
|
def Exp.f (x_1 : @& tobj) : tobj :=
|
|
let x_2 : tobj := getAppFn x_1;
|
|
ret x_2
|
|
def Exp.f._boxed (x_1 : tobj) : tobj :=
|
|
let x_2 : tobj := Exp.f x_1;
|
|
dec x_1;
|
|
ret x_2
|