module TermShape where

open import Relation.Unary using (_∈_; _⊆_)
open import Size
open import Library
open import SizedInfiniteTypes
open import Terms
open import Substitution


-- Evaluation contexts.

data ECxt (Γ : Cxt) : (a b : Ty)  Set where
  appl  :  {a b} (u : Tm Γ a)   ECxt Γ (a →̂ b) b
  fst   :  {a b}  ECxt Γ (a ×̂ b) a
  snd   :  {a b}  ECxt Γ (a ×̂ b) b
  _∗l   :  {a b∞} (u : Tm Γ ( a))  ECxt Γ (▸̂ (delay a  b∞)) (▸̂ b∞)
  ∗r_   :  {a : Ty}{b∞} (t : Tm Γ (a →̂ force b∞))  ECxt Γ ( a) (▸̂ b∞)

-- Ehole Et E t ~~ Et = E[t]

data Ehole {Γ : Cxt} : {a b : Ty}  Tm Γ b  ECxt Γ a b  Tm Γ a  Set where
  appl  :  {a b t} (u : Tm Γ a)   Ehole (app t u) (appl u) (t  (a →̂ b))
  fst   :  {a b t}  Ehole {a = a ×̂ b} (fst t) fst t
  snd   :  {a b t}  Ehole {a = a ×̂ b} (snd t) snd t
  _∗l   :  {a b∞ t} (u : Tm Γ ( a))  Ehole {a = (▸̂ (delay a  b∞))} (t  u) (u ∗l) t
  ∗r_   :  {a : Ty}{b∞}{u} (t : Tm Γ (a →̂ force b∞))  Ehole ((( t)  (u   a))  ▸̂ b∞) (∗r t) u


-- Evaluation contexts are closed under substitution.

substEC :  {i vt Γ Δ a b}  (σ : RenSub {i} vt Γ Δ)  ECxt Γ a b  ECxt Δ a b
substEC σ (appl u) = appl (subst σ u)
substEC σ fst      = fst
substEC σ snd      = snd
substEC σ (u ∗l)   = subst σ u ∗l
substEC σ (∗r t₁)  = ∗r subst σ t₁

substEh :  {i vt Γ Δ a b}  (σ : RenSub {i} vt Γ Δ)   {E}{Et : Tm Γ b}{t : Tm Γ a}  (Eh : Ehole Et E t)
             Ehole (subst σ Et) (substEC σ E) (subst σ t)
substEh σ (appl u) = appl (subst σ u)
substEh σ fst      = fst
substEh σ snd      = snd
substEh σ (u ∗l)   = subst σ u ∗l
substEh σ (∗r t₁)  = ∗r subst σ t₁

mkEHole :  {Γ} {a b} (E : ECxt Γ a b) {t}  Σ _ \ E[t]  Ehole E[t] E t
mkEHole (appl u)  = _ , appl u
--mkEHole (appr t)  = _ , appr t
--mkEHole (pairl u) = _ , pairl u
--mkEHole (pairr t) = _ , pairr t
mkEHole fst       = _ , fst
mkEHole snd       = _ , snd
mkEHole (u ∗l)    = _ , u ∗l
mkEHole (∗r t)    = _ , ∗r t
--mkEHole abs       = _ , abs
--mkEHole ▹_        = _ , ▹_


_[_] :  {Γ} {a b} (E : ECxt Γ a b) (t : Tm Γ a)  Tm Γ b
E [ t ] = proj₁ (mkEHole E {t})

data ECxt* (Γ : Cxt) : Ty  Ty  Set where
  [] :  {a}  ECxt* Γ a a
  _∷_ :  {a₀ a₁ a₂}  ECxt Γ a₀ a₁  ECxt* Γ a₁ a₂  ECxt* Γ a₀ a₂

_[_]* :  {Γ} {a b} (E : ECxt* Γ a b) (t : Tm Γ a)  Tm Γ b
[] [ t ]* = t
(E  Es) [ t ]* = Es [ E [ t ] ]*

_++*_ :  {Γ a b c}  ECxt* Γ a b  ECxt* Γ b c  ECxt* Γ a c
[] ++* ys = ys
(x  xs) ++* ys = x  (xs ++* ys)

_∷r_ :  {Γ a b c}  ECxt* Γ a b  ECxt Γ b c  ECxt* Γ a c
xs ∷r x = xs ++* (x  [])

data Ehole* {Γ : Cxt} : {a b : Ty}  Tm Γ b  ECxt* Γ a b  Tm Γ a  Set where
  [] :  {a} {t : Tm Γ a}  Ehole* t [] t
  _∷_ :  {a b c t} {E : ECxt Γ b c} {Es : ECxt* Γ a b} {EEst Est}
         Ehole EEst E Est  Ehole* Est Es t  Ehole* EEst (Es ∷r E) t


-- Inductive definition of strong normalization.


-- Parameterized evaluation contexts

data PCxt {Γ : Cxt} (P : ∀{c}  Tm Γ c  Set) : {a b : Ty}  Tm Γ b  ECxt Γ a b  Tm Γ a  Set where

  appl  :  {a b t u}
           (𝒖 : P u)
           PCxt P (app t u) (appl u) (t  (a →̂ b))

  fst   :  {a b t}                  PCxt P (fst {a = a} {b = b} t) fst t

  snd   :  {a b t}                  PCxt P (snd {a = a} {b = b} t) snd t

  _∗l   :  {a b∞ t u} (𝒖 : P u)  PCxt P (_∗_ {a = a} {b∞} t u) (u ∗l) t

  ∗r_   :  {a : Ty}{b∞}{u t}
            (𝒕 : P (▹_ {a∞ = delay a  b∞} t))
                                     PCxt P (_<$>_ {a = a} {b∞} t u) (∗r t) u

-- Parameterized neutral terms.

data PNe {Γ} (P : ∀{c}  Tm Γ c  Set) {b} : Tm Γ b  Set where

  var  :  x                               PNe P (var x)

  elim :  {a} {t : Tm Γ a} {E Et}
          (𝒏 : PNe P t) (𝑬𝒕 : PCxt P Et E t)  PNe P Et

-- Parametrized weak head reduction

data _/_⇒_ {Γ} (P : ∀{c}  Tm Γ c  Set):  {a}  Tm Γ a   Tm Γ a  Set where

  β     :  {a b}{t : Tm (a  Γ) b}{u}
           (𝒖 : P u)
           P / (app (abs t) u)  subst0 u t

  β▹    :  {a b∞}{t : Tm Γ (a →̂  force b∞)}{u : Tm Γ a}
            P / ( t   u)  (▹_ {a∞ = b∞} (app t u))

  βfst  :  {a b}{t : Tm Γ a}{u : Tm Γ b}
           (𝒖 : P u)
           P / fst (pair t u)  t

  βsnd  :  {a b}{t : Tm Γ a}{u : Tm Γ b}
           (𝒕 : P t)
           P / snd (pair t u)  u

  cong  :  {a b t t' Et Et'}{E : ECxt Γ a b}
           (𝑬𝒕 : Ehole Et E t)
           (𝑬𝒕' : Ehole Et' E t')
           (t⇒ : P / t  t')
           P / Et  Et'

-- Weak head reduction is deterministic.

detP⇒ :  {a Γ} {P :  {c}  Tm Γ c  Set} {t t₁ t₂ : Tm Γ a}
        (t⇒₁ : P / t  t₁) (t⇒₂ : P / t  t₂)  t₁  t₂
detP⇒ (β _) (β _)                                              = ≡.refl
detP⇒ (β _) (cong (appl u) (appl .u) (cong () _ _))
detP⇒ β▹ β▹ = ≡.refl
detP⇒ β▹ (cong (._ ∗l) (._ ∗l) (cong () _ _))
detP⇒ β▹ (cong (∗r t) (∗r .t) (cong () _ _ ))
detP⇒ (βfst _) (βfst _)                                        = ≡.refl
detP⇒ (βfst _) (cong fst fst (cong () _ _))
detP⇒ (βsnd _) (βsnd _)                                        = ≡.refl
detP⇒ (βsnd 𝒕) (cong snd snd (cong () _ _))
detP⇒ (cong (appl u) (appl .u) (cong () _ _)) (β _)
detP⇒ (cong (._ ∗l) (._ ∗l) (cong () _ _)) β▹
detP⇒ (cong (∗r t₁) (∗r .t₁) (cong () _ _)) β▹
detP⇒ (cong fst fst (cong () _ _ )) (βfst _)
detP⇒ (cong snd snd (cong () _ _ )) (βsnd _)
detP⇒ (cong (appl u) (appl .u) x) (cong (appl .u) (appl .u) y) = ≡.cong  t  app t u) (detP⇒ x y)
detP⇒ (cong fst fst x) (cong fst fst y)                        = ≡.cong fst             (detP⇒ x y)
detP⇒ (cong snd snd x) (cong snd snd y)                        = ≡.cong snd             (detP⇒ x y)
detP⇒ (cong (u ∗l) (.u ∗l) x) (cong (.u ∗l) (.u ∗l) y)         = ≡.cong  t  t  u)   (detP⇒ x y)
detP⇒ (cong (∗r t) (∗r .t) x) (cong (∗r .t) (∗r .t) y)         = ≡.cong (_∗_ ( t))     (detP⇒ x y)
detP⇒ (cong (u ∗l) (.u ∗l) (cong () _ _)) (cong (∗r t) (∗r .t) _)
detP⇒ (cong (∗r t) (∗r .t) _) (cong (u ∗l) (.u ∗l) (cong () _ _))

-- Neutrals are closed under application.

pneApp : ∀{Γ a b}{P : ∀{c}  Tm Γ c  Set}{t : Tm Γ (a →̂ b)}{u : Tm Γ a} 
  PNe P t  P u  PNe P (app t u)
pneApp 𝒏 𝒖 = elim 𝒏 (appl 𝒖)


-- Functoriality of the notions wrt. P.

mapPCxt :  {Γ} {P Q : ∀{c}  Tm Γ c  Set} (P⊆Q :  {c}{t : Tm Γ c}  P t  Q t) {a b} {E : ECxt Γ a b}{Et t}  PCxt P Et E t -> PCxt Q Et E t
mapPCxt P⊆Q (appl u∈P) = appl (P⊆Q u∈P)
mapPCxt P⊆Q fst = fst
mapPCxt P⊆Q snd = snd
mapPCxt P⊆Q (u∈P ∗l) = P⊆Q u∈P ∗l
mapPCxt P⊆Q (∗r t∈P) = ∗r P⊆Q t∈P

mapPNe :  {Γ} {P Q : ∀{c}  Tm Γ c  Set} (P⊆Q :  {c}{t : Tm Γ c}  P t  Q t) {a}{t : Tm Γ a}  PNe P t -> PNe Q t
mapPNe P⊆Q (var x) = var x
mapPNe P⊆Q (elim t∈Ne E∈SNh) = elim (mapPNe P⊆Q t∈Ne) (mapPCxt P⊆Q E∈SNh)

mapP⇒ :  {Γ} {P Q : ∀{c}  Tm Γ c  Set} (P⊆Q :  {c}{t : Tm Γ c}  P t  Q t) {a}{t t' : Tm Γ a}  P / t  t'  Q / t  t'
mapP⇒ P⊆Q (β t∈P) = β (P⊆Q t∈P)
mapP⇒ P⊆Q (β▹ {a = a}) = β▹ {a = a}
mapP⇒ P⊆Q (βfst t∈P) = βfst (P⊆Q t∈P)
mapP⇒ P⊆Q (βsnd t∈P) = βsnd (P⊆Q t∈P)
mapP⇒ P⊆Q (cong Et Et' t→t') = cong Et Et' (mapP⇒ P⊆Q t→t')


_[_]⇒ :  {Γ} {P : ∀{c}  Tm Γ c  Set} {a b} (E : ECxt Γ a b) {t₁ t₂ : Tm Γ a}  P / t₁  t₂  P / E [ t₁ ]  E [ t₂ ]
E [ t⇒ ]⇒ = cong (proj₂ (mkEHole E)) (proj₂ (mkEHole E)) t⇒

_[_]⇒* :  {Γ} {P : ∀{c}  Tm Γ c  Set} {a b} (E : ECxt* Γ a b) {t₁ t₂ : Tm Γ a}  P / t₁  t₂  P / E [ t₁ ]*  E [ t₂ ]*
[]       [ t⇒ ]⇒* = t⇒
(E  Es) [ t⇒ ]⇒* = Es [ E [ t⇒ ]⇒ ]⇒*

hole→≡ :  {Γ a b}{Et t}{E : ECxt Γ a b}  (Es : Ehole Et E t)  Et  E [ t ]
hole→≡ (appl u) = ≡.refl
hole→≡ fst = ≡.refl
hole→≡ snd = ≡.refl
hole→≡ (u ∗l) = ≡.refl
hole→≡ (∗r t₁) = ≡.refl

lemma :  {Γ b} {a} {t : Tm Γ a} (Es : ECxt* Γ a b)
         {b₁} {E : ECxt Γ b b₁}
          E [ Es [ t ]* ]  (Es ++* (E  [])) [ t ]*
lemma [] = ≡.refl
lemma (x  Es) = lemma Es

hole*→≡ :  {Γ a b}{Et t}{E : ECxt* Γ a b}  (Es : Ehole* Et E t)  Et  E [ t ]*
hole*→≡ [] = ≡.refl
hole*→≡ {t = t} (_∷_ {Es = Es} x Es₁) rewrite hole→≡ x | hole*→≡ Es₁ = lemma Es

++*-unit :  {Γ a b}  (xs : ECxt* Γ a b)  xs ++* []  xs
++*-unit [] = ≡.refl
++*-unit (x  xs) = ≡.cong (_∷_ x) (++*-unit xs)
++*-assoc :  {Γ a b c d}  (xs : ECxt* Γ a b)  {ys : ECxt* Γ b c}  {zs : ECxt* Γ c d}  xs ++* (ys ++* zs)  (xs ++* ys) ++* zs
++*-assoc [] = ≡.refl
++*-assoc (x  xs) = ≡.cong (_∷_ x) (++*-assoc xs)

_++h*_ :  {Γ a b c} {Es1 : ECxt* Γ a b} {Es2 : ECxt* Γ b c}   {t1 t2 t3}  Ehole* t2 Es1 t3  Ehole* t1 Es2 t2   Ehole* t1 (Es1 ++* Es2) t3
_++h*_ {Es1 = Es1} xs [] rewrite ++*-unit Es1      = xs
_++h*_ {Es1 = Es1} xs (_∷_ {E = E} {Es = Es} x ys) rewrite ++*-assoc Es1 {Es} {E  []} = x  (xs ++h* ys)


mkEhole* :  {Γ} {a b} (E : ECxt* Γ a b) {t}  Ehole* (E [ t ]*) E t
mkEhole* [] = []
mkEhole* (E  Es) {t} = (proj₂ (mkEHole E)  []) ++h* mkEhole* Es