{-|
This module defines types and contexts for Davies' λ○ calculus,
as described in "A Temporal-Logic Approach to Binding-Time Analysis."
We use a single base type `Bool to match with λ○▷.
-}

{-# OPTIONS --safe #-}
module Splice.Context where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)

variable
  n m n′ m′ n″ m″ : ℕ
  m≥n m′≥n : m ≥‴ n

data Type : (n : ℕ) → Set where
  ◯ : Type (suc n) → Type n
  `Bool : Type n
  _⇒_ : Type n → Type n → Type n

variable
  A B A′ B′ : Type n

-- | Context is a list of types
-- As in StagedList, we represent concatenation as a constructor 
-- to simplify proofs (see Data.StagedList for details).
infixl 5 _++_
data Context : Set where
  ∅ : Context
  _,_ : (Γ : Context) → (A : Type m) → Context
  _++_ : Context → Context → Context

infixl 5 _,_^_
pattern _,_^_ Γ A m = _,_ {m = m} Γ A 

variable
  Γ Δ Γ′ Δ′ : Context
  Γ₁ Γ₂ Γ₃ : Context

-- | Membership relation for contexts
infix 4 Contains
syntax Contains {m = m} Γ A = Γ ∋ A ^ m
data Contains : Context → Type m → Set where
  Z : Γ , A ^ m ∋ A ^ m
  S : (x : Γ ∋ A ^ m) → Γ , A′ ^ m′ ∋ A ^ m
  L : Γ₁ ∋ A ^ m → Γ₁ ++ Γ₂ ∋ A ^ m
  R : Γ₂ ∋ A ^ m → Γ₁ ++ Γ₂ ∋ A ^ m

-- | Renaming functions between contexts, i.e. ⊆
Rename : Context → Context → Set
Rename Γ Γ′ = ∀ {m} {A} → Γ ∋ A ^ m → Γ′ ∋ A ^ m

-- | (Γ₁ ++ Γ₂) , A′ ⊆ Γ₁ ++ (Γ₂ , A′)
∋-++-, : Γ₁ ++ Γ₂ , A′ ^ m′ ∋ A ^ m → Γ₁ ++ (Γ₂ , A′ ^ m′) ∋ A ^ m
∋-++-, Z = R Z
∋-++-, (S (L Γ₁∋A)) = L Γ₁∋A
∋-++-, (S (R Γ₂∋A)) = R (S Γ₂∋A)

-- | Γ₁ ++ (Γ₂ , A′) ⊆ (Γ₁ ++ Γ₂) , A′
∋-++-,⁻¹ : Γ₁ ++ (Γ₂ , A′ ^ m′) ∋ A ^ m → Γ₁ ++ Γ₂ , A′ ^ m′ ∋ A ^ m
∋-++-,⁻¹ (L Γ₁∋A) = S (L Γ₁∋A)
∋-++-,⁻¹ (R (S Γ₂∋A)) = S (R Γ₂∋A)
∋-++-,⁻¹ (R Z) = Z

-- | (Γ₁ ++ Γ₂) ++ Γ₃ ⊆ Γ₁ ++ (Γ₂ ++ Γ₃)
∋-++-++ : (Γ₁ ++ Γ₂ ++ Γ₃) ∋ A ^ m → Γ₁ ++ (Γ₂ ++ Γ₃) ∋ A ^ m
∋-++-++ (L (L Γ₁∋A)) = L Γ₁∋A
∋-++-++ (L (R Γ₂∋A)) = R (L Γ₂∋A)
∋-++-++ (R Γ₃∋A) = R (R Γ₃∋A)

-- | Γ₁ ++ (Γ₂ ++ Γ₃) ⊆ (Γ₁ ++ Γ₂) ++ Γ₃
∋-++-++⁻¹ : Γ₁ ++ (Γ₂ ++ Γ₃) ∋ A ^ m → Γ₁ ++ Γ₂ ++ Γ₃ ∋ A ^ m
∋-++-++⁻¹ (L Γ₁∋A) = L (L Γ₁∋A)
∋-++-++⁻¹ (R (L Γ₂∋A)) = L (R Γ₂∋A)
∋-++-++⁻¹ (R (R Γ₃∋A)) = R Γ₃∋A