-{-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
{-# LANGUAGE PatternSynonyms #-}
-- |
( -- * Types
VarName
, Term(..)
- -- * Parsing terms
- , parseTerm
- , tRead
-- * Reduction
+ , alphaNorm
, reduce
, toNormalForm
, Strategy(..)
) where
-import Data.Text as T hiding (map)
-import Data.Attoparsec.Text
-import Control.Applicative
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]
--
-- TODO: shrink Terms
-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)"
-
-type VarName = String
-
--- |
--- >>> print $ Lambda "x" (Var "x")
--- (λx.x)
-
-data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
-
varnames :: [VarName]
varnames = map (:[]) ['a'..'z'] ++ [c : s | s <- varnames, c <- ['a'..'z']]
alphaNorm :: Term -> Term
alphaNorm t = alpha varnames t
where
- alpha (v:vs) (Lambda x t) = Lambda v . alpha vs $ substitute x (Var v) t
+ 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)
- alpha vs (Var x) = Var x
-
-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)
-
-
-instance Show Term where
- show (Var x) = x
- show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
- show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
- show (AppApp a b c) = show a ++ " " ++ braced (App b c)
- show (App t r) = show t ++ " " ++ show r
-
-braced :: Term -> String
-braced t = "(" ++ show t ++ ")"
-
--- |
--- prop> t == tRead (show (t :: Term))
-
-tRead :: String -> Term
-tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
- (Right t) -> t
- (Left e) -> error e
-
-parseVar :: Parser Term
-parseVar = do
- x <- many1 (letter <|> digit)
- return $! Var x
-
-parseLambda :: Parser Term
-parseLambda = do
- char '\\' <|> char 'λ'
- vars <- sepBy1 parseVar (char ' ')
- char '.'
- t <- parseTerm
- return $! createLambda vars t
-
-createLambda :: [Term] -> Term -> Term
-createLambda (Var x : vs) t = Lambda x $ createLambda vs t
-createLambda [] t = t
-createLambda _ _ = error "createLambda failed"
-
-parseApp :: Parser Term
-parseApp = do
- aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
- return $! createApp aps
-
-createApp :: [Term] -> Term
-createApp [t] = t
-createApp (t:ts:tss) = createApp (App t ts : tss)
-createApp [] = error "empty createApp"
-
-parseBraces :: Parser Term
-parseBraces = do
- char '('
- t <- parseTerm
- char ')'
- return t
-
-parseTerm :: Parser Term
-parseTerm = parseApp <|>
- parseBraces <|>
- parseLambda <|>
- parseVar
-
--------------------------------------------------
+ alpha _ (Var x) = Var x
+ alpha [] _ = undefined
isFreeIn :: VarName -> Term -> Bool
isFreeIn x (Var v) = x == v
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
+-}
-- |
--
--- /dev/null
+{-# OPTIONS_GHC
+ -fno-warn-unused-do-bind
+ -fno-warn-orphans
+#-}
+{-# LANGUAGE PatternSynonyms #-}
+
+-- |
+-- Module : Lambda.Parser.Fancy
+-- Copyright : Tomáš Musil 2014
+-- License : BSD-3
+--
+-- Maintainer : tomik.musil@gmail.com
+-- Stability : experimental
+--
+-- Parser for λ-terms. '.' in λ implies brackets to the end of the context.
+
+-- TODO: proper documentation
+
+module Lambda.Parser.Fancy where
+
+import Data.Text as T hiding (map)
+import Data.Attoparsec.Text
+import Control.Applicative
+
+import Lambda.Term
+
+-- |
+-- >>> print $ Lambda "x" (Var "x")
+-- (λx.x)
+
+instance Show Term where
+ show (Var x) = x
+ show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
+ show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
+ show (AppApp a b c) = show a ++ " " ++ braced (App b c)
+ show (App t r) = show t ++ " " ++ show r
+
+braced :: Term -> String
+braced t = "(" ++ show t ++ ")"
+
+-- |
+-- prop> t == tRead (show (t :: Term))
+
+tRead :: String -> Term
+tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
+ (Right t) -> t
+ (Left e) -> error e
+
+parseVar :: Parser Term
+parseVar = do
+ x <- many1 (letter <|> digit)
+ return $! Var x
+
+parseLambda :: Parser Term
+parseLambda = do
+ char '\\' <|> char 'λ'
+ vars <- sepBy1 parseVar (char ' ')
+ char '.'
+ t <- parseTerm
+ return $! createLambda vars t
+
+parseApp :: Parser Term
+parseApp = do
+ aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
+ return $! createApp aps
+
+parseBraces :: Parser Term
+parseBraces = do
+ char '('
+ t <- parseTerm
+ char ')'
+ return t
+
+parseTerm :: Parser Term
+parseTerm = parseApp <|>
+ parseBraces <|>
+ parseLambda <|>
+ parseVar
+
+createLambda :: [Term] -> Term -> Term
+createLambda (Var x : vs) t = Lambda x $ createLambda vs t
+createLambda [] t = t
+createLambda _ _ = error "createLambda failed"
+
+createApp :: [Term] -> Term
+createApp [t] = t
+createApp (t:ts:tss) = createApp (App t ts : tss)
+createApp [] = error "empty createApp"
+
projekty / fp.git / commitdiff