------------------------------------------------------------------------
-- A type soundness result
------------------------------------------------------------------------

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

module Lambda.Delay-monad.Type-soundness where

open import Equality.Propositional
open import Prelude

open import Function-universe equality-with-J
open import Maybe equality-with-J
open import Monad equality-with-J

open import Delay-monad.Always
open import Delay-monad.Monad
open import Delay-monad.Weak-bisimilarity

open import Lambda.Delay-monad.Interpreter
open import Lambda.Syntax

open Closure Tm

-- If we can prove □ ∞ (WF-MV σ) (run x), then x does not "go wrong".

does-not-go-wrong :  {σ} {x : M  Value} 
                      (WF-MV σ) (run x)  ¬ x ≈M fail
does-not-go-wrong (now {x = nothing} ())
does-not-go-wrong (now {x = just x} x-wf) ()
does-not-go-wrong (later x-wf)            (laterˡ x↯) =
  does-not-go-wrong (force x-wf) x↯

-- A "constructor" for □ i ∘ WF-MV.

_>>=-wf_ :
   {i σ τ} {x : M  Value} {f : Value  M  Value} 
   i (WF-MV σ) (run x) 
  (∀ {v}  WF-Value σ v   i (WF-MV τ) (run (f v))) 
   i (WF-MV τ) (MaybeT.run (x >>= f))
x-wf >>=-wf f-wf =
  □->>= x-wf λ { {nothing} ()
               ; {just v}  v-wf  f-wf v-wf
               }

-- Well-typed programs do not "go wrong".

mutual

  ⟦⟧-wf :  {i n Γ} (t : Tm n) {σ}  Γ  t  σ 
           {ρ}  WF-Env Γ ρ 
           i (WF-MV σ) (run ( t  ρ))
  ⟦⟧-wf (con i)   con             ρ-wf = now con
  ⟦⟧-wf (var x)   var             ρ-wf = now (ρ-wf x)
  ⟦⟧-wf (ƛ t)     (ƛ t∈)          ρ-wf = now (ƛ t∈ ρ-wf)
  ⟦⟧-wf (t₁ · t₂) (t₁∈ · t₂∈) {ρ} ρ-wf =
    ⟦⟧-wf t₁ t₁∈ ρ-wf >>=-wf λ f-wf 
    ⟦⟧-wf t₂ t₂∈ ρ-wf >>=-wf λ v-wf 
    ∙-wf f-wf v-wf

  ∙-wf :  {i σ τ f v} 
         WF-Value (σ  τ) f  WF-Value (force σ) v 
          i (WF-MV (force τ)) (run (f  v))
  ∙-wf (ƛ t₁∈ ρ₁-wf) v₂-wf =
    later λ { .force  ⟦⟧-wf _ t₁∈ (snoc-wf ρ₁-wf v₂-wf) }

type-soundness :  {t : Tm 0} {σ} 
                 empty  t  σ  ¬  t  empty ≈M fail
type-soundness {t} {σ} =
  empty  t  σ                      ↝⟨  t∈  ⟦⟧-wf _ t∈ empty-wf) 
    (WF-MV σ) (run ( t  empty))  ↝⟨ does-not-go-wrong ⟩□
  ¬  t  empty ≈M fail