X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/7be2a6546f666dbbc5e3fe756766ee17e3c3d46a..HEAD:/src/Lambda.hs?ds=inline diff --git a/src/Lambda.hs b/src/Lambda.hs index 3026b75..428ac99 100644 --- a/src/Lambda.hs +++ b/src/Lambda.hs @@ -26,6 +26,9 @@ import Control.Monad.State import Lambda.Term +import Debug.Trace +import Lambda.Parser.Fancy () + -- $setup -- >>> import Control.Applicative -- >>> import Lambda.Parser.Fancy @@ -133,14 +136,22 @@ travPre fnc term = tr fnc (term, E, Down) -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY) -- Just (λx.x) -- --- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 1000 x) (alphaNorm <$> toNormalForm Eager 1000 x) +-- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 100 x) (alphaNorm <$> toNormalForm Eager 100 x) -- inf = tRead "(\\d.a ((\\d c.c d c) (\\x y z.x z (y z)) (\\f.(\\x.f (x x)) (\\x.f (x x))) e))" + +toNormalFormDebug :: Strategy -> Int -> Term -> Maybe Term +toNormalFormDebug Eager n = flip evalStateT 0 . travPost (prnt >=> cnt >=> short n >=> return . reduceStep) +toNormalFormDebug Lazy n = flip evalStateT 0 . travPre (prnt >=> cnt >=> short n >=> return . reduceStep) + toNormalForm :: Strategy -> Int -> Term -> Maybe Term toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep) toNormalForm Lazy n = flip evalStateT 0 . travPre (cnt >=> short n >=> return . reduceStep) +prnt :: (Monad m) => Term -> StateT Int m Term +prnt t = traceShow t $ return t + cnt :: (Monad m) => Term -> StateT Int m Term cnt t@RedEx{} = do modify (+ 1)