Complete Section 2 - Structure.

1 files changed, 51 insertions, 0 deletions

diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda
new file mode 100644
index 0000000..b7f9af4
--- /dev/null
+++ b/src/Wasm/Expression/Utilities.agda
@@ -0,0 +1,51 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Wasm.Expression.Utilities where
+
+open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ; _^_)
+open import Data.Vec.Bounded using (Vec≤)
+
+Vec′ : ∀ {a} → Set a → Set a
+Vec′ A = Vec≤ A (2 ^ 32)
+
+data Signedness : Set where
+  Signed   : Signedness
+  Unsigned : Signedness
+
+data BitWidth : Set where
+  32Bit : BitWidth
+  64Bit : BitWidth
+
+module BitWidth′ where
+  toℕ : BitWidth → ℕ
+  toℕ 32Bit = 32
+  toℕ 64Bit = 64
+
+module Indices where
+  TypeIdx : Set
+  TypeIdx = Fin (2 ^ 32)
+
+  FuncIdx : Set
+  FuncIdx = Fin (2 ^ 32)
+
+  TableIdx : Set
+  TableIdx = Fin (2 ^ 32)
+
+  MemIdx : Set
+  MemIdx = Fin (2 ^ 32)
+
+  GlobalIdx : Set
+  GlobalIdx = Fin (2 ^ 32)
+
+  ElemIdx : Set
+  ElemIdx = Fin (2 ^ 32)
+
+  DataIdx : Set
+  DataIdx = Fin (2 ^ 32)
+
+  LocalIdx : Set
+  LocalIdx = Fin (2 ^ 32)
+
+  LabelIdx : Set
+  LabelIdx = Fin (2 ^ 32)