Initial implementation of resource type validation#192
Initial implementation of resource type validation#192pl-semiotics wants to merge 1 commit intomainfrom
Conversation
|
Sorry for the slow reply, but excited to check this out! Could you perhaps add a README.md to the |
|
One other thing that would be super-useful is to see if this reference interpreter can run the tests in |
lukewagner
left a comment
lukewagner
left a comment
There was a problem hiding this comment.
Lots of great tests in there! Just a few nits and a question.
| (type $t (resource (rep i32))) | ||
| (component | ||
| (alias outer $C $t (type)))) | ||
| "Cannot export type containing bare resource type") |
There was a problem hiding this comment.
Might be nice to distinguish this case in the error string (e.g. "Cannot outer alias resource types across components" or something)
| ) | ||
|
|
||
| (component | ||
| (instance $deftype (instantiate $dt)) | ||
| (instance (instantiate $use2c | ||
| (with "deftype" (instance $deftype)) | ||
| (with "two" (component $use1))))) |
There was a problem hiding this comment.
It seems like this test is missing a final part that, e.g., requires one and two to have the same function type.
| (component | ||
| (instance (instantiate $needs_dt2i_backwards | ||
| (with "deftype" (component $dt2))))) | ||
| "Type variable u0.0 is not u0.1") |
There was a problem hiding this comment.
Perhaps also add an invalid testcase that tries to import one and two with the same resource type?
| (instance $ii (instantiate $in)) | ||
| (alias export $ii "t" (type $t)) | ||
| (export "t" (type $t))) | ||
| "Component type may not refer to non-imported uvar") |
There was a problem hiding this comment.
I would think that the problem here was the lack of ascribed type, but if you did ascribe a (sub resource) type, it would be valid, and thus the error of "may not refer to non-imported uvar" doesn't make sense to me.
lukewagner
force-pushed
the
main
branch
3 times, most recently
from
824fdc5 to
74bd278
Compare
2 participants
This adds a relatively direct OCaml implementation of the current formalisation (essentially that given in #101), focusing on the rules around how resource types are treated as creating quantified component types.
It is designed to layer cleanly around the Core WebAssembly reference interpreter, but presently requires minor changes to expose certain parsing-related information and entrypoints.