, 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
-- $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
-- >>> 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)
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)
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)
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)
-- >>> 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)
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