From: TomᚠMusil Date: Fri, 12 Dec 2014 20:53:38 +0000 (+0100) Subject: fix doctests X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/356502c3cf71bb0e19a1c2166fcbbf5ae88a1805 fix doctests --- diff --git a/src/Lambda.hs b/src/Lambda.hs index f828f4d..0cedf4a 100644 --- a/src/Lambda.hs +++ b/src/Lambda.hs @@ -20,10 +20,12 @@ module Lambda , tRead -- * Reduction , reduce + , toNormalForm + , Strategy(..) ) where -import Data.Text as T +import Data.Text as T hiding (map) import Data.Attoparsec.Text import Control.Applicative import Control.Monad.State @@ -31,8 +33,10 @@ import Control.Monad.State -- $setup -- >>> import Test.QuickCheck -- >>> import Control.Applicative --- >>> let aTerm 0 = liftA (Var . ("x" ++) . show) (arbitrary :: Gen Int) --- >>> let aTerm n = oneof [aTerm 0, liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))] +-- >>> let aVarName = oneof . map (pure . (:[])) $ ['a'..'e'] +-- >>> let aVar = liftA Var aVarName +-- >>> let aTerm 0 = aVar +-- >>> let aTerm n = oneof [aVar, liftA2 Lambda aVarName $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))] -- >>> instance Arbitrary Term where arbitrary = sized aTerm cY :: Term @@ -50,7 +54,7 @@ type VarName = String -- >>> print $ Lambda "x" (Var "x") -- (λx.x) -data Term = EmptyT | Var VarName | Lambda VarName Term | App Term Term deriving (Eq) +data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq) pattern RedEx x t s = App (Lambda x t) s pattern AppApp a b c = App a (App b c) @@ -155,20 +159,11 @@ reduceStep :: (Monad m) => Term -> m Term reduceStep (RedEx x s t) = return $ substitute x t s reduceStep t = return $ t -traversPost :: (Monad m) => (Term -> m Term) -> Term -> m Term -traversPost f (App t u) = do - nt <- traversPost f t - nu <- traversPost f u - case App nt nu of - l@(RedEx _ _ _) -> traversPost f =<< f l - r -> return r -traversPost f (Lambda x t) = return . Lambda x =<< traversPost f t -traversPost f (Var x) = return $ (Var x) - data Z = R Term Z | L Z Term | ZL VarName Z | E data D = Up | Down -data Zip = Zip Z Term +type TermZipper = (Term, Z, D) +move :: TermZipper -> TermZipper move (App l r, c, Down) = (l, L c r, Down) move (Lambda x t, c, Down) = (t, ZL x c, Down) move (Var x, c, Down) = (Var x, c, Up) @@ -177,18 +172,17 @@ move (t, R l c, Up) = (App l t, c, Up) move (t, ZL x c, Up) = (Lambda x t, c, Up) move (t, E, Up) = (t, E, Up) +unmove :: TermZipper -> TermZipper unmove (t, L c r, Down) = (App t r, c, Down) unmove x = x -getF (t, _, _) = t - travPost :: (Monad m) => (Term -> m Term) -> Term -> m Term travPost fnc term = tr fnc (term, E, Down) where tr f (t@(RedEx _ _ _), c, Up) = do nt <- f t tr f $ (nt, c, Down) - tr f (t, E, Up) = return t + tr _ (t, E, Up) = return t tr f (t, c, Up) = tr f $ move (t, c, Up) tr f (t, c, Down) = tr f $ move (t, c, Down) @@ -198,7 +192,7 @@ travPre fnc term = tr fnc (term, E, Down) tr f (t@(RedEx _ _ _), c, Down) = do nt <- f t tr f $ unmove (nt, c, Down) - tr f (t, E, Up) = return t + tr _ (t, E, Up) = return t tr f (t, c, Up) = tr f $ move (t, c, Up) tr f (t, c, Down) = tr f $ move (t, c, Down) @@ -215,10 +209,10 @@ printT t = do -- >>> toNormalForm Eager 100 $ App cI cI -- Just (λx.x) -- --- >>> toNormalForm Eager 1000 $ (App (App cK cI) cY) +-- >>> toNormalForm Eager 100 $ (App (App cK cI) cY) -- Nothing -- --- >>> toNormalForm Lazy 1000 $ (App (App cK cI) cY) +-- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY) -- Just (λx.x) -- -- prop> (\ t u -> t == u || t == Nothing || u == Nothing) (toNormalForm Lazy 1000 x) (toNormalForm Eager 1000 x) @@ -235,8 +229,8 @@ cnt t@(RedEx _ _ _) = do cnt t = return t short :: Int -> Term -> StateT Int Maybe Term -short max t = do +short maxN t = do n <- get - if n > max + if n > maxN then lift Nothing else return t