-- | Module for printing the trace of the execution of an abstract
--   machine. Some examples are below.
module Trace(Node : Set) where

open import GeneralLemmas
open import Relation

infixr 4 _⟶⟨_⟩_

data Trace {A}(R : Rel A A) : Rel A A where
  _end : (a : A)  Trace R a a
  _⟶⟨_⟩_ : (a : A){b c : A}  R a b  Trace R b c  Trace R a c

*-to-Trace :  {A}{a b : A}{R}  (R *) a b  Trace R a b
*-to-Trace [] = _ end
*-to-Trace (x  steps) = _ ⟶⟨ x  *-to-Trace steps

det-Trace :  {A}{R : Rel A A}(steps : )(a : A)  R is-decidable   λ b  Trace R a b
det-Trace zero a dec = a , a end
det-Trace (suc steps) a dec with dec a
det-Trace (suc steps) a dec | yes (b , step) =
  let (c , steps) = det-Trace steps b dec
   in c , a ⟶⟨ step  steps
det-Trace (suc steps) a dec | no _ = a , a end

open import CES Node
open import CES.Properties Node
open import Lambda Node
open import Data.Nat
open import MachineCode Node

codeExample-trace :   b  Trace _⟶CES_ ((codeExample , [] , [])) b)
codeExample-trace = det-Trace 100 (codeExample , [] , []) ⟶CES-is-decidable

codeExample-result = proj₁ codeExample-trace

factorial : Term
factorial =
  let
    v₀ = var 0
    v₁ = var 1
    l1 = lit 1
    _*'_ = op _*_
    _-'_ = op _∸_
    Z = let x = ƛ (v₁ $ (ƛ (v₁ $ v₁ $ v₀)))
         in ƛ (x $ x)
    fact = ƛ (ƛ (if0 v₀ then l1 else (v₀ *' (v₁ $ (v₀ -' l1)))))
   in Z $ fact $ lit 5

factorial' : Code
factorial' = compile factorial

factorial-trace :  λ b  Trace _⟶CES_ (factorial' , [] , []) b
factorial-trace = det-Trace 130 (factorial' , [] , []) ⟶CES-is-decidable

factorial-result = proj₁ factorial-trace