src/Lambda.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3
   4 module Lambda where
   5
   6 import Data.Text as T
   7 import Data.Attoparsec.Text
   8 import Control.Applicative
   9
  10 type VarName = String
  11 data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
  12
  13 pattern RedEx x t s = App (Lambda x t) s
  14 pattern AppApp a b c = App a (App b c)
  15 pattern EmLambda x y t = Lambda x (Lambda y t)
  16
  17 -- $setup
  18 -- >>> import Test.QuickCheck
  19 -- >>> import Control.Applicative
  20 -- >>> let aTerm 0 = pure $ Var "x"
  21 -- >>> let aTerm n = oneof [pure (Var "x"), liftA (Lambda "x") $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))]
  22 -- >>> instance Arbitrary Term where arbitrary = sized aTerm
  23
  24 -- | Read and show λ-terms
  25 --
  26 --   >>> print $ Lambda "x" (Var "x")
  27 --   (λx.x)
  28 --
  29 --   prop> t == tRead (show (t :: Term))
  30
  31 instance Show Term where
  32   show (Var x) = x
  33   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  34   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  35   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  36   show (App t r) = show t ++ " " ++ show r
  37
  38 braced :: Term -> String
  39 braced t = "(" ++ show t ++ ")"
  40
  41 --instance Read Term where
  42 tRead :: String -> Term
  43 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  44     (Right t) -> t
  45     (Left e) -> error e
  46
  47 parseVar :: Parser Term
  48 parseVar = do
  49   x <- many1 letter
  50   return $! Var x
  51
  52 parseLambda :: Parser Term
  53 parseLambda = do
  54   char '\\' <|> char 'λ'
  55   vars <- sepBy1 parseVar (char ' ')
  56   char '.'
  57   t <- parseTerm
  58   return $! createLambda vars t
  59
  60 createLambda :: [Term] -> Term -> Term
  61 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  62 createLambda [] t = t
  63 createLambda _ _ = error "createLambda failed"
  64
  65 parseApp :: Parser Term
  66 parseApp = do
  67   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  68   return $! createApp aps
  69
  70 createApp :: [Term] -> Term
  71 createApp [t] = t
  72 createApp (t:ts:tss) = createApp (App t ts : tss)
  73 createApp [] = error "empty createApp"
  74
  75 parseBraces :: Parser Term
  76 parseBraces = do
  77   char '('
  78   t <- parseTerm
  79   char ')'
  80   return t
  81
  82 parseTerm :: Parser Term
  83 parseTerm = parseApp <|>
  84             parseBraces <|>
  85             parseLambda <|>
  86             parseVar
  87
  88 -------------------------------------------------
  89
  90 isFreeIn :: VarName -> Term -> Bool
  91 isFreeIn x (Var v) = x == v
  92 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  93 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  94
  95 rename :: Term -> Term
  96 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  97   where n = rnm x
  98         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  99 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
 100
 101 substitute :: VarName -> Term -> Term -> Term
 102 substitute a b (Var x) = if x == a then b else Var x
 103 substitute a b (Lambda x t)
 104   | x == a = Lambda x t
 105   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
 106   | otherwise = Lambda x (substitute a b t)
 107 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
 108
 109 reduce :: Term -> Term
 110 reduce (Var x) = Var x
 111 reduce (Lambda x t) = Lambda x (reduce t)
 112 reduce (App t u) = app (reduce t) u
 113   where app (Lambda x v) w = reduce $ substitute x w v
 114         app a b = App a (reduce b)