------------------------------------------------------------------------
-- A semantics which uses closures and environments
------------------------------------------------------------------------

module Lambda.Closure where

open import Coinduction
open import Data.Fin
open import Data.Function
open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality

open import Lambda.Syntax using (Tm; con; var; ƛ; _·_)

------------------------------------------------------------------------
-- Environments and values

-- Defined in a module parametrised on the type of values.

module Closure (Tm :   Set) where

 mutual

  -- Environments.

  Env :   Set
  Env n = Vec Value n

  -- Values. Lambdas are represented using closures, so values do not
  -- contain any free variables.

  data Value : Set where
    con : (i : )  Value
    ƛ   :  {n} (t : Tm (suc n)) (ρ : Env n)  Value

open Closure Tm public

------------------------------------------------------------------------
-- Big-step semantics (for both terminating and non-terminating
-- computations)

-- Semantic domain. ⊥ represents non-termination.

data Sem : Set where
     : Sem
  val : (v : Value)  Sem

-- Conditional coinduction: coinduction only for ⊥.

∞? : Sem  Set  Set
∞?        = 
∞? (val v) = id₁

-- Big-step semantics.

infix 4 _⊢_⇒_

data _⊢_⇒_ {n} (ρ : Env n) : Tm n  Sem  Set where
  var :  {x}  ρ  var x  val (lookup x ρ)
  con :  {i}  ρ  con i  val (con i)
  ƛ   :  {t}  ρ  ƛ t  val (ƛ t ρ)
  app :  {t₁ t₂ n t} {ρ′ : Env n} {v s}
        (t₁⇓   : ρ  t₁  val (ƛ t ρ′))
        (t₂⇓   : ρ  t₂  val v)
        (t₁t₂⇒ : ∞? s (v  ρ′  t  s)) 
        ρ  t₁ · t₂  s
  ·ˡ  :  {t₁ t₂}
        (t₁⇑ :  (ρ  t₁  )) 
        ρ  t₁ · t₂  
  ·ʳ  :  {t₁ t₂ v}
        (t₁⇓ : ρ  t₁  val v)
        (t₂⇑ :  (ρ  t₂  )) 
        ρ  t₁ · t₂  

------------------------------------------------------------------------
-- The semantics is deterministic

private
 mutual

  lemma₁ :  {n} {ρ : Env n} {t v₁ v₂} 
           ρ  t  val v₁  ρ  t  val v₂  val v₁  val v₂
  lemma₁ var                 var                    = refl
  lemma₁ con                 con                    = refl
  lemma₁ ƛ                   ƛ                      = refl
  lemma₁ (app t₁⇓ t₂⇓ t₁t₂⇓) (app t₁⇓′ t₂⇓′ t₁t₂⇓′)
    with lemma₁ t₁⇓ t₁⇓′ | lemma₁ t₂⇓ t₂⇓′
  ... | refl | refl = lemma₁ t₁t₂⇓ t₁t₂⇓′

  lemma₂ :  {n} {ρ : Env n} {t v} 
           ρ  t  val v  ρ  t    val v  
  lemma₂ var ()
  lemma₂ con ()
  lemma₂ ƛ   ()
  lemma₂ (app t₁⇓ t₂⇓ t₁t₂⇓) (app t₁⇓′ t₂⇓′ t₁t₂⇑)
    with lemma₁ t₁⇓ t₁⇓′ | lemma₁ t₂⇓ t₂⇓′
  ... | refl | refl = lemma₂ t₁t₂⇓ ( t₁t₂⇑)
  lemma₂ (app t₁⇓ t₂⇓ t₁t₂⇓) (·ˡ t₁⇑)      with lemma₂ t₁⇓ ( t₁⇑)
  ... | ()
  lemma₂ (app t₁⇓ t₂⇓ t₁t₂⇓) (·ʳ t₁⇓′ t₂⇑) with lemma₂ t₂⇓ ( t₂⇑)
  ... | ()

deterministic :  {n} {ρ : Env n} {t} v₁ v₂ 
                ρ  t  v₁  ρ  t  v₂  v₁  v₂
deterministic                 d₁ d₂ = refl
deterministic (val v₁)         d₁ d₂ = lemma₂ d₁ d₂
deterministic         (val v₂) d₁ d₂ = sym $ lemma₂ d₂ d₁
deterministic (val v₁) (val v₂) d₁ d₂ = lemma₁ d₁ d₂