Complete Section 3 - Validation.

1 files changed, 63 insertions, 0 deletions

diff --git a/src/Wasm/Validation/Context.agda b/src/Wasm/Validation/Context.agda
new file mode 100644
index 0000000..f7c2564
--- /dev/null
+++ b/src/Wasm/Validation/Context.agda
@@ -0,0 +1,63 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- Type Context
+
+module Wasm.Validation.Context where
+
+open import Data.Fin using (Fin; toℕ; fromℕ<)
+open import Data.List using (List; length; lookup)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (_<?_; _^_)
+open import Data.Unit using (⊤)
+open import Relation.Nullary using (yes; no)
+open import Wasm.Constants
+open import Wasm.Expression.Types
+open import Wasm.Expression.Utilities using (module Indices)
+
+record Context : Set where
+  field
+    types : List FuncType
+    funcs : List FuncType
+    tables : List TableType
+    mems   : List MemType
+    globals : List GlobalType
+    elems   : List RefType
+    datas   : List ⊤
+    locals  : List ValType
+    labels  : List ResultType
+    return  : Maybe ResultType
+    refs    : List Indices.FuncIdx
+
+  private
+    get : ∀ {A} → List A → Fin 2^32 → Maybe A
+    get xs idx with toℕ idx <? length xs
+    ... | yes idx<∣xs∣ = just (lookup xs (fromℕ< idx<∣xs∣))
+    ... | no _         = nothing
+
+  getType : Indices.TypeIdx → Maybe FuncType
+  getType = get types
+
+  getFunc : Indices.FuncIdx → Maybe FuncType
+  getFunc = get funcs
+
+  getTable : Indices.TableIdx → Maybe TableType
+  getTable = get tables
+
+  getMem : Indices.MemIdx → Maybe MemType
+  getMem = get mems
+
+  getGlobal : Indices.GlobalIdx → Maybe GlobalType
+  getGlobal = get globals
+
+  getElem : Indices.ElemIdx → Maybe RefType
+  getElem = get elems
+
+  getData : Indices.DataIdx → Maybe ⊤
+  getData = get datas
+
+  getLocal : Indices.LocalIdx → Maybe ValType
+  getLocal = get locals
+
+  getLabel : Indices.LabelIdx → Maybe ResultType
+  getLabel = get labels