1 files changed, 56 insertions, 0 deletions
diff --git a/src/Wasm/Type.agda b/src/Wasm/Type.agda
new file mode 100644
index 0000000..7a82aa8
--- /dev/null
+++ b/src/Wasm/Type.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Type where
+
+open import Data.Fin using (Fin; Fin′)
+open import Data.List using (List)
+open import Data.Maybe using (Maybe; maybe)
+open import Data.Nat using (ℕ)
+open import Wasm.Value using (I32)
+
+infix 4 _⟶_ _,_
+
+record Limits (k : ℕ) : Set where
+  constructor _,_
+  field
+    max     : Maybe (Fin k)
+    min     : maybe Fin′ (Fin k) max
+
+data NumType : Set where
+  i32 : NumType
+  i64 : NumType
+  f32 : NumType
+  f64 : NumType
+
+data RefType : Set where
+  funcref   : RefType
+  externref : RefType
+
+data ValType : Set where
+  num : NumType → ValType
+  ref : RefType → ValType
+
+record FuncType : Set where
+  constructor _⟶_
+  field
+    from : List ValType
+    to   : List ValType
+
+data Mutability : Set where
+  const : Mutability
+  var   : Mutability
+
+record GlobalType : Set where
+  constructor _,_
+  field
+    mut  : Mutability
+    type : ValType
+
+record TableType : Set where
+  field
+    limits : Limits 4294967295
+    type   : RefType
+
+record MemType : Set where
+  field
+    limits : Limits 65536