------------------------------------------------------------------------
-- A virtual machine
------------------------------------------------------------------------

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

module Lambda.Simplified.Delay-monad.Virtual-machine 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 Lambda.Simplified.Delay-monad.Interpreter
open import Lambda.Simplified.Syntax
open import Lambda.Simplified.Virtual-machine

open Closure Code

mutual

  -- A functional semantics for the VM.

  exec : ∀ {i} → State → Delay (Maybe Value) i
  exec s with step s
  ... | continue s′ = later (∞exec s′)
  ... | done v      = return (just v)
  ... | crash       = return nothing

  ∞exec : ∀ {i} → State → ∞Delay (Maybe Value) i
  force (∞exec s) = exec s