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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
