-- checked on Agda 2.5.2, standard library 0.13

module normal-pe where

open import Data.List
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import deBruijn-cbn
open import reduce-pe

-- Church Rosser
postulate
  ChurchRosser : {Γ : Cxt} {τ : typ} {e₁ e₂ : term Γ τ} → equal e₁ e₂ →
                 Σ[ e ∈ term Γ τ ] reduce* e₁ e × reduce* e₂ e

-- terminating
terminating : {Γ : Cxt} → {τ : typ} → term Γ τ → Set
terminating {Γ} {τ} e = Σ[ nf ∈ nf Γ τ ] reduce* e (embedNf nf)
-- The result is a normal form, rather than a value.

terminatingNe : {Γ : Cxt} → {τ : typ} → term Γ τ → Set
terminatingNe {Γ} {τ} e = Σ[ ne ∈ ne Γ τ ] reduce* e (embedNe ne)

terminating-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} {e : term Δ τ} →
                  terminating e → terminating (ren xs e)
terminating-ren xs (nf , red*)
  with reduce*-ren xs red*
... | red*′ rewrite sym (embedNf-ren xs nf)= (renNf xs nf , red*′)

-- stuck due to a variable at the head of application
isStuck : {Γ : Cxt} {τ : typ} → (e : term Γ τ) → Set
isStuck (Val v) = ⊥
isStuck (Var x) = ⊤
isStuck (App e₁ e₂) = isStuck e₁ × terminating e₂

isStuck-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (e : term Δ τ) → 
              isStuck e → isStuck (ren xs e)
isStuck-ren xs (Val v) ()
isStuck-ren xs (Var x) p = tt
isStuck-ren xs (App e₁ e₂) (p₁ , p₂) =
  (isStuck-ren xs e₁ p₁ , terminating-ren xs p₂)

stuck-terminating : {Γ : Cxt} → {τ : typ} → (e : term Γ τ) →
                    isStuck e → terminatingNe e
stuck-terminating (Val v) ()
stuck-terminating (Var x) stuck = (Var x , r*Id)
stuck-terminating (App e₁ e₂) (stuck , (nf₂ , red₂))
  with stuck-terminating e₁ stuck
... | (ne₁ , red₁) = (App ne₁ nf₂ , (begin
    App e₁ e₂
  ⟶*⟨ rApp₁* e₂ red₁ ⟩
    App (embedNe ne₁) e₂
  ⟶*⟨ rApp₂* (embedNe ne₁) red₂ ⟩
    App (embedNe ne₁) (embedNf nf₂)
  ∎))
  where open red-Reasoning

-- TAPL: definition 12.1.2
R : (Γ : Cxt) → (τ : typ) → term Γ τ → Set
R Γ Nat e₁ = terminating e₁
R Γ (τ₂ ⇒ τ₁) e₁ =
  terminating e₁ ×
  ({Δ : Cxt} → (xs : Ren Δ Γ) →
   (e₂ : term Δ τ₂) → R Δ τ₂ e₂ → R Δ τ₁ (App (ren xs e₁) e₂))

R-ren : ∀ {τ Γ} (e : term Γ τ) {Δ} (xs : Ren Δ Γ) →
        R Γ τ e → R Δ τ (ren xs e)
R-ren {Nat} e xs t = terminating-ren xs t
R-ren {τ₂ ⇒ τ₁} e xs (t , r) =
  (terminating-ren xs t , f e xs r)
  where
  f : ∀ {τ₂ τ₁ Γ Δ} (e : term Γ (τ₂ ⇒ τ₁)) (xs : Ren Δ Γ) →
    (∀ {Δ₁} (xs₁ : Ren Δ₁ Γ) (v₂ : term Δ₁ τ₂) →
     R Δ₁ τ₂ v₂ → R Δ₁ τ₁ (App (ren xs₁ e) v₂)) →
    ∀ {Δ₁} (xs₁ : Ren Δ₁ Δ) (v₂ : term Δ₁ τ₂) →
    R Δ₁ τ₂ v₂ → R Δ₁ τ₁ (App (ren xs₁ (ren xs e)) v₂)
  f e xs r ys v₂ rv₂ rewrite sym (rencomp ys xs e) =
    r (renComp ys xs) v₂ rv₂
  -- To use r here, the environment in R has to be extended.

R-weak : {τ : typ} {Γ : Cxt} {e : term Γ τ} → (σ : typ) →
         R Γ τ e → R (σ ∷ Γ) τ (weak σ e)
R-weak {e = e} σ r = R-ren e (wkr renId) r

-- TAPL: lemma 12.1.3
R-terminating : {Γ : Cxt} {τ : typ} {e : term Γ τ} → R Γ τ e → terminating e
R-terminating {τ = Nat} t = t
R-terminating {τ = τ₂ ⇒ τ₁} (t , f) = t

Rstuck : {Γ : Cxt} {τ : typ} (e : term Γ τ) → isStuck e → R Γ τ e
Rstuck {τ = Nat} e stuck with stuck-terminating e stuck
... | (ne , red*) = (Ne ne , red*)
Rstuck {τ = τ₂ ⇒ τ₁} e stuck with stuck-terminating e stuck
... | (ne , red*) =
  ((Ne ne , red*) ,
   λ xs v r →
     Rstuck (App (ren xs e) v) (isStuck-ren xs e stuck , R-terminating r))

-- termination preserved by equality, reduction
terminating-eq : {Γ : Cxt} → {τ : typ} → {e₁ e₂ : term Γ τ} →
                 equal e₁ e₂ → terminating e₁ → terminating e₂
terminating-eq {e₁ = e₁} {e₂} eq (nf , red₁*)
  with let open eq-Reasoning in
       ChurchRosser (begin
           e₂
         ⟵⟨ eq ⟩
           e₁
         ⟶⟨ reduce*-equal red₁* ⟩
           embedNf nf
         ∎)
... | (e , red₂* , red*) rewrite reduce*-nf nf red* = (nf , red₂*)

terminating-red : {Γ : Cxt} → {τ : typ} → {e₁ e₂ : term Γ τ} →
                  reduce e₁ e₂ → terminating e₁ → terminating e₂
terminating-red red t = terminating-eq (reduce-equal red) t

terminating-red-inv : {Γ : Cxt} → {τ : typ} → {e₁ e₂ : term Γ τ} →
                      reduce e₁ e₂ → terminating e₂ → terminating e₁
terminating-red-inv red t = terminating-eq (eq-sym (reduce-equal red)) t

-- TAPL: lemma 12.1.4 (only if)
reduce-R : {τ : typ} → {Γ : Cxt} → {e e′ : term Γ τ} →
           reduce e e′ → R Γ τ e → R Γ τ e′
reduce-R {τ = Nat} red t = terminating-red red t
reduce-R {τ = τ₂ ⇒ τ₁} red (t , f) =
  (terminating-red red t ,
   (λ xs v₂ r → reduce-R (rApp₁ v₂ (reduce-ren xs red)) (f xs v₂ r)))

equal-R : {τ : typ} → {Γ : Cxt} → {e e′ : term Γ τ} →
          equal e e′ → R Γ τ e → R Γ τ e′
equal-R {Nat} eq t = terminating-eq eq t
equal-R {τ ⇒ τ₁} eq (t , f) =
  (terminating-eq eq t ,
   λ xs v₂ r → equal-R (eqApp₁ v₂ (equal-ren xs eq)) (f xs v₂ r))

reduce*-R : {Γ : Cxt} → {τ : typ} → {e e′ : term Γ τ} →
               reduce* e e′ → R Γ τ e → R Γ τ e′
reduce*-R r*Id r = r
reduce*-R (r*Trans e₁ e₂ e₃ red red*) r =
  reduce*-R red* (reduce-R red r)

-- TAPL: lemma 12.1.4 (if)
reduce-inv-R : {Γ : Cxt} → {τ : typ} → {e e′ : term Γ τ} →
               reduce e e′ → R Γ τ e′ → R Γ τ e
reduce-inv-R {τ = Nat} red t = terminating-red-inv red t
reduce-inv-R {τ = τ₂ ⇒ τ₁} red (t , f) =
  (terminating-red-inv red t ,
   (λ xs v₂ r → reduce-inv-R (rApp₁ v₂ (reduce-ren xs red)) (f xs v₂ r)))

equal-inv-R : {Γ : Cxt} → {τ : typ} → {e e′ : term Γ τ} →
              equal e e′ → R Γ τ e′ → R Γ τ e
equal-inv-R {τ = Nat} eq t = terminating-eq (eq-sym eq) t
equal-inv-R {τ = τ₂ ⇒ τ₁} eq (t , f) =
  (terminating-eq (eq-sym eq) t ,
   λ xs v₂ r → equal-inv-R (eqApp₁ v₂ (equal-ren xs eq)) (f xs v₂ r))

reduce*-inv-R : {Γ : Cxt} → {τ : typ} → {e e′ : term Γ τ} →
                reduce* e e′ → R Γ τ e′ → R Γ τ e
reduce*-inv-R r*Id r = r
reduce*-inv-R (r*Trans e₁ e₂ e₃ red red*) r =
  reduce-inv-R red (reduce*-inv-R red* r)

-- equational reasoning for R
module R-red-Reasoning (Γ : Cxt) (τ : typ) where
  infix  3 _∈_∎
  infixr 2  _⟵⟨_⟩_ _⟵*⟨_⟩_ _⟶⟨_⟩_ _⟶*⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_

  begin_ : {e : term Γ τ} → R Γ τ e → R Γ τ e
  begin_ r = r

  _⟵⟨_⟩_ : (e₁ {e₂} : term Γ τ) → reduce e₂ e₁ → R Γ τ e₂ → R Γ τ e₁
  _⟵⟨_⟩_ e₁ {e₂} red r = reduce-R red r

  _⟵*⟨_⟩_ : (e₁ {e₂} : term Γ τ) → reduce* e₂ e₁ → R Γ τ e₂ → R Γ τ e₁
  _⟵*⟨_⟩_ e₁ {e₂} red* r = reduce*-R red* r

  _⟶⟨_⟩_ : (e₁ {e₂} : term Γ τ) → reduce e₁ e₂ → R Γ τ e₂ → R Γ τ e₁
  _⟶⟨_⟩_ e₁ {e₂} red r = reduce-inv-R red r

  _⟶*⟨_⟩_ : (e₁ {e₂} : term Γ τ) → reduce* e₁ e₂ → R Γ τ e₂ → R Γ τ e₁
  _⟶*⟨_⟩_ e₁ {e₂} red* r = reduce*-inv-R red* r

  _≡⟨_⟩_ : (e₁ {e₂} : term Γ τ) → e₁ ≡ e₂ → R Γ τ e₂ → R Γ τ e₁
  _≡⟨_⟩_ e₁ {e₂} refl r = r

  _∈_∎ : (e : term Γ τ) → R Γ τ e → R Γ τ e
  _∈_∎ e r = r

module R-eq-Reasoning (Γ : Cxt) (τ : typ) where
  infix  3 _∈_∎
  infixr 2  _⟵⟨_⟩_ _⟶⟨_⟩_ _⟷⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_

  begin_ : {e : term Γ τ} → R Γ τ e → R Γ τ e
  begin_ r = r

  _⟵⟨_⟩_ : (e₁ {e₂} : term Γ τ) → equal e₂ e₁ → R Γ τ e₂ → R Γ τ e₁
  _⟵⟨_⟩_ e₁ {e₂} red r = equal-R red r

  _⟶⟨_⟩_ : (e₁ {e₂} : term Γ τ) → equal e₁ e₂ → R Γ τ e₂ → R Γ τ e₁
  _⟶⟨_⟩_ e₁ {e₂} red r = equal-inv-R red r

  _⟷⟨_⟩_ : (e₁ {e₂} : term Γ τ) → equal e₁ e₂ → R Γ τ e₂ → R Γ τ e₁
  _⟷⟨_⟩_ e₁ {e₂} red r = equal-inv-R red r

  _≡⟨_⟩_ : (e₁ {e₂} : term Γ τ) → e₁ ≡ e₂ → R Γ τ e₂ → R Γ τ e₁
  _≡⟨_⟩_ e₁ {e₂} refl r = r

  _∈_∎ : (e : term Γ τ) → R Γ τ e → R Γ τ e
  _∈_∎ e r = r

-- Rvs
Rvs : {Γ : Cxt} → (Δ : Cxt) → (vs : Sub Δ Γ) → Set
Rvs Δ [] = ⊤
Rvs Δ (_∷_ {τ = τ} v vs) = R Δ τ v × Rvs Δ vs

Rvs-ren : ∀ {Γ Δ} {vs : Sub Δ Γ} {Δ′} (xs : Ren Δ′ Δ) →
          Rvs Δ vs → Rvs Δ′ (subComp (ren2sub xs) vs)
Rvs-ren {Δ = Δ} {[]} {Δ′} xs rvs = tt
Rvs-ren {Δ = Δ₁} {v ∷ vs} {Δ′} xs (rv , rvs)
  rewrite sym (ren2subren xs v)
  = (R-ren v xs rv , Rvs-ren xs rvs)

Rvs-lift : {Γ : Cxt} → (τ : typ) → (Δ : Cxt) → {vs : Sub Δ Γ} →
           (rvs : Rvs Δ vs) →
           Rvs (τ ∷ Δ) (Var zero ∷ wks vs)
Rvs-lift τ Δ {[]} tt = (Rstuck {τ ∷ Δ} {τ} (Var zero) tt , tt)
Rvs-lift τ Δ {v ∷ vs} (r , rvs) with Rvs-lift τ Δ rvs
... | (rv , rvs′) = (rv , R-weak {e = v} τ r , rvs′)

-- TAPL: lemma 12.1.5
lookup-var : {Γ Δ : Cxt} → {vs : Sub Δ Γ} → {τ : typ} →
             (x : var Γ τ) → Rvs Δ vs → R Δ τ (looks vs x)
lookup-var {[]} () rvs
lookup-var {τ ∷ Γ} {vs = v ∷ vs} zero (r , rvs) = r
lookup-var {τ ∷ Γ} {vs = v ∷ vs} (suc x) (r , rvs) = lookup-var x rvs

mutual
  eval-value : {Γ Δ : Cxt} → {vs : Sub Δ Γ} → {τ : typ} →
               (v : value Γ τ) → Rvs Δ vs → R Δ τ (sub vs (Val v))
  eval-value (Num n) rvs = (Num n , r*Id)
  eval-value {Γ} {Δ} {vs} (Fun τ {τ₁} e) rvs
    with eval-term e (Rvs-lift τ Δ rvs) -- evaluate under lambda
  ... | r with R-terminating {τ ∷ Δ} {τ₁} r
  ... | (nf , red*) =
    ((Fun τ nf , rFun* red*) ,
     λ xs e₂ r₂ → eval-lambda xs vs e rvs e₂ r₂)
    where
    eval-lambda : ∀ {τ τ₁ Γ Δ} {Δ₁} (xs : Ren Δ₁ Δ) (vs : Sub Δ Γ)
      (e : term (τ ∷ Γ) τ₁) → Rvs Δ vs → (e₂ : term Δ₁ τ) →
      R Δ₁ τ e₂ → R Δ₁ τ₁
      (App (Val (Fun τ (ren (zero ∷ wkr xs) (sub (Var zero ∷ wks vs) e)))) e₂)
    eval-lambda {τ₂} {τ₃} {Δ₁ = Δ₂} xs vs e rvs v₂ rv₂ = begin
        App (Val (Fun τ₂ (ren (zero ∷ wkr xs) (sub (Var zero ∷ wks vs) e))))
            v₂
      ≡⟨ refl ⟩
        App (Val (Fun τ₂ (ren (liftr xs) (sub (lifts vs) e))))
            v₂
      ≡⟨ cong (λ l → App (Val (Fun τ₂ l)) v₂)
              (rensub (liftr xs) (lifts vs) e) ⟩
        App (Val (Fun τ₂ (sub (subComp (ren2sub (liftr xs)) (lifts vs)) e)))
            v₂
      ≡⟨ cong (λ l → App (Val (Fun τ₂ (sub l e))) v₂)
              (liftrscomp xs vs) ⟩
        App (Val (Fun τ₂ (sub (lifts (subComp (ren2sub xs) vs)) e)))
            v₂
      ⟶⟨ rBeta (sub (lifts (subComp (ren2sub xs) vs)) e) v₂ ⟩
        sub0 v₂ (sub (lifts (subComp (ren2sub xs) vs)) e)
      ≡⟨ sub0sub v₂ (subComp (ren2sub xs) vs) e ⟩
        sub (v₂ ∷ subComp (ren2sub xs) vs) e
      ∈ eval-term e (rv₂ , Rvs-ren xs rvs)
      ∎
      where open R-red-Reasoning Δ₂ τ₃

  eval-term : {Γ Δ : Cxt} → {vs : Sub Δ Γ} → {τ : typ} →
              (e : term Γ τ) → Rvs Δ vs → R Δ τ (sub vs e)
  eval-term (Val v) rvs = eval-value v rvs
  eval-term (Var x) rvs = lookup-var x rvs
  eval-term {Δ = Δ} {vs} {τ} (App {τ₂} e₁ e₂) rvs
    rewrite sym (renid (sub vs e₁))
    with eval-term e₁ rvs | eval-term e₂ rvs
  ... | ((nf₁ , red₁*) , r₁) | r₂
    = r₁ renId (sub vs e₂) r₂

-- TAPL: lemma 12.1.6
eval : {τ : typ} → (e : term [] τ) → terminating e
eval e with eval-term {Δ = []} e tt
... | r rewrite subid e = R-terminating r