Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions specification/wasm-3.0/1.2-syntax.types.spectec
Original file line number Diff line number Diff line change
Expand Up @@ -197,7 +197,7 @@ def $size(numtype) : nat hint(show |%|)
def $vsize(vectype) : nat hint(show |%|)
def $psize(packtype) : nat hint(show |%|)
def $lsize(lanetype) : nat hint(show |%|)
def $zsize(storagetype) : nat hint(show |%|)
def $zsize(storagetype) : nat hint(show |%|) hint(partial)
def $isize(Inn) : nat hint(show |%|) hint(inverse $inv_isize)
def $jsize(Jnn) : nat hint(show |%|) hint(inverse $inv_jsize)
def $fsize(Fnn) : nat hint(show |%|) hint(inverse $inv_fsize)
Expand Down Expand Up @@ -297,7 +297,7 @@ def $diffrt((REF null_1? ht_1), (REF NULL ht_2)) = (REF ht_1)
def $diffrt((REF null_1? ht_1), (REF ht_2)) = (REF null_1? ht_1)

;; TODO(3, rossberg): Could this be inferable as a narrowing coercion?
def $as_deftype(typeuse) : deftype hint(show %)
def $as_deftype(typeuse) : deftype hint(show %) hint(partial)
def $as_deftype(dt) = dt


Expand Down Expand Up @@ -494,13 +494,13 @@ def $free_comptype(comptype) : free
def $free_subtype(subtype) : free
def $free_rectype(rectype) : free

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

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.

def $free_globaltype(globaltype) : free
def $free_memtype(memtype) : free
def $free_tabletype(tabletype) : free
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

Choose a reason for hiding this comment

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

Same here.

def $free_moduletype(moduletype) : free


Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-3.0/3.1-numerics.scalar.spectec
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ def $inv_signed_(N, i) = i -- if $(0 <= i < 2^(N-1))
def $inv_signed_(N, i) = $(i + 2^N) -- if $(-2^(N-1) <= i < 0)


def $sx(storagetype) : sx? hint(show $sx(%))
def $sx(storagetype) : sx? hint(show $sx(%)) hint(partial)
def $sx(consttype) = eps
def $sx(packtype) = S

Expand Down
69 changes: 37 additions & 32 deletions spectec/test-middlend/specification.03-totalize.exp

Large diffs are not rendered by default.

75 changes: 40 additions & 35 deletions spectec/test-middlend/specification.04-else.exp

Large diffs are not rendered by default.

88 changes: 53 additions & 35 deletions spectec/test-middlend/specification.05-sideconditions.exp

Large diffs are not rendered by default.

88 changes: 53 additions & 35 deletions spectec/test-middlend/specification.06-sub.exp

Large diffs are not rendered by default.

88 changes: 53 additions & 35 deletions spectec/test-middlend/specification.07-alias-demut.exp

Large diffs are not rendered by default.

Loading