Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 219 deletions

diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
deleted file mode 100644
index 3fa96be..0000000
--- a/src/Wasm/Expression/Instructions.agda
+++ /dev/null
@@ -1,219 +0,0 @@
-{-# 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 : Maybe (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
-  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
-
-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