module CBPV.Context where

open import Data.Bool using (Bool)
open import Data.List using (List; []; _∷_)
open import Data.String using (String)
import Data.String.Properties as String

open import Relation.Binary.Definitions using (DecidableEquality)

open import CBPV.Type

abstract
  Name : Set
  Name = String

  𝔪 : Name
  𝔪 = "𝔪"

record GenNamed (A : Set) : Set where
  constructor _:-_
  field
    name   : Name
    ofType : A

open GenNamed public

Named : Set
Named = GenNamed ValType

infixl 5 _:<_ _++_ _<><_

data GenContext (A : Set) : Set where
  [<]  : GenContext A
  _:<_ : GenContext A → (ex : GenNamed A) → GenContext A

Context : Set
Context = GenContext ValType

map : {A B : Set} → (A → B) → GenContext A → GenContext B
map f [<] = [<]
map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty)

foldr : {A B : Set} → (A → B → B) → B → GenContext A → B
foldr f z [<] = z
foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ

pattern [<_:-_] x A = [<] :< (x :- A)
pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)

_++_ : {A : Set} → GenContext A → GenContext A → GenContext A
Γ ++ [<] = Γ
Γ ++ (Δ :< ex) = Γ ++ Δ :< ex

_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A
Γ <>< [] = Γ
Γ <>< (x ∷ xs) = Γ :< x <>< xs