module STLC.Common where

open import STLC.Prelude hiding (_≤?_)

----------------------------------------------------------------------
--+                             Syntax                             +--
----------------------------------------------------------------------

infixr 5  ƛ_
infixl 7  _·_
infix  9  `_
infix  5  _⦂_
infixr 8  _`→_

-- simple types only: integer types and function types
data Type : Set where
  Int : Type
  _`→_ : Type  Type  Type

-- expressions
data Term : Set where
  lit      :   Term           -- literals
  `_       :   Term           -- variables
  ƛ_       : Term  Term        -- unannotated lambdas, we use de bruijn indices to deal with binding
  _·_      : Term  Term  Term -- applications
  _⦂_      : Term  Type  Term -- annotated terms

-- typing environment containing a sequence of types
infixl 5  _,_
data Env : Set where
       : Env
  _,_   : Env  Type  Env

-- environment lookup: fetch the type according to the indices
infix  4  _∋_⦂_
data _∋_⦂_ : Env    Type  Set where

  Z :  {Γ A}
     Γ , A  zero  A

  S :  {Γ A B n}
     Γ  n  A
     Γ , B  (suc n)  A

----------------------------------------------------------------------
--+                             Shift                              +--
----------------------------------------------------------------------

abstract
  _≤?_ : (x y : )  Dec (x  y)
  _≤?_ = STLC.Prelude._≤?_

-- shifti case for variables
↑-var :     
↑-var n x with n ≤? x
... | yes n≤x = suc x
... | no  n>x = x

-- e ↑ k : shift e at k-th position
infixl 7 _↑_
_↑_ : Term    Term
lit i  n = lit i
` x  n = ` (↑-var n x)
(ƛ e)  n = ƛ (e  (suc n))
e₁ · e₂  n = (e₁  n) · (e₂  n)
(e  A)  n = (e  n)  A

-- unshift case for variables
↓-var :     
↓-var n x with n ≤? x
... | yes n≤x = pred x
... | no n>x   = x

-- e ↓ k : unshift e at k-th posititon
infixl 7 _↓_
_↓_ : Term    Term
lit i  n = lit i
` x  n = ` (↓-var n x)
(ƛ e)  n = ƛ (e  (suc n))
e₁ · e₂  n = (e₁  n) · (e₂  n)
(e  A)  n = (e  n)  A

-- var case: shift and unshift can commute
↑-↓-var :  x n  ↓-var n (↑-var n x)  x
↑-↓-var x n with n ≤? x
...         | yes n≤x with n ≤? suc x
...                   | yes n≤x+1 = refl
...                   | no  n≰x+1 = ⊥-elim (n≰x+1 (m≤n⇒m≤1+n n≤x))
↑-↓-var x n | no  n≰x with n ≤? x
...                   | yes n≤x = ⊥-elim (n≰x n≤x)
...                   | no  n≰x = refl

-- shift and unshift can commute
↑-↓-id :  e n
   e  n  n  e
↑-↓-id (lit _) n = refl
↑-↓-id (` x) n = cong `_ (↑-↓-var x n)
↑-↓-id (ƛ e) n rewrite ↑-↓-id e (suc n) = refl
↑-↓-id (e₁ · e₂) n rewrite ↑-↓-id e₁ n | ↑-↓-id e₂ n = refl
↑-↓-id (e  A) n rewrite ↑-↓-id e n = refl

↑-↑-comm-var :  m n x
   m  n
   ↑-var (suc n) (↑-var m x)  ↑-var m (↑-var n x)
↑-↑-comm-var m n x m≤n with m ≤? x | n ≤? x
...               | yes m≤x | yes n≤x with suc n ≤? suc x | m ≤? suc x
...                                   | yes n+1≤x+1 | yes m≤x+1 = refl
...                                   | yes n+1≤x+1 | no  m≰x+1 = ⊥-elim (m≰x+1 (m≤n⇒m≤1+n m≤x))
...                                   | no  n+1≰x+1 | yes m≤x+1 = ⊥-elim (n+1≰x+1 (s≤s n≤x))
...                                   | no  n+1≰x+1 | no  m≰x+1 = refl
↑-↑-comm-var m n x m≤n | yes m≤x | no n≰x  with suc n ≤? suc x | m ≤? x
...                                   | yes n+1≤x+1 | yes m≤x = ⊥-elim (n≰x (≤-pred n+1≤x+1))
...                                   | yes n+1≤x+1 | no  m≰x = ⊥-elim (m≰x m≤x)
...                                   | no  n+1≰x+1 | yes m≤x = refl
...                                   | no  n+1≰x+1 | no  m≰x = ⊥-elim (m≰x m≤x)
↑-↑-comm-var m n x m≤n | no  m≰x | yes n≤x with suc n ≤? x | m ≤? suc x
...                                   | yes n+1≤x | yes m≤x+1 = ⊥-elim (m≰x (≤-trans m≤n n≤x))
...                                   | yes n+1≤x | no  m≰x+1 = refl
...                                   | no  n+1≰x | yes m≤x+1 = ⊥-elim (m≰x (≤-trans m≤n n≤x))
...                                   | no  n+1≰x | no  m≰x+1 = ⊥-elim (m≰x (≤-trans m≤n n≤x))
↑-↑-comm-var m n x m≤n | no  m≰x | no n≰x  with suc n ≤? x | m ≤? x
...                                   | yes n+1≤x | yes m≤x = refl
...                                   | yes n+1≤x | no  m≰x = ⊥-elim (n≰x (m+1≤n→m≤n n+1≤x))
...                                   | no  n+1≰x | yes m≤x = ⊥-elim (m≰x m≤x)
...                                   | no  n+1≰x | no  m≰x = refl


↑-↑-comm :  e m n  m  n  e  m  suc n  e  n  m
↑-↑-comm (lit _) m n m≤n = refl
↑-↑-comm (` x) m n m≤n = cong `_ (↑-↑-comm-var m n x m≤n)
↑-↑-comm (ƛ e) m n m≤n rewrite ↑-↑-comm e (suc m) (suc n) (s≤s m≤n) = refl
↑-↑-comm (e₁ · e₂) m n m≤n rewrite ↑-↑-comm e₁ m n m≤n | ↑-↑-comm e₂ m n m≤n = refl
↑-↑-comm (e  A) m n m≤n rewrite ↑-↑-comm e m n m≤n = refl


-- shifted: a guarantee to state the typing strengthening lemma
infix 4 _~↑~_

data _~↑~_ : Term    Set where

  sd-lit :  {n i}
     (lit i) ~↑~ n

  sd-var :  {n x}
     n  x
     (` x) ~↑~ n

  sd-lam :  {n e}
     e ~↑~ (suc n)
     (ƛ e) ~↑~ n

  sd-app :  {n e₁ e₂}
     e₁ ~↑~ n
     e₂ ~↑~ n
     (e₁ · e₂) ~↑~ n

  sd-ann :  {n e A}
     e ~↑~ n
     (e  A) ~↑~ n

↑-shifted :  {e n}
   (e  n) ~↑~ n
↑-shifted {lit i} {n} = sd-lit
↑-shifted {` x} {n} with n ≤? x
... | yes p = sd-var (<⇒≢ (s≤s p))
... | no ¬p = sd-var (>⇒≢ (≰⇒> ¬p))
↑-shifted {ƛ e} {n} = sd-lam ↑-shifted
↑-shifted {e₁ · e₂} {n} = sd-app ↑-shifted ↑-shifted
↑-shifted {e  A} {n} = sd-ann ↑-shifted

-- var case: unshift commutes with shift
↓-↑-comm-var :  m n x
   m  n
   n  x
   ↑-var m (↓-var n x)  ↓-var (suc n) (↑-var m x)
↓-↑-comm-var m n x m≤n n≢x with n ≤? x | m ≤? x
...                        | yes n≤x | yes m≤x with m ≤? pred x | suc n ≤? suc x
...                                            | yes m≤x-1 | yes n+1≤x+1 = n-1+1≡n+1-1 (m<n⇒0<n (≤∧≢⇒< n≤x n≢x))
...                                            | yes m≤x-1 | no  n+1≰x+1 = ⊥-elim (n+1≰x+1 (s≤s n≤x))
...                                            | no  m≰x-1 | yes n+1≤x+1 = ⊥-elim (m≰x-1 (<⇒≤pred m<x)) where m<x = ≤-<-trans m≤n (≤∧≢⇒< n≤x n≢x)
...                                            | no  m≰x-1 | no  n+1≰x+1 = ⊥-elim (n+1≰x+1 (s≤s n≤x))
↓-↑-comm-var m n x m≤n n≢x | yes n≤x | no  m≰x with m ≤? pred x | suc n ≤? x
...                                            | yes m≤x-1 | yes n+1≤x = ⊥-elim (m≰x (≤-trans m≤n n≤x))
...                                            | yes m≤x-1 | no  n+1≰x = n-1+1≡n+1-1 (m<n⇒0<n (≤∧≢⇒< n≤x n≢x))
...                                            | no  m≰x-1 | yes n+1≤x = refl
...                                            | no  m≰x-1 | no  n+1≰x = ⊥-elim (n+1≰x (≤∧≢⇒< n≤x n≢x))
↓-↑-comm-var m n x m≤n n≢x | no  n≰x | yes m≤x with m ≤? x | suc n ≤? suc x
...                                            | yes m≤x | yes n+1≤x+1 = ⊥-elim (n≰x (≤-pred n+1≤x+1))
...                                            | yes m≤x | no  n+1≰x+1 = refl
...                                            | no  m≰x | yes n+1≤x+1 = refl
...                                            | no  m≰x | no  n+1≰x+1 = ⊥-elim (m≰x m≤x)
↓-↑-comm-var m n x m≤n n≢x | no  n≰x | no  m≰x with m ≤? x | suc n ≤? x
...                                            | yes m≤x | yes n+1≤x = ⊥-elim (m≰x m≤x)
...                                            | yes m≤x | no  n+1≰x = ⊥-elim (m≰x m≤x)
...                                            | no  m≰x | yes n+1≤x = ⊥-elim (n≰x (m+1≤n→m≤n n+1≤x))
...                                            | no  m≰x | no  n+1≰x = refl
  

↓-↑-comm :  e m n
   m  n
   e ~↑~ n
   e  n  m  e  m  (suc n)
↓-↑-comm (lit x) m n m≤n sd = refl
↓-↑-comm (` x) m n m≤n (sd-var n≢x) = cong `_ (↓-↑-comm-var m n x m≤n n≢x)
↓-↑-comm (ƛ e) m n m≤n (sd-lam sd) rewrite ↓-↑-comm e (suc m) (suc n) (s≤s m≤n) sd = refl
↓-↑-comm (e₁ · e₂) m n m≤n (sd-app sd₁ sd₂) rewrite ↓-↑-comm e₁ m n m≤n sd₁ | ↓-↑-comm e₂ m n m≤n sd₂ = refl
↓-↑-comm (e  A) m n m≤n (sd-ann sd) rewrite ↓-↑-comm e m n m≤n sd = refl


↑-shifted-n :  {e m n}
   m  suc n
   e ~↑~ n
   (e  m) ~↑~ suc n
↑-shifted-n {lit x} m≤n+1 sd = sd-lit
↑-shifted-n {` x} {m} m≤n+1 (sd-var x₁) with m ≤? x
... | yes p = sd-var λ n+1≡x+1  x₁ (cong pred n+1≡x+1)
... | no ¬p = sd-var (≢-sym (<⇒≢ (<-≤-trans (m≰n⇒n<m ¬p) m≤n+1)))
↑-shifted-n {ƛ e} m≤n+1 (sd-lam sd) = sd-lam (↑-shifted-n (s≤s m≤n+1) sd)
↑-shifted-n {e · e₁} m≤n+1 (sd-app sd sd₁) = sd-app (↑-shifted-n m≤n+1 sd) (↑-shifted-n m≤n+1 sd₁)
↑-shifted-n {e  x} m≤n+1 (sd-ann sd) = sd-ann (↑-shifted-n m≤n+1 sd)