X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/801f0c270025ca872a488690aca42b59eeee89aa..d276bbe5bee77bc96200366978c283993b8154c8:/src/Lambda.hs diff --git a/src/Lambda.hs b/src/Lambda.hs index f54a100..c570199 100644 --- a/src/Lambda.hs +++ b/src/Lambda.hs @@ -1,19 +1,32 @@ {-# OPTIONS_GHC -fno-warn-unused-do-bind #-} {-# LANGUAGE PatternSynonyms #-} -module Lambda where +-- | +-- Module : Lambda +-- Copyright : Tomáš Musil 2014 +-- License : BSD-3 +-- +-- Maintainer : tomik.musil@gmail.com +-- Stability : experimental +-- +-- This is a toy λ-calculus implementation. + +module Lambda + ( -- * Types + VarName + , Term(..) + -- * Parsing terms + , parseTerm + , tRead + -- * Reduction + , reduce + ) where + import Data.Text as T import Data.Attoparsec.Text import Control.Applicative -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) - -- $setup -- >>> import Test.QuickCheck -- >>> import Control.Applicative @@ -21,12 +34,18 @@ pattern EmLambda x y t = Lambda x (Lambda y t) -- >>> let aTerm n = oneof [pure (Var "x"), liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))] -- >>> instance Arbitrary Term where arbitrary = sized aTerm --- | Read and show λ-terms --- --- >>> print $ Lambda "x" (Var "x") --- (λx.x) --- --- prop> t == tRead (show (t :: Term)) +type VarName = String + +-- | +-- >>> print $ Lambda "x" (Var "x") +-- (λx.x) + +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) + instance Show Term where show (Var x) = x @@ -38,7 +57,9 @@ instance Show Term where braced :: Term -> String braced t = "(" ++ show t ++ ")" ---instance Read Term where +-- | +-- prop> t == tRead (show (t :: Term)) + tRead :: String -> Term tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of (Right t) -> t