Introduce type-safe instances and threadsHEADmaster

1 files changed, 33 insertions, 0 deletions

diff --git a/src/Wasm/Util/List/Map.agda b/src/Wasm/Util/List/Map.agda
new file mode 100644
index 0000000..a6da0d0
--- /dev/null
+++ b/src/Wasm/Util/List/Map.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- List where element types depend on another list.
+module Wasm.Util.List.Map where
+
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List as List using (List; []; _∷_)
+open import Data.Nat using (ℕ)
+open import Level using (Level; _⊔_)
+
+infixr 5 _∷_
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : A → Set b
+    xs : List A
+
+data Map {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+  [] : Map B []
+  _∷_ : ∀ {x xs} (y : B x) (ys : Map B xs) → Map B (x ∷ xs)
+
+length : Map B xs → ℕ
+length {xs = xs} ys = List.length xs
+
+lookup : (ys : Map B xs) → (i : Fin (length ys)) → B (List.lookup xs i)
+lookup (y ∷ ys) zero    = y
+lookup (y ∷ ys) (suc i) = lookup ys i
+
+map : ∀ {c} {C : A → Set c} → (∀ {x} → B x → C x) → Map B xs → Map C xs
+map f []       = []
+map f (y ∷ ys) = f y ∷ map f ys