library
exposed-modules: Lambda
- other-modules: Lambda.Term
Lambda.Parser.Fancy
+ other-modules: Lambda.Term
build-depends: base >=4.7 && <4.8
, text >=1.2 && <1.3
, attoparsec >=0.12 && <0.13
( -- * Types
VarName
, Term(..)
+ , pattern RedEx
-- * Reduction
, alphaNorm
, reduce
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 :: Term -> Term
+reduceStep (RedEx x s t) = substitute x t s
+reduceStep t = t
data Z = R Term Z | L Z Term | ZL VarName Z | E
data D = Up | Down
unmove (t, L c r, Down) = (App t r, c, Down)
unmove x = x
+-- getTerm :: TermZipper -> Term
+
travPost :: (Monad m) => (Term -> m Term) -> Term -> m Term
travPost fnc term = tr fnc (term, E, Down)
where
-- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
-- Just (λx.x)
--
--- prop> (\ 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 1000 x) (alphaNorm <$> toNormalForm Eager 1000 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))"
toNormalForm :: Strategy -> Int -> Term -> Maybe Term
-toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> reduceStep)
-toNormalForm Lazy n = flip evalStateT 0 . travPre (cnt >=> short n >=> reduceStep)
+toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep)
+toNormalForm Lazy n = flip evalStateT 0 . travPre (cnt >=> short n >=> return . reduceStep)
cnt :: (Monad m) => Term -> StateT Int m Term
cnt t@RedEx{} = do
-- TODO: proper documentation
-module Lambda.Parser.Fancy where
+module Lambda.Parser.Fancy
+ ( tRead
+ , parseTerm
+ ) where
import Data.Text as T hiding (map)
import Data.Attoparsec.Text
-- Data types for λ terms.
-module Lambda.Term where
+module Lambda.Term
+ ( -- * Types
+ VarName
+ , Term(..)
+ -- * Pattern synonyms
+ , pattern RedEx
+ , pattern AppApp
+ , pattern EmLambda
+ ) where
type VarName = String
pattern RedEx x t s = App (Lambda x t) s
pattern AppApp a b c = App a (App b c)
pattern EmLambda x y t = Lambda x (Lambda y t)
-
-