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

module Wasm.Expression.Utilities where

open import Data.Fin using (Fin)
open import Data.Nat using (ℕ; _^_)
open import Data.Vec.Bounded using (Vec≤)

Vec′ : ∀ {a} → Set a → Set a
Vec′ A = Vec≤ A (2 ^ 32)

data Signedness : Set where
  Signed   : Signedness
  Unsigned : Signedness

data BitWidth : Set where
  32Bit : BitWidth
  64Bit : BitWidth

module BitWidth′ where
  toℕ : BitWidth → ℕ
  toℕ 32Bit = 32
  toℕ 64Bit = 64

module Indices where
  TypeIdx : Set
  TypeIdx = Fin (2 ^ 32)

  FuncIdx : Set
  FuncIdx = Fin (2 ^ 32)

  TableIdx : Set
  TableIdx = Fin (2 ^ 32)

  MemIdx : Set
  MemIdx = Fin (2 ^ 32)

  GlobalIdx : Set
  GlobalIdx = Fin (2 ^ 32)

  ElemIdx : Set
  ElemIdx = Fin (2 ^ 32)

  DataIdx : Set
  DataIdx = Fin (2 ^ 32)

  LocalIdx : Set
  LocalIdx = Fin (2 ^ 32)

  LabelIdx : Set
  LabelIdx = Fin (2 ^ 32)