1 files changed, 128 insertions, 0 deletions
diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda
new file mode 100644
index 0000000..912d6da
--- /dev/null
+++ b/src/Wasm/Expression/Modules.agda
@@ -0,0 +1,128 @@
+{-# 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