{-# OPTIONS --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
mutual
data Instr (n : ℕ) : Type where
var : (x : Fin n) → Instr n
clo : (c : Code (suc n)) → Instr n
app : Instr n
ret : Instr n
Code : ℕ → Type
Code n = List (Instr n)
open Closure Code
data StackElement : Type where
val : (v : Value) → StackElement
ret : ∀ {n} (c : Code n) (ρ : Env n) → StackElement
Stack : Type
Stack = List StackElement
data State : Type where
⟨_,_,_⟩ : ∀ {n} (c : Code n) (s : Stack) (ρ : Env n) → State
pattern ⟨_∣_,_,_⟩ n c s ρ = ⟨_,_,_⟩ {n} c s ρ
data Result : Type where
continue : (s : State) → Result
done : (v : Value) → Result
crash : Result
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