specification/wasm-latest/1.1-syntax.values.spectec

;;
;; Syntax of Values
;;

;; Integers

syntax bit  hint(desc "bit") = 0 | 1
syntax byte hint(desc "byte") = 0x00 | ... | 0xFF

syntax uN(N) hint(desc "unsigned integer") hint(show u#%) hint(macro "uNX") =
  0 | ... | $nat$(2^N-1)
syntax sN(N) hint(desc "signed integer") hint(show s#%) hint(macro "sNX") =
  -2^(N-1) | ... | -1 | 0 | +1 | ... | +2^(N-1)-1
syntax iN(N) hint(desc "integer") hint(show i#%) hint(macro "iNX") =
  uN(N)

syntax u8  = uN(`8)
syntax u16 = uN(`16)
syntax u31 = uN(`31)
syntax u32 = uN(`32)
syntax u64 = uN(`64)
syntax s33 = sN(`33)
syntax i32 = iN(`32)
syntax i64 = iN(`64)
syntax i128 = iN(`128)

var b : byte


;; Floating-point

def $signif(N) : nat
def $signif(32) = 23
def $signif(64) = 52

def $expon(N) : nat
def $expon(32) = 8
def $expon(64) = 11

def $M(N) : nat hint(show `M) hint(macro none)
def $M(N) = $signif(N)

def $E(N) : nat hint(show `E) hint(macro none)
def $E(N) = $expon(N)

syntax fN(N) hint(desc "floating-point number") hint(show f#%) hint(macro "fNX") =
  | POS fNmag(N)  hint(show $(+%)) \
  | NEG fNmag(N)  hint(show $(-%))

syntax exp hint(show e) hint(macro none) = int
syntax fNmag(N) hint(desc "floating-point magnitude") hint(show fNmag) =
  | NORM m exp   hint(show $((1 + %*2^(-$M(N))) * 2^%))   -- if $(m < 2^$M(N) /\ 2-2^($E(N)-1) <= exp <= 2^($E(N)-1)-1)
  | SUBNORM m    hint(show $((0 + %*2^(-$M(N))) * 2^exp)) -- if $(m < 2^$M(N) /\ 2-2^($E(N)-1) = exp)
  | INF          hint(show infinity)
  | NAN (m)      hint(show NAN#(%))                       -- if $(1 <= m < 2^$M(N))

syntax f32 = fN(`32)
syntax f64 = fN(`64)

def $fzero(N) : fN(N) hint(show $(+0))
def $fzero(N) = POS (SUBNORM 0)

def $fnat(N, nat) : fN(N)  hint(show $(+%2))
def $fnat(N, n) = POS (NORM n 0)

def $fone(N) : fN(N)  hint(show $(+1))
def $fone(N) = POS (NORM 1 0)

def $canon_(N) : nat
def $canon_(N) = $(2^($signif(N)-1))


;; Vectors

syntax vN(N) hint(desc "vector") hint(show v#%) hint(macro "vNX") =
  uN(N)

syntax v128 = vN(`128)


;; Lists

;; TODO(3, rossberg): enable writing X^n
syntax list(syntax X) = X*  -- if |X*| < $(2^32)


;; Names

syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF

def $utf8(char*) : byte*

syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)

var nm : name


;; Indices

syntax idx hint(desc "index") = u32
syntax laneidx hint(desc "lane index") = u8

syntax typeidx hint(desc "type index") = idx
syntax funcidx hint(desc "function index") = idx
syntax globalidx hint(desc "global index") = idx
syntax tableidx hint(desc "table index") = idx
syntax memidx hint(desc "memory index") = idx
syntax tagidx hint(desc "tag index") = idx
syntax elemidx hint(desc "elem index") = idx
syntax dataidx hint(desc "data index") = idx
syntax labelidx hint(desc "label index") = idx
syntax localidx hint(desc "local index") = idx
syntax fieldidx hint(desc "field index") = idx

syntax externidx hint(desc "external index") hint(macro "%" "XX%") =
  | FUNC funcidx | GLOBAL globalidx | TABLE tableidx | MEM memidx | TAG tagidx

var x : idx
var y : idx
var l : labelidx
var xx : externidx
var x33 : s33 hint(show x)


;; Sort projection

;; TODO(3, rossberg): add built-in notation for comprehensions?

def $funcsxx(externidx*) : typeidx*      hint(show $funcs(%))   hint(macro "funcsxx")
def $globalsxx(externidx*) : globalidx*  hint(show $globals(%)) hint(macro "globalsxx")
def $tablesxx(externidx*) : tableidx*    hint(show $tables(%))  hint(macro "tablesxx")
def $memsxx(externidx*) : memidx*        hint(show $mems(%))    hint(macro "memsxx")
def $tagsxx(externidx*) : tagidx*        hint(show $tags(%))    hint(macro "tagsxx")

def $funcsxx(eps) = eps
def $funcsxx((FUNC x) xx*) = x $funcsxx(xx*)
def $funcsxx(externidx xx*) = $funcsxx(xx*)  -- otherwise

def $globalsxx(eps) = eps
def $globalsxx((GLOBAL x) xx*) = x $globalsxx(xx*)
def $globalsxx(externidx xx*) = $globalsxx(xx*)  -- otherwise

def $tablesxx(eps) = eps
def $tablesxx((TABLE x) xx*) = x $tablesxx(xx*)
def $tablesxx(externidx xx*) = $tablesxx(xx*)  -- otherwise

def $memsxx(eps) = eps
def $memsxx((MEM x) xx*) = x $memsxx(xx*)
def $memsxx(externidx xx*) = $memsxx(xx*)  -- otherwise

def $tagsxx(eps) = eps
def $tagsxx((TAG x) xx*) = x $tagsxx(xx*)
def $tagsxx(externidx xx*) = $tagsxx(xx*)  -- otherwise


;; Free indices

syntax free =
  { TYPES typeidx*,
    FUNCS funcidx*,
    GLOBALS globalidx*,
    TABLES tableidx*,
    MEMS memidx*,
    ELEMS elemidx*,
    DATAS dataidx*,
    LOCALS localidx*,
    LABELS labelidx*,
    TAGS tagidx*
  }


def $free_opt(free?) : free
def $free_list(free*) : free

def $free_opt(eps) = {}
def $free_opt(free) = free

def $free_list(eps) = {}
def $free_list(free free'*) = free ++ $free_list(free'*)


def $free_typeidx(typeidx) : free
def $free_funcidx(funcidx) : free
def $free_globalidx(globalidx) : free
def $free_tableidx(tableidx) : free
def $free_memidx(memidx) : free
def $free_elemidx(elemidx) : free
def $free_dataidx(dataidx) : free
def $free_localidx(localidx) : free
def $free_labelidx(labelidx) : free
def $free_externidx(externidx) : free
def $free_tagidx(tagidx) : free

def $free_typeidx(typeidx) = {TYPES typeidx}
def $free_funcidx(funcidx) = {FUNCS funcidx}
def $free_globalidx(globalidx) = {GLOBALS globalidx}
def $free_tableidx(tableidx) = {TABLES tableidx}
def $free_memidx(memidx) = {MEMS memidx}
def $free_elemidx(elemidx) = {ELEMS elemidx}
def $free_dataidx(dataidx) = {DATAS dataidx}
def $free_localidx(localidx) = {LOCALS localidx}
def $free_labelidx(labelidx) = {LABELS labelidx}
def $free_tagidx(tagidx) = {TAGS tagidx}

def $free_externidx(FUNC funcidx) = $free_funcidx(funcidx)
def $free_externidx(GLOBAL globalidx) = $free_globalidx(globalidx)
def $free_externidx(TABLE tableidx) = $free_tableidx(tableidx)
def $free_externidx(MEM memidx) = $free_memidx(memidx)
def $free_externidx(TAG tagidx) = $free_tagidx(tagidx)