module CBPV.Context where

open import Data.Bool using (Bool)
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 Named : Set where
  constructor _:-_
  field
    name   : Name
    ofType : ValType

open Named public

infixl 5 _:<_ _++_

data Context : Set where
  [<]  : Context
  _:<_ : Context → (ex : Named) → Context

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

_++_ : Context → Context → Context
Γ ++ [<] = Γ
Γ ++ (Δ :< ex) = Γ ++ Δ :< ex