diff options
Diffstat (limited to 'src/Wasm/Expression/Instructions.agda')
-rw-r--r-- | src/Wasm/Expression/Instructions.agda | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda index 6cd006b..3fa96be 100644 --- a/src/Wasm/Expression/Instructions.agda +++ b/src/Wasm/Expression/Instructions.agda @@ -122,7 +122,7 @@ data RefInstr : Set where data ParametricInstr : Set where drop : ParametricInstr - select : List ValType → ParametricInstr + select : Maybe (List ValType) → ParametricInstr ------------------------------------------------------------------------ -- 2.4.4 Variable Instructions @@ -138,14 +138,14 @@ data VarInstr : Set where -- 2.4.5 Table Instructions data TableInstr : Set where - table-get : Indices.TableIdx → TableInstr - table-set : Indices.TableIdx → TableInstr - table-size : Indices.TableIdx → TableInstr - table-grow : Indices.TableIdx → TableInstr - table-fill : Indices.TableIdx → TableInstr - table-copy : Indices.TableIdx → Indices.TableIdx → TableInstr - table-init : Indices.TableIdx → Indices.ElemIdx → TableInstr - elem-drop : Indices.ElemIdx → TableInstr + get : Indices.TableIdx → TableInstr + set : Indices.TableIdx → TableInstr + size : Indices.TableIdx → TableInstr + grow : Indices.TableIdx → TableInstr + fill : Indices.TableIdx → TableInstr + copy : Indices.TableIdx → Indices.TableIdx → TableInstr + init : Indices.TableIdx → Indices.ElemIdx → TableInstr + drop : Indices.ElemIdx → TableInstr ------------------------------------------------------------------------ -- 2.4.6 Memory Instructions @@ -210,7 +210,7 @@ data Instr : Set where br-table : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr return : Instr call : Indices.FuncIdx → Instr - call_indirect : Indices.TableIdx → Indices.TypeIdx → Instr + call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr ------------------------------------------------------------------------ -- 2.4.8 Expressions |