Rewrite so only valid modules can be constructed.

5 files changed, 0 insertions, 633 deletions

diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
deleted file mode 100644
index 3fa96be..0000000
--- a/src/Wasm/Expression/Instructions.agda
+++ /dev/null
@@ -1,219 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.4 Types
-
-module Wasm.Expression.Instructions where
-
-open import Data.List using (List)
-open import Data.Maybe using (Maybe)
-open import Data.Product using (∃)
-open import Data.Sum using (_⊎_)
-open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float)
-open import Wasm.Expression.Types using (ValType; RefType)
-open import Wasm.Expression.Utilities
-
-------------------------------------------------------------------------
--- 2.4.1 Numeric Instructions
-
-module IntOp (w : BitWidth) where
-  data Unary : Set where
-    clz    : Unary
-    ctz    : Unary
-    popcnt : Unary
-
-  data Binary : Set where
-    add  : Binary
-    sub  : Binary
-    mul  : Binary
-    div  : Signedness → Binary
-    rem  : Signedness → Binary
-    and  : Binary
-    or   : Binary
-    xor  : Binary
-    shl  : Binary
-    shr  : Signedness → Binary
-    rotl : Binary
-    rotr : Binary
-
-  data Test : Set where
-    eqz : Test
-
-  data Rel : Set where
-    eq : Rel
-    ne : Rel
-    lt : Signedness → Rel
-    gt : Signedness → Rel
-    le : Signedness → Rel
-    ge : Signedness → Rel
-
-  data IntInstr : Set where
-    const         : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr
-    iunop         : Unary → IntInstr
-    ibinop        : Binary → IntInstr
-    itestop       : Test → IntInstr
-    irelop        : Rel → IntInstr
-    extend8-s     : IntInstr
-    extend16-s    : IntInstr
-    trunc-f       : BitWidth → Signedness → IntInstr
-    trunc-sat-f   : BitWidth → Signedness → IntInstr
-    reinterpret-f : IntInstr
-
-data IntInstr : Set where
-  ixx            : ∀ w → IntOp.IntInstr w → IntInstr
-  i64-extend32-s : IntInstr
-  i32-wrap-i64   : IntInstr
-  i64-extend-i32 : Signedness → IntInstr
-
-module FloatOp (w : BitWidth) where
-  data Unary : Set where
-    abs     : Unary
-    neg     : Unary
-    sqrt    : Unary
-    ceil    : Unary
-    floor   : Unary
-    trunc   : Unary
-    nearest : Unary
-
-  data Binary : Set where
-    add      : Binary
-    sub      : Binary
-    mul      : Binary
-    div      : Binary
-    min      : Binary
-    max      : Binary
-    copysign : Binary
-
-  data Rel : Set where
-    eq : Rel
-    ne : Rel
-    lt : Rel
-    gt : Rel
-    le : Rel
-    ge : Rel
-
-  data FloatInstr : Set where
-    const         : Float w → FloatInstr
-    funop         : Unary → FloatInstr
-    fbinop        : Binary → FloatInstr
-    frelop        : Rel → FloatInstr
-    convert-i     : BitWidth → Signedness → FloatInstr
-    reinterpret-i : FloatInstr
-
-data FloatInstr : Set where
-  fxx             : ∀ w → FloatOp.FloatInstr w → FloatInstr
-  f32-demote-f64  : FloatInstr
-  f64-promote-f32 : FloatInstr
-
-data NumInstr : Set where
-  int   : IntInstr → NumInstr
-  float : FloatInstr → NumInstr
-
-------------------------------------------------------------------------
--- 2.4.2 Reference Instructions
-
-data RefInstr : Set where
-  null    : RefType → RefInstr
-  is-null : RefInstr
-  func    : Indices.FuncIdx → RefInstr
-
-------------------------------------------------------------------------
--- 2.4.3 Parametric Instructions
-
-data ParametricInstr : Set where
-  drop   : ParametricInstr
-  select : Maybe (List ValType) → ParametricInstr
-
-------------------------------------------------------------------------
--- 2.4.4 Variable Instructions
-
-data VarInstr : Set where
-  local-get  : Indices.LocalIdx → VarInstr
-  local-set  : Indices.LocalIdx → VarInstr
-  local-tee  : Indices.LocalIdx → VarInstr
-  global-get : Indices.GlobalIdx → VarInstr
-  global-set : Indices.GlobalIdx → VarInstr
-
-------------------------------------------------------------------------
--- 2.4.5 Table Instructions
-
-data TableInstr : Set where
-  get  : Indices.TableIdx → TableInstr
-  set  : Indices.TableIdx → TableInstr
-  size : Indices.TableIdx → TableInstr
-  grow : Indices.TableIdx → TableInstr
-  fill : Indices.TableIdx → TableInstr
-  copy : Indices.TableIdx → Indices.TableIdx → TableInstr
-  init : Indices.TableIdx → Indices.ElemIdx → TableInstr
-  drop  : Indices.ElemIdx → TableInstr
-
-------------------------------------------------------------------------
--- 2.4.6 Memory Instructions
-
-record MemArg : Set where
-  field
-    offset : UnsignedInteger 32
-    align  : UnsignedInteger 32
-
-module IntMem (w : BitWidth) where
-  data IntMemInstr : Set where
-    load    : MemArg → IntMemInstr
-    store   : MemArg → IntMemInstr
-    load8   : Signedness → MemArg → IntMemInstr
-    load16  : Signedness → MemArg → IntMemInstr
-    store8  : MemArg → IntMemInstr
-    store16 : MemArg → IntMemInstr
-
-data IntMemInstr : Set where
-  ixx         : ∀ w → IntMem.IntMemInstr w → IntMemInstr
-  i64-load32  : Signedness → MemArg → IntMemInstr
-  i64-store32 : MemArg → IntMemInstr
-
-module FloatMem (w : BitWidth) where
-  data FloatMemInstr : Set where
-    load  : MemArg → FloatMemInstr
-    store : MemArg → FloatMemInstr
-
-FloatMemInstr : Set
-FloatMemInstr = ∃ FloatMem.FloatMemInstr
-
-data MemInstr : Set where
-  int   : IntMemInstr → MemInstr
-  float : FloatMemInstr → MemInstr
-  size  : MemInstr
-  grow  : MemInstr
-  fill  : MemInstr
-  copy  : MemInstr
-  init  : Indices.DataIdx → MemInstr
-  drop  : Indices.DataIdx → MemInstr
-
-------------------------------------------------------------------------
--- 2.4.7 Control Instructions
-
-BlockType : Set
-BlockType = Indices.TypeIdx ⊎ Maybe ValType
-
-data Instr : Set where
-  num           : NumInstr → Instr
-  ref           : RefInstr → Instr
-  parametric    : ParametricInstr → Instr
-  var           : VarInstr → Instr
-  table         : TableInstr → Instr
-  mem           : MemInstr → Instr
-  nop           : Instr
-  unreachable   : Instr
-  block         : BlockType → List Instr → Instr
-  loop          : BlockType → List Instr → Instr
-  if-else       : BlockType → List Instr → List Instr → Instr
-  br            : Indices.LabelIdx → Instr
-  br-if         : Indices.LabelIdx → Instr
-  br-table      : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr
-  return        : Instr
-  call          : Indices.FuncIdx → Instr
-  call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr
-
-------------------------------------------------------------------------
--- 2.4.8 Expressions
-
-Expr : Set
-Expr = List Instr
diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda
deleted file mode 100644
index 912d6da..0000000
--- a/src/Wasm/Expression/Modules.agda
+++ /dev/null
@@ -1,128 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.5 Modules
-
-module Wasm.Expression.Modules where
-
-open import Data.Maybe using (Maybe)
-open import Wasm.Expression.Types
-open import Wasm.Expression.Utilities using (Vec′; module Indices)
-open import Wasm.Expression.Values using (Byte; Name)
-open import Wasm.Expression.Instructions using (Expr)
-
-------------------------------------------------------------------------
--- 2.5.1 Indices
-
--- NOTE: defined in Wasm.Expression.Utilities
-
-------------------------------------------------------------------------
--- 2.5.2 Types
-
--- NOTE: no new definitions
-
-------------------------------------------------------------------------
--- 2.5.3 Functions
-
-record Func : Set where
-  field
-    type   : Indices.TypeIdx
-    locals : Vec′ ValType
-    body   : Expr
-
-------------------------------------------------------------------------
--- 2.5.4 Tables
-
-Table : Set
-Table = TableType
-
-------------------------------------------------------------------------
--- 2.5.5 Memories
-
-Mem : Set
-Mem = MemType
-
-------------------------------------------------------------------------
--- 2.5.6 Globals
-
-record Global : Set where
-  field
-    type : GlobalType
-    init : Expr
-
-------------------------------------------------------------------------
--- 2.5.7 Element Segments
-
-data ElemMode : Set where
-  passive     : ElemMode
-  active      : (table : Indices.TableIdx) → (offset : Expr) → ElemMode
-  declarative : ElemMode
-
-record Elem : Set where
-  field
-    type : RefType
-    init : Vec′ Expr
-    mode : ElemMode
-
-------------------------------------------------------------------------
--- 2.5.8 Data Segments
-
-data DataMode : Set where
-  passive : DataMode
-  active  : (memory : Indices.MemIdx) → (offset : Expr) → DataMode
-
-record Data : Set where
-  field
-    init : Vec′ Byte
-    mode : DataMode
-
-------------------------------------------------------------------------
--- 2.5.9 Start Function
-
-Start : Set
-Start = Indices.FuncIdx
-
-------------------------------------------------------------------------
--- 2.5.10 Exports
-
-data ExportDesc : Set where
-  func   : Indices.FuncIdx → ExportDesc
-  table  : Indices.TableIdx → ExportDesc
-  mem    : Indices.MemIdx → ExportDesc
-  global : Indices.GlobalIdx → ExportDesc
-
-record Export : Set where
-  field
-    name : Name
-    desc : ExportDesc
-
-------------------------------------------------------------------------
--- 2.5.11 Imports
-
-data ImportDesc : Set where
-  func   : Indices.TypeIdx → ImportDesc
-  table  : TableType → ImportDesc
-  mem    : MemType → ImportDesc
-  global : GlobalType → ImportDesc
-
-record Import : Set where
-  field
-    mod  : Name
-    name : Name
-    desc : ImportDesc
-
-------------------------------------------------------------------------
--- Module definition
-
-record Mod : Set where
-  field
-    types   : Vec′ FuncType
-    funcs   : Vec′ Func
-    tables  : Vec′ Table
-    mems    : Vec′ Mem
-    globals : Vec′ Global
-    elems   : Vec′ Elem
-    datas   : Vec′ Data
-    start   : Maybe Start
-    imports : Vec′ Import
-    exports : Vec′ Export
diff --git a/src/Wasm/Expression/Types.agda b/src/Wasm/Expression/Types.agda
deleted file mode 100644
index 02661e8..0000000
--- a/src/Wasm/Expression/Types.agda
+++ /dev/null
@@ -1,112 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.3 Types
-
-module Wasm.Expression.Types where
-
-open import Data.Maybe using (Maybe; just; nothing)
-open import Data.Product using (_×_)
-open import Data.Sum using (_⊎_)
-open import Wasm.Expression.Values using (UnsignedInteger)
-open import Wasm.Expression.Utilities using (Vec′)
-
-------------------------------------------------------------------------
--- 2.3.1 Number Types
-
-data NumType : Set where
-  i32 : NumType
-  i64 : NumType
-  f32 : NumType
-  f64 : NumType
-
-------------------------------------------------------------------------
--- 2.3.2 Reference Types
-
-data RefType : Set where
-  funcref   : RefType
-  externref : RefType
-
-------------------------------------------------------------------------
--- 2.3.3 Value Types
-
-ValType : Set
-ValType = NumType ⊎ RefType
-
-------------------------------------------------------------------------
--- 2.3.4 Result Types
-
-ResultType : Set
-ResultType = Vec′ ValType
-
-------------------------------------------------------------------------
--- 2.3.5 Function Types
-
-record FuncType : Set where
-  constructor _⟶_
-  field
-    from : ResultType
-    to   : ResultType
-
-------------------------------------------------------------------------
--- 2.3.6 Limits
-
-record Limits : Set where
-  field
-    min : UnsignedInteger 32
-    max : Maybe (UnsignedInteger 32)
-
-------------------------------------------------------------------------
--- 2.3.7 Memory Types
-
-MemType : Set
-MemType = Limits
-
-------------------------------------------------------------------------
--- 2.3.8 Table Types
-
-TableType : Set
-TableType = Limits × RefType
-
-------------------------------------------------------------------------
--- 2.3.9 Global Types
-
-data Mut : Set where
-  const : Mut
-  var   : Mut
-
-GlobalType : Set
-GlobalType = Mut × ValType
-
-------------------------------------------------------------------------
--- 2.3.10 External Types
-
-data ExternType : Set where
-  func   : FuncType → ExternType
-  table  : TableType → ExternType
-  mem    : MemType → ExternType
-  global : GlobalType → ExternType
-
-func? : ExternType → Maybe FuncType
-func? (func t)   = just t
-func? (table t)  = nothing
-func? (mem t)    = nothing
-func? (global t) = nothing
-
-table? : ExternType → Maybe TableType
-table? (func t)   = nothing
-table? (table t)  = just t
-table? (mem t)    = nothing
-table? (global t) = nothing
-
-mem? : ExternType → Maybe MemType
-mem? (func t)   = nothing
-mem? (table t)  = nothing
-mem? (mem t)    = just t
-mem? (global t) = nothing
-
-global? : ExternType → Maybe GlobalType
-global? (func t)   = nothing
-global? (table t)  = nothing
-global? (mem t)    = nothing
-global? (global t) = just t
diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda
deleted file mode 100644
index 129af14..0000000
--- a/src/Wasm/Expression/Utilities.agda
+++ /dev/null
@@ -1,52 +0,0 @@
-{-# 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≤)
-open import Wasm.Constants
-
-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
diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda
deleted file mode 100644
index 283e325..0000000
--- a/src/Wasm/Expression/Values.agda
+++ /dev/null
@@ -1,122 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.2 Values
-
-module Wasm.Expression.Values where
-
-open import Data.Char using (Char; toℕ)
-open import Data.Empty using (⊥)
-open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; zero; suc; _^_; pred)
-open import Wasm.Constants
-open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit)
-
-infix 8 +_ -_
-
-------------------------------------------------------------------------
--- 2.2.1 Bytes
-
-Byte : Set
-Byte = Fin 256
-
-------------------------------------------------------------------------
--- 2.2.2 Integers
-
-UnsignedInteger : ℕ → Set
-UnsignedInteger n = Fin (2 ^ n)
-
-data SignedInteger : ℕ → Set where
-  +_     : ∀ {n} → Fin n → SignedInteger (suc n)
-  -[1+_] : ∀ {n} → Fin n → SignedInteger (suc n)
-
-UninterpretedInteger : ℕ → Set
-UninterpretedInteger = UnsignedInteger
-
-------------------------------------------------------------------------
--- 2.2.3 Floating-Point
-
-signif : BitWidth → ℕ
-signif 32Bit = 23
-signif 64Bit = 52
-
-expon : BitWidth → ℕ
-expon 32Bit = 8
-expon 64Bit = 11
-
-data FloatMag : BitWidth → Set where
-  nan       : ∀ {w} → (n : Fin (pred (2 ^ (signif w)))) → FloatMag w
-  ∞         : ∀ {w} → FloatMag w
-  normal    : ∀ {w} → (e : Fin (pred (pred (2 ^ (expon w))))) → (t : Fin (2 ^ (signif w))) → FloatMag w
-  subnormal : ∀ {w} → (t : Fin (pred (2 ^ (signif w)))) → FloatMag w
-  zero      : ∀ {w} → FloatMag w
-
-data Float : BitWidth → Set where
-  +_ : ∀ {w} → FloatMag w → Float w
-  -_ : ∀ {w} → FloatMag w → Float w
-
-------------------------------------------------------------------------
--- 2.2.4 Names
-
-module _ where
-  open import Data.Bool using (Bool; true; false; if_then_else_)
-  open import Data.List using (List; []; _∷_; length; map; sum)
-  open import Data.Nat using (_≤ᵇ_; _<_; z≤n; s≤s)
-  open import Data.Nat.Properties using (≤-step)
-  open import Data.Product using (_×_; _,_; proj₂; map₂)
-  open import Data.String using (String; toList)
-
-  halfEven? : ℕ → Bool × ℕ
-  halfEven? zero          = true , 0
-  halfEven? (suc zero)    = false , 0
-  halfEven? (suc (suc n)) = map₂ suc (halfEven? n)
-
-  n≢0⇒halfEven?<n : ∀ n → proj₂ (halfEven? (suc n)) < (suc n)
-  n≢0⇒halfEven?<n zero = s≤s z≤n
-  n≢0⇒halfEven?<n (suc zero) = s≤s (n≢0⇒halfEven?<n zero)
-  n≢0⇒halfEven?<n (suc (suc n)) = s≤s (≤-step (n≢0⇒halfEven?<n n))
-
-  asBits : ℕ → List Bool
-  asBits n = All.wfRec <-wellFounded _ Pred helper n
-    where
-    open import Data.Nat.Induction using (<-wellFounded)
-    open import Data.Nat.Properties using (module ≤-Reasoning)
-    open import Induction.WellFounded using (WfRec; module All)
-    open import Relation.Binary.PropositionalEquality using (cong; inspect; [_])
-
-    open ≤-Reasoning
-
-    Pred : ℕ → Set
-    Pred n = List Bool
-
-    helper : ∀ n → WfRec _<_ Pred n → List Bool
-    helper zero rec = []
-    helper (suc n) rec with halfEven? (suc n) | inspect halfEven? (suc n)
-    ...                   | true , m  | [ m≡n+1/2 ] = false ∷ rec m (begin-strict
-                                                        m ≡˘⟨ cong proj₂ m≡n+1/2 ⟩
-                                                        proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
-                                                        suc n ∎)
-    ...                   | false , m | [ m≡n/2 ]   = true ∷ rec m (begin-strict
-                                                        m ≡˘⟨ cong proj₂ m≡n/2 ⟩
-                                                        proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
-                                                        suc n ∎)
-
-  utf8Bytes : Char → ℕ
-  utf8Bytes c with asBits (toℕ c)
-  ... | bits = if length bits ≤ᵇ 7 then
-                  1
-               else if length bits ≤ᵇ 11 then
-                  2
-               else if length bits ≤ᵇ 16 then
-                  3
-               else
-                  4
-
-  byteLength : String → ℕ
-  byteLength s = sum (map utf8Bytes (toList s))
-
-  data Name : Set where
-    name : ∀ s → {len : byteLength s < 2^32} → Name
-
-  toString : Name → String
-  toString (name s) = s