------------------------------------------------------------------------
-- Most of a virtual machine
------------------------------------------------------------------------

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

module Lambda.Simplified.Virtual-machine where

open import Equality.Propositional
open import Prelude

open import Vec.Function equality-with-J

open import Lambda.Simplified.Syntax

------------------------------------------------------------------------
-- Instruction set

mutual

  -- Instructions.

  data Instr (n : ) : Set where
    var : (x : Fin n)  Instr n
    clo : (c : Code (suc n))  Instr n
    app : Instr n
    ret : Instr n

  -- Code.

  Code :   Set
  Code n = List (Instr n)

-- Environments and values.

open Closure Code

------------------------------------------------------------------------
-- Stacks and states

-- Stacks.

data StackElement : Set where
  val : (v : Value)  StackElement
  ret :  {n} (c : Code n) (ρ : Env n)  StackElement

Stack : Set
Stack = List StackElement

-- States.

data State : Set where
  ⟨_,_,_⟩ :  {n} (c : Code n) (s : Stack) (ρ : Env n)  State

pattern ⟨_∣_,_,_⟩ n c s ρ = ⟨_,_,_⟩ {n} c s ρ

------------------------------------------------------------------------
-- A kind of small-step semantics for the virtual machine

-- The result of running the VM one step.

data Result : Set where
  continue : (s : State)  Result
  done     : (v : Value)  Result
  crash    : Result

-- A single step of the computation.

step : State  Result
step  var x   c ,                          s , ρ  = continue  c  , val (ρ x)     s ,        ρ  
step  clo c′  c ,                          s , ρ  = continue  c  , val (ƛ c′ ρ)  s ,        ρ  
step  app     c , val v  val (ƛ c′ ρ′)   s , ρ  = continue  c′ , ret c ρ       s , cons v ρ′ 
step  ret     c , val v  ret c′ ρ′       s , ρ  = continue  c′ , val v         s ,        ρ′ 
step  zero  []  ,                 val v  [] , ρ  = done v
step _                                               = crash