| ;; |
| ;; Lists |
| ;; |
| |
| ;; TODO: enable writing X^n |
| syntax list(syntax X) = X* -- if |X*| < $(2^32) |
| |
| |
| ;; |
| ;; Values |
| ;; |
| |
| ;; Integers |
| |
| syntax byte hint(desc "byte") = 0x00 | ... | 0xFF |
| |
| syntax uN(N) hint(desc "unsigned integer") hint(show u#%) = |
| 0 | ... | $nat$(2^N-1) |
| syntax sN(N) hint(desc "signed integer") hint(show s#%) = |
| -2^(N-1) | ... | -1 | 0 | +1 | ... | 2^(N-1)-1 |
| syntax iN(N) hint(desc "integer") hint(show i#%) = |
| uN(N) |
| |
| syntax u31 = uN(31) |
| syntax u32 = uN(32) |
| syntax u64 = uN(64) |
| |
| 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) |
| def $M(N) = $signif(N) |
| |
| def $E(N) : nat hint(show `E) |
| def $E(N) = $expon(N) |
| |
| syntax fN(N) hint(desc "floating-point number") hint(show f#%) = |
| | POS fNmag(N) hint(show $(+%)) \ |
| | NEG fNmag(N) hint(show $(-%)) |
| |
| syntax exp hint(show e) = 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 $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)) |
| |
| |
| ;; |
| ;; 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 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 labelidx hint(desc "label index") = idx |
| syntax localidx hint(desc "local index") = idx |
| |
| var x : idx |
| var y : idx |
| var l : labelidx |
| |
| |
| ;; Types |
| |
| syntax valtype hint(desc "number type") = |
| | I32 | I64 | F32 | F64 |
| |
| syntax Inn hint(show I#n) = I32 | I64 |
| syntax Fnn hint(show F#n) = F32 | F64 |
| |
| var t : valtype |
| |
| syntax resulttype hint(desc "result type") = |
| valtype? |
| |
| syntax mut = MUT? |
| |
| syntax limits hint(desc "limits") = |
| `[u32 .. u32?] |
| syntax globaltype hint(desc "global type") = |
| mut valtype |
| syntax functype hint(desc "function type") = |
| valtype* -> valtype* |
| syntax tabletype hint(desc "table type") = |
| limits |
| syntax memtype hint(desc "memory type") = |
| limits |
| syntax externtype hint(desc "external type") = |
| | FUNC functype | GLOBAL globaltype | TABLE tabletype | MEM memtype |
| |
| var lim : limits |
| var ft : functype |
| var gt : globaltype |
| var tt : tabletype |
| var mt : memtype |
| var xt : externtype |
| |
| |
| ;; Constants |
| |
| def $size(valtype) : nat hint(show |%|) |
| |
| syntax val_(valtype) |
| syntax val_(Inn) = iN($size(Inn)) |
| syntax val_(Fnn) = fN($size(Fnn)) |
| |
| |
| ;; Operators |
| |
| syntax sx hint(desc "signedness") = U | S |
| syntax sz hint(desc "pack size") = `8 | `16 | `32 | `64 |
| |
| syntax unop_(valtype) |
| syntax unop_(Inn) = CLZ | CTZ | POPCNT |
| syntax unop_(Fnn) = ABS | NEG | SQRT | CEIL | FLOOR | TRUNC | NEAREST |
| |
| syntax binop_(valtype) |
| syntax binop_(Inn) = |
| | ADD | SUB | MUL | DIV sx hint(show DIV_#%) | REM sx hint(show REM_#%) |
| | AND | OR | XOR | SHL | SHR sx hint(show SHR_#%) | ROTL | ROTR |
| syntax binop_(Fnn) = |
| | ADD | SUB | MUL | DIV | MIN | MAX | COPYSIGN |
| |
| syntax testop_(valtype) |
| syntax testop_(Inn) = EQZ |
| ;; syntax testop_(Fnn) = | ;; uninhabited |
| |
| syntax relop_(valtype) |
| syntax relop_(Inn) = |
| | EQ | NE \ |
| | LT sx hint(show LT_#%) | GT sx hint(show GT_#%) \ |
| | LE sx hint(show LE_#%) | GE sx hint(show GE_#%) |
| syntax relop_(Fnn) = |
| | EQ | NE | LT | GT | LE | GE |
| |
| syntax cvtop = |
| | EXTEND sx | WRAP | CONVERT sx | TRUNC sx | PROMOTE | DEMOTE | REINTERPRET |
| |
| |
| ;; Memory operators |
| |
| syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32} |
| |
| var ao : memarg |
| |
| syntax loadop_(valtype) |
| syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $size(Inn) |
| |
| |
| ;; Instructions |
| |
| syntax blocktype hint(desc "block type") = valtype? |
| |
| var bt : blocktype |
| |
| syntax instr/parametric hint(desc "parametric instruction") = |
| | NOP |
| | UNREACHABLE |
| | DROP |
| | SELECT |
| | ... |
| |
| syntax instr/block hint(desc "block instruction") = ... |
| | BLOCK blocktype instr* |
| | LOOP blocktype instr* |
| | IF blocktype instr* ELSE instr* |
| | ... |
| |
| syntax instr/br hint(desc "branch instruction") = ... |
| | BR labelidx |
| | BR_IF labelidx |
| | BR_TABLE labelidx* labelidx |
| | ... |
| |
| syntax instr/call hint(desc "call instruction") = ... |
| | CALL funcidx |
| | CALL_INDIRECT typeidx |
| | RETURN |
| | ... |
| |
| syntax instr/num hint(desc "numeric instruction") = ... |
| | CONST valtype val_(valtype) hint(show %.CONST %) |
| | UNOP valtype unop_(valtype) hint(show %.%) |
| | BINOP valtype binop_(valtype) hint(show %.%) |
| | TESTOP valtype testop_(valtype) hint(show %.%) |
| | RELOP valtype relop_(valtype) hint(show %.%) |
| | CVTOP valtype_1 valtype_2 cvtop hint(show %1.%3#_#%2) |
| -- if valtype_1 =/= valtype_2 |
| | ... |
| |
| syntax instr/local hint(desc "local instruction") = ... |
| | LOCAL.GET localidx |
| | LOCAL.SET localidx |
| | LOCAL.TEE localidx |
| | ... |
| |
| syntax instr/global hint(desc "global instruction") = ... |
| | GLOBAL.GET globalidx |
| | GLOBAL.SET globalidx |
| | ... |
| |
| syntax instr/memory hint(desc "memory instruction") = ... |
| | LOAD valtype loadop_(valtype)? memarg hint(show %.LOAD % %) hint(show %.LOAD# ##% %) |
| | STORE valtype sz? memarg hint(show %.STORE % %) hint(show %.STORE#% %) |
| -- (if valtype = Inn /\ sz < $size(Inn))? |
| | MEMORY.SIZE |
| | MEMORY.GROW |
| |
| syntax expr hint(desc "expression") = |
| instr* |
| |
| syntax instr hint(desc "instruction") |
| |
| var in : instr |
| var e : expr |
| |
| |
| ;; Modules |
| |
| syntax type hint(desc "type") = |
| TYPE functype |
| syntax local hint(desc "local") = |
| LOCAL valtype |
| syntax func hint(desc "function") = |
| FUNC typeidx local* expr |
| syntax global hint(desc "global") = |
| GLOBAL globaltype expr |
| syntax table hint(desc "table") = |
| TABLE tabletype |
| syntax mem hint(desc "memory") = |
| MEMORY memtype |
| syntax elem hint(desc "table segment") = |
| ELEM expr funcidx* |
| syntax data hint(desc "memory segment") = |
| DATA expr byte* |
| syntax start hint(desc "start function") = |
| START funcidx |
| |
| syntax externidx hint(desc "external index") = |
| | FUNC funcidx | GLOBAL globalidx | TABLE tableidx | MEM memidx |
| syntax export hint(desc "export") = |
| EXPORT name externidx |
| syntax import hint(desc "import") = |
| IMPORT name name externtype |
| |
| syntax module hint(desc "module") = |
| MODULE type* import* func* global* table* mem* elem* data* start? export* |
| |
| |
| var ty : type |
| var loc : local |
| var glob : global |
| var tab : table |
| var im : import |
| var ex : export |
| var st : start |
| var xx : externidx |
