Skip to content

mark zsize and as_deftype as partial #199

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
nomeata wants to merge 1 commit into from
Closed

mark zsize and as_deftype as partial #199

nomeata wants to merge 1 commit into from

Conversation

@nomeata
Copy link

@nomeata nomeata commented Nov 13, 2025

these functions seem to be partial, as uncovered by #195.

rossberg
rossberg reviewed Nov 13, 2025
View reviewed changes
specification/wasm-3.0/1.2-syntax.types.spectec
def $free_rectype(rectype) : free

def $free_tagtype(tagtype) : free
def $free_tagtype(tagtype) : free hint(partial)
Copy link
Collaborator

@rossberg rossberg Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, this is annoying. I think we should rather add the missing cases to free_deftype.

specification/wasm-3.0/1.2-syntax.types.spectec
def $free_datatype(datatype) : free
def $free_elemtype(elemtype) : free
def $free_externtype(externtype) : free
def $free_externtype(externtype) : free hint(partial)
Copy link
Collaborator

@rossberg rossberg Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here.

@nomeata nomeata marked this pull request as draft November 13, 2025 14:51
@nomeata nomeata force-pushed the joachim-rqmusqmykons branch from 80b307f to edba519 Compare November 13, 2025 15:24
@DCupello1
Copy link

DCupello1 commented Nov 13, 2025 •
edited
Loading

Just noting another case that is partial (that I found due to Rocq complaining):
In 1.2-syntax.types.spectec:

def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*)
def $minus_recs(eps, eps) = (eps, eps)
def $minus_recs((REC n) tv*, tu_1 tu*) = $minus_recs(tv*, tu*)
def $minus_recs((_IDX x) tv*, tu_1 tu*) = ((_IDX x) tv'*, tu_1 tu'*)
  -- if (tv'*, tu'*) = $minus_recs(tv*, tu*)

Probably want to add the missing cases here too

@nomeata nomeata closed this Nov 13, 2025
@DCupello1
Copy link

DCupello1 commented Nov 20, 2025

Just curious, why did this get closed?

@nomeata
Copy link
Author

nomeata commented Nov 20, 2025

I closed it because the proper solution is different:

I think we should rather add the missing cases to free_deftype.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rossberg rossberg rossberg left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@nomeata @DCupello1 @rossberg