src/Lambda.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
   2
   3 module Lambda where
   4
   5 import Data.Text as T
   6 import Data.Attoparsec.Text
   7 import Control.Applicative
   8
   9 type VarName = String
  10 data Term = Var VarName | Lambda VarName Term | App Term Term
  11
  12 instance Show Term where
  13   show (Var x) = x
  14   show (Lambda x t) = "\\" ++ x ++ "." ++ show t
  15   show (App t r) = "(" ++ show t ++ " " ++ show r ++ ")"
  16
  17 --instance Read Term where
  18 tRead :: String -> Term
  19 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  20     (Right t) -> t
  21     (Left e) -> error e
  22
  23 parseVar :: Parser Term
  24 parseVar = do
  25   x <- many1 letter
  26   return $! Var x
  27
  28 parseLambda :: Parser Term
  29 parseLambda = do
  30   char '\\'
  31   vars <- sepBy1 parseVar (char ' ')
  32   char '.'
  33   t <- parseTerm
  34   return $! createLambda vars t
  35
  36 createLambda :: [Term] -> Term -> Term
  37 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
  38 createLambda [] t = t
  39 createLambda _ _ = error "createLambda failed"
  40
  41 parseApp :: Parser Term
  42 parseApp = do
  43   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
  44   return $! createApp aps
  45
  46 createApp :: [Term] -> Term
  47 createApp [t] = t
  48 createApp (t:ts:tss) = createApp (App t ts : tss)
  49 createApp [] = error "empty createApp"
  50
  51 parseBraces :: Parser Term
  52 parseBraces = do
  53   char '('
  54   t <- parseTerm
  55   char ')'
  56   return t
  57
  58 parseTerm :: Parser Term
  59 parseTerm = parseApp <|>
  60             parseBraces <|>
  61             parseLambda <|>
  62             parseVar
  63
  64 -------------------------------------------------
  65
  66 isFreeIn :: VarName -> Term -> Bool
  67 isFreeIn x (Var v) = x == v
  68 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  69 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  70
  71 rename :: Term -> Term
  72 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  73   where n = rnm x
  74         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  75 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
  76
  77 substitute :: VarName -> Term -> Term -> Term
  78 substitute a b (Var x) = if x == a then b else Var x
  79 substitute a b (Lambda x t)
  80   | x == a = Lambda x t
  81   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
  82   | otherwise = Lambda x (substitute a b t)
  83 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  84
  85 reduce :: Term -> Term
  86 reduce (Var x) = Var x
  87 reduce (Lambda x t) = Lambda x (reduce t)
  88 reduce (App t u) = app (reduce t) u
  89   where app (Lambda x v) w = reduce $ substitute x w v
  90         app a b = App a (reduce b)