1 files changed, 118 insertions, 0 deletions
diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda
new file mode 100644
index 0000000..d6bce60
--- /dev/null
+++ b/src/Wasm/Expression/Values.agda
@@ -0,0 +1,118 @@
+{-# 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.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