module Evaluation where

open import Library
open import Delay
open import Syntax
open import RenamingAndSubstitution

-- Identity environment.

ide :  Γ  Env  Γ Γ
ide ε       = ε
ide (Γ , a) = renenv (wkr renId) (ide Γ) , ne (var zero)

-- Looking up in an environment.

lookup :  {i Γ Δ a}  Var Γ a  Env i Δ Γ  Val i Δ a
lookup zero    (ρ , v) = v
lookup (suc x) (ρ , v) = lookup x ρ

lookup≤ :  {Γ Δ Δ' a} (x : Var Γ a) (ρ : Env  Δ Γ) (η : Ren Δ' Δ) 
          Val∋ renval η (lookup x ρ)  lookup x (renenv η ρ)
lookup≤ zero    (ρ , v) η = ≈reflVal (renval η v)
lookup≤ (suc x) (ρ , v) η = lookup≤ x ρ η

-- Weakening a value to an extended context.

weakVal :  {i Δ a c}  Val i Δ c  Val i (Δ , a) c
weakVal = renval (wkr renId)

mutual
  eval : ∀{i Γ Δ a}  Tm Γ a  Env i Δ Γ  Val i Δ a
  eval (var x)   ρ = lookup x ρ
  eval (abs t)   ρ = lam t ρ
  eval (app t u) ρ = apply (eval t ρ) (eval u ρ)

  apply :  {i Δ a b}  Val i Δ (a  b)  Val i Δ a  Val i Δ b
  apply (ne w)    v = ne (app w v)
  apply (lam t ρ) v = later (beta t ρ v)
  apply (later w) v = later (∞apply w v)

  ∞apply :  {i Δ a b}  ∞Val i Δ (a  b)  Val i Δ a  ∞Val i Δ b
  force (∞apply w v) = apply (force w) v

  beta :  {i Γ a b} (t : Tm (Γ , a) b)
    {Δ : Cxt} (ρ : Env i Δ Γ) (v : Val i Δ a)  ∞Val i Δ b
  force (beta t ρ v) = eval t (ρ , v)

-- apply-cong
mutual
  eval-cong : ∀{i Γ Δ a}(t : Tm Γ a){ρ ρ' : Env  Δ Γ}  Env∋ ρ ≈⟨ i ⟩≈ ρ' 
              Val∋ eval t ρ ≈⟨ i ⟩≈ eval t ρ'
  eval-cong (var zero)    (p ≈, q) = q
  eval-cong (var (suc x)) (p ≈, q) = eval-cong (var x) p
  eval-cong (abs t)   p = ≈lam p
  eval-cong (app t u) p = apply-cong (eval-cong t p) (eval-cong u p)

  apply-cong :  {i Δ a b}{f f' : Val  Δ (a  b)}{v v' : Val  Δ a} 
               Val∋ f ≈⟨ i ⟩≈ f'  Val∋ v ≈⟨ i ⟩≈ v' 
               Val∋ apply f v ≈⟨ i ⟩≈ apply f' v'
  apply-cong (≈lam p)    q = ≈later (beta-cong _ p q)
  apply-cong (≈ne p)     q = ≈ne (≈app p q)
  apply-cong (≈later p) q = ≈later (∞apply-cong p q)

  ∞apply-cong :  {i Δ a b}{f f' : ∞Val  Δ (a  b)}{v v' : Val  Δ a} 
                ∞Val∋ f ≈⟨ i ⟩≈ f'  Val∋ v ≈⟨ i ⟩≈ v' 
                ∞Val∋ ∞apply f v ≈⟨ i ⟩≈ ∞apply f' v'
  ≈force (∞apply-cong p q) = apply-cong (≈force p) q

  beta-cong :  {i Γ a b} (t : Tm (Γ , a) b)
    {Δ : Cxt}{ρ ρ' : Env  Δ Γ}{v v' : Val  Δ a} 
    Env∋ ρ ≈⟨ i ⟩≈ ρ'  Val∋ v ≈⟨ i ⟩≈ v' 
    ∞Val∋ beta t ρ v ≈⟨ i ⟩≈ beta t ρ' v'
  ≈force (beta-cong t p q) = eval-cong t (p ≈, q)

mutual
  reneval :  {i Γ Δ Δ′ a} (t : Tm Γ a) (ρ : Env  Δ Γ) (η : Ren Δ′ Δ) 
    Val∋ (renval η $ eval t ρ) ≈⟨ i ⟩≈ (eval t $ renenv η ρ)
  reneval (var x)   ρ η = lookup≤ x ρ η
  reneval (abs t)   ρ η = ≈lam (≈reflEnv (renenv η ρ))
  reneval (app t u) ρ η = begin
    renval η (apply (eval t ρ) (eval u ρ))
    ≈⟨ renapply (eval t ρ) (eval u ρ) η 
    apply (renval η (eval t ρ)) (renval η (eval u ρ))
    ≈⟨ apply-cong (reneval t ρ η) (reneval u ρ η) 
    apply (eval t (renenv η ρ)) (eval u (renenv η ρ))
     where open ≈Val-Reasoning

  renapply  : ∀{i Γ Δ a b} (f : Val  Γ (a  b))(v : Val  Γ a)(η : Ren Δ Γ) 
    Val∋ (renval η $ apply f v) ≈⟨ i ⟩≈ (apply (renval η f) (renval η v))
  renapply (ne x)    v η = ≈reflVal _
  renapply (lam t ρ) v η = ≈later (renbeta t ρ v η)
  renapply (later p) v η = ≈later (∞renapply p v η)

  ∞renapply  : ∀{i Γ Δ a b}(f : ∞Val  Γ (a  b))(v : Val  Γ a)(η : Ren Δ Γ) 
     ∞Val∋ (∞renval η $ ∞apply f v) ≈⟨ i ⟩≈ (∞apply (∞renval η f) (renval η v))
  ≈force (∞renapply f v η) = renapply (force f) v η

  renbeta :  {i Γ Δ E a b} (t : Tm (Γ , a) b)(ρ : Env  Δ Γ) (v : Val  Δ a) 
    (η : Ren E Δ) 
     ∞Val∋ ∞renval η $ (beta t ρ v) ≈⟨ i ⟩≈ (beta t (renenv η ρ) (renval η v))
  ≈force (renbeta t ρ v η) = reneval t (ρ , v) η

mutual
  readback : ∀{i Γ a}  Val i Γ a  Delay i (Nf Γ a)
  readback {a = } (ne w)    = ne  <$> nereadback w
  readback {a = } (later w) = later (∞readback w)
  readback {a = _  _} v     = later (abs ∞<$> eta v)

  ∞readback : ∀{i Γ a}  ∞Val i Γ a  ∞Delay i (Nf Γ a)
  force (∞readback w) = readback (force w)

  eta : ∀{i Γ a b}  Val i Γ (a  b)  ∞Delay i (Nf (Γ , a) b)
  force (eta v) = readback (apply (weakVal v) (ne (var zero)))

  nereadback : ∀{i Γ a}  NeVal i Γ a  Delay i (Ne Γ a)
  nereadback (var x)   = now (var x)
  nereadback (app w v) = app <$> nereadback w <*> readback v


mutual
  readback-cong : ∀{i Γ} a {v v' : Val  Γ a}  Val∋ v ≈⟨ i ⟩≈ v' 
                  readback v ≈⟨ i ⟩≈ readback v'
  readback-cong        (≈ne p)    = map-cong ne (nereadback-cong  p)
  readback-cong        (≈later p) = ≈later (∞readback-cong _ p)
  readback-cong (a  b) p          =
    ≈later (∞map-cong abs (eta-cong p))

  ∞readback-cong : ∀{i Γ} a {v v' : ∞Val  Γ a}  ∞Val∋ v ≈⟨ i ⟩≈ v' 
                  ∞readback v ∞≈⟨ i ⟩≈ ∞readback v'
  ≈force (∞readback-cong a p) = readback-cong a (≈force p)

  nereadback-cong : ∀{i Γ} a {n n' : NeVal  Γ a}  NeVal∋ n ≈⟨ i ⟩≈ n' 
                  nereadback n ≈⟨ i ⟩≈ nereadback n'
  nereadback-cong a ≈var       = ≈now _ _ refl
  nereadback-cong a (≈app p q) =
    *-cong (map-cong app (nereadback-cong _ p)) (readback-cong _ q)

  eta-cong : ∀{i Γ a b}{v v' : Val  Γ (a  b)} 
             Val∋ v ≈⟨ i ⟩≈ v'  eta v ∞≈⟨ i ⟩≈ eta v'
  ≈force (eta-cong p) =
    readback-cong _ (apply-cong (renval-cong (wkr renId) p) (≈ne ≈var))

-- these proofs could surely be shortened, readback-cong would help

mutual
  rennereadback : ∀{i Γ Δ a}(η : Ren Δ Γ)(t : NeVal  Γ a) 
                (rennen η <$> nereadback t) ≈⟨ i ⟩≈ (nereadback (rennev η t))
  rennereadback η (var x) = ≈now _ _ refl
  rennereadback η (app t u) = begin
    rennen η <$> (app <$> nereadback t <*> readback u)
    ≈⟨ lifta2lem1 app (rennen η) (nereadback t) (readback u)  
     m n  rennen η (app m n)) <$> nereadback t <*> readback u
    ≡⟨⟩
     m n  app (rennen η m) (rennf η n)) <$> nereadback t <*> readback u
    ≈⟨ lifta2lem2 app (rennen η) (rennf η) (nereadback t) (readback u) 
    app <$> (rennen η <$> nereadback t) <*> (rennf η <$> readback u)
    ≈⟨ *-cong (map-cong app (rennereadback η t)) (renreadback _ η u) 
    (app <$> nereadback (rennev η t) <*> readback (renval η u))
    
    where open ≈-Reasoning

  renreadback   : ∀{i Γ Δ} a (η : Ren Δ Γ)(v : Val  Γ a) 
                (rennf η <$> readback v) ≈⟨ i ⟩≈ (readback (renval η v))
  renreadback  η (ne w) =
    begin
      rennf η  <$>  (ne  <$> nereadback w)
      ≈⟨ map-compose (nereadback w) 
      (rennf η  ne)     <$> nereadback w
      ≡⟨⟩
      (Nf.ne  rennen η) <$> nereadback w
      ≈⟨ ≈sym (map-compose (nereadback w)) 
      ne <$>  (rennen η  <$> nereadback w)
      ≈⟨ map-cong ne (rennereadback η w) 
      ne <$>   nereadback (rennev η w)
    
    where open ≈-Reasoning

  renreadback  η (later p) = ≈later (∞renreadback  η p)
  renreadback (a  b) η f   = ≈later (begin
    (eta f ∞>>=  a₁  now (abs a₁))) ∞>>=  x'  now (rennf η x'))
    ∞≈⟨ ∞bind-assoc (eta f) 
    (eta f ∞>>= λ a₁  now (abs a₁) >>= λ x'  now (rennf η x'))
    ≡⟨⟩
    (eta f ∞>>=  a₁  now (abs (rennf (liftr η) a₁))))
    ≡⟨⟩
    (eta f ∞>>= λ a₁  now (rennf (liftr η) a₁) >>= λ a₁  now (abs a₁))
    ∞≈⟨ ∞≈sym (∞bind-assoc (eta f)) 
    (eta f ∞>>=  a₁  now (rennf (liftr η) a₁))) ∞>>=  a₁  now (abs a₁))
    ∞≈⟨ ∞bind-cong-l (reneta η f)  a  now (abs a)) 
    eta (renval η f) ∞>>=  a₁  now (abs a₁))
    )
    where open ∞≈-Reasoning

  ∞renreadback   : ∀{i Γ Δ} a (η : Ren Δ Γ)(v : ∞Val  Γ a) 
                (rennf η ∞<$> ∞readback v) ∞≈⟨ i ⟩≈ (∞readback (∞renval η v))
  ≈force (∞renreadback a η v) = renreadback a η (force v)

  reneta  : ∀{i Γ Δ a b} (η : Ren Δ Γ)(v : Val  Γ (a  b)) 
          (rennf (liftr η) ∞<$> eta v) ∞≈⟨ i ⟩≈ (eta (renval η v))
  ≈force (reneta η f) = begin
    readback (apply (renval (wkr renId) f) (ne (var zero))) Bind.>>=
       a  now (rennf (wkr η , zero) a))
    ≈⟨ renreadback _ (liftr η) (apply (renval (wkr renId) f) (ne (var zero))) 
    readback (renval (wkr η , zero)
                     (apply (renval (wkr renId) f) (ne (var zero))))
    ≈⟨ readback-cong _ (renapply (renval (wkr renId) f) (ne (var zero))
                      (liftr η) ) 
    readback (apply (renval (liftr η) (renval (wkr renId) f)) (ne (var zero)))
    ≈⟨  readback-cong _ (apply-cong (renvalcomp (liftr η) (wkr renId) f)
                                    (≈reflVal _))  
    readback (apply (renval (renComp (liftr η) (wkr renId)) f) (ne (var zero)))
    ≡⟨ cong  η  readback (apply (renval η f) (ne (var zero))))
            (lemrr (wkr η) zero renId)  
    readback (apply (renval (renComp (wkr η) renId) f) (ne (var zero)))
    ≡⟨ cong  η  readback (apply (renval η f) (ne (var zero))))
            (wkrcomp η renId) 
    readback (apply (renval (wkr (renComp η renId)) f) (ne (var zero)))
    ≡⟨ cong  η  readback (apply (renval (wkr η) f) (ne (var zero))))
            (trans (ridr η) (sym $ lidr η) ) 
    readback (apply (renval (wkr (renComp renId η)) f) (ne (var zero)))
    ≡⟨ cong  η  readback (apply (renval η f) (ne (var zero))))
            (sym (wkrcomp renId η)) 
    readback (apply (renval (renComp (wkr renId) η) f) (ne (var zero)))
    ≈⟨ readback-cong _ (apply-cong (≈symVal (renvalcomp (wkr renId) η f))
                                 (≈reflVal _)) 
    readback (apply (renval (wkr renId) (renval η f)) (ne (var zero)))
     where open ≈-Reasoning

nf : ∀{Γ a}(t : Tm Γ a)  Delay  (Nf Γ a)
nf t = readback (eval t (ide _))

-- this stuff is for the substitution lemma primarily
evalS : ∀{Γ Δ Δ′}  Sub Δ Γ  Env  Δ′ Δ  Env  Δ′ Γ
evalS ε       ρ = ε
evalS (σ , v) ρ = evalS σ ρ , eval v ρ

renevalS :  {i Γ Γ' Δ Δ′} (σ : Sub Γ Γ') (ρ : Env  Δ Γ) (η : Ren Δ′ Δ) 
    Env∋ (renenv η $ evalS σ ρ) ≈⟨ i ⟩≈ (evalS σ $ renenv η ρ)
renevalS ε       ρ η = ≈ε
renevalS (σ , t) ρ η = renevalS σ ρ η ≈, reneval t ρ η

lookupR : ∀{Γ Γ' Δ}(σ : Ren Γ' Γ)(ρ : Env  Δ Γ')  Env  Δ Γ
lookupR ε       ρ = ε
lookupR (σ , x) ρ = lookupR σ ρ , lookup x ρ

renlookupR : ∀{Γ Γ' Δ Δ'}(η : Ren Δ' Δ)(σ : Ren Γ' Γ)(ρ : Env  Δ Γ') 
             Env∋ renenv η (lookupR σ ρ) ≈⟨  ⟩≈ lookupR σ (renenv η ρ)
renlookupR η ε       ρ = ≈ε
renlookupR η (σ , x) ρ = renlookupR η σ ρ ≈, lookup≤ x ρ η

lookupRwkr : ∀{Γ Γ' Δ a}(u : Val  Δ a)(σ : Ren Γ' Γ)(ρ : Env  Δ Γ') 
      Env∋  lookupR σ ρ ≈⟨  ⟩≈ lookupR (wkr σ) (ρ , u)
lookupRwkr u ε       ρ = ≈ε
lookupRwkr u (σ , x) ρ = (lookupRwkr u σ ρ) ≈, ≈reflVal (lookup x ρ)

lookupRrenId : ∀{Γ Δ}(ρ : Env  Δ Γ) 
      Env∋  lookupR renId ρ ≈⟨  ⟩≈ ρ
lookupRrenId ε       = ≈ε
lookupRrenId (ρ , v) =
  ≈transEnv (≈symEnv (lookupRwkr v renId ρ)) (lookupRrenId ρ) ≈, ≈reflVal v

lookuplookr : ∀{Γ Γ' Δ a}(ρ : Env  Δ Γ')(σ : Ren Γ' Γ)(x : Var Γ a) 
              Val∋ lookup (lookr σ x) ρ ≈⟨  ⟩≈ lookup x (lookupR σ ρ)
lookuplookr ρ (σ , y) zero    = ≈reflVal (lookup y ρ)
lookuplookr ρ (σ , y) (suc x) = lookuplookr ρ σ x