7f5fac9d9f
This PR adds a `linter.redundantExpose` option (default `true`) that warns when `@[expose]` or `@[no_expose]` attributes have no effect: - `@[expose]` on `abbrev` (always exposed) or non-Prop `instance` (always exposed) - `@[expose]` on a `def` inside an `@[expose] section` (already exposed by the section) - `@[expose]`/`@[no_expose]` in a non-`module` file (no module system) - `@[no_expose]` on a declaration that wouldn't be exposed by default --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
239 lines
8 KiB
Text
239 lines
8 KiB
Text
import Std.Do.Triple.SpecLemmas
|
||
|
||
@[specialize]
|
||
def List.newForIn (l : List α) (b : β) (kcons : α → (β → γ) → β → γ) (knil : β → γ) : γ :=
|
||
match l with
|
||
| [] => knil b
|
||
| a :: l => kcons a (l.newForIn · kcons knil) b
|
||
|
||
/--
|
||
trace: [Compiler.saveMono] size: 7
|
||
def List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
|
||
return _x.2
|
||
| List.cons head.3 tail.4 =>
|
||
let _x.5 := Nat.add b i;
|
||
let x := Nat.add _x.5 head.3;
|
||
let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
|
||
return _x.6
|
||
[Compiler.saveMono] size: 7
|
||
def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.1 i l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
|
||
return _x.2
|
||
| List.cons head.3 tail.4 =>
|
||
let _x.5 := Nat.add b i;
|
||
let x := Nat.add _x.5 head.3;
|
||
let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
|
||
return _x.6
|
||
[Compiler.saveMono] size: 12
|
||
def List.newForIn._at_.testing.spec_1 l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
return b
|
||
| List.cons head.1 tail.2 =>
|
||
let _x.3 := 1;
|
||
let _x.4 := 10;
|
||
let _x.5 := Nat.sub _x.4 head.1;
|
||
let _x.6 := Nat.add _x.5 _x.3;
|
||
let _x.7 := Nat.sub _x.6 _x.3;
|
||
let _x.8 := Nat.add head.1 _x.7;
|
||
let _x.9 := [] ◾;
|
||
let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
|
||
let _x.11 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.2 head.1 _x.10 b;
|
||
return _x.11
|
||
[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.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
|
||
def testing :=
|
||
let x := 42;
|
||
List.newForIn (β := Nat) (γ := Id Nat)
|
||
[1,2,3]
|
||
x
|
||
(fun i kcontinue s =>
|
||
let x := s;
|
||
List.newForIn
|
||
[i:10].toList x
|
||
(fun j kcontinue s =>
|
||
let x := s;
|
||
let x := x + i + j;
|
||
kcontinue x)
|
||
kcontinue)
|
||
pure
|
||
|
||
|
||
/--
|
||
trace: [Compiler.saveMono] size: 7
|
||
def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
let _x.2 := List.newForIn._at_.testing2.spec_0 tail.1 b;
|
||
return _x.2
|
||
| List.cons head.3 tail.4 =>
|
||
let _x.5 := Nat.add b i;
|
||
let x := Nat.add _x.5 head.3;
|
||
let _x.6 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i tail.4 x;
|
||
return _x.6
|
||
[Compiler.saveMono] size: 14
|
||
def List.newForIn._at_.testing2.spec_0 l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
return b
|
||
| List.cons head.1 tail.2 =>
|
||
let _x.3 := 1;
|
||
let _x.4 := 37;
|
||
let x := Nat.add b _x.4;
|
||
let _x.5 := 10;
|
||
let _x.6 := Nat.sub _x.5 head.1;
|
||
let _x.7 := Nat.add _x.6 _x.3;
|
||
let _x.8 := Nat.sub _x.7 _x.3;
|
||
let _x.9 := Nat.add head.1 _x.8;
|
||
let _x.10 := [] ◾;
|
||
let _x.11 := List.range'TR.go _x.3 _x.8 _x.9 _x.10;
|
||
let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.2 head.1 _x.11 x;
|
||
return _x.12
|
||
[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.7 x;
|
||
return _x.8
|
||
-/
|
||
#guard_msgs in
|
||
set_option trace.Compiler.saveMono true in
|
||
def testing2 :=
|
||
let x := 42;
|
||
List.newForIn (β := Nat) (γ := Id Nat)
|
||
[1,2,3]
|
||
x
|
||
(fun i kcontinue s =>
|
||
-- difference to testing1 here
|
||
let x := s + 37;
|
||
List.newForIn
|
||
[i:10].toList x
|
||
(fun j kcontinue s =>
|
||
let x := s;
|
||
let x := x + i + j;
|
||
kcontinue x)
|
||
kcontinue)
|
||
pure
|
||
|
||
/--
|
||
trace: [Compiler.saveMono] size: 9
|
||
def List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
|
||
return _x.2
|
||
| List.cons head.3 tail.4 =>
|
||
let _x.5 := Nat.add b b;
|
||
let x := Nat.add _x.5 s;
|
||
let _x.6 := Nat.add x i;
|
||
let x := Nat.add _x.6 head.3;
|
||
let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
|
||
return _x.7
|
||
[Compiler.saveMono] size: 9
|
||
def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.1 s i l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
|
||
return _x.2
|
||
| List.cons head.3 tail.4 =>
|
||
let _x.5 := Nat.add b b;
|
||
let x := Nat.add _x.5 s;
|
||
let _x.6 := Nat.add x i;
|
||
let x := Nat.add _x.6 head.3;
|
||
let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
|
||
return _x.7
|
||
[Compiler.saveMono] size: 12
|
||
def List.newForIn._at_.testing3.spec_1 l b : Nat :=
|
||
cases l : Nat
|
||
| List.nil =>
|
||
return b
|
||
| List.cons head.1 tail.2 =>
|
||
let _x.3 := 1;
|
||
let _x.4 := 10;
|
||
let _x.5 := Nat.sub _x.4 head.1;
|
||
let _x.6 := Nat.add _x.5 _x.3;
|
||
let _x.7 := Nat.sub _x.6 _x.3;
|
||
let _x.8 := Nat.add head.1 _x.7;
|
||
let _x.9 := [] ◾;
|
||
let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
|
||
let _x.11 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.2 b head.1 _x.10 b;
|
||
return _x.11
|
||
[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.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
|
||
def testing3 :=
|
||
let x := 42;
|
||
List.newForIn (β := Nat) (γ := Id Nat)
|
||
[1,2,3]
|
||
x
|
||
(fun i kcontinue s =>
|
||
let x := s;
|
||
List.newForIn
|
||
[i:10].toList x
|
||
(fun j kcontinue s =>
|
||
-- difference to testing1 here
|
||
let x := s + s + x;
|
||
let x := x + i + j;
|
||
kcontinue x)
|
||
kcontinue)
|
||
pure
|