From: Tomas Musil Date: Tue, 16 Dec 2014 17:55:47 +0000 (+0100) Subject: separate the parser X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/e26e565842cd4c347f93b3bbf1a4363f05d1cc2f separate the parser --- diff --git a/fp.cabal b/fp.cabal index 8be11df..e1636b0 100644 --- a/fp.cabal +++ b/fp.cabal @@ -17,6 +17,8 @@ cabal-version: >=1.10 library exposed-modules: Lambda + other-modules: Lambda.Term + Lambda.Parser.Fancy build-depends: base >=4.7 && <4.8 , text >=1.2 && <1.3 , attoparsec >=0.12 && <0.13 @@ -25,15 +27,14 @@ library hs-source-dirs: src default-language: Haskell2010 -executable fp +executable fp-interpret main-is: Main.hs - other-modules: Lambda - -- other-extensions: build-depends: base >=4.7 && <4.8 , text >=1.2 && <1.3 , attoparsec >=0.12 && <0.13 , containers , mtl + , fp hs-source-dirs: src default-language: Haskell2010 @@ -45,7 +46,4 @@ test-suite doctests build-depends: base , doctest >= 0.8 , QuickCheck >= 2.7 - , text >=1.2 && <1.3 - , attoparsec >=0.12 && <0.13 - , containers default-language: Haskell2010 diff --git a/src/Lambda.hs b/src/Lambda.hs index 07d1f4b..5c3ecda 100644 --- a/src/Lambda.hs +++ b/src/Lambda.hs @@ -1,4 +1,3 @@ -{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} {-# LANGUAGE PatternSynonyms #-} -- | @@ -15,24 +14,28 @@ module Lambda ( -- * 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] @@ -42,104 +45,16 @@ import Control.Monad.State -- -- 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 @@ -215,10 +130,12 @@ travPre fnc term = tr fnc (term, E, Down) 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 +-} -- | -- diff --git a/src/Lambda/Parser/Fancy.hs b/src/Lambda/Parser/Fancy.hs new file mode 100644 index 0000000..6e87da1 --- /dev/null +++ b/src/Lambda/Parser/Fancy.hs @@ -0,0 +1,89 @@ +{-# 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" + diff --git a/src/Lambda/Term.hs b/src/Lambda/Term.hs new file mode 100644 index 0000000..e3682c1 --- /dev/null +++ b/src/Lambda/Term.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | +-- Module : Lambda.Term +-- Copyright : Tomáš Musil 2014 +-- License : BSD-3 +-- +-- Maintainer : tomik.musil@gmail.com +-- Stability : experimental +-- +-- Data types for λ terms. + + +module Lambda.Term where + +type VarName = String + +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) +pattern EmLambda x y t = Lambda x (Lambda y t) + + diff --git a/src/Main.hs b/src/Main.hs index 1405086..4ddfe2d 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -11,6 +11,7 @@ import Control.Monad import System.Environment import Lambda +import Lambda.Parser.Fancy data Definition = Definition String Term