{-# OPTIONS --without-K --safe #-}

module STLC.Dynamics where

open import Lib
open import STLC.Statics

open import Data.Unit using (tt; )
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_; _◅◅_) renaming (gmap to *map)

data Value : Trm Γ T  Set where
  *  : Value (* {Γ})
  pr :  {s : Trm Γ S} {u : Trm Γ U}  Value s  Value u  Value (pr s u)
  Λ  : (t : Trm (S  Γ) T)  Value (Λ t)

infix 3 _↦_ _↦*_

data _↦_ : Trm Γ T  Trm Γ T  Set where
  π₁-pr    :  {s : Trm Γ S} {u : Trm Γ U} (vs : Value s) (vu : Value u)  π₁ (pr s u)  s
  π₂-pr    :  {s : Trm Γ S} {u : Trm Γ U} (vs : Value s) (vu : Value u)  π₂ (pr s u)  u
  Λ-$      : (t : Trm (S  Γ) T) {s : Trm Γ S} (vs : Value s)  (Λ t) $ s  t  s ⟧!

  π₁-cong  :  {t t′ : Trm Γ (S X U)}  t  t′  π₁ t  π₁ t′
  π₂-cong  :  {t t′ : Trm Γ (S X U)}  t  t′  π₂ t  π₂ t′
  pr-cong₁ :  {s s′ : Trm Γ S} (u : Trm Γ U)  s  s′  pr s u  pr s′ u
  pr-cong₂ :  {s : Trm Γ S} {u u′ : Trm Γ U} (vs : Value s)  u  u′  pr s u  pr s u′
  $-cong₁  :  {t t′ : Trm Γ (S  U)} (s : Trm Γ S)  t  t′  t $ s  t′ $ s
  $-cong₂  :  {t : Trm Γ (S  U)} {s s′ : Trm Γ S} (vt : Value t)  s  s′  t $ s  t $ s′

_↦*_ : Trm Γ T  Trm Γ T  Set
_↦*_ = Star _↦_

↦-¬Value :  {t t′ : Trm Γ T}  t  t′  ¬ Value t
↦-¬Value (pr-cong₁ u r) (pr vs vu) = ↦-¬Value r vs
↦-¬Value (pr-cong₂ vs r) (pr _ vu) = ↦-¬Value r vu

↦-determ :  {t t′ t″ : Trm Γ T}  t  t′  t  t″  t′  t″
↦-determ (π₁-pr vs vu) (π₁-pr vs′ vu′)     = refl
↦-determ (π₁-pr vs vu) (π₁-cong r′)        = ⊥-elim (↦-¬Value r′ (pr vs vu))
↦-determ (π₂-pr vs vu) (π₂-pr vs′ vu′)     = refl
↦-determ (π₂-pr vs vu) (π₂-cong r′)        = ⊥-elim (↦-¬Value r′ (pr vs vu))
↦-determ (Λ-$ t vs) (Λ-$ .t vs₁)           = refl
↦-determ (Λ-$ t vs) ($-cong₂ vt r′)        = ⊥-elim (↦-¬Value r′ vs)
↦-determ (π₁-cong r) (π₁-pr vs vu)         = ⊥-elim (↦-¬Value r (pr vs vu))
↦-determ (π₁-cong r) (π₁-cong r′)          = cong π₁ (↦-determ r r′)
↦-determ (π₂-cong r) (π₂-pr vs vu)         = ⊥-elim (↦-¬Value r (pr vs vu))
↦-determ (π₂-cong r) (π₂-cong r′)          = cong π₂ (↦-determ r r′)
↦-determ (pr-cong₁ u r) (pr-cong₁ .u r′)   = cong  z  pr z u) (↦-determ r r′)
↦-determ (pr-cong₁ u r) (pr-cong₂ vs r′)   = ⊥-elim (↦-¬Value r vs)
↦-determ (pr-cong₂ vs r) (pr-cong₁ _ r′)   = ⊥-elim (↦-¬Value r′ vs)
↦-determ (pr-cong₂ vs r) (pr-cong₂ vs₁ r′) = cong (pr _) (↦-determ r r′)
↦-determ ($-cong₁ s r) ($-cong₁ .s r′)     = cong  z  z $ s) (↦-determ r r′)
↦-determ ($-cong₁ s r) ($-cong₂ vt r′)     = ⊥-elim (↦-¬Value r vt)
↦-determ ($-cong₂ vt r) (Λ-$ t vs)         = ⊥-elim (↦-¬Value r vs)
↦-determ ($-cong₂ vt r) ($-cong₁ _ r′)     = ⊥-elim (↦-¬Value r′ vt)
↦-determ ($-cong₂ vt r) ($-cong₂ vt′ r′)   = cong (_ $_) (↦-determ r r′)

module ↦* where

  map :  {t t′ : Trm Γ T} (f : Trm Γ T  Trm Γ S)  (∀ {t t′ : Trm Γ T}  t  t′  f t ↦* f t′)  t ↦* t′  f t ↦* f t′
  map f pf ε        = ε
  map f pf (r  r*) = pf r ◅◅ map f pf r*

Halts : Trm Γ T  Set
Halts t =   t′  t ↦* t′ × Value t′)

Value⇒Halts : {t : Trm Γ T}  Value t  Halts t
Value⇒Halts {t = t} v = t , ε , v

↦-resp-Halts₁ :  {t t′ : Trm Γ T}  t  t′  Halts t  Halts t′
↦-resp-Halts₁ (π₁-pr vs vu) _                                 = _ , ε , vs
↦-resp-Halts₁ (π₂-pr vs vu) _                                 = _ , ε , vu
↦-resp-Halts₁ (Λ-$ t vs) (t″ , Λ-$ .t _  r′ , vt″)           = t″ , r′ , vt″
↦-resp-Halts₁ (Λ-$ t vs) (t″ , $-cong₂ vt st  r′ , vt″)      = ⊥-elim (↦-¬Value st vs)
↦-resp-Halts₁ (π₁-cong r) (t″ , π₁-pr vs vu  r′ , vt″)       = ⊥-elim (↦-¬Value r (pr vs vu))
↦-resp-Halts₁ (π₁-cong r) (t″ , π₁-cong st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″
↦-resp-Halts₁ (π₂-cong r) (t″ , π₂-pr vs vu  r′ , vt″)       = ⊥-elim (↦-¬Value r (pr vs vu))
↦-resp-Halts₁ (π₂-cong r) (t″ , π₂-cong st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″
↦-resp-Halts₁ (pr-cong₁ u r) (.(pr _ u) , ε , pr vs vu)       = ⊥-elim (↦-¬Value r vs)
↦-resp-Halts₁ (pr-cong₁ u r) (t″ , pr-cong₁ .u st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″
↦-resp-Halts₁ (pr-cong₁ u r) (t″ , pr-cong₂ vs st  r′ , vt″) = ⊥-elim (↦-¬Value r vs)
↦-resp-Halts₁ (pr-cong₂ vs r) (.(pr _ _) , ε , pr _ vu)       = ⊥-elim (↦-¬Value r vu)
↦-resp-Halts₁ (pr-cong₂ vs r) (t″ , pr-cong₁ _ st  r′ , vt″) = ⊥-elim (↦-¬Value st vs)
↦-resp-Halts₁ (pr-cong₂ vs r) (t″ , pr-cong₂ _ st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″
↦-resp-Halts₁ ($-cong₁ s r) (t″ , $-cong₁ .s st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″
↦-resp-Halts₁ ($-cong₁ s r) (t″ , $-cong₂ vt st  r′ , vt″)   = ⊥-elim (↦-¬Value r vt)
↦-resp-Halts₁ ($-cong₂ vt r) (t″ , Λ-$ t vs  r′ , vt″)       = ⊥-elim (↦-¬Value r vs)
↦-resp-Halts₁ ($-cong₂ vt r) (t″ , $-cong₁ _ st  r′ , vt″)   = ⊥-elim (↦-¬Value st vt)
↦-resp-Halts₁ ($-cong₂ vt r) (t″ , $-cong₂ _ st  r′ , vt″)
  rewrite ↦-determ r st                                       = t″ , r′ , vt″

↦-resp-Halts₂ :  {t t′ : Trm Γ T}  t  t′  Halts t′  Halts t
↦-resp-Halts₂ r (t″ , r′ , vt″) = t″ , r  r′ , vt″

Λ-$-subst : (t : Trm (S  Γ) T) (σ : Subst Δ Γ) {s : Trm Δ S}  Value s  (Λ t  σ ) $ s  t  s  σ 
Λ-$-subst t σ vs = subst  t′  (Λ t  σ ) $ _  t′) (Subst′.extend-qweaken-apply _ σ t) (Λ-$ (t  Subst′.qweaken _ σ ) vs)

module Direct where
  R : Trm [] T  Set
  R′ : Trm [] T  Set

  R t = Halts t × R′ t

  R′ {*} t     = 
  R′ {S X U} t = R (π₁ t) × R (π₂ t)
  R′ {S  U} t =  {s : Trm [] S}  R s  R (t $ s)

  R⇒Halts : {t : Trm [] T}  R t  Halts t
  R⇒Halts (h , _) = h

  ↦-resp-R₁ :  {t t′ : Trm [] T}  t  t′  R t  R t′
  ↦-resp-R′₁ :  {t t′ : Trm [] T}  t  t′  R′ t  R′ t′

  ↦-resp-R₁ r (ht , R′t) = ↦-resp-Halts₁ r ht , ↦-resp-R′₁ r R′t

  ↦-resp-R′₁ {*} r R′t           = tt
  ↦-resp-R′₁ {S X U} r (Rs , Ru) = ↦-resp-R₁ (π₁-cong r) Rs , ↦-resp-R₁ (π₂-cong r) Ru
  ↦-resp-R′₁ {S  U} r R′t Rs    = ↦-resp-R₁ ($-cong₁ _ r) (R′t Rs)

  ↦*-resp-R₁ :  {t t′ : Trm [] T}  t ↦* t′  R t  R t′
  ↦*-resp-R₁ ε Rt        = Rt
  ↦*-resp-R₁ (r  r*) Rt = ↦*-resp-R₁ r* (↦-resp-R₁ r Rt)

  ↦-resp-R₂ :  {t t′ : Trm [] T}  t  t′  R t′  R t
  ↦-resp-R′₂ :  {t t′ : Trm [] T}  t  t′  R′ t′  R′ t

  ↦-resp-R₂ r (Ht′ , R′t′) = ↦-resp-Halts₂ r Ht′ , ↦-resp-R′₂ r R′t′

  ↦-resp-R′₂ {*} r Rt′             = tt
  ↦-resp-R′₂ {S X U} r (Rs′ , Ru′) = ↦-resp-R₂ (π₁-cong r) Rs′ , ↦-resp-R₂ (π₂-cong r) Ru′
  ↦-resp-R′₂ {S  U} r Rt′ Rs′     = ↦-resp-R₂ ($-cong₁ _ r) (Rt′ Rs′)

  ↦*-resp-R₂ :  {t t′ : Trm [] T}  t ↦* t′  R t′  R t
  ↦*-resp-R₂ ε Rt′        = Rt′
  ↦*-resp-R₂ (r  r*) Rt′ = ↦-resp-R₂ r (↦*-resp-R₂ r* Rt′)

  R-pr : {s : Trm [] S} {u : Trm [] U}  R s  R u  R (pr s u)
  R-pr {_} {_} {s} {u} Rs@((s′ , rs′ , vs′) , R′s) Ru@((u′ , ru′ , vu′) , R′u)
    = (pr s′ u′ , rs,u , pr vs′ vu′)
    , ↦*-resp-R₂ (↦*.map π₁  r  π₁-cong r  ε) rs,u ◅◅ π₁-pr vs′ vu′  ε) (↦*-resp-R₁ rs′ Rs)
    , ↦*-resp-R₂ (↦*.map π₂  r  π₂-cong r  ε) rs,u ◅◅ π₂-pr vs′ vu′  ε) (↦*-resp-R₁ ru′ Ru)
    where rs,u : pr s u ↦* pr s′ u′
          rs,u = ↦*.map  s  pr s u)  r  pr-cong₁ _ r  ε) rs′ ◅◅ ↦*.map (pr s′)  r  pr-cong₂ vs′ r  ε) ru′

  R-π₁ : {t : Trm [] (S X U)}  R t  R (π₁ t)
  R-π₁ (_ , Rs , _) = Rs

  R-π₂ : {t : Trm [] (S X U)}  R t  R (π₂ t)
  R-π₂ (_ , _ , Ru) = Ru

  R-$ : {t : Trm [] (S  U)} {s : Trm [] S}  R t  R s  R (t $ s)
  R-$ (_ , R′t) Rs = R′t Rs

  R-subst : {σ : Subst [] Γ}  Forall R σ  (t : Trm Γ T)  R (t  σ )
  R-subst R* *                 = (* , ε , *) , tt
  R-subst R* (var T∈)          = Forall′.lookup′ R* T∈
  R-subst R* (pr s u)          = R-pr (R-subst R* s) (R-subst R* u)
  R-subst R* (π₁ t)            = R-π₁ (R-subst R* t)
  R-subst R* (π₂ t)            = R-π₂ (R-subst R* t)
  R-subst R* (s $ u)           = R-$ (R-subst R* s) (R-subst R* u)
  R-subst {_} {_} {σ} R* (Λ {S} t) = (Λ t′ , ε , Λ t′) , helper
    where t′ : Trm (S  []) _
          t′ = t  Subst′.qweaken S σ 
          helper : {s : Trm [] S}  R s  R ((Λ t  σ ) $ s)
          helper Rs@((s′ , rs , vs′) , R′s) =
            let Rs′ = R-subst (↦*-resp-R₁ rs Rs  R*) t
            in ↦*-resp-R₂ (↦*.map (_ $_)  r  $-cong₂ (Λ t′) r  ε) rs ◅◅ Λ-$-subst t σ vs′  ε) Rs′

  Rt : (t : Trm [] T)  R t
  Rt t with R-subst [] t
  ... | Rt′ rewrite Subst′.id-apply t = Rt′

  normalize : (t : Trm [] T)  Halts t
  normalize t = let Ht , _ = Rt t in Ht


module Another where

  mutual
    R : Trm [] T  Set
    R {T} t =  λ t′  t ↦* t′ × Σ (Value t′) λ v  RV t′ v

    RV : (t : Trm [] T) (v : Value t)  Set
    RV {*} .* *                    = 
    RV {S X T} .(pr _ _) (pr v v′) = RV _ v × RV _ v′
    RV {S  T} t v                 =  {s : Trm [] S} {v : Value s}  RV s v  R (t $ s)

  R⇒Halts : {t : Trm [] T}  R t  Halts t
  R⇒Halts (t′ , ↦t′ , v , _) = t′ , ↦t′ , v

  RV⇒R : {t : Trm [] T} {v : Value t}  RV t v  R t
  RV⇒R Rv = -, ε , -, Rv

  R-subst : {σ : Subst [] Γ}  Forall  t  Σ (Value t) (RV t)) σ  (t : Trm Γ T)  R (t  σ )
  R-subst R* *                              = * , ε , * , tt
  R-subst R* (var T∈)                       = RV⇒R (proj₂ (Forall′.lookup′ R* T∈))
  R-subst R* (pr s u)
    with R-subst R* s | R-subst R* u
  ...  | s′ , ↦*s′ , v  , Rv
       | u′ , ↦*u′ , v′ , Rv′               = pr s′ u′ , *map  s  pr s (u  _ )) (pr-cong₁ (u  _ )) ↦*s′ ◅◅ *map (pr s′) (pr-cong₂ v) ↦*u′ , pr v v′ , Rv , Rv′
  R-subst R* (π₁ t)
    with R-subst R* t
  ... | pr t _ , ↦*t′ , pr v v′ , Rv , Rv′  = t , *map π₁ π₁-cong ↦*t′ ◅◅ π₁-pr v v′  ε  , v , Rv
  R-subst R* (π₂ t)
    with R-subst R* t
  ... | pr _ t′ , ↦*t′ , pr v v′ , Rv , Rv′ = t′ , *map π₂ π₂-cong ↦*t′ ◅◅ π₂-pr v v′  ε  , v′ , Rv′
  R-subst R* (s $ u)
    with R-subst R* s | R-subst R* u
  ...  | s′ , ↦*s′ , v , Rv
       | Ru@(u′ , ↦*u′ , v′ , Rv′)
       with Rv Rv′
  ...     | su , ↦*su , v′ , Rv′            = su , *map (_$ (u  _ )) ($-cong₁ (u  _ )) ↦*s′ ◅◅ *map (_ $_) ($-cong₂ v) ↦*u′ ◅◅ ↦*su , v′ , Rv′
  R-subst {_} {S  T} {σ} R* (Λ t)          = Λ t′ , ε , Λ t′ , helper
    where t′ : Trm (S  []) _
          t′ = t  Subst′.qweaken S σ 
          helper : {s : Trm [] S} {v : Value s}  RV s v  R (Λ t′ $ s)
          helper {s} {v} Rv
            with R-subst ((v , Rv)  R*) t
          ...  | ts , ↦*ts , v″ , Rv″ = ts , (Λ-$-subst t σ v  ε) ◅◅ ↦*ts , v″ , Rv″

  Rt : (t : Trm [] T)  R t
  Rt t with R-subst [] t
  ... | Rt′ rewrite Subst′.id-apply t = Rt′

  normalize : (t : Trm [] T)  Halts t
  normalize t = R⇒Halts (Rt t)