{-# OPTIONS --without-K --safe #-}
module Lambda.Virtual-machine.Instructions (Name : Set) where
open import Equality.Propositional
open import Prelude
open import Lambda.Syntax Name
mutual
data Instr (n : ℕ) : Set where
var : Fin n → Instr n
clo : Code (suc n) → Instr n
app ret : Instr n
cal tcl : Name → Instr n
con : Bool → Instr n
bra : Code n → Code n → Instr n
Code : ℕ → Set
Code n = List (Instr n)
open Closure Code
data Stack-element : Set where
val : Value → Stack-element
ret : ∀ {n} → Code n → Env n → Stack-element
Stack : Set
Stack = List Stack-element
data State : Set where
⟨_,_,_⟩ : ∀ {n} → Code n → Stack → Env n → State
data Result : Set where
continue : State → Result
done : Value → Result
crash : Result