Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 191 deletions

diff --git a/src/Wasm/Validation/Modules.agda b/src/Wasm/Validation/Modules.agda
deleted file mode 100644
index 1e0ca0a..0000000
--- a/src/Wasm/Validation/Modules.agda
+++ /dev/null
@@ -1,191 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 3.4 Modules
-
-module Wasm.Validation.Modules where
-
-open import Data.List using (List; []; _∷_; _++_; map; mapMaybe; allFin; replicate)
-open import Data.List.Relation.Unary.All using (All)
-open import Data.List.Relation.Unary.AllPairs using (AllPairs)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise)
-open import Data.Maybe using (just; nothing; maybe)
-open import Data.Nat using (_≤_; z≤n; s≤s; _^_)
-open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂)
-open import Data.Sum using (inj₁)
-open import Data.Unit using (⊤)
-open import Data.Vec using ([]; _∷_)
-open import Data.Vec.Bounded using (Vec≤; _,_; toList)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
-open import Wasm.Constants
-open import Wasm.Expression.Modules
-open import Wasm.Expression.Types
-open import Wasm.Expression.Utilities using (module Indices)
-open import Wasm.Expression.Values using (toString)
-open import Wasm.Validation.Context
-open import Wasm.Validation.Instructions hiding (_≤_)
-open import Wasm.Validation.Types
-
-------------------------------------------------------------------------
--- 3.4.1 Functions
-
-record FuncOk (C : Context) (F : Func) (τ : FuncType) : Set where
-  private
-    module C = Context C
-    module F = Func F
-    module τ = FuncType τ
-
-  field
-    typeEq : C.getType F.type ≡ just τ
-    exprOk : record C
-      { locals = toList F.locals ++ toList τ.from
-      ; labels = τ.to ∷ []
-      ; return = just τ.to
-      } ⊢ᵉ F.body ∶ τ.to
-
-------------------------------------------------------------------------
--- 3.4.2 Tables
-
-TableOk : Context → Table → TableType → Set
-TableOk C tbl τ = tbl ≡ τ × TableTypeOk τ
-
-------------------------------------------------------------------------
--- 3.4.3 Memories
-
-MemOk : Context → Mem → MemType → Set
-MemOk C mry τ = mry ≡ τ × MemTypeOk τ
-
-------------------------------------------------------------------------
--- 3.4.4 Globals
-
-record GlobalOk (C : Context) (G : Global) (τ : GlobalType) : Set where
-  private
-    module C = Context C
-    module G = Global G
-    mut = proj₁ τ
-    t = proj₂ τ
-
-  field
-    typeEq    : G.type ≡ τ
-    typeOk    : GlobalTypeOk τ
-    initOk    : C ⊢ᵉ G.init ∶ t ∷ [] , s≤s z≤n
-    initConst : C ⊢* G.init const
-
-------------------------------------------------------------------------
--- 3.4.5 Element Segments
-
-data ElemModeOk : Context → ElemMode → RefType → Set where
-  passive : ∀ {C τ} → ElemModeOk C passive τ
-  active : ∀ {C x lim off t} → Context.getTable C x ≡ just (lim , t) → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → ElemModeOk C (active x off) t
-  declarative : ∀ {C τ} → ElemModeOk C declarative τ
-
-record ElemOk (C : Context) (E : Elem) (τ : RefType) : Set where
-  private
-    module C = Context C
-    module E = Elem E
-
-  field
-    typeEq     : E.type ≡ τ
-    initsOk    : All (λ e → ∃ (C ⊢ᵉ e ∶_)) (toList E.init)
-    initsConst : All (C ⊢*_const) (toList E.init)
-    modeOk     : ElemModeOk C E.mode E.type
-
-------------------------------------------------------------------------
--- 3.4.6 Data Segments
-
-data DataModeOk : Context → DataMode → Set where
-  passive : ∀ {C} → DataModeOk C passive
-  active : ∀ {C x lim off} → Context.getMem C x ≡ just lim → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → DataModeOk C (active x off)
-
-DataOk : Context → Data → Set
-DataOk C D = DataModeOk C (Data.mode D)
-
-------------------------------------------------------------------------
--- 3.4.7 Start Function
-
-StartOk : Context → Start → Set
-StartOk C x = Context.getFunc C x ≡ just (([] , z≤n) ⟶ ([] , z≤n))
-
-------------------------------------------------------------------------
--- 3.4.8 Exports
-
-data ExportDescOk : Context → ExportDesc → ExternType → Set where
-  func   : ∀ {C x t} → Context.getFunc C x ≡ just t → ExportDescOk C (func x) (func t)
-  table  : ∀ {C x t} → Context.getTable C x ≡ just t → ExportDescOk C (table x) (table t)
-  mem    : ∀ {C x t} → Context.getMem C x ≡ just t → ExportDescOk C (mem x) (mem t)
-  global : ∀ {C x t} → Context.getGlobal C x ≡ just t → ExportDescOk C (global x) (global t)
-
-ExportOk : Context → Export → ExternType → Set
-ExportOk C exp t = ExportDescOk C (Export.desc exp) t
-
-------------------------------------------------------------------------
--- 3.4.9 Imports
-
-data ImportDescOk : Context → ImportDesc → ExternType → Set where
-  func   : ∀ {C x t} → Context.getType C x ≡ just t → ImportDescOk C (func x) (func t)
-  table  : ∀ {C t} → TableTypeOk t → ImportDescOk C (table t) (table t)
-  mem    : ∀ {C t} → MemTypeOk t → ImportDescOk C (mem t) (mem t)
-  global : ∀ {C t} → GlobalTypeOk t → ImportDescOk C (global t) (global t)
-
-ImportOk : Context → Import → ExternType → Set
-ImportOk C imp t = ImportDescOk C (Import.desc imp) t
-
-------------------------------------------------------------------------
--- 3.4.10 Modules
-
-record _⊢ᴹ_∶_⟶_ (M : Mod) (it : List ExternType) (et : List ExternType) : Set where
-  field
-    {ft} : List FuncType
-    {tt} : List TableType
-    {mt} : List MemType
-    {gt} : List GlobalType
-    {rt} : List RefType
-
-  private
-    module M = Mod M
-    ift = mapMaybe func? it
-    itt = mapMaybe table? it
-    imt = mapMaybe mem? it
-    igt = mapMaybe global? it
-    -- FIXME: find real references
-    x = []
-    C = record
-      { types = toList M.types
-      ; funcs = ft ++ ift
-      ; tables = tt ++ itt
-      ; mems = mt ++ imt
-      ; globals = gt ++ igt
-      ; elems = rt
-      ; datas = replicate (Vec≤.length M.datas) _
-      ; locals = []
-      ; labels = []
-      ; return = nothing
-      ; refs = x
-      }
-    C′ = record
-       { types = []
-       ; funcs = Context.funcs C
-       ; tables = []
-       ; mems = []
-       ; globals = igt
-       ; elems = []
-       ; datas = []
-       ; locals = []
-       ; labels = []
-       ; return = nothing
-       ; refs = Context.refs C
-       }
-
-  field
-    typesOk        : All FuncTypeOk (toList M.types)
-    funcsOk        : Pointwise (FuncOk C) (toList M.funcs) ft
-    tablesOk       : Pointwise (TableOk C) (toList M.tables) tt
-    memsOk         : Pointwise (MemOk C) (toList M.mems) mt
-    globalsOk      : Pointwise (GlobalOk C′) (toList M.globals) gt
-    elemsOk        : Pointwise (ElemOk C) (toList M.elems) rt
-    datasOk        : All (DataOk C) (toList M.datas)
-    startOk        : maybe (StartOk C) ⊤ M.start
-    importsOk      : Pointwise (ImportOk C) (toList M.imports) it
-    exportsOk      : Pointwise (ExportOk C) (toList M.exports) et
-    memsCount      : Vec≤.length M.mems ≤ 1
-    exportDisjoint : AllPairs _≢_ (map (λ x → toString (Export.name x)) (toList M.exports))