Prolog interpreter

database.pl

likes(bob, apple).
likes(bob, grape).
likes(ronald, X) :- yellow(X), likes(alice, x).

yellow(banana).

append(nil, M, M).
append([H | T], X, [H | R]) :- append(T, X, R).

prolog.hs

module Main where
import Control.Applicative (liftA2)
import Control.Monad
import System.IO
import System.Environment
import Data.Maybe
import Data.List
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Char

main :: IO ()
main = do
  args <- getArgs
  case args of
    []     -> putStrLn "Please specify a file to run."
    [file] -> run file
    _      -> putStrLn "Please only specify one file!"

comment :: Parser ()
comment = () <$ (char '%' *> many (noneOf "\n") *> char '\n') <?> "comment"

whitespace :: Parser ()
whitespace = skipMany (void space <|> comment) <?> "whitespace"

idChar :: Parser Char
idChar = letter <|> digit <|> char '_'

name :: Parser String
name = liftA2 (:) lower (many idChar) <* whitespace

atom :: Parser Term
atom = Atom <$> (name <|> many1 digit) <?> "atom"

variable :: Parser Term
variable = Var . Name 0 <$> liftA2 (:) upper (many idChar) <* whitespace <?> "variable"

args :: Parser [Term]
args = char '(' *> term `sepBy` (char ',' <* whitespace) <* char ')' <* whitespace

predicate :: Parser Predicate
predicate = normal
  where normal  =  try list <|> Predicate <$> name <*> args <?> "predicate"
        list = do char '[' *> whitespace
                  cars <- term `sepBy1` (char ',' *> whitespace)
                  cdr <- rest <* whitespace
                  let end = Predicate "cons" [last cars, cdr]
                  return . foldr cons end $ init cars
        rest =  whitespace *> char '|' *> whitespace *> term <* char ']'
            <|> Atom "nil" <$ char ']'
        cons term rest = Predicate "cons" [term, Pred rest]

term :: Parser Term
term = try (Pred <$> predicate) <|> atom <|> variable <?> "term"

rule ::  Parser [Rule]
rule = do hd     <- predicate
          bodies <- end <|> string ":-" *> whitespace *> (body `sepBy` (char ';' *> whitespace)) <* end
          return $ Rule hd <$> bodies
  where end  = [[]] <$ char '.' <* whitespace
        body = predicate `sepBy` (char ',' <* whitespace)

rules :: Parser [Rule]
rules = whitespace *> (concat <$> many1 rule)

run :: FilePath -> IO ()
run file = do
  source <- readFile file
  case parse rules file source of
    Right database -> repl database
    Left error -> print error

repl :: [Rule] -> IO ()
repl rules = do
  print rules
  putStr "?- "
  hFlush stdout
  line <- getLine
  case parse predicate "<stdin>" line of
    Right pred -> do
      let res = resolve pred rules
      showEachLine $ showResult pred res
    _ -> do
      putStrLn "Invalid predicate!"
  repl rules

showEachLine [] = do
  return ()
showEachLine (x:xs) = do
  putStrLn $ "  " ++ x
  showEachLine xs

data Term = Atom String
          | Var Name
          | Pred Predicate deriving Show

data Name = Name Int String deriving (Show, Eq)

data Rule = Rule Predicate [Predicate] deriving Show

data Predicate = Predicate String [Term] deriving Show

type MGU = [(Name, Term)]

showResult :: Predicate -> [MGU] -> [String]
showResult _ []  = ["No"]
showResult q res = showMgu . filter (contains (Pred q) . Var . fst) . reverse <$> res
  where showMgu []  = "Yes"
        showMgu mgu = intercalate " " $ map showBinding (reverse mgu)
        showBinding (n,v) = showName n ++ " = " ++ showVal v
        showName (Name 0 n) = n
        showName (Name i n) = n ++ "_" ++ show i
        showVal (Atom atom) = atom
        showVal (Var n)     = showName n
        showVal (Pred p)    = showPred p
        showPred list@(Predicate "cons" _) = "[" ++ showList list ++ "]"
        showPred (Predicate n b) = n ++ "(" ++ intercalate ", " (showVal <$> b) ++ ")"
        showList (Predicate _ [a, b]) = showVal a ++ rest b
          where rest (Pred pr@(Predicate "cons" _)) = ", " ++ showList pr
                rest (Atom "nil")                     = ""
                rest term                             = "|" ++ showVal term

merge :: MGU -> MGU -> MGU
merge t1 ((name, term):xs) =
  (name, substTerm t1 term) : merge t1 xs
merge t1 [] =
  t1

freshen :: Rule -> Rule
freshen (Rule hd body) = Rule (freshenPred hd) $ freshenPred <$> body
  where freshenPred (Predicate n args) = Predicate n $ freshenTerm <$> args
        freshenTerm (Var (Name i n)) = Var $ Name (i + 1) n
        freshenTerm (Pred p)         = Pred $ freshenPred p
        freshenTerm term             = term

substPred :: MGU -> Predicate -> Predicate
substPred mgu (Predicate n b) = Predicate n $ substTerm mgu <$> b

substTerm :: MGU -> Term -> Term
substTerm mgu var@(Var name) = fromMaybe var $ lookup name mgu
substTerm mgu (Pred p)       = Pred $ substPred mgu p
substTerm _ atom             = atom

substList :: MGU -> [Term] -> [Term]
substList = fmap . substTerm

unifyPredicate :: Predicate -> Predicate -> Maybe MGU
unifyPredicate (Predicate name1 body1) (Predicate name2 body2) =
  if name1 == name2 then
    unifyBody body1 body2
  else
    Nothing

unifyBody :: [Term] -> [Term] -> Maybe MGU
unifyBody [] [] =
  Just []
unifyBody (x:xs) (y:ys) = do
  t1 <- unifyTerm x y
  t2 <- unifyBody (substList t1 xs) (substList t1 ys)
  return $ merge t2 t1
unifyBody a b = do
  Nothing

unifyTerm :: Term -> Term -> Maybe MGU
unifyTerm (Var x) y =
  if contains y (Var x) then
    Nothing
  else
    Just [(x, y)]
unifyTerm x (Var y) =
  if contains x (Var y) then
    Nothing
  else
    Just [(y, x)]
unifyTerm (Atom x) (Atom y) =
  if x == y then
    Just []
  else
    Nothing
unifyTerm (Pred x) (Pred y) =
  unifyPredicate x y
unifyTerm _ _ =
  Nothing

contains :: Term -> Term -> Bool
contains (Var v1) (Var v2) = v1 == v2
contains (Pred (Predicate _ p)) n = or $ (`contains` n) <$> p
contains _ _                        = False

resolve :: Predicate -> [Rule] -> [MGU]
resolve goal rules = do
  Rule head body <- fmap freshen rules
  case unifyPredicate goal head of
    Just mgu ->
      resolveBody rules mgu body
    Nothing ->
      []

resolveBody :: [Rule] -> MGU -> [Predicate] -> [MGU]
resolveBody rules t1 [] =
  return t1
resolveBody rules t1 (p:ps) = do
  t2 <- resolve (substPred t1 p) (fmap freshen rules)
  resolveBody rules (merge t2 t1) ps