Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 128 deletions

diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda
deleted file mode 100644
index 912d6da..0000000
--- a/src/Wasm/Expression/Modules.agda
+++ /dev/null
@@ -1,128 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.5 Modules
-
-module Wasm.Expression.Modules where
-
-open import Data.Maybe using (Maybe)
-open import Wasm.Expression.Types
-open import Wasm.Expression.Utilities using (Vec′; module Indices)
-open import Wasm.Expression.Values using (Byte; Name)
-open import Wasm.Expression.Instructions using (Expr)
-
-------------------------------------------------------------------------
--- 2.5.1 Indices
-
--- NOTE: defined in Wasm.Expression.Utilities
-
-------------------------------------------------------------------------
--- 2.5.2 Types
-
--- NOTE: no new definitions
-
-------------------------------------------------------------------------
--- 2.5.3 Functions
-
-record Func : Set where
-  field
-    type   : Indices.TypeIdx
-    locals : Vec′ ValType
-    body   : Expr
-
-------------------------------------------------------------------------
--- 2.5.4 Tables
-
-Table : Set
-Table = TableType
-
-------------------------------------------------------------------------
--- 2.5.5 Memories
-
-Mem : Set
-Mem = MemType
-
-------------------------------------------------------------------------
--- 2.5.6 Globals
-
-record Global : Set where
-  field
-    type : GlobalType
-    init : Expr
-
-------------------------------------------------------------------------
--- 2.5.7 Element Segments
-
-data ElemMode : Set where
-  passive     : ElemMode
-  active      : (table : Indices.TableIdx) → (offset : Expr) → ElemMode
-  declarative : ElemMode
-
-record Elem : Set where
-  field
-    type : RefType
-    init : Vec′ Expr
-    mode : ElemMode
-
-------------------------------------------------------------------------
--- 2.5.8 Data Segments
-
-data DataMode : Set where
-  passive : DataMode
-  active  : (memory : Indices.MemIdx) → (offset : Expr) → DataMode
-
-record Data : Set where
-  field
-    init : Vec′ Byte
-    mode : DataMode
-
-------------------------------------------------------------------------
--- 2.5.9 Start Function
-
-Start : Set
-Start = Indices.FuncIdx
-
-------------------------------------------------------------------------
--- 2.5.10 Exports
-
-data ExportDesc : Set where
-  func   : Indices.FuncIdx → ExportDesc
-  table  : Indices.TableIdx → ExportDesc
-  mem    : Indices.MemIdx → ExportDesc
-  global : Indices.GlobalIdx → ExportDesc
-
-record Export : Set where
-  field
-    name : Name
-    desc : ExportDesc
-
-------------------------------------------------------------------------
--- 2.5.11 Imports
-
-data ImportDesc : Set where
-  func   : Indices.TypeIdx → ImportDesc
-  table  : TableType → ImportDesc
-  mem    : MemType → ImportDesc
-  global : GlobalType → ImportDesc
-
-record Import : Set where
-  field
-    mod  : Name
-    name : Name
-    desc : ImportDesc
-
-------------------------------------------------------------------------
--- Module definition
-
-record Mod : Set where
-  field
-    types   : Vec′ FuncType
-    funcs   : Vec′ Func
-    tables  : Vec′ Table
-    mems    : Vec′ Mem
-    globals : Vec′ Global
-    elems   : Vec′ Elem
-    datas   : Vec′ Data
-    start   : Maybe Start
-    imports : Vec′ Import
-    exports : Vec′ Export