module RegisterMachine.PartialEvaluationTest where

open import RegisterMachine.PartialEvaluation
import RegisterMachine
open RegisterMachine 

open import Data.Fin
open import Data.Nat
open import Data.List using (_∷_; []; _++_; replicate)

v0 : Reg
v0 = inject₁ (fromℕ )

v1 : Reg
v1 = fromℕ 

p : ℕ → Prog
p x = setup ++ v1←2v0
  where
  setup : Prog
  setup = replicate x (inc v0)

  v1←2v0 : Prog
  v1←2v0 = loop v0 (inc v1 ∷ inc v1 ∷ dec v0 ∷ []) ∷ []

open import Data.Nat.Show using (show)
open import Data.String using (String)
open import Data.Colist
open import Category.Monad.Partiality
open import Function using (_∘_)
open import Coinduction using (♭; ♯_)

trace : Prog → Colist String
trace prog = go (eval∗ prog Σ₀)
  where
  go : State ⊥ → Colist String
  go (now Σ) = (show ∘ toℕ ∘ getVar v1) Σ ∷ ♯ []
  go (later Σ⊥) = "Didn't terminate" ∷ ♯ (go (♭ Σ⊥))

open import IO

main = run (mapM putStrLn (trace (p )))