-- Proof of termination based on TAPL chaper 12
-- checked on Agda 2.5.2, standard library 0.13

module normal-cbn 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-cbn

-- terminating
terminating : {Γ : Cxt} → {τ : typ} → term Γ τ → Set
terminating {Γ} {τ} e = Σ[ v ∈ value Γ τ ] reduce* e (Val v)
-- The result is a value.

-- TAPL: definition 12.1.2
R : (τ : typ) → term [] τ → Set
R Nat e₁ = terminating e₁
R (τ₂ ⇒ τ₁) e₁ =
  terminating e₁ ×
  ((e₂ : term [] τ₂) → R τ₂ e₂ → R τ₁ (App e₁ e₂))

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

terminating-red : {Γ : Cxt} → {τ : typ} → {e₁ e₂ : term Γ τ} →
                  reduce e₁ e₂ → terminating e₁ → terminating e₂
terminating-red () (v , r*Id)
terminating-red red (v , r*Trans e₁ e₂ .(Val v) red′ red*)
  with reduction-unique red red′
... | refl = (v , red*)

terminating-red-inv : {Γ : Cxt} → {τ : typ} → {e₁ e₂ : term Γ τ} →
                      reduce e₁ e₂ → terminating e₂ → terminating e₁
terminating-red-inv {e₁ = e₁} {e₂} red (v , red*) =
  (v , (begin e₁ ⟶⟨ red ⟩ e₂ ⟶*⟨ red* ⟩ (Val v) ∎))
  where open red-Reasoning

-- TAPL: lemma 12.1.4 (only if)
reduce-R : {τ : typ} → {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 ,
   (λ v₂ r → reduce-R (rApp₁ v₂ red) (f v₂ r)))

reduce*-R : {τ : 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 : {τ : 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 ,
   (λ v₂ r → reduce-inv-R (rApp₁ v₂ red) (f v₂ r)))

reduce*-inv-R : {τ : 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-Reasoning (τ : 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

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

-- 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 τ (Val (subV vs v))
  eval-value (Num n) rvs = (Num n , r*Id)
  eval-value {vs = vs} (Fun τ e) rvs =
    ((Fun τ (sub (lifts vs) e) , r*Id) ,
     (λ e₂ r₂ → eval-lambda vs e rvs e₂ r₂))
    where
    eval-lambda : ∀ {τ τ₁ Γ} (vs : Sub [] Γ) (e : term (τ ∷ Γ) τ₁) →
              Rvs vs →
              (e₂ : term [] τ) →
              R τ e₂ → R τ₁ (App (Val (Fun τ (sub (Var zero ∷ wks vs) e))) e₂)
    eval-lambda {τ₂} {τ₃} vs e rvs e₂ r₂ = begin
        App (Val (Fun τ₂ (sub (Var zero ∷ wks vs) e))) e₂
      ⟶⟨ rBeta (sub (Var zero ∷ wks vs) e) e₂ ⟩
        sub0 e₂ (sub (Var zero ∷ wks vs) e)
      ≡⟨ sub0sub e₂ vs e ⟩
        sub (e₂ ∷ vs) e
      ∈ eval-term e (r₂ , rvs)
      ∎
      where open R-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 = vs} (App e₁ e₂) rvs
    with eval-term e₁ rvs | eval-term e₂ rvs
  ... | ((v₁ , red₁*) , r₁) | r₂ = r₁ (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