{-# 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