Cleanup before working on 'Modules'

5 files changed, 62 insertions, 22 deletions

diff --git a/src/Wasm/Constants.agda b/src/Wasm/Constants.agda
new file mode 100644
index 0000000..74682a8
--- /dev/null
+++ b/src/Wasm/Constants.agda
@@ -0,0 +1,11 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- Big constant values
+
+module Wasm.Constants where
+
+open import Data.Nat using (ℕ)
+
+2^32 : ℕ
+2^32 = 4294967296
diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
index 6cd006b..3fa96be 100644
--- a/src/Wasm/Expression/Instructions.agda
+++ b/src/Wasm/Expression/Instructions.agda
@@ -122,7 +122,7 @@ data RefInstr : Set where
 
 data ParametricInstr : Set where
   drop   : ParametricInstr
-  select : List ValType → ParametricInstr
+  select : Maybe (List ValType) → ParametricInstr
 
 ------------------------------------------------------------------------
 -- 2.4.4 Variable Instructions
@@ -138,14 +138,14 @@ data VarInstr : Set where
 -- 2.4.5 Table Instructions
 
 data TableInstr : Set where
-  table-get  : Indices.TableIdx → TableInstr
-  table-set  : Indices.TableIdx → TableInstr
-  table-size : Indices.TableIdx → TableInstr
-  table-grow : Indices.TableIdx → TableInstr
-  table-fill : Indices.TableIdx → TableInstr
-  table-copy : Indices.TableIdx → Indices.TableIdx → TableInstr
-  table-init : Indices.TableIdx → Indices.ElemIdx → TableInstr
-  elem-drop  : Indices.ElemIdx → TableInstr
+  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
@@ -210,7 +210,7 @@ data Instr : Set where
   br-table      : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr
   return        : Instr
   call          : Indices.FuncIdx → Instr
-  call_indirect : Indices.TableIdx → Indices.TypeIdx → Instr
+  call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr
 
 ------------------------------------------------------------------------
 -- 2.4.8 Expressions
diff --git a/src/Wasm/Expression/Types.agda b/src/Wasm/Expression/Types.agda
index f72df93..02661e8 100644
--- a/src/Wasm/Expression/Types.agda
+++ b/src/Wasm/Expression/Types.agda
@@ -5,7 +5,7 @@
 
 module Wasm.Expression.Types where
 
-open import Data.Maybe using (Maybe)
+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)
@@ -86,3 +86,27 @@ data ExternType : Set where
   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
index b7f9af4..129af14 100644
--- a/src/Wasm/Expression/Utilities.agda
+++ b/src/Wasm/Expression/Utilities.agda
@@ -5,9 +5,10 @@ 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)
+Vec′ A = Vec≤ A 2^32
 
 data Signedness : Set where
   Signed   : Signedness
@@ -24,28 +25,28 @@ module BitWidth′ where
 
 module Indices where
   TypeIdx : Set
-  TypeIdx = Fin (2 ^ 32)
+  TypeIdx = Fin 2^32
 
   FuncIdx : Set
-  FuncIdx = Fin (2 ^ 32)
+  FuncIdx = Fin 2^32
 
   TableIdx : Set
-  TableIdx = Fin (2 ^ 32)
+  TableIdx = Fin 2^32
 
   MemIdx : Set
-  MemIdx = Fin (2 ^ 32)
+  MemIdx = Fin 2^32
 
   GlobalIdx : Set
-  GlobalIdx = Fin (2 ^ 32)
+  GlobalIdx = Fin 2^32
 
   ElemIdx : Set
-  ElemIdx = Fin (2 ^ 32)
+  ElemIdx = Fin 2^32
 
   DataIdx : Set
-  DataIdx = Fin (2 ^ 32)
+  DataIdx = Fin 2^32
 
   LocalIdx : Set
-  LocalIdx = Fin (2 ^ 32)
+  LocalIdx = Fin 2^32
 
   LabelIdx : Set
-  LabelIdx = Fin (2 ^ 32)
+  LabelIdx = Fin 2^32
diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda
index d6bce60..283e325 100644
--- a/src/Wasm/Expression/Values.agda
+++ b/src/Wasm/Expression/Values.agda
@@ -9,6 +9,7 @@ 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 +_ -_
@@ -115,4 +116,7 @@ module _ where
   byteLength s = sum (map utf8Bytes (toList s))
 
   data Name : Set where
-    name : ∀ s → {len : byteLength s < 2 ^ 32} → Name
+    name : ∀ s → {len : byteLength s < 2^32} → Name
+
+  toString : Name → String
+  toString (name s) = s