Introduce type-safe instances and threadsHEADmaster

3 files changed, 81 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
diff --git a/src/Wasm/Util/List/Map/Any.agda b/src/Wasm/Util/List/Map/Any.agda
new file mode 100644
index 0000000..196ecc5
--- /dev/null
+++ b/src/Wasm/Util/List/Map/Any.agda
@@ -0,0 +1,12 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Util.List.Map.Any where
+
+open import Data.List using (_∷_)
+open import Level using (_⊔_)
+open import Relation.Unary using (Pred)
+open import Wasm.Util.List.Map
+
+data Any {a b p} {A : Set a} {B : A → Set b} (P : ∀ {x} → Pred (B x) p) : ∀ {xs} → Pred (Map B xs) (a ⊔ b ⊔ p) where
+  here : ∀ {x xs y ys} (py : P y) → Any P {x ∷ xs} (y ∷ ys)
+  there : ∀ {x xs y ys} (pys : Any P ys) → Any P {x ∷ xs} (y ∷ ys)
diff --git a/src/Wasm/Util/List/Prefix.agda b/src/Wasm/Util/List/Prefix.agda
new file mode 100644
index 0000000..6216c39
--- /dev/null
+++ b/src/Wasm/Util/List/Prefix.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Util.List.Prefix where
+
+open import Data.Fin using (Fin; zero; suc; inject≤)
+open import Data.List as L using (List; []; _∷_; _++_; length; take)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.Nat using (_≤_; z≤n; s≤s)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Wasm.Util.List.Map as M using ([]; _∷_)
+
+private
+  variable
+    a b c q r : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+    R : Rel A r
+
+Prefix : ∀ {A : Set a} (R : Rel A r) (xs ys : List A) → Set (a ⊔ r)
+Prefix R xs ys = Pointwise R xs (take (length xs) ys)
+
+data Map {A : Set a} {B : A → Set b} {C : A → Set c} {R : Rel A r} (Q : ∀ {x y} → R x y → B x → C y → Set q) : Prefix R xs ys → M.Map B xs → M.Map C ys → Set (a ⊔ b ⊔ c ⊔ q ⊔ r) where
+  [] : ∀ {ws : M.Map C ys} → Map Q [] [] ws
+  _∷_ : ∀ {z : B x} {w : C y} {zs : M.Map B xs} {ws : M.Map C ys} {r} {rs} → (q : Q r z w) → (qs : Map Q rs zs ws) → Map Q (r ∷ rs) (z ∷ zs) (w ∷ ws)
+
+length≤ : Prefix R xs ys → length xs ≤ length ys
+length≤ {ys = []}     []            = z≤n
+length≤ {ys = y ∷ ys} []            = z≤n
+length≤ {ys = y ∷ ys} (x∼y ∷ xs∼ys) = s≤s (length≤ xs∼ys)
+
+lookup : ∀ {xs ys} → (rs : Prefix R xs ys) → (i : Fin (length xs)) → R (L.lookup xs i) (L.lookup ys (inject≤ i (length≤ rs)))
+lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) zero    = x∼y
+lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) (suc i) = lookup xs∼ys i