------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

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

module Lambda.Simplified.Delay-monad.Interpreter where

open import Equality.Propositional
open import Prelude

open import Monad equality-with-J

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

open import Lambda.Simplified.Syntax

open Closure Tm

------------------------------------------------------------------------
-- The interpreter

infix  _∙_

mutual

  ⟦_⟧ : ∀ {i n} → Tm n → Env n → Delay Value i
  ⟦ var x ⟧   ρ = return (ρ x)
  ⟦ ƛ t ⟧     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ >>= λ v₁ →
                  ⟦ t₂ ⟧ ρ >>= λ v₂ →
                  v₁ ∙ v₂

  _∙_ : ∀ {i} → Value → Value → Delay Value i
  ƛ t₁ ρ ∙ v₂ = later (∞⟦ t₁ ⟧ (snoc ρ v₂))

  ∞⟦_⟧ : ∀ {i n} → Tm n → Env n → ∞Delay Value i
  force (∞⟦ t ⟧ ρ) = ⟦ t ⟧ ρ

------------------------------------------------------------------------
-- An example

mutual

  -- The semantics of Ω is the non-terminating computation never.

  Ω-loops : ⟦ Ω ⟧ empty ∼ never
  Ω-loops = later-cong ∞Ω-loops

  ∞Ω-loops : ⟦ Ω ⟧ empty ∞∼ never
  force ∞Ω-loops = Ω-loops