From 904924c33720c3481f738966f32e9c34736f92cf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 10 Aug 2021 19:11:38 +0100
Subject: Rewrite so only valid modules can be constructed.

---
 src/Wasm/Type.agda | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 src/Wasm/Type.agda

(limited to 'src/Wasm/Type.agda')

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
-- 
cgit v1.2.3