feat: Protocol checking#1765
Conversation
|
| Branch | cr/proto-check |
| Testbed | Linux |
Click to view all benchmark results
| Benchmark | hugr_bytes | Benchmark Result bytes x 1e3 (Result Δ%) | Upper Boundary bytes x 1e3 (Limit %) | hugr_nodes | Benchmark Result nodes (Result Δ%) | Upper Boundary nodes (Limit %) |
|---|---|---|---|---|---|---|
| tests/benchmarks/test_big_array.py::test_big_array_compile | 📈 view plot 🚷 view threshold | 158.77 x 1e3(0.00%)Baseline: 158.77 x 1e3 | 160.36 x 1e3 (99.01%) | 📈 view plot 🚷 view threshold | 6,641.00(0.00%)Baseline: 6,641.00 | 6,707.41 (99.01%) |
| tests/benchmarks/test_ctrl_flow.py::test_many_ctrl_flow_compile | 📈 view plot 🚷 view threshold | 27.53 x 1e3(0.00%)Baseline: 27.53 x 1e3 | 27.81 x 1e3 (99.01%) | 📈 view plot 🚷 view threshold | 1,074.00(0.00%)Baseline: 1,074.00 | 1,084.74 (99.01%) |
| tests/benchmarks/test_queue_push_pop.py::test_queue_push_benchmark_compile | 📈 view plot 🚷 view threshold | 10.91 x 1e3(0.00%)Baseline: 10.91 x 1e3 | 11.02 x 1e3 (99.01%) | 📈 view plot 🚷 view threshold | 308.00(0.00%)Baseline: 308.00 | 311.08 (99.01%) |
| tests/benchmarks/test_queue_push_pop.py::test_queue_push_pop_benchmark_compile | 📈 view plot 🚷 view threshold | 14.84 x 1e3(0.00%)Baseline: 14.84 x 1e3 | 14.98 x 1e3 (99.01%) | 📈 view plot 🚷 view threshold | 435.00(0.00%)Baseline: 435.00 | 439.35 (99.01%) |
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #1765 +/- ##
==========================================
+ Coverage 92.98% 93.30% +0.32%
==========================================
Files 135 136 +1
Lines 13053 13278 +225
==========================================
+ Hits 12137 12389 +252
+ Misses 916 889 -27 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
mark-koch
left a comment
There was a problem hiding this comment.
🔥 🔥 🔥
Sorry I didn't have the time to look through everything in detail yet, but here are some comments from a first read through. Will have a closer look next week
| if isinstance(defn, ParsedProtocolDef): | ||
| assert isinstance(func_ty, FunctionType) | ||
| raise GuppyError( | ||
| UnsupportedError( | ||
| node.func, "Checking protocol method calls", singular=True | ||
| ) | ||
| ) | ||
| raise RequiresMonomorphizationError |
There was a problem hiding this comment.
Why would defn ever be a ParsedProtocolDef?
There was a problem hiding this comment.
Ah I see because attribute accesses are turned into Global names with the protocol id.
I think it would be better to add a new node type that holds a protocol id and the name of the method that is used. Then we wouldn't need to cop out here
| member_ty, | ||
| with_loc( | ||
| node, | ||
| GlobalName(id=member_name, def_id=proto.def_id), |
There was a problem hiding this comment.
Returning a global name with the id of the full protocol feels a bit weird. Don't we want some sort of identifier for wich method of the protocol is used?
| "Self", copyable=self_ty_head.copyable, droppable=self_ty_head.droppable | ||
| "Self", copyable=True, droppable=True |
| ) | ||
|
|
||
|
|
||
| def handle_implicit_proto_self_arg( |
There was a problem hiding this comment.
Could you add a docstring explaining what this function does
|
|
||
|
|
||
| @dataclass(frozen=True) | ||
| class ImplProofBase(ABC): |
There was a problem hiding this comment.
Also docstrings for the things in this file
| 6 | def foo(self) -> None: ... | ||
| | ^^^^ Inference of type for `self` is not supported in protocol | ||
| | methods |
There was a problem hiding this comment.
Imo better to use the regular MissingArgAnnotationError error (maybe with a note that self inference on protcols is not supported)
| 5 | class Foo: | ||
| 6 | @guppy.require | ||
| 7 | def foo(n: nat) -> None: ... | ||
| | ^^^ `n` must be of type `self` |
There was a problem hiding this comment.
Self (captitalised) or Foo?
| 23 | @guppy | ||
| 24 | def baz(f: FooInt) -> None: | ||
| 25 | return eat_foostr(f) | ||
| | ^ Type `FooInt` does not implement protocol `Foo` |
There was a problem hiding this comment.
Shouldnt it be "does not implement protocol Foo[str]"?
| 5 | class Proto[T]: | ||
| 6 | @guppy.require | ||
| 7 | def foo[T](t: T) -> T: ... | ||
| | ^^^^ Type `T` does not implement protocol `Proto` |
There was a problem hiding this comment.
A nice future improvement would be to add notes explaining why the protocol is not implemented
| ## TODO: See if this can work in light of the monomorphisation changes assuming | ||
| ## check and compile are called on entrypoints |
There was a problem hiding this comment.
Are these TODOs resolved?
Closes #1396, closes #1210, closes #1653