{-# OPTIONS --safe #-}

module CBPV.Family where

open import Data.List using (List; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product using (_,_) renaming (_×_ to _×′_)
open import Level using (Level; suc; _⊔_)

open import CBPV.Type

private
  variable
    ℓ ℓ′ : Level

Context : Set
Context = List ValType

ValFamily : (ℓ : Level) → Set (suc ℓ)
ValFamily ℓ = Context → ValType → Set ℓ

CompFamily : (ℓ : Level) → Set (suc ℓ)
CompFamily ℓ = Context → CompType → Set ℓ

δᵛ : Context → ValFamily ℓ → ValFamily ℓ
δᵛ Δ V Γ A = V (Γ ++ Δ) A

δᶜ : Context → CompFamily ℓ → CompFamily ℓ
δᶜ Δ C Γ B = C (Γ ++ Δ) B

infix 0 _⇒ᵛ_ _⇒ᶜ_ _~[_]↝ᵛ_ _~[_]↝ᶜ_

_⇒ᵛ_ : ValFamily ℓ → ValFamily ℓ′ → Set (ℓ ⊔ ℓ′)
V ⇒ᵛ V′ = ∀ {Γ A} → V Γ A → V′ Γ A

_⇒ᶜ_ : CompFamily ℓ → CompFamily ℓ′ → Set (ℓ ⊔ ℓ′)
C ⇒ᶜ C′ = ∀ {Γ B} → C Γ B → C′ Γ B

_~[_]↝ᵛ_ : List ValType → ValFamily ℓ → Context → Set ℓ
As ~[ V ]↝ᵛ Γ = ∀ {A} → A ∈ As → V Γ A

_~[_]↝ᶜ_ : List CompType → CompFamily ℓ → Context → Set ℓ
Bs ~[ C ]↝ᶜ Γ = ∀ {B} → B ∈ Bs → C Γ B

I : ValFamily _
I Γ A = A ∈ Γ

⌞_⌟ᵛ : List (Context ×′ ValType) → ValFamily _
⌞ Vs ⌟ᵛ Γ A = (Γ , A) ∈ Vs

⌞_⌟ᶜ : List (Context ×′ CompType) → CompFamily _
⌞ Cs ⌟ᶜ Γ B = (Γ , B) ∈ Cs