{-# 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≤) open import Wasm.Constants 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