1 files changed, 219 insertions, 0 deletions
diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
new file mode 100644
index 0000000..6cd006b
--- /dev/null
+++ b/src/Wasm/Expression/Instructions.agda
@@ -0,0 +1,219 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- 2.4 Types
+
+module Wasm.Expression.Instructions where
+
+open import Data.List using (List)
+open import Data.Maybe using (Maybe)
+open import Data.Product using (∃)
+open import Data.Sum using (_⊎_)
+open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float)
+open import Wasm.Expression.Types using (ValType; RefType)
+open import Wasm.Expression.Utilities
+
+------------------------------------------------------------------------
+-- 2.4.1 Numeric Instructions
+
+module IntOp (w : BitWidth) where
+  data Unary : Set where
+    clz    : Unary
+    ctz    : Unary
+    popcnt : Unary
+
+  data Binary : Set where
+    add  : Binary
+    sub  : Binary
+    mul  : Binary
+    div  : Signedness → Binary
+    rem  : Signedness → Binary
+    and  : Binary
+    or   : Binary
+    xor  : Binary
+    shl  : Binary
+    shr  : Signedness → Binary
+    rotl : Binary
+    rotr : Binary
+
+  data Test : Set where
+    eqz : Test
+
+  data Rel : Set where
+    eq : Rel
+    ne : Rel
+    lt : Signedness → Rel
+    gt : Signedness → Rel
+    le : Signedness → Rel
+    ge : Signedness → Rel
+
+  data IntInstr : Set where
+    const         : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr
+    iunop         : Unary → IntInstr
+    ibinop        : Binary → IntInstr
+    itestop       : Test → IntInstr
+    irelop        : Rel → IntInstr
+    extend8-s     : IntInstr
+    extend16-s    : IntInstr
+    trunc-f       : BitWidth → Signedness → IntInstr
+    trunc-sat-f   : BitWidth → Signedness → IntInstr
+    reinterpret-f : IntInstr
+
+data IntInstr : Set where
+  ixx            : ∀ w → IntOp.IntInstr w → IntInstr
+  i64-extend32-s : IntInstr
+  i32-wrap-i64   : IntInstr
+  i64-extend-i32 : Signedness → IntInstr
+
+module FloatOp (w : BitWidth) where
+  data Unary : Set where
+    abs     : Unary
+    neg     : Unary
+    sqrt    : Unary
+    ceil    : Unary
+    floor   : Unary
+    trunc   : Unary
+    nearest : Unary
+
+  data Binary : Set where
+    add      : Binary
+    sub      : Binary
+    mul      : Binary
+    div      : Binary
+    min      : Binary
+    max      : Binary
+    copysign : Binary
+
+  data Rel : Set where
+    eq : Rel
+    ne : Rel
+    lt : Rel
+    gt : Rel
+    le : Rel
+    ge : Rel
+
+  data FloatInstr : Set where
+    const         : Float w → FloatInstr
+    funop         : Unary → FloatInstr
+    fbinop        : Binary → FloatInstr
+    frelop        : Rel → FloatInstr
+    convert-i     : BitWidth → Signedness → FloatInstr
+    reinterpret-i : FloatInstr
+
+data FloatInstr : Set where
+  fxx             : ∀ w → FloatOp.FloatInstr w → FloatInstr
+  f32-demote-f64  : FloatInstr
+  f64-promote-f32 : FloatInstr
+
+data NumInstr : Set where
+  int   : IntInstr → NumInstr
+  float : FloatInstr → NumInstr
+
+------------------------------------------------------------------------
+-- 2.4.2 Reference Instructions
+
+data RefInstr : Set where
+  null    : RefType → RefInstr
+  is-null : RefInstr
+  func    : Indices.FuncIdx → RefInstr
+
+------------------------------------------------------------------------
+-- 2.4.3 Parametric Instructions
+
+data ParametricInstr : Set where
+  drop   : ParametricInstr
+  select : List ValType → ParametricInstr
+
+------------------------------------------------------------------------
+-- 2.4.4 Variable Instructions
+
+data VarInstr : Set where
+  local-get  : Indices.LocalIdx → VarInstr
+  local-set  : Indices.LocalIdx → VarInstr
+  local-tee  : Indices.LocalIdx → VarInstr
+  global-get : Indices.GlobalIdx → VarInstr
+  global-set : Indices.GlobalIdx → VarInstr
+
+------------------------------------------------------------------------
+-- 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
+
+------------------------------------------------------------------------
+-- 2.4.6 Memory Instructions
+
+record MemArg : Set where
+  field
+    offset : UnsignedInteger 32
+    align  : UnsignedInteger 32
+
+module IntMem (w : BitWidth) where
+  data IntMemInstr : Set where
+    load    : MemArg → IntMemInstr
+    store   : MemArg → IntMemInstr
+    load8   : Signedness → MemArg → IntMemInstr
+    load16  : Signedness → MemArg → IntMemInstr
+    store8  : MemArg → IntMemInstr
+    store16 : MemArg → IntMemInstr
+
+data IntMemInstr : Set where
+  ixx         : ∀ w → IntMem.IntMemInstr w → IntMemInstr
+  i64-load32  : Signedness → MemArg → IntMemInstr
+  i64-store32 : MemArg → IntMemInstr
+
+module FloatMem (w : BitWidth) where
+  data FloatMemInstr : Set where
+    load  : MemArg → FloatMemInstr
+    store : MemArg → FloatMemInstr
+
+FloatMemInstr : Set
+FloatMemInstr = ∃ FloatMem.FloatMemInstr
+
+data MemInstr : Set where
+  int   : IntMemInstr → MemInstr
+  float : FloatMemInstr → MemInstr
+  size  : MemInstr
+  grow  : MemInstr
+  fill  : MemInstr
+  copy  : MemInstr
+  init  : Indices.DataIdx → MemInstr
+  drop  : Indices.DataIdx → MemInstr
+
+------------------------------------------------------------------------
+-- 2.4.7 Control Instructions
+
+BlockType : Set
+BlockType = Indices.TypeIdx ⊎ Maybe ValType
+
+data Instr : Set where
+  num           : NumInstr → Instr
+  ref           : RefInstr → Instr
+  parametric    : ParametricInstr → Instr
+  var           : VarInstr → Instr
+  table         : TableInstr → Instr
+  mem           : MemInstr → Instr
+  nop           : Instr
+  unreachable   : Instr
+  block         : BlockType → List Instr → Instr
+  loop          : BlockType → List Instr → Instr
+  if-else       : BlockType → List Instr → List Instr → Instr
+  br            : Indices.LabelIdx → Instr
+  br-if         : Indices.LabelIdx → Instr
+  br-table      : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr
+  return        : Instr
+  call          : Indices.FuncIdx → Instr
+  call_indirect : Indices.TableIdx → Indices.TypeIdx → Instr
+
+------------------------------------------------------------------------
+-- 2.4.8 Expressions
+
+Expr : Set
+Expr = List Instr