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   (Var x) <- parseVar
  32   char '.'
  33   t <- parseTerm
  34   return $! Lambda x t
  35
  36 parseApp :: Parser Term
  37 parseApp = do
  38   char '('
  39   t <- parseTerm
  40   char ' '
  41   r <- parseTerm
  42   char ')'
  43   return $! App t r
  44
  45 parseTerm :: Parser Term
  46 parseTerm = parseVar <|> parseLambda <|> parseApp
  47
  48 -------------------------------------------------
  49
  50 isFreeIn :: VarName -> Term -> Bool
  51 isFreeIn x (Var v) = x == v
  52 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  53 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  54
  55 rename :: Term -> Term
  56 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  57   where n = rnm x
  58         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  59 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
  60
  61 substitute :: VarName -> Term -> Term -> Term
  62 substitute a b (Var x) = if x == a then b else Var x
  63 substitute a b (Lambda x t)
  64   | x == a = Lambda x t
  65   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
  66   | otherwise = Lambda x (substitute a b t)
  67 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  68
  69 reduce :: Term -> Term
  70 reduce (Var x) = Var x
  71 reduce (Lambda x t) = Lambda x (reduce t)
  72 reduce (App t u) = app (reduce t) u
  73   where app (Lambda x v) w = reduce $ substitute x w v
  74         app a b = App a (reduce b)