From 2d2af9eded0d0e4968cf21746f3772f61caecd73 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Tom=C3=A1=C5=A1=20Musil?= Date: Wed, 24 Dec 2014 20:11:42 +0100 Subject: [PATCH 1/1] reenable tests --- fp.cabal | 7 ++++++- src/Lambda.hs | 37 ++++++++----------------------------- src/Lambda/Parser/Fancy.hs | 4 ++++ tests/Test/Term.hs | 41 +++++++++++++++++++++++++++++++++++++++++ tests/doctest.hs | 2 +- 5 files changed, 60 insertions(+), 31 deletions(-) create mode 100644 tests/Test/Term.hs diff --git a/fp.cabal b/fp.cabal index e1636b0..4c137d1 100644 --- a/fp.cabal +++ b/fp.cabal @@ -41,9 +41,14 @@ executable fp-interpret test-suite doctests type: exitcode-stdio-1.0 hs-source-dirs: tests - ghc-options: -threaded main-is: doctest.hs + ghc-options: -threaded build-depends: base + , text >=1.2 && <1.3 + , attoparsec >=0.12 && <0.13 + , containers + , mtl + , fp , doctest >= 0.8 , QuickCheck >= 2.7 default-language: Haskell2010 diff --git a/src/Lambda.hs b/src/Lambda.hs index 5c3ecda..b3a25ce 100644 --- a/src/Lambda.hs +++ b/src/Lambda.hs @@ -20,36 +20,22 @@ module Lambda , toNormalForm , Strategy(..) ) where - import Control.Monad.State import Lambda.Term -- $setup --- >>> import Test.QuickCheck -- >>> import Control.Applicative -- >>> import Lambda.Parser.Fancy --- >>> import Lambda.Term --- >>> let cP = tRead "(λa d c.(λa.e) b (λc.d)) ((λa.(λd.a) (λd c.b ((λa.a) a)) (a ((λa.(λd.e) ((λe.(λd b.a) (λa c.(λa a d.(λd.b (λa d.c) e) (λb b.c a (a d (λb d d e a.d (λb b.d))))) ((λb.a) c)) (d ((λc.(λd.a (λe.e)) (c d)) ((λe.b) a))) c (λa.d (e (λe.(λd c.b) a))) (c (b a)) a (λe.(λa b e b a.d) b)) ((λe.b) (λa.b)) ((λe d.b) b) e) b) ((λc c.a e) (λb.(λb.e) a)))) (λe.e) b (λd c e e c a.c)) a)" --- >>> cY = tRead "λf.(λx.f (x x)) (λx.f (x x))" --- >>> cI = tRead "λx.x" --- >>> cK = tRead "λx y.x" --- >>> cS = tRead "λx y z.x z (y z)" --- >>> let aVarName = oneof . map (pure . (:[])) $ ['a'..'e'] --- >>> let aVar = liftA Var aVarName --- >>> let aComb = oneof . map pure $ [cS, cK, cI, cY] --- >>> let aTerm 0 = aVar --- >>> let aTerm n = oneof [aVar, aComb, liftA2 Lambda aVarName $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))] --- >>> instance Arbitrary Term where arbitrary = sized aTerm --- --- TODO: shrink Terms +-- >>> import Test.Term +-- >>> import Test.QuickCheck varnames :: [VarName] varnames = map (:[]) ['a'..'z'] ++ [c : s | s <- varnames, c <- ['a'..'z']] alphaNorm :: Term -> Term -alphaNorm t = alpha varnames t +alphaNorm = alpha varnames where alpha (v:vs) (Lambda x r) = Lambda v . alpha vs $ substitute x (Var v) r alpha vs (App u v) = App (alpha vs u) (alpha vs v) @@ -91,7 +77,7 @@ data Strategy = Eager | Lazy reduceStep :: (Monad m) => Term -> m Term reduceStep (RedEx x s t) = return $ substitute x t s -reduceStep t = return $ t +reduceStep t = return t data Z = R Term Z | L Z Term | ZL VarName Z | E data D = Up | Down @@ -113,9 +99,9 @@ unmove x = x 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 + tr f (t@RedEx{}, c, Up) = do nt <- f t - tr f $ (nt, c, Down) + tr f (nt, c, Down) 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) @@ -123,20 +109,13 @@ travPost fnc term = tr fnc (term, E, Down) travPre :: (Monad m) => (Term -> m Term) -> Term -> m Term travPre fnc term = tr fnc (term, E, Down) where - tr f (t@(RedEx _ _ _), c, Down) = do + tr f (t@RedEx{}, c, Down) = do nt <- f t tr f $ unmove (nt, c, Down) 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) -{- -printT :: Term -> IO Term -printT t = do - print t - return t --} - -- | -- -- >>> toNormalForm Eager 100 cI @@ -159,7 +138,7 @@ toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> reduceS toNormalForm Lazy n = flip evalStateT 0 . travPre (cnt >=> short n >=> reduceStep) cnt :: (Monad m) => Term -> StateT Int m Term -cnt t@(RedEx _ _ _) = do +cnt t@RedEx{} = do modify (+ 1) return t cnt t = return t diff --git a/src/Lambda/Parser/Fancy.hs b/src/Lambda/Parser/Fancy.hs index 6e87da1..48593dd 100644 --- a/src/Lambda/Parser/Fancy.hs +++ b/src/Lambda/Parser/Fancy.hs @@ -24,6 +24,10 @@ import Control.Applicative import Lambda.Term +-- $setup +-- >>> import Test.QuickCheck +-- >>> import Test.Term + -- | -- >>> print $ Lambda "x" (Var "x") -- (λx.x) diff --git a/tests/Test/Term.hs b/tests/Test/Term.hs new file mode 100644 index 0000000..befeb6a --- /dev/null +++ b/tests/Test/Term.hs @@ -0,0 +1,41 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Test.Term where + +import Test.QuickCheck +import Control.Applicative +import Lambda.Parser.Fancy +import Lambda.Term + +cP :: Term +cP = tRead "(λa d c.(λa.e) b (λc.d)) ((λa.(λd.a) (λd c.b ((λa.a) a)) (a ((λa.(λd.e) ((λe.(λd b.a) (λa c.(λa a d.(λd.b (λa d.c) e) (λb b.c a (a d (λb d d e a.d (λb b.d))))) ((λb.a) c)) (d ((λc.(λd.a (λe.e)) (c d)) ((λe.b) a))) c (λa.d (e (λe.(λd c.b) a))) (c (b a)) a (λe.(λa b e b a.d) b)) ((λe.b) (λa.b)) ((λe d.b) b) e) b) ((λc c.a e) (λb.(λb.e) a)))) (λe.e) b (λd c e e c a.c)) a)" + +cY :: Term +cY = tRead "λf.(λx.f (x x)) (λx.f (x x))" +cI :: Term +cI = tRead "λx.x" +cK :: Term +cK = tRead "λx y.x" +cS :: Term +cS = tRead "λx y z.x z (y z)" + +instance Arbitrary Term + where arbitrary = sized aTerm + +aVarName :: Gen String +aVarName = oneof . map (pure . (:[])) $ ['a'..'e'] + +aComb :: Gen Term +aComb = oneof . map pure $ [cS, cK, cI, cY] + +aVar :: Gen Term +aVar = liftA Var aVarName + +aTerm :: Int -> Gen Term +aTerm 0 = aVar +aTerm n = oneof [aVar, aComb, liftA2 Lambda aVarName $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))] +-- +-- TODO: shrink Terms +-- TODO: timed tests + + diff --git a/tests/doctest.hs b/tests/doctest.hs index 793c0ab..258b4dd 100644 --- a/tests/doctest.hs +++ b/tests/doctest.hs @@ -1,4 +1,4 @@ import Test.DocTest main :: IO () -main = doctest ["-isrc", "src/Main.hs"] +main = doctest ["-isrc", "src/Main.hs", "tests/Test/Term.hs"] -- 2.4.2