Skip to content

Commit 601f2d0

Browse files
hargoniXhargoniX
committed
fix tests
1 parent da36541 commit 601f2d0

File tree

3 files changed

+243
-5
lines changed

3 files changed

+243
-5
lines changed

‎src/Lean/Compiler/LCNF/SpecInfo.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,6 @@ def computeSpecEntries (decls : Array Decl) (autoSpecialize : Name → Option (A
219219
let decl := decls[i]
220220
let mut paramsInfo := declsInfo[i]!
221221
let some mask := m.find? decl.name | unreachable!
222-
trace[Compiler.specialize.info] "{decl.name} {mask}"
223222
paramsInfo := Array.zipWith (as := paramsInfo) (bs := mask) fun info fixed =>
224223
if fixed || info matches .user then
225224
info

‎tests/lean/run/do_for_loop_compiler_test.lean‎

Lines changed: 242 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,242 @@
1+
import Std.Do.Triple.SpecLemmas
2+
3+
@[specialize, expose]
4+
def List.newForIn (l : List α) (b : β) (kcons : α → (β → γ) → β → γ) (knil : β → γ) : γ :=
5+
match l with
6+
| [] => knil b
7+
| a :: l => kcons a (l.newForIn · kcons knil) b
8+
9+
/--
10+
trace: [Compiler.saveMono] size: 7
11+
def 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 l b : Nat :=
12+
cases l : Nat
13+
| List.nil =>
14+
let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
15+
return _x.3
16+
| List.cons head.4 tail.5 =>
17+
let _x.6 := Nat.add b i;
18+
let x := Nat.add _x.6 head.4;
19+
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;
20+
return _x.7
21+
[Compiler.saveMono] size: 7
22+
def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
23+
cases l : Nat
24+
| List.nil =>
25+
let _x.1 := kcontinue b;
26+
return _x.1
27+
| List.cons head.2 tail.3 =>
28+
let _x.4 := Nat.add b i;
29+
let x := Nat.add _x.4 head.2;
30+
let _x.5 := List.newForIn._at_.testing.spec_0 i kcontinue tail.3 x;
31+
return _x.5
32+
[Compiler.saveMono] size: 7
33+
def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.2 i l b : Nat :=
34+
cases l : Nat
35+
| List.nil =>
36+
let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
37+
return _x.3
38+
| List.cons head.4 tail.5 =>
39+
let _x.6 := Nat.add b i;
40+
let x := Nat.add _x.6 head.4;
41+
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;
42+
return _x.7
43+
[Compiler.saveMono] size: 9
44+
def testing : Nat :=
45+
let x := 42;
46+
let _x.1 := 1;
47+
let _x.2 := 2;
48+
let _x.3 := 3;
49+
let _x.4 := [] ◾;
50+
let _x.5 := List.cons ◾ _x.3 _x.4;
51+
let _x.6 := List.cons ◾ _x.2 _x.5;
52+
let _x.7 := List.cons ◾ _x.1 _x.6;
53+
let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
54+
return _x.8
55+
[Compiler.saveMono] size: 13
56+
def List.newForIn._at_.testing.spec_1 _x.1 l b : Nat :=
57+
cases l : Nat
58+
| List.nil =>
59+
return b
60+
| List.cons head.2 tail.3 =>
61+
let _x.4 := 10;
62+
let _x.5 := Nat.sub _x.4 head.2;
63+
let _x.6 := Nat.add _x.5 _x.1;
64+
let _x.7 := 1;
65+
let _x.8 := Nat.sub _x.6 _x.7;
66+
let _x.9 := Nat.mul _x.1 _x.8;
67+
let _x.10 := Nat.add head.2 _x.9;
68+
let _x.11 := [] ◾;
69+
let _x.12 := List.range'TR.go _x.1 _x.8 _x.10 _x.11;
70+
let _x.13 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.3 head.2 _x.12 b;
71+
return _x.13
72+
-/
73+
#guard_msgs in
74+
set_option trace.Compiler.saveMono true in
75+
def testing :=
76+
let x := 42;
77+
List.newForIn (β := Nat) (γ := Id Nat)
78+
[1,2,3]
79+
x
80+
(fun i kcontinue s =>
81+
let x := s;
82+
List.newForIn
83+
[i:10].toList x
84+
(fun j kcontinue s =>
85+
let x := s;
86+
let x := x + i + j;
87+
kcontinue x)
88+
kcontinue)
89+
pure
90+
91+
92+
/--
93+
trace: [Compiler.saveMono] size: 7
94+
def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i l b : Nat :=
95+
cases l : Nat
96+
| List.nil =>
97+
let _x.3 := List.newForIn._at_.testing2.spec_0 _x.1 tail.2 b;
98+
return _x.3
99+
| List.cons head.4 tail.5 =>
100+
let _x.6 := Nat.add b i;
101+
let x := Nat.add _x.6 head.4;
102+
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;
103+
return _x.7
104+
[Compiler.saveMono] size: 9
105+
def testing2 : Nat :=
106+
let x := 42;
107+
let _x.1 := 1;
108+
let _x.2 := 2;
109+
let _x.3 := 3;
110+
let _x.4 := [] ◾;
111+
let _x.5 := List.cons ◾ _x.3 _x.4;
112+
let _x.6 := List.cons ◾ _x.2 _x.5;
113+
let _x.7 := List.cons ◾ _x.1 _x.6;
114+
let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
115+
return _x.8
116+
[Compiler.saveMono] size: 15
117+
def List.newForIn._at_.testing2.spec_0 _x.1 l b : Nat :=
118+
cases l : Nat
119+
| List.nil =>
120+
return b
121+
| List.cons head.2 tail.3 =>
122+
let _x.4 := 37;
123+
let x := Nat.add b _x.4;
124+
let _x.5 := 10;
125+
let _x.6 := Nat.sub _x.5 head.2;
126+
let _x.7 := Nat.add _x.6 _x.1;
127+
let _x.8 := 1;
128+
let _x.9 := Nat.sub _x.7 _x.8;
129+
let _x.10 := Nat.mul _x.1 _x.9;
130+
let _x.11 := Nat.add head.2 _x.10;
131+
let _x.12 := [] ◾;
132+
let _x.13 := List.range'TR.go _x.1 _x.9 _x.11 _x.12;
133+
let _x.14 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.3 head.2 _x.13 x;
134+
return _x.14
135+
-/
136+
#guard_msgs in
137+
set_option trace.Compiler.saveMono true in
138+
def testing2 :=
139+
let x := 42;
140+
List.newForIn (β := Nat) (γ := Id Nat)
141+
[1,2,3]
142+
x
143+
(fun i kcontinue s =>
144+
-- difference to testing1 here
145+
let x := s + 37;
146+
List.newForIn
147+
[i:10].toList x
148+
(fun j kcontinue s =>
149+
let x := s;
150+
let x := x + i + j;
151+
kcontinue x)
152+
kcontinue)
153+
pure
154+
155+
/--
156+
trace: [Compiler.saveMono] size: 9
157+
def 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 l b : Nat :=
158+
cases l : Nat
159+
| List.nil =>
160+
let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
161+
return _x.3
162+
| List.cons head.4 tail.5 =>
163+
let _x.6 := Nat.add b b;
164+
let x := Nat.add _x.6 s;
165+
let _x.7 := Nat.add x i;
166+
let x := Nat.add _x.7 head.4;
167+
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;
168+
return _x.8
169+
[Compiler.saveMono] size: 9
170+
def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
171+
cases l : Nat
172+
| List.nil =>
173+
let _x.1 := kcontinue b;
174+
return _x.1
175+
| List.cons head.2 tail.3 =>
176+
let _x.4 := Nat.add b b;
177+
let x := Nat.add _x.4 s;
178+
let _x.5 := Nat.add x i;
179+
let x := Nat.add _x.5 head.2;
180+
let _x.6 := List.newForIn._at_.testing3.spec_0 s i kcontinue tail.3 x;
181+
return _x.6
182+
[Compiler.saveMono] size: 9
183+
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 :=
184+
cases l : Nat
185+
| List.nil =>
186+
let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
187+
return _x.3
188+
| List.cons head.4 tail.5 =>
189+
let _x.6 := Nat.add b b;
190+
let x := Nat.add _x.6 s;
191+
let _x.7 := Nat.add x i;
192+
let x := Nat.add _x.7 head.4;
193+
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;
194+
return _x.8
195+
[Compiler.saveMono] size: 9
196+
def testing3 : Nat :=
197+
let x := 42;
198+
let _x.1 := 1;
199+
let _x.2 := 2;
200+
let _x.3 := 3;
201+
let _x.4 := [] ◾;
202+
let _x.5 := List.cons ◾ _x.3 _x.4;
203+
let _x.6 := List.cons ◾ _x.2 _x.5;
204+
let _x.7 := List.cons ◾ _x.1 _x.6;
205+
let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
206+
return _x.8
207+
[Compiler.saveMono] size: 13
208+
def List.newForIn._at_.testing3.spec_1 _x.1 l b : Nat :=
209+
cases l : Nat
210+
| List.nil =>
211+
return b
212+
| List.cons head.2 tail.3 =>
213+
let _x.4 := 10;
214+
let _x.5 := Nat.sub _x.4 head.2;
215+
let _x.6 := Nat.add _x.5 _x.1;
216+
let _x.7 := 1;
217+
let _x.8 := Nat.sub _x.6 _x.7;
218+
let _x.9 := Nat.mul _x.1 _x.8;
219+
let _x.10 := Nat.add head.2 _x.9;
220+
let _x.11 := [] ◾;
221+
let _x.12 := List.range'TR.go _x.1 _x.8 _x.10 _x.11;
222+
let _x.13 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.3 b head.2 _x.12 b;
223+
return _x.13
224+
-/
225+
#guard_msgs in
226+
set_option trace.Compiler.saveMono true in
227+
def testing3 :=
228+
let x := 42;
229+
List.newForIn (β := Nat) (γ := Id Nat)
230+
[1,2,3]
231+
x
232+
(fun i kcontinue s =>
233+
let x := s;
234+
List.newForIn
235+
[i:10].toList x
236+
(fun j kcontinue s =>
237+
-- difference to testing1 here
238+
let x := s + s + x;
239+
let x := x + i + j;
240+
kcontinue x)
241+
kcontinue)
242+
pure

‎tests/lean/run/specFixedHOParamModuloErased.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,4 @@
1-
/--
2-
trace: [Compiler.specialize.info] pmap [true, true, false, true]
3-
[Compiler.specialize.info] pmap [N, N, O, H]
4-
-/
1+
/-- trace: [Compiler.specialize.info] pmap [N, N, O, H] -/
52
#guard_msgs in
63
set_option trace.Compiler.specialize.info true in
74
@[specialize]

0 commit comments

Comments
 (0)