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

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

import Lambda.Virtual-machine.Instructions

module Lambda.Virtual-machine
  {Name : Set}
  (open Lambda.Virtual-machine.Instructions Name)
  (def : Name → Code )
  where

open import Colist using (Colist)
open import Equality.Propositional
open import Prelude

open import List equality-with-J using (_++_)
open import Monad equality-with-J
open import Vec.Data equality-with-J

open import Lambda.Delay-crash using (Delay-crash)
open import Lambda.Delay-crash-trace
open import Lambda.Syntax Name

open Closure Code

-- A single step of the computation.

step : State → Result
step ⟨ var x     ∷ c ,                           s  , ρ  ⟩ = cont ⟨ c       , val (index x ρ) ∷ s ,     ρ  ⟩
step ⟨ clo c′    ∷ c ,                           s  , ρ  ⟩ = cont ⟨ c       , val (lam c′ ρ)  ∷ s ,     ρ  ⟩
step ⟨ app       ∷ c , val v ∷ val (lam c′ ρ′) ∷ s  , ρ  ⟩ = cont ⟨ c′      , ret c ρ         ∷ s , v ∷ ρ′ ⟩
step ⟨ ret       ∷ c , val v ∷       ret c′ ρ′ ∷ s  , ρ  ⟩ = cont ⟨ c′      , val v           ∷ s ,     ρ′ ⟩
step ⟨ cal f     ∷ c ,                   val v ∷ s  , ρ  ⟩ = cont ⟨ def f   , ret c ρ         ∷ s , v ∷ [] ⟩
step ⟨ tcl f     ∷ c ,                   val v ∷ s  , ρ  ⟩ = cont ⟨ def f   ,                   s , v ∷ [] ⟩
step ⟨ con b     ∷ c ,                           s  , ρ  ⟩ = cont ⟨ c       , val (con b)     ∷ s ,     ρ  ⟩
step ⟨ bra c₁ c₂ ∷ c ,         val (con true)  ∷ s  , ρ  ⟩ = cont ⟨ c₁ ++ c ,                   s ,     ρ  ⟩
step ⟨ bra c₁ c₂ ∷ c ,         val (con false) ∷ s  , ρ  ⟩ = cont ⟨ c₂ ++ c ,                   s ,     ρ  ⟩
step ⟨ []            ,                   val v ∷ [] , [] ⟩ = done v
step _                                                     = crash

-- A functional semantics for the VM. The result includes a trace of
-- all the encountered states.

mutual

  exec⁺ : ∀ {i} → State → Delay-crash-trace State Value i
  exec⁺ s = later s λ { .force → exec⁺′ (step s) }

  exec⁺′ : ∀ {i} → Result → Delay-crash-trace State Value i
  exec⁺′ (cont s) = exec⁺ s
  exec⁺′ (done v) = now v
  exec⁺′ crash    = crash

-- The semantics without the trace of states.

exec : ∀ {i} → State → Delay-crash Value i
exec = delay-crash ∘ exec⁺

-- The stack sizes of all the encountered states.

stack-sizes : ∀ {i} → State → Colist ℕ i
stack-sizes = Colist.map stack-size ∘ trace ∘ exec⁺