{-# OPTIONS --safe --without-K #-}

module Wasm.Type where

open import Data.Fin using (Fin; Fin′; inject)
open import Data.List using (List)
open import Data.Maybe using (Maybe; nothing; just; maybe)
open import Data.Nat using (ℕ)
open import Wasm.Value using (I32)

infix 4 _⟶_ _,_

record Limits (k : ℕ) : Set where
  constructor _,_
  field
    max     : Maybe (Fin k)
    min     : maybe Fin′ (Fin k) max

  min′ : Fin k
  min′ with max     | min
  ...     | nothing | m = m
  ...     | just _  | m = inject m

data NumType : Set where
  i32 : NumType
  i64 : NumType
  f32 : NumType
  f64 : NumType

data RefType : Set where
  funcref   : RefType
  externref : RefType

data ValType : Set where
  num : NumType → ValType
  ref : RefType → ValType

record FuncType : Set where
  constructor _⟶_
  field
    from : List ValType
    to   : List ValType

data Mutability : Set where
  const : Mutability
  var   : Mutability

record GlobalType : Set where
  constructor _,_
  field
    mut  : Mutability
    type : ValType

record TableType : Set where
  field
    limits : Limits 4294967295
    type   : RefType

record MemType : Set where
  field
    limits : Limits 65536