Rewrite so only valid modules can be constructed.

1 files changed, 272 insertions, 0 deletions

diff --git a/src/Wasm/Data.agda b/src/Wasm/Data.agda
new file mode 100644
index 0000000..f7ed8da
--- /dev/null
+++ b/src/Wasm/Data.agda
@@ -0,0 +1,272 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Data where
+
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List using (List; []; _∷_; _++_; length; lookup; map)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise)
+open import Data.List.Relation.Unary.All using (All)
+open import Data.List.Relation.Unary.Any using (Any)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs)
+open import Data.Maybe using (Maybe; just; nothing; maybe)
+open import Data.Nat using (ℕ; suc; _+_; _≤_; z≤n)
+open import Data.Product using (_×_; _,_; proj₁)
+open import Data.Sum using (_⊎_)
+open import Data.Unit using (⊤)
+open import Data.Vec using (Vec)
+open import Function as _ using (_∋_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+open import Wasm.Data.Instruction as Inst using (Expression; Constant)
+open import Wasm.Value using (Byte; Name)
+open import Wasm.Type
+
+record ExternTypes : Set where
+  field
+    funcs   : List FuncType
+    tables  : List TableType
+    mems    : List MemType
+    globals : List GlobalType
+
+record Context : Set where
+  field
+    funcs   : List FuncType
+    tables  : List TableType
+    mems    : List MemType
+    globals : List GlobalType
+    elems   : List RefType
+    datas   : ℕ
+
+private
+  makeContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
+  makeContext Cᵢ Cₘ refs = record
+    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
+    ; tables  = Cᵢ.tables ++ Cₘ.tables
+    ; mems    = Cᵢ.mems ++ Cₘ.mems
+    ; globals = Cᵢ.globals ++ Cₘ.globals
+    ; elems   = Cₘ.elems
+    ; datas   = Cₘ.datas
+    ; locals  = []
+    ; labels  = []
+    ; return  = nothing
+    ; refs    = refs
+    }
+    where
+    module Cᵢ = ExternTypes Cᵢ
+    module Cₘ = Context Cₘ
+
+  makeGlobalContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
+  makeGlobalContext Cᵢ Cₘ refs = record
+    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
+    ; tables  = []
+    ; mems    = []
+    ; globals = Cᵢ.globals
+    ; elems   = []
+    ; datas   = 0
+    ; locals  = []
+    ; labels  = []
+    ; return  = nothing
+    ; refs    = refs
+    }
+    where
+    module Cᵢ = ExternTypes Cᵢ
+    module Cₘ = Context Cₘ
+
+record Function (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.funcs Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+
+  type = lookup Cₘ.funcs idx
+
+  private
+    module type = FuncType type
+
+  field
+    locals : List ValType
+
+  private
+    C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs)
+      { locals  = type.from ++ locals
+      ; labels  = type.to ∷ []
+      ; return  = just type.to
+      }
+  field
+    body : Expression C type.to
+
+record Global (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.globals Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+    C = Inst.Context ∋ makeGlobalContext Cᵢ Cₘ refs
+
+  type = lookup Cₘ.globals idx
+
+  private
+    module type = GlobalType type
+
+  field
+    {body}   : Expression C (type.type ∷ [])
+    constant : Constant body
+
+GlobalRef : ∀ {Cᵢ Cₘ refs idx} → Global Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+GlobalRef global x = Inst.InstructionRef (Global.body global) x
+
+data ElemMode (C : Inst.Context) : RefType → Set where
+  passive : ∀ {τ} → ElemMode C τ
+  active : ∀ table {offset : Expression C (num i32 ∷ [])} → Constant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table))
+  declarative : ∀ {τ} → ElemMode C τ
+
+data ElemModeRef {C : Inst.Context} : ∀ {τ} → ElemMode C τ → Fin (length (Inst.Context.funcs C)) → Set where
+  activeRef : ∀ {x} table {offset} constant → Inst.InstructionRef offset x → ElemModeRef (active table {offset} constant) x
+
+record Elem (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.elems Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+
+  type = lookup Cₘ.elems idx
+
+  field
+    {inits}  : List (Expression C (ref type ∷ []))
+    constant : All Constant inits
+    mode     : ElemMode C type
+
+data ElemRef {Cᵢ} {Cₘ} {refs} {idx} (elem : Elem Cᵢ Cₘ refs idx) (x : Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ))) : Set where
+  initsRef : Any (λ init → Inst.InstructionRef init x) (Elem.inits elem) → ElemRef elem x
+  modeRef  : ElemModeRef (Elem.mode elem) x → ElemRef elem x
+
+data DataMode (C : Inst.Context) : Set where
+  passive : DataMode C
+  active  : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → Constant offset → DataMode C
+
+
+data DataModeRef {C : Inst.Context} : DataMode C → Fin (length (Inst.Context.funcs C)) → Set where
+  activeRef : ∀ {x} memory {offset} constant → Inst.InstructionRef offset x → DataModeRef (active memory {offset} constant) x
+
+record Data (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (Context.datas Cₘ)) : Set where
+  private
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+  field
+    init : List Byte
+    mode : DataMode C
+
+DataRef : ∀ {Cᵢ Cₘ refs idx} → Data Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+DataRef dta x = DataModeRef (Data.mode dta) x
+
+record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (Cₑ : ExternTypes) : Set where
+  private
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+    module Cₑ = ExternTypes Cₑ
+    module C = Inst.Context C
+  field
+    funcs     : List (Name × Fin (length (C.funcs)))
+    tables    : List (Name × Fin (length (C.tables)))
+    mems      : List (Name × Fin (length (C.mems)))
+    globals   : List (Name × Fin (length (C.globals)))
+    funcsOk   : Pointwise (λ (_ , x) τ → lookup C.funcs x ≡ τ) funcs Cₑ.funcs
+    tablesOk  : Pointwise (λ (_ , x) τ → lookup C.tables x ≡ τ) tables Cₑ.tables
+    memsOk    : Pointwise (λ (_ , x) τ → lookup C.mems x ≡ τ) mems Cₑ.mems
+    globalsOk : Pointwise (λ (_ , x) τ → lookup C.globals x ≡ τ) globals Cₑ.globals
+  names = map proj₁ funcs ++ map proj₁ tables ++ map proj₁ mems ++ map proj₁ globals
+  field
+    namesDisjoint : AllPairs _≢_ names
+
+ExportsRef : ∀ {Cᵢ Cₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+ExportsRef exports x = Any (λ (_ , y) → y ≡ x) (Exports.funcs exports)
+
+record Imports (Cᵢ : ExternTypes) : Set where
+  private
+    module Cᵢ = ExternTypes Cᵢ
+  field
+    funcs   : Vec (Name × Name) (length Cᵢ.funcs)
+    tables  : Vec (Name × Name) (length Cᵢ.tables)
+    mems    : Vec (Name × Name) (length Cᵢ.mems)
+    globals : Vec (Name × Name) (length Cᵢ.globals)
+
+infixr 5 _∷_
+
+data DList : ∀ {n} → (A : Fin n → Set) → Set₁ where
+  [] : ∀ {A} → DList {0} A
+  _∷_ : ∀ {n A} → A zero → DList {n} (λ i → A (suc i)) → DList A
+
+data DAny : ∀ {n A} → (∀ {i} → A i → Set) → DList {n} A → Set₁ where
+  here  : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → P x → DAny {suc n} {A} P (x ∷ xs)
+  there : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → DAny (λ {i} → P {suc i}) xs → DAny {suc n} {A} P (x ∷ xs)
+
+record Module (it et : ExternTypes) : Set₁ where
+  private
+    module it = ExternTypes it
+  field
+    ft     : List FuncType
+    tables : List TableType
+    mems   : List MemType
+    rt     : List RefType
+    n      : ℕ
+    start  : Maybe (Fin (length (it.funcs ++ ft)))
+  private
+    Cₘ = Context ∋ record
+      { funcs   = ft
+      ; tables  = tables
+      ; mems    = mems
+      ; globals = it.globals
+      ; elems   = rt
+      ; datas   = n
+      }
+  field
+    refs     : List (Fin (length (it.funcs ++ ft)))
+    funcs    : DList (Function it Cₘ refs)
+    globals  : DList (Global it Cₘ refs)
+    elems    : DList (Elem it Cₘ refs)
+    datas    : DList (Data it Cₘ refs)
+    startOk  : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start
+    exports  : Exports it Cₘ refs et
+    memCount : length it.mems + length mems ≤ 1
+    refsUsed : All (λ i → DAny (λ g → GlobalRef g i) globals
+                        ⊎ DAny (λ e → ElemRef e i) elems
+                        ⊎ DAny (λ d → DataRef d i) datas
+                        ⊎ ExportsRef exports i)
+                   refs
+
+private
+  module Test where
+    open import Data.List.Relation.Binary.Pointwise using ([]; _∷_)
+    open import Data.List.Relation.Unary.All using ([])
+    open import Data.List.Relation.Unary.AllPairs using ([]; _∷_)
+    open import Relation.Binary.PropositionalEquality using (refl)
+    open Inst
+
+    addTwoImports : ExternTypes
+    addTwoImports = record { funcs = [] ; tables = [] ; mems = [] ; globals = [] }
+
+    addTwoExports : ExternTypes
+    addTwoExports = record { funcs = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ [] ; tables = [] ; mems = [] ; globals = [] }
+
+    addTwoModule : Module addTwoImports addTwoExports
+    addTwoModule = record
+      { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ []
+      ; tables = []
+      ; mems = []
+      ; rt = []
+      ; n = 0
+      ; start = nothing
+      ; refs = []
+      ; funcs = record
+        { locals = []
+        ; body = seq (local-get zero) (seq (frame (local-get (suc zero))) (i32-binop i32.add))
+        } ∷ []
+      ; globals = []
+      ; elems = []
+      ; datas = []
+      ; startOk = _
+      ; exports = record
+        { funcs = ("addTwo" , zero) ∷ []
+        ; tables = []
+        ; mems = []
+        ; globals = []
+        ; funcsOk = refl ∷ []
+        ; tablesOk = []
+        ; memsOk = []
+        ; globalsOk = []
+        ; namesDisjoint = [] ∷ []
+        }
+      ; memCount = z≤n
+      ; refsUsed = []
+      }