module Wasm.Types where

open import Prelude renaming (Nat to ℕ) hiding (const; min; max)

record Sized (A : Set) : Set where
  field
    --| Bit width: A has size of (2 ^ ∥ A ∥)
    ∥_∥ : A → ℕ

open Sized ⦃ ... ⦄

data numtype : Set where
  i32 i64 f32 f64 : numtype

u32 = Fin (2 ^ 32)
u64 = Fin (2 ^ 64)

record _↔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from-to : ∀ a → from (to a) ≡ a
    to-from : ∀ b → to (from b) ≡ b

instance
  Sized-numtype : Sized numtype
  ∥_∥ ⦃ Sized-numtype ⦄ i32 = 5
  ∥_∥ ⦃ Sized-numtype ⦄ i64 = 6
  ∥_∥ ⦃ Sized-numtype ⦄ f32 = 5
  ∥_∥ ⦃ Sized-numtype ⦄ f64 = 6

data vectype : Set where
  v128 : vectype

instance
  Sized-vectype : Sized vectype
  ∥_∥ ⦃ Sized-vectype ⦄ v128 = 7

data reftype : Set where
  funcref externref : reftype

data valtype : Set where
  num : numtype → valtype
  vec : vectype → valtype
  ref : reftype → valtype

resulttype : Set
resulttype = List valtype

data functype : Set where
  _⇒_ : (input output : resulttype) → functype

-- data valueOf : valtype → Set where

record limits : Set where
  field
    min : u32
    max : Maybe u32

record limited (A : Set) : Set where
  field
    proj : A → u32
    L : limits

memtype : Set
memtype = limits

tabletype = limited reftype

data mut : Set where
  const var : mut

record globaltype : Set where
  field
    inner-type : valtype
    mutability : mut

data externtype : Set where
  func : functype → externtype
  table : tabletype → externtype
  mem : memtype → externtype
  global : globaltype → externtype