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