{-# 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