open import Data.Nat

module RegisterMachine.PartialEvaluation {n : ℕ} where

import RegisterMachine
open RegisterMachine n

open import Function
open import Data.Fin
open import Relation.Nullary
open import Data.List using (_∷_; [])

----------------------------------------------------------------------
-- Evaluation state
--
open import Relation.Binary

State : Set
State = Mem

Σ₀ : State
Σ₀ = const zero

getVar : Reg → State → Val
getVar x Σ = Σ x

incVar : Reg → State → State
incVar x Σ = Σ′
  where
  Σ′ : State
  Σ′ y with toℕ x ≟ toℕ y
  ... | yes _ = +1 (getVar y Σ)
  ... | no _ = getVar y Σ

decVar : Reg → State → State
decVar x Σ = Σ′
  where
  Σ′ : State
  Σ′ y with toℕ x ≟ toℕ y
  ... | yes _ = -1 (Σ y)
  ... | no _ = Σ y

----------------------------------------------------------------------
-- Interpreter for RM
--
open import Coinduction
open import Category.Monad.Partiality
open Category.Monad.Partiality.Workaround
open import Category.Monad

private
  mutual
    eval∗P : Prog → State → State ⊥P
    eval∗P [] Σ = now Σ
    eval∗P (i ∷ is) Σ = evalP i Σ >>= eval∗P is

    evalP : Inst → State → State ⊥P
    evalP (inc x) Σ = now (incVar x Σ)
    evalP (dec x) Σ = now (decVar x Σ)
    evalP (loop x is) Σ with getVar x Σ
    ... | zero = now Σ
    ... | suc _ = eval∗P is Σ >>= λ Σ′ → later (♯ evalP (loop x is) Σ′)

eval∗ : Prog → State → State ⊥
eval∗ prog Σ = ⟦ eval∗P prog Σ ⟧P