Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 122 deletions

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