d56424b587
This PR introduces the `weak_specialize` attribute. Unlike the `nospecialize` attribute it does not block specialization for parameters marked with this type completely. Instead, `weak_specialize` parameters are only specialized for if another parameter provokes specialization. If no such parameter exists, they are treated like `nospecialize`.
34 lines
969 B
Text
34 lines
969 B
Text
module
|
||
|
||
public section
|
||
|
||
/-!
|
||
This test checks that weak_specialize:
|
||
- doesn't trigger specialization on its own
|
||
- does get included in specialization if other parameters provoke specialization
|
||
- does not affect the semantics of nospecialize parameters
|
||
-/
|
||
|
||
@[weak_specialize] class MyWeak (α : Type) where
|
||
val : α
|
||
|
||
/-- -/
|
||
#guard_msgs in
|
||
set_option trace.Compiler.specialize.info true in
|
||
def weakOnly [MyWeak α] (x : α) : α := x
|
||
|
||
class MyStrong (α : Type) where
|
||
op : α → α
|
||
|
||
/-- trace: [Compiler.specialize.info] weakAndStrong [N, W, I, O] -/
|
||
#guard_msgs in
|
||
set_option trace.Compiler.specialize.info true in
|
||
def weakAndStrong [MyWeak α] [MyStrong α] (x : α) : α := MyStrong.op x
|
||
|
||
@[nospecialize] class MyNoSpec (α : Type) where
|
||
val : α
|
||
|
||
/-- trace: [Compiler.specialize.info] nospecAndStrong [N, O, I, O] -/
|
||
#guard_msgs in
|
||
set_option trace.Compiler.specialize.info true in
|
||
def nospecAndStrong [MyNoSpec α] [MyStrong α] (x : α) : α := MyStrong.op x
|