{-# OPTIONS --copatterns --sized-types #-}

module Terms where

open import Library
open import SizedInfiniteTypes

-- * Variables
------------------------------------------------------------------------

-- Typing contexts.

Cxt = List Ty

-- Type equality lifted to contexts.

_≅C_ : Cxt  Cxt  Set
_≅C_ = ≅L _≅_

-- Variables.

data Var : (Γ : Cxt) (a : Ty)  Set where
  zero : ∀{Γ a}                  Var (a  Γ) a
  suc  : ∀{Γ a b} (x : Var Γ a)  Var (b  Γ) a

-- De Bruijn index 0.

v₀ :  {a Γ}  Var (a  Γ) a
v₀ = zero

-- A congruence on variables.  Ignores the equality proofs embedded in zero.
-- Two variables are equal if they have the same de Bruijn index.

data _≅V_ :  {Γ Γ' a a'}  Var Γ a  Var Γ' a'  Set where

  zero :  {Γ a} {Γ' a'}

          zero {Γ = Γ} {a} ≅V zero {Γ = Γ'} {a'}

  suc  :  {Γ a b} {x : Var Γ a} {Γ' a' b'} {x' : Var Γ' a'}

          x ≅V x'
          suc {b = b} x ≅V suc {b = b'} x'

-- We are indeed an equivalence relation.

Vrefl :  {Γ : Cxt} {a : Ty} {x : Var Γ a}  x ≅V x
Vrefl {x = zero}  = zero
Vrefl {x = suc t} = suc Vrefl

Vsym :  {Γ Γ' a a'} {x : Var Γ a} {x' : Var Γ' a'}  x ≅V x'  x' ≅V x
Vsym zero      = zero
Vsym (suc [x]) = suc (Vsym [x])

Vtrans :  {Γ Γ' Γ'' a a' a''} {x : Var Γ a} {x' : Var Γ' a'} {x'' : Var Γ'' a''}
        x ≅V x'  x' ≅V x''  x ≅V x''
Vtrans zero     zero      = zero
Vtrans (suc eq) (suc eq') = suc (Vtrans eq eq')

-- Coercion and coherence for variables.

castVar : ∀{Γ Δ a b} (Γ≅Δ : Γ ≅C Δ) (a≅b : a  b) (x : Var Γ a)  Var Δ b
castVar (a'≅b'  Γ≅Δ) a≅b zero rewrite ≅-to-≡ (≅trans (≅sym a'≅b') a≅b) = zero
castVar (_      Γ≅Δ) a≅b (suc x)                                       = suc  (castVar Γ≅Δ a≅b x)

cohV : ∀{Γ Δ a b} (eqC : Γ ≅C Δ) (eq : a  b) (x : Var Γ a)  castVar eqC eq x ≅V x
cohV (x∼y  eqC) eq zero with ≅-to-≡ (≅trans (≅sym x∼y) eq) 
cohV (x∼y  eqC) eq zero    | ≡.refl = zero
cohV (x∼y  eqC) eq (suc x₁) = suc (cohV eqC eq x₁)

-- * Terms
------------------------------------------------------------------------

-- Well-typed terms.

data Tm (Γ : Cxt) : (a : Ty)  Set where
  var  : ∀{a}          (x : Var Γ a)                    Tm Γ a
  abs  : ∀{a b}        (t : Tm (a  Γ) b)               Tm Γ (a →̂ b)
  app  : ∀{a b}        (t : Tm Γ (a →̂ b)) (u : Tm Γ a)  Tm Γ b
  pair : ∀{a b}        (t : Tm Γ a) (u : Tm Γ b)        Tm Γ (a ×̂ b)
  fst  : ∀{a b}        (t : Tm Γ (a ×̂ b))               Tm Γ a
  snd  : ∀{a b}        (t : Tm Γ (a ×̂ b))               Tm Γ b
  ▹_   : ∀{a∞}         (t : Tm Γ (force a∞))            Tm Γ (▸̂ a∞)

  -- `applicative'
  _∗_  : ∀{a : Ty}{b∞} (t : Tm Γ (▸̂ (delay a  b∞)))
                       (u : Tm Γ ( a))                 Tm Γ (▸̂ b∞)

-- Variable congruence extended to terms.

data _≅T_ {Γ Γ' : Cxt} : {a a' : Ty}  Tm Γ a  Tm Γ' a'  Set where

  var  :  {a a'}
          {x : Var Γ a}         {x' : Var Γ' a'}          ([x] : x ≅V x')
          var x ≅T var x'

  abs  :  {a b a' b'}
          {t : Tm (a  Γ) b}    {t' : Tm (a'  Γ') b'}    ([t] : t ≅T t')
          abs t ≅T abs t'

  app  :  {a b a' b'}
          {t : Tm Γ (a →̂ b)}    {t' : Tm Γ' (a' →̂ b')}    ([t] : t ≅T t')
          {u : Tm Γ a}          {u' : Tm Γ' a'}           ([u] : u ≅T u')
          app t u ≅T app t' u'

  pair :  {a b a' b'}
          {t : Tm Γ a}          {t' : Tm Γ' a'}           ([t] : t ≅T t')
          {u : Tm Γ b}          {u' : Tm Γ' b'}           ([u] : u ≅T u')
          pair t u ≅T pair t' u'

  fst  :  {a b a' b'}
          {t : Tm Γ (a ×̂ b)}    {t' : Tm Γ' (a' ×̂ b')}    ([t] : t ≅T t')
          fst t ≅T fst t'

  snd  :  {a b a' b'}
          {t : Tm Γ (a ×̂ b)}    {t' : Tm Γ' (a' ×̂ b')}    ([t] : t ≅T t')
          snd t ≅T snd t'

  ▹_   :  {a∞ a∞'}
          {t : Tm Γ (force a∞)} {t' : Tm Γ' (force a∞')}  ([t] : t ≅T t')
          ▹_ {a∞ = a∞} t ≅T ▹_ {a∞ = a∞'} t'

  -- `applicative'
  _∗_  :  {a : Ty}{b∞}{a' : Ty}{b∞'}
          {t  : Tm Γ  (▸̂ (delay a   b∞ ))}
          {t' : Tm Γ' (▸̂ (delay a'  b∞'))}               ([t] : t ≅T t')
          {u : Tm Γ ( a)} {u' : Tm Γ' ( a')}            ([u] : u ≅T u')
          (t  u) ≅T (t'  u')

-- The term congruence is an equivalence relation.

Trefl :  {Γ : Cxt} {a : Ty}  {t : Tm Γ a}  t ≅T t
Trefl {t = var x}     = var Vrefl
Trefl {t = abs t}     = abs Trefl
Trefl {t = app t u}   = app Trefl Trefl
Trefl {t =  t}       =  Trefl
Trefl {t = t  u}     = Trefl  Trefl
Trefl {t = pair t u}  = pair Trefl Trefl
Trefl {t = fst t}     = fst Trefl
Trefl {t = snd t}     = snd Trefl

Tsym :  {Γ Γ' a a'} {t : Tm Γ a} {t' : Tm Γ' a'}  t ≅T t'  t' ≅T t
Tsym (var [x]) = var (Vsym [x])
Tsym (abs t)     = abs (Tsym t)
Tsym (app t u)   = app (Tsym t) (Tsym u)
Tsym ( t)       =  (Tsym t)
Tsym (t  u)     = (Tsym t)  (Tsym u)
Tsym (pair t u)  = pair (Tsym t) (Tsym u)
Tsym (fst t)     = fst (Tsym t)
Tsym (snd t)     = snd (Tsym t)

Ttrans :  {Γ Γ' Γ'' a a' a''} {t : Tm Γ a} {t' : Tm Γ' a'} {t'' : Tm Γ'' a''}
          t ≅T t'  t' ≅T t''  t ≅T t''
Ttrans (var [x])  (var [x'])   = var (Vtrans [x] [x'])
Ttrans (abs t)    (abs t')     = abs (Ttrans t t')
Ttrans (app t u)  (app t' u')  = app (Ttrans t t') (Ttrans u u')
Ttrans ( t)      ( t')       =  (Ttrans t t')
Ttrans (t  u)    (t'  u')    = (Ttrans t t')  (Ttrans u u')
Ttrans (pair t u) (pair t' u') = pair (Ttrans t t') (Ttrans u u')
Ttrans (fst t)    (fst t')     = fst (Ttrans t t')
Ttrans (snd t)    (snd t')     = snd (Ttrans t t')

-- Coercion and coherence for terms.

castC : ∀{Γ Δ a b} (eqC : Γ ≅C Δ) (eq : a  b)  (t : Tm Γ a)       Tm Δ b
castC eqC eq         (var x)     = var (castVar eqC eq x)
castC eqC (eq →̂ eq₁) (abs t)     = abs (castC (≅sym eq  eqC) eq₁ t)
castC eqC eq         (app t t₁)  = app (castC eqC (≅refl →̂ eq) t) (castC eqC ≅refl t₁)
castC eqC (eq ×̂ eq₁) (pair t t₁) = pair (castC eqC eq t) (castC eqC eq₁ t₁)
castC eqC eq         (fst t)     = fst (castC eqC (eq ×̂ ≅refl) t)
castC eqC eq         (snd t)     = snd (castC eqC (≅refl ×̂ eq) t)
castC eqC (▸̂ a≅)     ( t)       =  (castC eqC (≅force a≅) t)
castC eqC (▸̂ a≅)     (t  t₁)    = (castC eqC (▸̂ (≅delay (≅refl →̂ (≅force a≅)))) t)  (castC eqC ≅refl t₁)

cast : ∀{Γ a b} (eq : a  b) (t : Tm Γ a)  Tm Γ b
cast = castC (≅L.refl ≅refl)

coh : ∀{Γ Δ a b} (eqC : Γ ≅C Δ) (eq : a  b) (t : Tm Γ a)  castC eqC eq t ≅T t
coh eqC eq         (var x)     = var (cohV eqC eq x)
coh eqC (eq →̂ eq₁) (abs t)     = abs (coh (≅sym eq  eqC) eq₁ t)
coh eqC eq         (app t t₁)  = app (coh eqC (≅refl →̂ eq) t) (coh eqC ≅refl t₁)
coh eqC (eq ×̂ eq₁) (pair t t₁) = pair (coh eqC eq t) (coh eqC eq₁ t₁)
coh eqC eq         (fst t)     = fst (coh eqC (eq ×̂ ≅refl) t)
coh eqC eq         (snd t)     = snd (coh eqC (≅refl ×̂ eq) t)
coh eqC (▸̂ a≅)     ( t)       = ▹_ (coh eqC (≅force a≅) t)
coh eqC (▸̂ a≅)     (t  t₁)    = coh eqC (▸̂ ≅delay (≅refl →̂ ≅force a≅)) t  coh eqC ≅refl t₁


-- Variants of _∗_.

▹app : ∀{Γ c∞ b∞}{a : Ty} (eq : c∞ ∞≅ (delay a  b∞))
                          (t : Tm Γ (▸̂ c∞)) (u : Tm Γ ( a))  Tm Γ (▸̂ b∞)
▹app eq t u = cast (▸̂ eq) t  u

_∗'_  : ∀{Γ a∞ b∞} (t : Tm Γ (▸̂ (a∞  b∞))) (u : Tm Γ (▸̂ a∞))  Tm Γ (▸̂ b∞)
_∗'_ {a∞ = a∞} t u = _∗_ {a = force a∞} (cast (▸̂ (≅delay ≅refl)) t) (cast ((▸̂ (≅delay ≅refl))) u)

_<$>_ : ∀{Γ}{a : Ty}{b∞} (t : Tm Γ (a →̂ force b∞)) (u : Tm Γ ( a))  Tm Γ (▸̂ b∞)
t <$> u =  t  u

-- Type annotation.

tmId :  {Γ} a  Tm Γ a  Tm Γ a
tmId a t = t

syntax tmId a t = t ∶ a

-- Equality of subterms

≡app₁ :  {Γ a a' b}{t : Tm Γ (a →̂ b)}{t' : Tm Γ (a' →̂ b)}{u u'}
          Tm.app t u  app t' u'
          (P : {a : Ty}  Tm Γ a  Set)  P t  P t'
≡app₁ ≡.refl P x = x

≡appTy : ∀{Γ a a' b}{t : Tm Γ (a →̂ b)}{t' : Tm Γ (a' →̂ b)}{u u'}  Tm.app t u  app t' u'  a  a'
≡appTy ≡.refl = ≡.refl

≡app₁' : ∀{Γ a b}{t t' : Tm Γ (a →̂ b)}{u u'}  Tm.app t u  app t' u'  t  t'
≡app₁' ≡.refl = ≡.refl