Skip to content

Commit 6f0b0ac

Browse files
hargoniXhargoniX
committed
fix tests
1 parent fd6e73e commit 6f0b0ac

File tree

8 files changed

+72
-61
lines changed

8 files changed

+72
-61
lines changed

‎src/include/lean/lean.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2829,12 +2829,12 @@ LEAN_EXPORT lean_obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname);
28292829

28302830
static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
28312831

2832-
static inline lean_obj_res lean_baseio_out_val(b_lean_obj_arg r) {
2832+
static inline b_lean_obj_res lean_baseio_out_val(b_lean_obj_arg r) {
28332833
// TODO: This function needs to become identity after we are done.
28342834
return lean_ctor_get(r, 0);
28352835
}
28362836

2837-
static inline lean_obj_res lean_mk_baseio_out(b_lean_obj_arg i) {
2837+
static inline lean_obj_res lean_mk_baseio_out(lean_obj_arg i) {
28382838
// TODO: This function needs to become identity after we are done.
28392839
lean_object * r = lean_alloc_ctor(0, 2, 0);
28402840
lean_ctor_set(r, 0, i);

‎tests/lean/baseIO.lean.expected.out‎

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,19 @@
1-
[Compiler.saveBase] size: 11
2-
def test a.1 : EStateM.Result Empty lcRealWorld UInt32 :=
1+
[Compiler.saveBase] size: 14
2+
def test a.1 : BaseIO.Out UInt32 :=
33
let _x.2 := 42;
4-
let _x.3 := @ST.Prim.mkRef _ _ _x.2 a.1;
5-
cases _x.3 : EStateM.Result Empty lcRealWorld UInt32
6-
| EStateM.Result.ok a.4 a.5 =>
4+
let _x.3 := @IO.mkRef _ _x.2 a.1;
5+
cases _x.3 : BaseIO.Out UInt32
6+
| BaseIO.Out.mk val.4 state.5 =>
77
let _x.6 := 10;
8-
let _x.7 := @ST.Prim.Ref.set _ _ a.4 _x.6 a.5;
9-
cases _x.7 : EStateM.Result Empty lcRealWorld UInt32
8+
let _x.7 := @ST.Prim.Ref.set _ _ val.4 _x.6 state.5;
9+
cases _x.7 : BaseIO.Out UInt32
1010
| EStateM.Result.ok a.8 a.9 =>
11-
let _x.10 := @ST.Prim.Ref.get _ _ a.4 a.9;
12-
return _x.10
13-
| EStateM.Result.error a.11 a.12 =>
11+
let _x.10 := @ST.Prim.Ref.get _ _ val.4 a.9;
12+
cases _x.10 : BaseIO.Out UInt32
13+
| EStateM.Result.ok a.11 a.12 =>
14+
let _x.13 := @BaseIO.Out.mk _ a.11 a.12;
15+
return _x.13
16+
| EStateM.Result.error a.14 a.15 =>
17+
⊥
18+
| EStateM.Result.error a.16 a.17 =>
1419
⊥
15-
| EStateM.Result.error a.13 a.14 =>
16-
⊥

‎tests/lean/jpClosureIssue.lean.expected.out‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
[Compiler.saveMono] size: 7
2-
def foo b a.1 : EStateM.Result IO.Error lcRealWorld PUnit :=
3-
cases b : EStateM.Result IO.Error lcRealWorld PUnit
2+
def foo b _y.1 : BaseIO.Out (Except IO.Error PUnit) :=
3+
cases b : BaseIO.Out (Except IO.Error PUnit)
44
| Bool.false =>
55
let _x.2 := 1;
6-
let _x.3 := print _x.2 a.1;
6+
let _x.3 := print _x.2 _y.1;
77
return _x.3
88
| Bool.true =>
99
let _x.4 := 0;
10-
let _x.5 := print _x.4 a.1;
10+
let _x.5 := print _x.4 _y.1;
1111
return _x.5

‎tests/lean/lcnfTypes.lean.expected.out‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,11 @@ Lean.getConstInfo : {m : Type → Type} → [Monad m] → [MonadEnv m] → [Mona
1919
Lean.Meta.instMonadMetaM : Monad fun α =>
2020
Context →
2121
ST.Ref lcRealWorld State →
22-
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld α
22+
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → BaseIO.Out (Except Exception α)
2323
Lean.Meta.inferType : Expr →
2424
Context →
2525
ST.Ref lcRealWorld State →
26-
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
26+
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → BaseIO.Out (Except Exception Expr)
2727
Lean.Elab.Term.elabTerm : Syntax →
2828
Option Expr →
2929
Bool →
@@ -32,7 +32,7 @@ Lean.Elab.Term.elabTerm : Syntax →
3232
ST.Ref lcRealWorld Elab.Term.State →
3333
Context →
3434
ST.Ref lcRealWorld State →
35-
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
35+
Core.Context → ST.Ref lcRealWorld Core.State → lcRealWorld → BaseIO.Out (Except Exception Expr)
3636
Nat.add : Nat → Nat → Nat
3737
Magma.mul : Magma → lcAny → lcAny → lcAny
3838
weird1 : Bool → lcAny
@@ -49,12 +49,12 @@ MonadControl.restoreM : {m n : lcErased} → [self : MonadControl lcAny lcAny]
4949
Decidable.casesOn : {p motive : lcErased} → Bool → (lcErased → lcAny) → (lcErased → lcAny) → lcAny
5050
Lean.getConstInfo : {m : lcErased} → [Monad lcAny] → [MonadEnv lcAny] → [MonadError lcAny] → Name → lcAny
5151
Lean.Meta.instMonadMetaM : Monad lcAny
52-
Lean.Meta.inferType : Expr → Context → lcAny → Core.Context → lcAny → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
52+
Lean.Meta.inferType : Expr → Context → lcAny → Core.Context → lcAny → lcRealWorld → BaseIO.Out (Except Exception Expr)
5353
Lean.Elab.Term.elabTerm : Syntax →
5454
Option Expr →
5555
Bool →
5656
Bool →
5757
Elab.Term.Context →
58-
lcAny → Context → lcAny → Core.Context → lcAny → lcRealWorld → EStateM.Result Exception lcRealWorld Expr
58+
lcAny → Context → lcAny → Core.Context → lcAny → lcRealWorld → BaseIO.Out (Except Exception Expr)
5959
Nat.add : Nat → Nat → Nat
6060
Fin.add : {n : Nat} → Nat → Nat → Nat

‎tests/lean/run/emptyLcnf.lean‎

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -11,15 +11,18 @@ trace: [Compiler.result] size: 0
1111
def f x : Nat :=
1212
⊥
1313
---
14-
trace: [Compiler.result] size: 5
15-
def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
14+
trace: [Compiler.result] size: 8
15+
def _eval._lam_0 _x.1 _x.2 _y.3 _y.4 _y.5 _y.6 _y.7 _y.8 _y.9 : BaseIO.Out (Except Lean.Exception PUnit) :=
1616
let _x.10 := Lean.Compiler.compile _x.1 _y.7 _y.8 _y.9;
17-
cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
18-
| EStateM.Result.ok a.11 a.12 =>
19-
let _x.13 := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
20-
return _x.13
21-
| EStateM.Result.error a.14 a.15 =>
22-
return _x.10
17+
cases _x.10 : BaseIO.Out (Except Lean.Exception PUnit)
18+
| BaseIO.Out.mk val.11 state.12 =>
19+
cases val.11 : BaseIO.Out (Except Lean.Exception PUnit)
20+
| Except.error a.13 =>
21+
return _x.10
22+
| Except.ok a.14 =>
23+
let _x.15 := Except.ok ◾ ◾ _x.2;
24+
let _x.16 := @BaseIO.Out.mk ◾ _x.15 state.12;
25+
return _x.16
2326
[Compiler.result] size: 1
2427
def _eval._closed_0 : String :=
2528
let _x.1 := "f";
@@ -41,15 +44,15 @@ trace: [Compiler.result] size: 5
4144
let _x.3 := Array.push ◾ _x.2 _x.1;
4245
return _x.3
4346
[Compiler.result] size: 8
44-
def _eval a.1 a.2 a.3 : EStateM.Result Lean.Exception lcRealWorld PUnit :=
47+
def _eval a.1 a.2 _y.3 : BaseIO.Out (Except Lean.Exception PUnit) :=
4548
let _x.4 := _eval._closed_0;
4649
let _x.5 := _eval._closed_1;
4750
let _x.6 := 1;
4851
let _x.7 := _eval._closed_2;
4952
let _x.8 := _eval._closed_3;
5053
let _x.9 := PUnit.unit;
5154
let _f.10 := _eval._lam_0 _x.8 _x.9;
52-
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
55+
let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 _y.3;
5356
return _x.11
5457
-/
5558
#guard_msgs in

‎tests/lean/run/erased.lean‎

Lines changed: 18 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -25,17 +25,20 @@ trace: [Compiler.result] size: 1
2525
let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
2626
return _x.1
2727
---
28-
trace: [Compiler.result] size: 5
28+
trace: [Compiler.result] size: 8
2929
def _eval._lam_0 (_x.1 : Array
30-
Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcRealWorld) : EStateM.Result
31-
Lean.Exception lcRealWorld PUnit :=
32-
let _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit := compile _x.1 _y.7 _y.8 _y.9;
33-
cases _x.10 : EStateM.Result Lean.Exception lcRealWorld PUnit
34-
| EStateM.Result.ok (a.11 : PUnit) (a.12 : lcRealWorld) =>
35-
let _x.13 : EStateM.Result Lean.Exception lcRealWorld PUnit := EStateM.Result.ok ◾ ◾ ◾ _x.2 a.12;
36-
return _x.13
37-
| EStateM.Result.error (a.14 : Lean.Exception) (a.15 : lcRealWorld) =>
38-
return _x.10
30+
Lean.Name) (_x.2 : PUnit) (_y.3 : Lean.Elab.Term.Context) (_y.4 : lcAny) (_y.5 : Lean.Meta.Context) (_y.6 : lcAny) (_y.7 : Lean.Core.Context) (_y.8 : lcAny) (_y.9 : lcRealWorld) : BaseIO.Out
31+
(Except Lean.Exception PUnit) :=
32+
let _x.10 : BaseIO.Out (Except Lean.Exception PUnit) := compile _x.1 _y.7 _y.8 _y.9;
33+
cases _x.10 : BaseIO.Out (Except Lean.Exception PUnit)
34+
| BaseIO.Out.mk (val.11 : Except Lean.Exception PUnit) (state.12 : lcRealWorld) =>
35+
cases val.11 : BaseIO.Out (Except Lean.Exception PUnit)
36+
| Except.error (a.13 : Lean.Exception) =>
37+
return _x.10
38+
| Except.ok (a.14 : PUnit) =>
39+
let _x.15 : Except Lean.Exception PUnit := Except.ok ◾ ◾ _x.2;
40+
let _x.16 : BaseIO.Out (Except Lean.Exception PUnit) := @BaseIO.Out.mk ◾ _x.15 state.12;
41+
return _x.16
3942
[Compiler.result] size: 1
4043
def _eval._closed_0 : String :=
4144
let _x.1 : String := "Erased";
@@ -62,8 +65,8 @@ trace: [Compiler.result] size: 5
6265
let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
6366
return _x.3
6467
[Compiler.result] size: 9
65-
def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcRealWorld) : EStateM.Result Lean.Exception
66-
lcRealWorld PUnit :=
68+
def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (_y.3 : lcRealWorld) : BaseIO.Out
69+
(Except Lean.Exception PUnit) :=
6770
let _x.4 : String := _eval._closed_0;
6871
let _x.5 : String := _eval._closed_1;
6972
let _x.6 : Lean.Name := _eval._closed_2;
@@ -76,9 +79,9 @@ trace: [Compiler.result] size: 5
7679
Lean.Meta.Context →
7780
lcAny →
7881
Lean.Core.Context →
79-
lcAny → lcRealWorld → EStateM.Result Lean.Exception lcRealWorld PUnit := _eval._lam_0 _x.9 _x.10;
80-
let _x.12 : EStateM.Result Lean.Exception lcRealWorld
81-
PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
82+
lcAny → lcRealWorld → BaseIO.Out (Except Lean.Exception PUnit) := _eval._lam_0 _x.9 _x.10;
83+
let _x.12 : BaseIO.Out
84+
(Except Lean.Exception PUnit) := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 _y.3;
8285
return _x.12
8386
-/
8487
#guard_msgs in

‎tests/lean/run/isDefEqProjIssue.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ instance g (x : Nat) : Foo :=
8484
{ x, y := ack 10 11 }
8585

8686
open Lean Meta
87-
set_option maxHeartbeats 500 in
87+
set_option maxHeartbeats 520 in
8888
run_meta do
8989
withLocalDeclD `x (mkConst ``Nat) fun x => do
9090
let lhs := Expr.proj ``Foo 0 <| mkApp (mkConst ``f) x

‎tests/lean/seqToCodeIssue.lean.expected.out‎

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,19 @@
1-
[Compiler.saveMono] size: 12
2-
def f b a.1 : EStateM.Result IO.Error lcRealWorld PUnit :=
3-
jp _jp.2 a _y.3 : EStateM.Result IO.Error lcRealWorld PUnit :=
1+
[Compiler.saveMono] size: 14
2+
def f b _y.1 : BaseIO.Out (Except IO.Error PUnit) :=
3+
jp _jp.2 a _y.3 : BaseIO.Out (Except IO.Error PUnit) :=
44
let _x.4 := print a _y.3;
5-
cases _x.4 : EStateM.Result IO.Error lcRealWorld PUnit
6-
| EStateM.Result.ok a.5 a.6 =>
7-
let _x.7 := print a a.6;
8-
return _x.7
9-
| EStateM.Result.error a.8 a.9 =>
10-
return _x.4;
11-
cases b : EStateM.Result IO.Error lcRealWorld PUnit
5+
cases _x.4 : BaseIO.Out (Except IO.Error PUnit)
6+
| BaseIO.Out.mk val.5 state.6 =>
7+
cases val.5 : BaseIO.Out (Except IO.Error PUnit)
8+
| Except.error a.7 =>
9+
return _x.4
10+
| Except.ok a.8 =>
11+
let _x.9 := print a state.6;
12+
return _x.9;
13+
cases b : BaseIO.Out (Except IO.Error PUnit)
1214
| Bool.false =>
1315
let _x.10 := 1;
14-
goto _jp.2 _x.10 a.1
16+
goto _jp.2 _x.10 _y.1
1517
| Bool.true =>
1618
let _x.11 := 0;
17-
goto _jp.2 _x.11 a.1
19+
goto _jp.2 _x.11 _y.1

0 commit comments

Comments
 (0)