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