{-# 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