Victor Nazarov wrote:
import Control.Monad.Writer
-- use a difference list or something for better performance type Trace v = [Zipper v]
whnf :: Term v -> Writer (Trace v) (Term v) whnf t = whnf' ([],t) where whnf' (AppL e':cxt, Lam x e) = tell (cxt, App (Lam x e) e') >> whnf' (cxt , subst x e' e) whnf' (cxt , App f e) = whnf' (AppL e:cxt, f) whnf' z = return $ unwind z
The definition of whnf is basically left unchanged, except that a redex is recorded via tell whenever a beta-reduction is about to be performed. The recorded terms can be printed afterwards
printTrace :: Writer (Trace v) (Term v) -> IO () printTrace w = let (t, ts) = runWriter t ts putStrLn . unlines . map show $ ts
Is this function lazy? Can I run this code on term without nf and print n-first steps:
printTraceN :: Int -> Writer (Trace v) (Term v) -> IO () printTraceN n w = let (t, ts) = runWriter t ts in putStrLn . unlines . map show $ take n ts
Will this work:
printTraceN 5 (read "(\x. x x x) (\x. x x x)")
Yes, it should (you can just try, right? :). That's because tell w >> something is basically let (w', x) = something in (w ++ w', x) Now, something may loop forever, but w ++ w' doesn't care, it prepends w no matter what w' is. Of course, asking for x (the normal form in our case) instead of w ++ w' won't succeed when something loops forever. (Cave: this is only true for the writer monad in Control.Monad.Writer.Lazy which is imported by default. The writer monad in Control.Monad.Writer.Strict intentionally behaves differently.) Regards, apfelmus