Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 63 deletions

diff --git a/src/Wasm/Validation/Context.agda b/src/Wasm/Validation/Context.agda
deleted file mode 100644
index f7c2564..0000000
--- a/src/Wasm/Validation/Context.agda
+++ /dev/null
@@ -1,63 +0,0 @@
-{-# 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