------------------------------------------------------------------------
-- A virtual machine for the language
------------------------------------------------------------------------

-- To avoid having to deal with labels/jumps this virtual machine is
-- non-standard in several ways:
--
-- • Instructions can contain instruction sequences.
-- • Instructions can contain uncompiled expressions.
-- • The virtual machine invokes the compiler.

module VirtualMachine where

open import Syntax
open import Infinite

open import Data.List
open import Data.Nat
open import Data.Star
open import Data.Product
open import Relation.Unary hiding (U)

------------------------------------------------------------------------
-- Virtual machine

mutual

  -- A virtual machine code snippet is a list of instructions.

  data Inst : Set where
    push   : (n : ℕ) → Inst
    throw  : Inst
    loop   : (x : Expr partial) → Inst
    add    : Inst
    pop    : Inst
    mark   : (ops : Code) → Inst
    unmark : Inst
    set    : (i : Status) → Inst
    reset  : Inst

  Code : Set
  Code = List Inst

-- The virtual machine operates on a stack of items.

data Item : Set where
  nat : (n : ℕ) → Item
  han : (ops : Code) → Item
  int : (i : Status) → Item

Stack : Set
Stack = List Item

-- The virtual machine's transition relation.

data State : Set where
  ⟨_,_,_⟩ : (ops : Code) (i : Status) (s : Stack) → State
  ⟪_,_⟫   :              (i : Status) (s : Stack) → State

mutual

  data _⟶_ : State → State → Set where
    push      : ∀ {n ops i s}    → ⟨ push n    ∷ ops , i , s ⟩                 ⟶ ⟨ ops , i  , nat n ∷ s ⟩
    add       : ∀ {ops i m n s}  → ⟨ add       ∷ ops , i , nat n ∷ nat m ∷ s ⟩ ⟶ ⟨ ops , i  , nat (m + n) ∷ s ⟩
    pop       : ∀ {ops i n s}    → ⟨ pop       ∷ ops , i , nat n ∷ s ⟩         ⟶ ⟨ ops , i  , s ⟩
    mark      : ∀ {ops' ops i s} → ⟨ mark ops' ∷ ops , i , s ⟩                 ⟶ ⟨ ops , i  , han ops' ∷ s ⟩
    unmark    : ∀ {ops i x c s}  → ⟨ unmark    ∷ ops , i , x ∷ han c ∷ s ⟩     ⟶ ⟨ ops , i  , x ∷ s ⟩
    set       : ∀ {i' ops i s}   → ⟨ set i'    ∷ ops , i , s ⟩                 ⟶ ⟨ ops , i' , int i ∷ s ⟩
    reset     : ∀ {ops i x i' s} → ⟨ reset     ∷ ops , i , x ∷ int i' ∷ s ⟩    ⟶ ⟨ ops , i' , x ∷ s ⟩
    loop      : ∀ {x ops i s}    → ⟨ loop x    ∷ ops , i , s ⟩                 ⟶ ⟨ comp x (pop ∷ loop x ∷ ops) , i , s ⟩
    throw     : ∀ {ops i s}      → ⟨ throw     ∷ ops , i , s ⟩                 ⟶ ⟪ i , s ⟫

    interrupt : ∀ {op ops s}     → ⟨ op        ∷ ops , U , s ⟩                 ⟶ ⟪ U , s ⟫

    nat       : ∀ {i n s}        → ⟪ i , nat n   ∷ s ⟫                         ⟶ ⟪ i  , s ⟫
    int       : ∀ {i i' s}       → ⟪ i , int i'  ∷ s ⟫                         ⟶ ⟪ i' , s ⟫
    han       : ∀ {i ops s}      → ⟪ i , han ops ∷ s ⟫                         ⟶ ⟨ ops , B , int i ∷ s ⟩

  -- Compiler from the high-level language to the virtual machine
  -- language.

  comp : ∀ {t} → Expr t → Code → Code
  comp ⌜ nat n ⌝   ops = push n ∷ ops
  comp ⌜ throw ⌝   ops = throw ∷ ops
  comp (loop x)    ops = loop x ∷ ops
  comp (x ⊕ y)     ops = comp x (comp y (add ∷ ops))
  comp (x >> y)    ops = comp x (pop ∷ comp y ops)
  comp (x catch y) ops = mark (comp y (reset ∷ ops)) ∷ comp x (unmark ∷ ops)
  comp (block x)   ops = set B ∷ comp x (reset ∷ ops)
  comp (unblock x) ops = set U ∷ comp x (reset ∷ ops)

infix 4 _⟶⋆_

-- Reflexive transitive closure.

_⟶⋆_ : State → State → Set
_⟶⋆_ = Star _⟶_

-- "Infinite closure".

_⟶∞ : State → Set
_⟶∞ = Infinite _⟶_

-- Starting states for the virtual machine.

start : ∀ {t} → Expr t → Status → State
start e i = ⟨ comp e [] , i , [] ⟩

-- Final states.

_↛ : State → Set
s₁ ↛ = ∄ λ s₂ → s₁ ⟶ s₂