blob: 6216c396d2200b1ac41a9cd1a5ad2212dc49bd93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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
|
