Shub.agda

open import Data.Nat
open import Relation.Binary.PropositionalEquality renaming (subst to ≡-subst)
open import Data.Empty
open import Data.Unit
open import Relation.Binary
open import Data.Star
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Product
open import Function using (_⟨_⟩_)
-- open import Function using (_∘_; id)

data Ty : Set where
  fun : Ty → Ty → Ty

infixl 21 _▷_

data Ctx : Set where
  [] : Ctx
  _▷_ : Ctx → Ty → Ctx

data Var (t : Ty) : Ctx → Set where
  vz : ∀ {Γ} → Var t (Γ ▷ t)
  vs : ∀ {Γ u} → Var t Γ → Var t (Γ ▷ u)

data _⊆_ : Ctx → Ctx → Set where
  done : [] ⊆ []
  keep : ∀ {a Γ Δ} → Γ ⊆ Δ → Γ ▷ a ⊆ Δ ▷ a
  drop : ∀ {a Γ Δ} → Γ ⊆ Δ → Γ ⊆ Δ ▷ a

⊆-refl : ∀ {Γ} → Γ ⊆ Γ
⊆-refl {[]} = done
⊆-refl {Γ ▷ _} = keep ⊆-refl

[]⊆ : ∀ Γ → [] ⊆ Γ
[]⊆ [] = done
[]⊆ (Γ ▷ _) = drop ([]⊆ Γ)

⊆-trans : ∀ {Γ Θ Δ} → Γ ⊆ Θ → Θ ⊆ Δ → Γ ⊆ Δ
⊆-trans done Θ⊆Δ = Θ⊆Δ
⊆-trans (keep Γ⊆Θ) (keep Θ⊆Δ) = keep (⊆-trans Γ⊆Θ Θ⊆Δ)
⊆-trans (drop Γ⊆Θ) (keep Θ⊆Δ) = drop (⊆-trans Γ⊆Θ Θ⊆Δ)
⊆-trans Γ⊆Θ (drop Θ⊆Δ) = drop (⊆-trans Γ⊆Θ Θ⊆Δ)

open import Data.List using (List; _∷_; [])

infixl 22 _<><_

_<><_ : Ctx → List Ty → Ctx
Γ <>< [] = Γ
Γ <>< (t ∷ Δ) = (Γ ▷ t) <>< Δ

data Tm (Γ : Ctx) : Ty → Set where
  var : ∀ {t} → Var t Γ → Tm Γ t
  lam : ∀ t {u} → (e : Tm (Γ ▷ t) u) → Tm Γ (fun t u)
  app : ∀ {u t} → (f : Tm Γ (fun u t)) → (e : Tm Γ u) → Tm Γ t

wk-var : ∀ {Γ Δ t} → Γ ⊆ Δ → Var t Γ → Var t Δ
wk-var done ()
wk-var (keep Γ⊆Δ) vz = vz
wk-var (keep Γ⊆Δ) (vs v) = vs (wk-var Γ⊆Δ v)
wk-var (drop Γ⊆Δ) v = vs (wk-var Γ⊆Δ v)

wk : ∀ {Γ Δ t} → Γ ⊆ Δ → Tm Γ t → Tm Δ t
wk Γ⊆Δ (var v) = var (wk-var Γ⊆Δ v)
wk Γ⊆Δ (lam t e) = lam t (wk (keep Γ⊆Δ) e)
wk Γ⊆Δ (app f e) = app (wk Γ⊆Δ f) (wk Γ⊆Δ e)

wk-var-refl : ∀ {Γ t} (x : Var t Γ) → wk-var ⊆-refl x ≡ x
wk-var-refl vz = refl
wk-var-refl (vs x) = cong vs (wk-var-refl x)

wk-refl : ∀ {Γ t} (e : Tm Γ t) → wk ⊆-refl e ≡ e
wk-refl (var x) = cong var (wk-var-refl x)
wk-refl (lam t e) = cong (lam t) (wk-refl e)
wk-refl (app f e) = cong₂ app (wk-refl f) (wk-refl e)

wk-var-trans : ∀ {Γ Θ Δ t} (Γ⊆Θ : Γ ⊆ Θ) (Θ⊆Δ : Θ ⊆ Δ) (x : Var t Γ) → wk-var Θ⊆Δ (wk-var Γ⊆Θ x) ≡ wk-var (⊆-trans Γ⊆Θ Θ⊆Δ) x
wk-var-trans done Θ⊆Δ ()
wk-var-trans (keep Γ⊆Θ) (keep Θ⊆Δ) vz = refl
wk-var-trans (keep Γ⊆Θ) (keep Θ⊆Δ) (vs x) rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl
wk-var-trans (drop Γ⊆Θ) (keep Θ⊆Δ) x rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl
wk-var-trans (keep Γ⊆Θ) (drop Θ⊆Δ) x rewrite wk-var-trans (keep Γ⊆Θ) Θ⊆Δ x = refl
wk-var-trans (drop Γ⊆Θ) (drop Θ⊆Δ) x rewrite wk-var-trans (drop Γ⊆Θ) Θ⊆Δ x = refl

wk-trans : ∀ {Γ Θ Δ t} (Γ⊆Θ : Γ ⊆ Θ) (Θ⊆Δ : Θ ⊆ Δ) (e : Tm Γ t) → wk Θ⊆Δ (wk Γ⊆Θ e) ≡ wk (⊆-trans Γ⊆Θ Θ⊆Δ) e
wk-trans Γ⊆Θ Θ⊆Δ (var x) rewrite wk-var-trans Γ⊆Θ Θ⊆Δ x = refl
wk-trans Γ⊆Θ Θ⊆Δ (lam t e) = cong (lam t) (wk-trans (keep Γ⊆Θ) (keep Θ⊆Δ) e)
wk-trans Γ⊆Θ Θ⊆Δ (app f e) = cong₂ app (wk-trans Γ⊆Θ Θ⊆Δ f) (wk-trans Γ⊆Θ Θ⊆Δ e)

_⊢⋆_ : Ctx → Ctx → Set
Γ ⊢⋆ Δ = ∀ {t} → Var t Δ → Tm Γ t

Shub : Ctx → Ctx → Set
Shub Γ Δ = ∀ Ξ → (Γ <>< Ξ) ⊢⋆ (Δ <>< Ξ)

subst : ∀ {Γ Δ t} → Shub Γ Δ → Tm Δ t → Tm Γ t
subst σ (var x) = σ [] x
subst σ (lam t e) = lam t (subst (σ ∘ (t ∷_)) e)
  where
    open import Function using (_∘_)
subst σ (app f e) = app (subst σ f) (subst σ e)

mono : ∀ {Γ Δ t} → Γ ⊢⋆ Δ → Γ ▷ t ⊢⋆ Δ ▷ t
mono σ vz = var vz
mono σ (vs x) = wk (drop ⊆-refl) (σ x)

wks : ∀ {Γ Δ Θ} → Γ ⊆ Θ → Γ ⊢⋆ Δ → Θ ⊢⋆ Δ
wks sub σ x = wk sub (σ x)

sub : ∀ {Γ Δ} → Γ ⊢⋆ Δ → Shub Γ Δ
sub σ [] = σ
sub σ (x ∷ Ξ) = sub (mono σ) Ξ

push : ∀ {Γ t} → Tm Γ t → Γ ⊢⋆ Γ ▷ t
push e₀ vz = e₀
push e₀ (vs x) = var x

extend : ∀ {Γ Δ t} → Tm Γ t → Γ ⊢⋆ Δ → Γ ⊢⋆ (Δ ▷ t)
extend e σ vz = e
extend e σ (vs x) = σ x

-- ⊆⇒⊢⋆ : ∀ {Γ Δ} → Δ ⊆ Γ → Γ ⊢⋆ Δ
-- ⊆⇒⊢⋆ sub e = wk sub e

-- ⊢⋆-trans : ∀ {Γ Δ Θ} → Γ ⊢⋆ Θ → Θ ⊢⋆ Δ → Γ ⊢⋆ Δ
-- ⊢⋆-trans σ [] = []
-- ⊢⋆-trans σ (ρ ▷ e) = ⊢⋆-trans σ ρ ▷ subst σ e

-- ⊢⋆-refl : ∀ {Γ} → Γ ⊢⋆ Γ
-- ⊢⋆-refl = ⊆⇒⊢⋆ ⊆-refl

-- subst-var-⊆ : ∀ {Δ Γ Γ′ t} σ (x : Var t Δ) (sub : Γ ⊆ Γ′) →
--               subst-var (⊢⋆-wk sub σ) x ≡ wk sub (subst-var σ x)
-- subst-var-⊆ {[]} [] () sub
-- subst-var-⊆ {Δ ▷ _} (σ ▷ e) vz sub = refl
-- subst-var-⊆ {Δ ▷ _} (σ ▷ e) (vs x) sub = subst-var-⊆ σ x sub

-- subst-wk-var : ∀ {Γ Δ t} (sub : Γ ⊆ Δ) (x : Var t Γ) → subst-var (⊆⇒⊢⋆ sub) x ≡ var (wk-var sub x)
-- subst-wk-var {[]} sub ()
-- subst-wk-var {Γ ▷ x} (keep sub) vz = refl
-- subst-wk-var {Γ ▷ _} (keep sub) (vs x) =
--     subst-var-⊆ (⊆⇒⊢⋆ sub) x (drop ⊆-refl)
--   ⟨ trans ⟩
--     cong (wk (drop ⊆-refl)) (subst-wk-var sub x)
--   ⟨ trans ⟩
--     cong (λ y → var (vs y)) (wk-var-refl (wk-var sub x))
-- subst-wk-var {Γ ▷ _} (drop sub) x =
--     subst-var-⊆ (⊆⇒⊢⋆ sub) x (drop ⊆-refl)
--   ⟨ trans ⟩
--     cong (wk (drop ⊆-refl)) (subst-wk-var sub x)
--   ⟨ trans ⟩
--     cong (λ y → var (vs y)) (wk-var-refl (wk-var sub x))

-- subst-wk : ∀ {Γ Δ t} (sub : Γ ⊆ Δ) (e : Tm Γ t) → subst (⊆⇒⊢⋆ sub) e ≡ wk sub e
-- subst-wk sub (var x) = subst-wk-var sub x
-- subst-wk sub (lam t e) = cong (lam t) (subst-wk (keep sub) e)
-- subst-wk sub (app f e) = cong₂ app (subst-wk sub f) (subst-wk sub e)

-- subst-refl : ∀ {Γ t} → (e : Tm Γ t) → subst ⊢⋆-refl e ≡ e
-- subst-refl {Γ} e = subst-wk ⊆-refl e ⟨ trans ⟩ wk-refl e

-- todo1 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e : Tm (Γ ▷ u) t) (e′ : Tm [] u) →
--         subst ([] ▷ e′) (subst (sub (wks σ)) e) ≡ subst (σ ▷ e′) e
-- -- todo1 σ e e′ rewrite sym (⊢⋆-wk-refl ([] ▷ e′)) | sym (⊢⋆-wk-refl (σ ▷ e′)) = todo11 ([] ▷ e′) σ e

data Value : {Γ : Ctx} → {t : Ty} → Tm Γ t → Set where
  lam : ∀ {Γ t} → ∀ u (e : Tm _ t) → Value {Γ} (lam u e)

data _==>_ {Γ} : ∀ {t} → Rel (Tm Γ t) lzero where
  app-lam : ∀ {t u} (f : Tm _ t) {v : Tm _ u} → Value v → app (lam u f) v ==> subst (sub (push v)) f
  appˡ : ∀ {t u} {f f′ : Tm Γ (fun u t)} → f ==> f′ → (e : Tm Γ u) → app f e ==> app f′ e
  appʳ : ∀ {t u} {f} → Value {Γ} {fun u t} f → ∀ {e e′ : Tm Γ u} → e ==> e′ → app f e ==> app f e′

_==>*_ : ∀ {Γ t} → Rel (Tm Γ t) _
_==>*_ = Star _==>_

NF : ∀ {a b} {A : Set a} → Rel A b → A → Set _
NF step x = ∄ (step x)

value⇒normal : ∀ {Γ t e} → Value {Γ} {t} e → NF _==>_ e
value⇒normal (lam t e) (_ , ())

Deterministic : ∀ {a b} {A : Set a} → Rel A b → Set _
Deterministic step = ∀ {x y y′} → step x y → step x y′ → y ≡ y′

deterministic : ∀ {Γ t} → Deterministic (_==>_ {Γ} {t})
deterministic (app-lam f _) (app-lam ._ _) = refl
deterministic (app-lam f v) (appˡ () _)
deterministic (app-lam f v) (appʳ f′ e) = ⊥-elim (value⇒normal v (, e))
deterministic (appˡ () e) (app-lam f v)
deterministic (appˡ f e) (appˡ f′ ._) = cong _ (deterministic f f′)
deterministic (appˡ f e) (appʳ f′ _) = ⊥-elim (value⇒normal f′ (, f))
deterministic (appʳ f e) (app-lam f′ v) = ⊥-elim (value⇒normal v (, e))
deterministic (appʳ f e) (appˡ f′ _) = ⊥-elim (value⇒normal f (, f′))
deterministic (appʳ f e) (appʳ f′ e′) = cong _ (deterministic e e′)

Halts : ∀ {Γ t} → Tm Γ t → Set
Halts e = ∃ λ e′ → e ==>* e′ × Value e′

value⇒halts : ∀ {Γ t e} → Value {Γ} {t} e → Halts e
value⇒halts {e = e} v = e , ε , v

-- -- This would not be strictly positive!
-- data Saturated : ∀ {Γ t} → Tm Γ t → Set where
--   fun : ∀ {t u} {f : Tm [] (fun t u)} → Halts f → (∀ {e} → Saturated e → Saturated (app f e)) → Saturated f

mutual
  Saturated : ∀ {t} → Tm [] t → Set
  Saturated e = Halts e × Saturated′ _ e

  Saturated′ : ∀ t → Tm [] t → Set
  Saturated′ (fun t u) f = ∀ {e} → Saturated e → Saturated (app f e)

saturated⇒halts : ∀ {t e} → Saturated {t} e → Halts e
saturated⇒halts = proj₁

open import Function.Equivalence hiding (sym)
open import Function.Equality using (_⟨$⟩_)

step‿preserves‿halting : ∀ {Γ t} {e e′ : Tm Γ t} → e ==> e′ → Halts e ⇔ Halts e′
step‿preserves‿halting {e = e} {e′ = e′} step = equivalence fwd bwd
  where
    fwd : Halts e → Halts e′
    fwd (e″ , ε , v) = ⊥-elim (value⇒normal v (, step))
    fwd (e″ , s ◅ steps , v) rewrite deterministic step s = e″ , steps , v

    bwd : Halts e′ → Halts e
    bwd (e″ , steps , v) = e″ , step ◅ steps , v

step‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e ⇔ Saturated e′
step‿preserves‿saturated step = equivalence (fwd step) (bwd step)
  where
    fwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e → Saturated e′
    fwd {fun s t} step (halts , sat) = Equivalence.to (step‿preserves‿halting step) ⟨$⟩ halts , λ e → fwd (appˡ step _) (sat e)

    bwd : ∀ {t} {e e′ : Tm _ t} → e ==> e′ → Saturated e′ → Saturated e
    bwd {fun s t} step (halts , sat) = Equivalence.from (step‿preserves‿halting step) ⟨$⟩ halts , λ e → bwd (appˡ step _) (sat e)

step*‿preserves‿saturated : ∀ {t} {e e′ : Tm _ t} → e ==>* e′ → Saturated e ⇔ Saturated e′
step*‿preserves‿saturated ε = id
step*‿preserves‿saturated (step ◅ steps) = step*‿preserves‿saturated steps ∘ step‿preserves‿saturated step

data Instantiation : ∀ Γ → Set where
  [] : Instantiation []
  _▷_ : ∀ {Γ t} → Instantiation Γ → Σ (Tm [] t) (λ e → Value e × Saturated e) → Instantiation (Γ ▷ t)

inst : ∀ {Γ} → Instantiation Γ → [] ⊢⋆ Γ
inst [] ()
inst (env ▷ (e , _ , _)) vz = e
inst (env ▷ _) (vs x) = inst env x

extend-env : ∀ {Γ t u } (e′ : Tm [] t ) {vs : Value e′ × Saturated e′} (env : Instantiation Γ) (x : Var u (Γ ▷ t)) → inst (env ▷ (e′ , vs)) x ≡ extend e′ (inst env) x
extend-env e′ env vz = refl
extend-env e′ env (vs x) = refl

saturate-var : ∀ {Γ} → (env : Instantiation Γ) → ∀ {t} (x : Var t Γ) → Saturated (sub (inst env) [] x)
saturate-var (_ ▷ (_ , _ , sat)) vz = sat
saturate-var (env ▷ _) (vs x) = saturate-var env x

app-lam* : ∀ {Γ t} {e e′ : Tm Γ t} → e ==>* e′ → Value e′ → ∀ {u} (f : Tm _ u) → app (lam t f) e ==>* subst (sub (push e′)) f
app-lam* steps v f = gmap _ (appʳ (lam _ _)) steps  ◅◅ app-lam f v ◅ ε

-- todo11 : ∀ {Γ Δ Θ Ξ t} (ρ : Θ ⊢⋆ Ξ) (σ : Γ ⊢⋆ Δ) (e : Tm (Δ ++ Ξ) t) → subst (Γ +▷ ρ) (subst (σ ▷+ Ξ) e) ≡ subst (σ ▷▷ ρ) e
-- todo11 {Γ} {Δ} {Θ} {Ξ} ρ σ e = {!!}

-- todo21 : ∀ {t u} → (e : Tm {!!} t) (e′ : Tm [] u) → subst {!!} (subst {!!} e) ≡ subst ({!!} ▷[ e′ ]▷ {!!}) e
-- todo21 = {!!}

open import Data.Sum

split : ∀ {Δ t} Ξ → Var t (Δ <>< Ξ) → Tm ([] <>< Ξ) t ⊎ Var t Δ
split [] x = inj₂ x
split (t ∷ Ξ) x = {!!}

_><_ : ∀ {Γ Δ} → Γ ⊢⋆ Δ → (Ξ : List Ty) → (Γ <>< Ξ) ⊢⋆ (Δ <>< Ξ)
σ >< [] = σ
(σ >< (t ∷ Ξ)) x = {!!}

todo2-var : ∀ {Γ u t} Ξ → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (x : Var t ((Γ ▷ u) <>< Ξ)) →
            subst (sub (push e′ >< Ξ)) ((σ >< (u ∷ Ξ)) x) ≡ (extend e′ σ >< Ξ) x
todo2-var [] σ e′ vz = {!!}
todo2-var [] σ e′ (vs x) = {!!}
todo2-var (x₁ ∷ Ξ) σ e′ x = {!!}

todo1-var : ∀ {Γ u t} → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (x : Var t (Γ ▷ u)) →
            subst (sub (push e′)) (mono σ x) ≡ extend e′ σ x
todo1-var σ e′ vz = refl
todo1-var σ e′ (vs x) with σ x
todo1-var σ e′ (vs x) | var y = wk-refl (var y)
todo1-var σ e′ (vs x) | lam t e = cong (lam t) {!mono σ!}
todo1-var σ e′ (vs x) | app f e = {!!}

todo2 : ∀ {Γ Ξ u t} → (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm ((Γ ▷ u) <>< Ξ) t) →
         subst (sub (push e′ >< Ξ)) (subst (sub (σ >< (u ∷ Ξ))) e) ≡ subst (sub ((extend e′ σ >< Ξ))) e
todo2 = {!!}

-- todo2 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm (Γ ▷ u) t) →
--         subst (sub (push e′)) (subst (sub (mono σ)) e) ≡ subst (sub (extend e′ σ)) e
-- todo2 = {!!}

todo1 : ∀ {Γ u t} (σ : [] ⊢⋆ Γ) (e′ : Tm [] u) (e : Tm (Γ ▷ u) t) →
        subst (sub (push e′)) (subst (sub (mono σ)) e) ≡ subst (sub (extend e′ σ)) e
todo1 σ e′ (var x) = todo1-var σ e′ x
todo1 σ e′ (lam t e) = cong (lam t) {!!}
todo1 σ e′ (app e e₁) = {!!}

saturate : ∀ {Γ} → (env : Instantiation Γ) → ∀ {t} → (e : Tm Γ t) → Saturated (subst (sub (inst env)) e)
saturate env (var x) = saturate-var env x
saturate env (app f e) with saturate env f | saturate env e
saturate env (app f e) | _ , sat-f | sat-e = sat-f sat-e
saturate {Γ} env {fun .u t} (lam u f) = value⇒halts (lam u (subst _ f)) , sat-f
  where
    sat-f : ∀ {e : Tm _ u} → Saturated e → Saturated (app (lam u (subst _ f)) e)
    sat-f {e} sat-e@((e′ , steps , v) , _) = Equivalence.from (step*‿preserves‿saturated f==>*f′) ⟨$⟩ sat-f′
      where
        sat-e′ : Saturated e′
        sat-e′ = Equivalence.to (step*‿preserves‿saturated steps) ⟨$⟩ sat-e

        f′ = subst (sub (inst (env ▷ (e′ , v , sat-e′)))) f

        sat-f′ : Saturated f′
        sat-f′ = saturate (env ▷ (e′ , v , sat-e′)) f

        lemma : subst (sub (push e′)) (subst (sub (mono (inst env))) f) ≡ subst (sub (inst (env ▷ (e′ , v , sat-e′)))) f
        lemma = todo1 (inst env) e′ f ⟨ trans ⟩ {!!}

        f==>*f′ : _ ==>* f′
        f==>*f′ = ≡-subst (λ f₀ → _ ==>* f₀) lemma (app-lam* steps v (subst (sub (mono (inst env))) f))

normalization : ∀ {t} → (e : Tm [] t) → Halts e
normalization e = {!!} -- rewrite sym (subst-refl e) = saturated⇒halts (saturate [] e)