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