{-# OPTIONS --safe --without-K #-}

module Wasm.Data.Instruction where

open import Data.Fin using (Fin)
open import Data.List using (List; []; _∷_; _++_; length; lookup)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All)
open import Data.Maybe using (Maybe; just)
open import Data.Nat using (ℕ; suc; _>_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Wasm.Type
open import Wasm.Value

infixr 4 _∙_ _∙₁_ _∙₂_

record Context : Set where
  field
    funcs   : List FuncType
    tables  : List TableType
    mems    : List MemType
    globals : List GlobalType
    elems   : List RefType
    datas   : ℕ
    locals  : List ValType
    labels  : List (List ValType)
    return  : Maybe (List ValType)
    refs    : List (Fin (length funcs))

data Signedness : Set where
  signed   : Signedness
  unsigned : Signedness

module i32 where
  data Unary : Set where
    clz        : Unary
    ctz        : Unary
    popcnt     : Unary
    extend8-s  : Unary
    extend16-s : 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 Convert : NumType → Set where
    wrap          : Convert i64
    trunc-f32     : Signedness → Convert f32
    trunc-f64     : Signedness → Convert f64
    trunc-sat-f32 : Signedness → Convert f32
    trunc-sat-f64 : Signedness → Convert f64
    reinterpret   : Convert f32

module i64 where
  data Unary : Set where
    clz        : Unary
    ctz        : Unary
    popcnt     : Unary
    extend8-s  : Unary
    extend16-s : Unary
    extend32-s : 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 Convert : NumType → Set where
    extend        : Convert i32
    trunc-f32     : Signedness → Convert f32
    trunc-f64     : Signedness → Convert f64
    trunc-sat-f32 : Signedness → Convert f32
    trunc-sat-f64 : Signedness → Convert f64
    reinterpret   : Convert f64

module f32 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 Convert : NumType → Set where
    demote      : Convert f64
    convert-i32 : Convert i32
    convert-i64 : Convert i64
    reinterpret : Convert i32

module f64 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 Convert : NumType → Set where
    promote     : Convert f32
    convert-i32 : Convert i32
    convert-i64 : Convert i64
    reinterpret : Convert i64

record MemArg (t : ℕ): Set where
  field
    offset : I32
    align  : Fin (suc t)

data BlockType : Context → Set where
  idx : ∀ {C} → FuncType → BlockType C
  val : ∀ {C} → ValType → BlockType C
  nothing : ∀ {C} → BlockType C

blockTypeAsFunc : ∀ {C} → BlockType C → FuncType
blockTypeAsFunc {C} (idx τ) = τ
blockTypeAsFunc (val x) = [] ⟶ x ∷ []
blockTypeAsFunc nothing = [] ⟶ []

data Instruction (C : Context) : FuncType → Set
data Sequence (C : Context) : FuncType → Set

data Instruction C where
  ---- Numeric instructions
  -- const
  i32-const : (c : I32) → Instruction C ([] ⟶ num i32 ∷ [])
  i64-const : (c : I64) → Instruction C ([] ⟶ num i64 ∷ [])
  f32-const : (c : F32) → Instruction C ([] ⟶ num f32 ∷ [])
  f64-const : (c : F64) → Instruction C ([] ⟶ num f64 ∷ [])
  -- unop
  i32-unop : (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-unop : (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ [])
  f32-unop : (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ [])
  f64-unop : (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ [])
  -- binop
  i32-binop : (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-binop : (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ [])
  f32-binop : (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ [])
  f64-binop : (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ [])
  -- testop
  i32-testop : (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-testop : (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ [])
  -- relop
  i32-relop : (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-relop : (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ [])
  f32-relop : (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ [])
  f64-relop : (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ [])
  -- cvtop
  i32-cvtop : ∀ {τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ [])
  i64-cvtop : ∀ {τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ [])
  f32-cvtop : ∀ {τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ [])
  f64-cvtop : ∀ {τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ [])

  ---- Reference instructions
  ref-null : ∀ τ → Instruction C ([] ⟶ ref τ ∷ [])
  ref-is-null : ∀ {τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ [])
  ref-func : ∀ {x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ [])

  ---- Parametric instructions
  drop : ∀ {τ} → Instruction C (τ ∷ [] ⟶ [])
  select : ∀ {τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ [])

  ---- Variable instructions
  local-get : ∀ x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ [])
  local-set : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ [])
  local-tee : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ [])
  global-get : ∀ x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ [])
  global-set : ∀ x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ [])

  ---- Table instructions
  table-get : ∀ x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ [])
  table-set : ∀ x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
  table-size : ∀ (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ [])
  table-grow : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ [])
  table-fill : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
  table-copy : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  table-init : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  elem-drop : ∀ (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ [])

  ---- Memory instructions
  -- load
  i32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  f32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ [])
  f64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ [])
  -- loadN
  i32-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i32-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  i64-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  i64-load32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  -- store
  i32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  f32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ [])
  f64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ [])
  -- storeN
  i32-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i32-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i64-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  i64-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  i64-store32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  -- other
  memory-size : length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ [])
  memory-grow : length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  memory-fill : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  memory-copy : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  memory-init : (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  data-drop : (x : Fin (Context.datas C)) → Instruction C ([] ⟶ [])

  ---- Control instructions
  block : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ
  loop : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    Sequence (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ
  if : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    (then else : Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)
  br_if : ∀ l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ)
  call : ∀ x → Instruction C (lookup (Context.funcs C) x)
  call_indirect : ∀ x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)

data Sequence C where
  nop         : ∀ {τ} → Sequence C (τ ⟶ τ)
  unreachable : ∀ {τ} → Sequence C τ
  br          : ∀ {τ₁ τ₂} l → Sequence C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂)
  br_table    : ∀ {τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Sequence C (τ ++ τ₁ ⟶ τ₂)
  return      : ∀ {τ τ₁ τ₂} → Context.return C ≡ just τ → Sequence C (τ ++ τ₁ ⟶ τ₂)
  _∙_         : ∀ {τ₀ τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Sequence C (τ₂ ++ τ₀ ⟶ τ₃) → Sequence C (τ₁ ++ τ₀ ⟶ τ₃)

Expression : Context → List ValType → Set
Expression C τ = Sequence C ([] ⟶ τ)

data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set
data SequenceRef {C} : ∀ {τ} → Sequence C τ → Fin (length (Context.funcs C)) → Set

data InstructionRef {C} where
  ---- Direct
  ref-func : ∀ {x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x
  call     : ∀ x → InstructionRef (call {C} x) x

  ---- Structural
  block : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (block {C} bt i) x
  loop : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (loop {C} bt i) x
  if₁ : ∀ {x} bt {i₁} → SequenceRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x
  if₂ : ∀ {x} bt i₁ {i₂} → SequenceRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x

data SequenceRef {C} where
  _∙₁_ : ∀ {x τ₀ τ₁ τ₂ τ₃ i} → InstructionRef i x → ∀ i* → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x
  _∙₂_ : ∀ {x τ₀ τ₁ τ₂ τ₃} i {i*} → SequenceRef i* x → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x

data InstructionConstant {C} : ∀ {τ} → Instruction C τ → Set
data SequenceConstant {C} : ∀ {τ} → Sequence C τ → Set

data InstructionConstant {C} where
  ---- Direct
  -- const
  i32-const : ∀ c → InstructionConstant (i32-const c)
  i64-const : ∀ c → InstructionConstant (i64-const c)
  f32-const : ∀ c → InstructionConstant (f32-const c)
  f64-const : ∀ c → InstructionConstant (f64-const c)

  -- refs
  ref-null : ∀ τ → InstructionConstant (ref-null τ)
  ref-func : ∀ {x} x∈refs → InstructionConstant (ref-func {x = x} x∈refs)

  -- global
  global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → InstructionConstant (global-get x)

data SequenceConstant {C} where
  nop : ∀ {τ} → SequenceConstant (nop {C} {τ})
  _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃ i i*} → InstructionConstant i → SequenceConstant i* → SequenceConstant (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*)