diff options
Diffstat (limited to 'src/Wasm/Expression/Utilities.agda')
-rw-r--r-- | src/Wasm/Expression/Utilities.agda | 52 |
1 files changed, 0 insertions, 52 deletions
diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda deleted file mode 100644 index 129af14..0000000 --- a/src/Wasm/Expression/Utilities.agda +++ /dev/null @@ -1,52 +0,0 @@ -{-# 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 |