Introduce type-safe instances and threadsHEADmaster

1 files changed, 36 insertions, 0 deletions

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