diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/prolog.cabal b/prolog.cabal new file mode 100644 --- /dev/null +++ b/prolog.cabal @@ -0,0 +1,40 @@ +Name: prolog +Version: 0.1 +Synopsis: A Prolog interpreter written in Haskell. +Description: A Prolog interpreter written in Haskell. +License: PublicDomain +Author: Matthias Bartsch +Maintainer: bartsch@cs.uni-bonn.de +Homepage: https://github.com/Erdwolf/prolog +Category: Language +Build-type: Simple +Cabal-version: >=1.6 + +Source-repository head + type: git + location: git://github.com/Erdwolf/prolog.git + +Library + Exposed-modules: Language.Prolog + Language.Prolog.IsString + Language.Prolog.Quote + Other-modules: Prolog + Interpreter + Database + Unifier + Parser + Syntax + IsString + Quote + Hs-Source-Dirs: src + + Build-depends: + base >=4 && <5, + parsec >= 3.1.1, + syb >= 0.3, + mtl >= 2.0.1.0, + containers >=0.4 && <0.5, + + template-haskell, + th-lift >=0.5.3, + transformers >=0.2.2.0 diff --git a/src/Database.hs b/src/Database.hs new file mode 100644 --- /dev/null +++ b/src/Database.hs @@ -0,0 +1,43 @@ +module Database + ( createDB + , hasPredicate + , getClauses + , asserta + , assertz + , abolish + , Signature(), signature + ) +where + +import Data.Map (Map) +import qualified Data.Map as Map + +import Syntax + + +data Signature = Signature Atom Int deriving (Ord, Eq) +instance Show Signature where + show (Signature name arity) = name ++ "/" ++ show arity + +signature :: Term -> Signature +signature (Struct name ts) = Signature name (length ts) + + +newtype Database = DB (Map Signature [Clause]) + +hasPredicate sig (DB index) = Map.member sig index + +createDB clauses emptyPredicates = DB $ + foldr (\clause -> Map.insertWith' (++) (signature (lhs clause)) [clause]) + (Map.fromList [ (signature (Struct name []), []) | name <- emptyPredicates ]) + clauses + +getClauses term (DB index) = maybe [] id $ Map.lookup (signature term) index + + +asserta fact (DB index) = DB $ Map.insertWith (++) (signature fact) [Clause fact []] index +assertz fact (DB index) = DB $ Map.insertWith (flip (++)) (signature fact) [Clause fact []] index +abolish fact (DB index) = DB $ Map.adjust deleteFact (signature fact) index + where deleteFact (Clause t []:cs) | t == fact = cs + deleteFact (_ :cs) = cs + deleteFact [] = [] diff --git a/src/Interpreter.hs b/src/Interpreter.hs new file mode 100644 --- /dev/null +++ b/src/Interpreter.hs @@ -0,0 +1,254 @@ +{-# LANGUAGE ViewPatterns, GeneralizedNewtypeDeriving, FlexibleInstances, FlexibleContexts, UndecidableInstances, IncoherentInstances #-} +module Interpreter + ( resolve, resolve_ + , MonadTrace(..), withTrace + , MonadGraphGen(..), runNoGraphT + ) +where +import Control.Monad.Reader +import Control.Monad.Writer +import Control.Monad.State +import Control.Monad.Error +import Data.Maybe (isJust) +import Data.Generics (everywhere, mkT) +import Control.Applicative ((<$>),(<*>),(<$),(<*), Applicative(..)) +import Data.List (sort, nub) + +import Syntax +import Unifier +import Database + + +builtins :: [Clause] +builtins = + [ Clause (Struct "=" [var "X", var "X"]) [] + , Clause (Struct "\\=" [var "X", var "X"]) [cut, Struct "false" []] + , Clause (Struct "\\=" [var "X", var "Y"]) [] + , Clause (Struct "not" [var "A"]) [var "A", cut, Struct "false" []] + , Clause (Struct "not" [var "A"]) [] + , Clause (Struct "\\+" [var "A"]) [var "A", cut, Struct "false" []] + , Clause (Struct "\\+" [var "A"]) [] + , Clause (Struct "true" []) [] + , Clause (Struct "," [var "A", var "B"]) [var "A", var "B"] + , Clause (Struct ";" [var "A", Wildcard]) [var "A"] + , Clause (Struct ";" [Wildcard, var "B"]) [var "B"] + , ClauseFn (Struct "is" [var "L", var "R"]) is + , ClauseFn (Struct "<" [var "N", var "M"]) (binaryIntegerPredicate (<)) + , ClauseFn (Struct ">" [var "N", var "M"]) (binaryIntegerPredicate (>)) + , ClauseFn (Struct "=<" [var "N", var "M"]) (binaryIntegerPredicate (<=)) + , ClauseFn (Struct ">=" [var "N", var "M"]) (binaryIntegerPredicate (>=)) + , ClauseFn (Struct "=:=" [var "N", var "M"]) (binaryIntegerPredicate (==)) + , ClauseFn (Struct "@<" [var "T1", var "T2"]) (binaryPredicate (<)) + , ClauseFn (Struct "@>" [var "T1", var "T2"]) (binaryPredicate (>)) + , ClauseFn (Struct "@=<"[var "T1", var "T2"]) (binaryPredicate (<=)) + , ClauseFn (Struct "@>="[var "T1", var "T2"]) (binaryPredicate (>=)) + , ClauseFn (Struct "==" [var "T1", var "T2"]) (binaryPredicate (==)) + , ClauseFn (Struct "sort" [var "Input", var "Output"]) (function sort_pl) + , Clause (Struct "member" [var "X", Struct "." [var "X", Wildcard]]) [] + , Clause (Struct "member" [var "X", Struct "." [Wildcard, var "Xs"]]) + [Struct "member" [var "X", var "Xs"]] + , ClauseFn (Struct "=.." [var "Term", var "List"]) univ + , ClauseFn (Struct "atom" [var "T"]) atom + , ClauseFn (Struct "char_code" [var "Atom", var "Code"]) char_code + , Clause (Struct "phrase" [var "RuleName", var "InputList"]) + [Struct "phrase" [var "RuleName", var "InputList", Struct "[]" []]] + , Clause (Struct "phrase" [var "Rule", var "InputList", var "Rest"]) + [ Struct "=.." [var "Rule", var "L"] + , Struct "append" [var "L", foldr cons nil (arguments [{- already in L -}] (var "InputList") (var "Rest")), var "L1"] -- FIXME This makes assumptions about "arguments" + , Struct "=.." [var "Goal", var "L1"] + , var "Goal" + ] + , Clause (Struct "append" [Struct "[]" [], var "YS", var "YS"]) [] + , Clause (Struct "append" [Struct "." [var "X", var "XS"], var "YS", Struct "." [var "X", var "XSYS"]]) [Struct "append" [var "XS", var "YS", var "XSYS"]] + ] + where + binaryIntegerPredicate :: (Integer -> Integer -> Bool) -> ([Term] -> [Goal]) + binaryIntegerPredicate p [eval->Just n, eval->Just m] | n `p` m = [] + binaryIntegerPredicate p _ = [Struct "false" []] + + binaryPredicate :: (Term -> Term -> Bool) -> ([Term] -> [Goal]) + binaryPredicate p [t1, t2] | t1 `p` t2 = [] + binaryPredicate p _ = [Struct "false" []] + + is [t, eval->Just n] = [Struct "=" [t, Struct (show n) []]] + is _ = [Struct "false" []] + + eval (Struct (reads->[(n,"")]) []) = return n :: Maybe Integer + eval (Struct "+" [t1, t2]) = (+) <$> eval t1 <*> eval t2 + eval (Struct "*" [t1, t2]) = (*) <$> eval t1 <*> eval t2 + eval (Struct "-" [t1, t2]) = (-) <$> eval t1 <*> eval t2 + eval (Struct "mod" [t1, t2]) = mod <$> eval t1 <*> eval t2 + eval (Struct "-" [t]) = negate <$> eval t + eval _ = mzero + + univ [Struct a ts, list] = [Struct "=" [Struct "." [Struct a [], foldr cons nil ts], list]] + univ [term, Struct "." [Struct a [], t]] = [Struct "=" [term, Struct a (foldr_pl (:) [] t)]] + univ _ = [Struct "false" []] + + atom [Struct _ []] = [] + atom _ = [Struct "false" []] + + char_code [Struct [c] [], t] = [Struct "=" [Struct (show (fromEnum c)) [], t]] + char_code [t, Struct (reads->[(n,"")]) []] = [Struct "=" [t, Struct [toEnum n] []]] + char_code _ = [Struct "false" []] + + function :: (Term -> Term) -> ([Term] -> [Goal]) + function f [input, output] = [Struct "=" [output, f input]] + + sort_pl = foldr cons nil . nub . sort . foldr_pl (:) [] + +class Monad m => MonadTrace m where + trace :: String -> m () +instance MonadTrace (Trace IO) where + trace = Trace . putStrLn +instance MonadTrace IO where + trace _ = return () +instance MonadTrace (Either err) where + trace _ = return () +instance (MonadTrace m, MonadTrans t, Monad (t m)) => MonadTrace (t m) where + trace x = lift (trace x) + + +newtype Trace m a = Trace { withTrace :: m a } deriving (Functor, Monad, MonadError e) + +trace_ label x = trace (label++":\t"++show x) + + +class Monad m => MonadGraphGen m where + createConnections :: Unifier -> [Goal] -> [Branch] -> m () + markSolution :: Unifier -> m () + markCutBranches :: Stack -> m () + +instance MonadGraphGen m => MonadGraphGen (ReaderT r m) where + createConnections x y z = lift (createConnections x y z) + markSolution = lift . markSolution + markCutBranches = lift . markCutBranches + + +newtype NoGraphT m a = NoGraphT {runNoGraphT :: m a} deriving (Monad, Functor, MonadFix, MonadPlus, Applicative, MonadError e) +instance MonadTrans NoGraphT where + lift = NoGraphT + +instance Monad m => MonadGraphGen (NoGraphT m) where + createConnections _ _ _ = NoGraphT $ return () + markSolution _ = NoGraphT $ return () + markCutBranches _ = NoGraphT $ return () + + +type Stack = [(Unifier, [Goal], [Branch])] +type Branch = (Unifier, [Goal]) + +resolve :: (Functor m, MonadTrace m, Error e, MonadError e m) => Program -> [Goal] -> m [Unifier] +resolve program goals = runNoGraphT (resolve_ program goals) + +resolve_ :: (Functor m, MonadTrace m, Error e, MonadError e m, MonadGraphGen m) => Program -> [Goal] -> m [Unifier] +-- Yield all unifiers that resolve using the clauses from . +resolve_ program goals = map cleanup <$> runReaderT (resolve' 1 [] goals []) (createDB (builtins ++ program) ["false","fail"]) -- NOTE Is it a good idea to "hardcode" the builtins like this? + where + cleanup = filter ((\(VariableName i _) -> i == 0) . fst) + + whenPredicateIsUnknown sig action = asks (hasPredicate sig) >>= flip unless action + + --resolve' :: Int -> Unifier -> [Goal] -> Stack -> m [Unifier] + resolve' depth usf [] stack = do + trace "=== yield solution ===" + trace_ "Depth" depth + trace_ "Unif." usf + + markSolution usf + + (cleanup usf:) <$> backtrack depth stack + resolve' depth usf (Cut n:gs) stack = do + trace "=== resolve' (Cut) ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" (Cut n:gs) + mapM_ (trace_ "Stack") stack + + createConnections usf (Cut n:gs) [(usf, gs)] + + markCutBranches (take n stack) + + resolve' depth usf gs (drop n stack) + resolve' depth usf goals@(Struct "asserta" [fact]:gs) stack = do + trace "=== resolve' (asserta/1) ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" goals + mapM_ (trace_ "Stack") stack + + createConnections usf goals [(usf, gs)] + + local (asserta fact) $ resolve' depth usf gs stack + resolve' depth usf goals@(Struct "assertz" [fact]:gs) stack = do + trace "=== resolve' (assertz/1) ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" goals + mapM_ (trace_ "Stack") stack + + createConnections usf goals [(usf, gs)] + + local (assertz fact) $ resolve' depth usf gs stack + resolve' depth usf goals@(Struct "retract" [t]:gs) stack = do + trace "=== resolve' (retract/1) ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" goals + mapM_ (trace_ "Stack") stack + + createConnections usf goals [(usf, gs)] + + clauses <- asks (getClauses t) + case [ t' | Clause t' [] <- clauses, isJust (unify t t') ] of + [] -> return (fail "retract/1") + (fact:_) -> local (abolish fact) $ resolve' depth usf gs stack + resolve' depth usf (nextGoal:gs) stack = do + trace "=== resolve' ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" (nextGoal:gs) + mapM_ (trace_ "Stack") stack + let sig = signature nextGoal + whenPredicateIsUnknown sig $ do + throwError $ strMsg $ "Unknown predicate: " ++ show sig + branches <- getBranches + + createConnections usf (nextGoal:gs) branches + + choose depth usf gs branches stack + where + getBranches = do + clauses <- asks (getClauses nextGoal) + return $ do + clause <- renameVars clauses + u <- unify (apply usf nextGoal) (lhs clause) + let newGoals = rhs clause (map snd u) + let u' = usf +++ u + let gs' = map (apply u') $ newGoals ++ gs + let gs'' = everywhere (mkT shiftCut) gs' + return (u', gs'') + + shiftCut (Cut n) = Cut (succ n) + shiftCut t = t + + renameVars = everywhere $ mkT $ \(VariableName _ v) -> VariableName depth v + + choose depth _ _ [] stack = backtrack depth stack + choose depth u gs ((u',gs'):alts) stack = do + trace "=== choose ===" + trace_ "Depth" depth + trace_ "Unif." u + trace_ "Goals" gs + mapM_ (trace_ "Alt.") ((u',gs'):alts) + mapM_ (trace_ "Stack") stack + resolve' (succ depth) u' gs' ((u,gs,alts) : stack) + + backtrack _ [] = do + trace "=== give up ===" + return (fail "Goal cannot be resolved!") + backtrack depth ((u,gs,alts):stack) = do + trace "=== backtrack ===" + choose (pred depth) u gs alts stack + + diff --git a/src/IsString.hs b/src/IsString.hs new file mode 100644 --- /dev/null +++ b/src/IsString.hs @@ -0,0 +1,27 @@ +-- Allow specification through string literals by using OverloadedStrings. +-- +module IsString () where + +import GHC.Exts (IsString(..)) +import Control.Applicative ((<*)) +import Text.Parsec (parse, eof) + +import Prolog ( vname, term, clause + , VariableName, Term, Clause ) + + +instance IsString Clause where + fromString s = + case parse (clause <* eof) "(Clause literal)" s of + Left e -> error (show e) + Right c -> c +instance IsString Term where + fromString s = + case parse (term <* eof) "(Term literal)" s of + Left e -> error (show e) + Right c -> c +instance IsString VariableName where + fromString s = + case parse (vname <* eof) "(VariableName literal)" s of + Left e -> error (show e) + Right c -> c diff --git a/src/Language/Prolog.hs b/src/Language/Prolog.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog.hs @@ -0,0 +1,2 @@ +module Language.Prolog (module Prolog) where +import Prolog diff --git a/src/Language/Prolog/IsString.hs b/src/Language/Prolog/IsString.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/IsString.hs @@ -0,0 +1,2 @@ +module Language.Prolog.IsString (module IsString) where +import IsString diff --git a/src/Language/Prolog/Quote.hs b/src/Language/Prolog/Quote.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/Quote.hs @@ -0,0 +1,2 @@ +module Language.Prolog.Quote (module Quote) where +import Quote diff --git a/src/Parser.hs b/src/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Parser.hs @@ -0,0 +1,128 @@ +module Parser + ( consult, consultString, parseQuery + , program, whitespace, comment, clause, terms, term, bottom, vname + ) where + +import Text.Parsec +import Text.Parsec.Expr hiding (Assoc(..)) +import qualified Text.Parsec.Expr as Parsec +import qualified Text.Parsec.Token as P +import Text.Parsec.Language (emptyDef) +import Control.Applicative ((<$>),(<*>),(<$),(<*)) + +import Syntax + +consult = fmap consultString . readFile + +consultString :: String -> Either ParseError Program +consultString = parse (whitespace >> program <* eof) "(input)" + +parseQuery = parse (whitespace >> terms <* eof) "(query)" + +program = many (clause <* char '.' <* whitespace) + +whitespace = skipMany (comment <|> skip space "") +comment = skip $ choice + [ string "/*" >> (manyTill anyChar $ try $ string "*/") + , char '%' >> (manyTill anyChar $ try $ skip newline <|> eof) + ] + +skip = (>> return ()) + +clause = do t <- struct <* whitespace + dcg t <|> normal t + where + normal t = do + ts <- option [] $ do string ":-" <* whitespace + terms + return (Clause t ts) + + dcg t = do + string "-->" <* whitespace + ts <- terms + return (translate (t,ts)) + + translate ((Struct a ts), rhs) = + let lhs' = Struct a (arguments ts (head vars) (last vars)) + vars = map (var.("d_"++).(a++).show) [0..length rhs] -- We explicitly choose otherwise invalid variable names + rhs' = zipWith3 translate' rhs vars (tail vars) + in Clause lhs' rhs' + + translate' t s s0 | isList t = Struct "=" [ s, foldr_pl cons s0 t ] -- Terminal + translate' t@(Struct "{}" ts) s s0 = foldr and (Struct "=" [ s, s0 ]) ts -- Braced terms + translate' (Struct a ts) s s0 = Struct a (arguments ts s s0) -- Non-Terminal + + and x y = Struct "," [x,y] + + + +isList (Struct "." [_,_]) = True +isList (Struct "[]" []) = True +isList _ = False + + + +terms = sepBy1 termWithoutConjunction (charWs ',') + +term = term' False +termWithoutConjunction = term' True + + + +term' ignoreConjunction = buildExpressionParser (reverse $ map (map toParser) $ hierarchy ignoreConjunction) (bottom <* whitespace) + +bottom = variable + <|> struct + <|> list + <|> stringLiteral + <|> cut <$ char '!' + <|> Struct "{}" <$> between (charWs '{') (char '}') terms + <|> between (charWs '(') (char ')') term + +toParser (PrefixOp name) = Prefix (reservedOp name >> return (\t -> Struct name [t])) +toParser (InfixOp assoc name) = Infix (reservedOp name >> return (\t1 t2 -> Struct name [t1, t2])) + (case assoc of AssocLeft -> Parsec.AssocLeft + AssocRight -> Parsec.AssocRight) +reservedOp = P.reservedOp $ P.makeTokenParser $ emptyDef + { P.opStart = oneOf ";,<=>\\i*+m@" + , P.opLetter = oneOf "=.:<+" + , P.reservedOpNames = operatorNames + , P.caseSensitive = True + } + +charWs c = char c <* whitespace + +operatorNames = [ ";", ",", "<", "=..", "=:=", "=<", "=", ">=", ">", "\\=", "is", "*", "+", "-", "\\", "mod", "\\+" ] + +variable = (Wildcard <$ try (char '_' <* notFollowedBy (alphaNum <|> char '_'))) + <|> Var <$> vname + "variable" + +vname = VariableName 0 <$> ((:) <$> upper <*> many (alphaNum <|> char '_') <|> + (:) <$> char '_' <*> many1 (alphaNum <|> char '_')) + +atom = (:) <$> lower <*> many (alphaNum <|> char '_') + <|> many1 digit + <|> choice (map string operatorNames) + <|> many1 (oneOf "#$&*+/.<=>\\^~") + <|> between (char '\'') (char '\'') (many (noneOf "'")) + "atom" + +struct = do a <- atom + ts <- option [] $ between (charWs '(') (char ')') terms + return (Struct a ts) + +list = between (charWs '[') (char ']') $ + flip (foldr cons) <$> option [] terms + <*> option nil (charWs '|' >> term) + + +stringLiteral = foldr cons nil . map representChar <$> between (char '"') (char '"') (try (many (noneOf "\""))) + +representChar c = Struct (show (fromEnum c)) [] -- This is the classical Prolog representation of chars as code points. +--representChar c = Struct [c] [] -- This is the more natural representation as one-character atoms. +--representChar c = Struct "char" [Struct (show (fromEnum c)) []] -- This is a representation as tagged code points. +--toChar :: Term -> Maybe Char +--toChar (Struct "char" [Struct (toEnum . read->c) []]) = Just c +--toChar _ = Nothing + diff --git a/src/Prolog.hs b/src/Prolog.hs new file mode 100644 --- /dev/null +++ b/src/Prolog.hs @@ -0,0 +1,21 @@ +module Prolog + ( Term(..), var, cut + , Clause(..), rhs + , VariableName(..), Atom, Unifier, Substitution, Program, Goal + , unify, unify_with_occurs_check + , apply + , MonadTrace(..) + , withTrace + , MonadGraphGen(..) + , runNoGraphT + , resolve, resolve_ + , (+++) + , consult, consultString, parseQuery + , program, whitespace, comment, clause, terms, term, bottom, vname + ) +where + +import Syntax +import Parser +import Unifier +import Interpreter diff --git a/src/Quote.hs b/src/Quote.hs new file mode 100644 --- /dev/null +++ b/src/Quote.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE TemplateHaskell, FlexibleInstances #-} +module Quote (t,ts,c,pl) where + +import Control.Applicative ((<*)) +import Data.Functor.Identity (Identity) + +import Language.Haskell.TH (listE, varE, viewP, mkName, Q, Exp, Pat) +import Language.Haskell.TH.Syntax (Lift(lift)) +import Language.Haskell.TH.Lift (deriveLiftMany) +import Language.Haskell.TH.Quote (QuasiQuoter(..)) +import Text.Parsec (parse, eof, ParsecT) +import Data.Generics (extQ, typeOf, Data) + +import Prolog ( Term(..), VariableName, Clause(..), Goal + , term, terms, clause, program, whitespace + ) + +$(deriveLiftMany [''Term, ''VariableName, ''Clause]) + +instance Lift ([Term] -> [Goal]) where + lift _ = fail "Clauses using Haskell functions can't be lifted." + + +t = prologQuasiQuoter term "term" +ts = prologQuasiQuoter terms "term list" +c = prologQuasiQuoter clause "clause" +pl = prologQuasiQuoter program "program" + +prologQuasiQuoter parser name = + QuasiQuoter { quoteExp = parsePrologExp parser name + , quotePat = parsePrologPat parser name + , quoteType = fail ("Prolog "++ name ++"s can't be Haskell types!") + , quoteDec = fail ("Prolog "++ name ++"s can't be Haskell declarations!") + } + +parsePrologExp :: (Data a, Lift a) => ParsecT [Char] () Identity a -> String -> String -> Q Exp +parsePrologExp parser name str = do + case parse (whitespace >> parser <* eof) ("(Prolog " ++ name ++ " expression)") str of + Right x -> const (fail $ "Quasi-quoted expressions of type " ++ show (typeOf x) ++ " are not implemented.") + `extQ` unquote -- Term + `extQ` (listE . map unquote) -- [Term] + `extQ` unquoteClause -- Clause + `extQ` (listE . map unquoteClause) -- [Clause] + $ x + Left e -> fail (show e) + where + unquote (Struct "$" [Struct var []]) = + [e| Struct (show $(varE (mkName var))) [] |] + unquote (Struct "$" _) = fail "Found '$' with non-unquotable arguments" + unquote (Struct a ts) = [e| Struct a $(listE $ map unquote ts) |] + unquote t = lift t + + unquoteClause (Clause lhs rhs) = + [e| Clause $(unquote lhs) $(listE $ map unquote rhs) |] + unquoteClause (ClauseFn _ _) = + fail "Clauses using Haskell functions are not quasi-quotable." + + +parsePrologPat :: (Data a, Lift a) => ParsecT [Char] () Identity a -> String -> String -> Q Pat +parsePrologPat parser name str = do + case parse (whitespace >> parser <* eof) ("(Prolog " ++ name ++ " pattern)") str of + Right x -> viewP [e| (== $(lift x)) |] [p| True |] diff --git a/src/Syntax.hs b/src/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Syntax.hs @@ -0,0 +1,162 @@ +{-# LANGUAGE DeriveDataTypeable, ViewPatterns, ScopedTypeVariables #-} +module Syntax + ( Term(..), var, cut + , Clause(..), rhs + , VariableName(..), Atom, Goal, Program + , cons, nil, foldr_pl + , arguments -- FIXME Should not be exposed + , hierarchy + , Operator(..), Assoc(..) + ) +where + +import Data.Generics (Data(..), Typeable(..)) +import Data.List (intercalate) +import Data.Char (isLetter) + + +data Term = Struct Atom [Term] + | Var VariableName + | Wildcard + | Cut Int + deriving (Eq, Data, Typeable) +var = Var . VariableName 0 +cut = Cut 0 + +data Clause = Clause { lhs :: Term, rhs_ :: [Goal] } + | ClauseFn { lhs :: Term, fn :: [Term] -> [Goal] } + deriving (Data, Typeable) +rhs (Clause _ rhs) = const rhs +rhs (ClauseFn _ fn ) = fn + +data VariableName = VariableName Int String + deriving (Eq, Data, Typeable, Ord) + +type Atom = String +type Goal = Term +type Program = [Clause] + +instance Ord Term where + (<=) = wildcards <=! variables <=! atoms <=! compound_terms <=! error "incomparable" + +infixr 4 <=! +(q <=! _) (q->Just l) (q->Just r) = l <= r +(q <=! _) (q->Just _) _ = True +(q <=! _) _ (q->Just _) = False +(_ <=! c) x y = c x y + +wildcards Wildcard = Just () +wildcards _ = Nothing + +variables (Var v) = Just v +variables _ = Nothing + +numbers (Struct (reads->[(n :: Integer,"")]) []) = Just n +numbers _ = Nothing + +atoms (Struct a []) = Just [a] +atoms _ = Nothing + +compound_terms (Struct a ts) = Just (length ts, a, ts) +compound_terms _ = Nothing + + +instance Show Term where + show = prettyPrint False 0 + + +prettyPrint True _ t@(Struct "," [_,_]) = + "(" ++ prettyPrint False 0 t ++ ")" + +prettyPrint f n (Struct (flip lookup operatorTable->Just (p,InfixOp assoc name)) [l,r]) = + parensIf (n >= p) $ prettyPrint f n_l l ++ spaced name ++ prettyPrint f n_r r + where (n_l,n_r) = case assoc of + AssocLeft -> (p-1, p) + AssocRight -> (p, p-1) + +prettyPrint f n (Struct (flip lookup operatorTable->Just (p,PrefixOp name)) [r]) = + parensIf (n >= p) $ name ++ prettyPrint f (p {- Non-associative -}) r + +prettyPrint _ _ t@(Struct "." [_,_]) = + let (ts,rest) = g [] t in + --case guard (isNil rest) >> sequence (map toChar ts) of + -- Just str -> prettyPrint str + -- Nothing -> + "[" ++ intercalate "," (map (prettyPrint True 0) ts) ++ (if isNil rest then "" else "|" ++ (prettyPrint True 0) rest) ++ "]" + where g ts (Struct "." [h,t]) = g (h:ts) t + g ts t = (reverse ts, t) + isNil (Struct "[]" []) = True + isNil _ = False + +prettyPrint _ _ (Struct a []) = a +prettyPrint _ _ (Struct a ts) = a ++ "(" ++ intercalate ", " (map (prettyPrint True 0) ts) ++ ")" +prettyPrint _ _ (Var v) = show v +prettyPrint _ _ Wildcard = "_" +prettyPrint _ _ ((==cut)->True) = "!" +prettyPrint _ _ (Cut n) = "!^" ++ show n + + +spaced s = let h = head s + l = last s + in spaceIf (isLetter h) ++ s ++ spaceIf (isLetter l || ',' == l) + +spaceIf True = " " +spaceIf False = "" + +parensIf :: Bool -> String -> String +parensIf True s = "(" ++ s ++")" +parensIf False s = s + + +operatorTable :: [(String, (Int,Operator))] +operatorTable = concat $ zipWith (map . g) [1..] $ hierarchy False + where g p op@(InfixOp _ name) = (name,(p,op)) + g p op@(PrefixOp name) = (name,(p,op)) + +instance Show VariableName where + show (VariableName 0 v) = v + show (VariableName i v) = show i ++ "#" ++ v + +instance Show Clause where + show (Clause lhs [] ) = show $ show lhs + show (Clause lhs rhs) = show $ show lhs ++ " :- " ++ intercalate ", " (map show rhs) + show (ClauseFn lhs _ ) = show $ show lhs ++ " :- " ++ "" + + + + +foldr_pl f k (Struct "." [h,t]) = f h (foldr_pl f k t) +foldr_pl _ k (Struct "[]" []) = k + +cons t1 t2 = Struct "." [t1,t2] +nil = Struct "[]" [] + +data Operator = PrefixOp String + | InfixOp Assoc String +data Assoc = AssocLeft + | AssocRight + +hierarchy :: Bool -> [[Operator]] +hierarchy ignoreConjunction = + --[ [ InfixOp NonAssoc "-->", InfixOp NonAssoc ":-" ] + [ [ infixR ";" ] ] ++ + (if ignoreConjunction then [] else [ [ infixR "," ] ]) ++ + [ [ prefix "\\+" ] + , map infixL ["<", "=..", "=:=", "=<", "=", ">=", ">", "\\=", "is", "==", "@<", "@=<", "@>=", "@>"] + , map infixL ["+", "-", "\\"] + , [ infixL "*"] + , [ infixL "mod" ] + , [ prefix "-" ] + , [ prefix "$" ] -- used for quasi quotation + ] + where + prefix = PrefixOp + infixL = InfixOp AssocLeft + infixR = InfixOp AssocRight + + +--infix 6 \\ +--x \\ y = Struct "\\" [x,y] + +arguments ts xs ds = ts ++ [ xs, ds ] +-- arguments ts xs ds = [ xs \\ ds ] ++ ts diff --git a/src/Unifier.hs b/src/Unifier.hs new file mode 100644 --- /dev/null +++ b/src/Unifier.hs @@ -0,0 +1,62 @@ +module Unifier + ( Unifier, Substitution + , unify, unify_with_occurs_check + , apply, (+++) + ) +where + +import Control.Monad (MonadPlus, mzero) +import Control.Arrow (second) +import Data.Function (fix) +import Data.Generics (everything, mkQ) + +import Syntax + +type Unifier = [Substitution] +type Substitution = (VariableName, Term) + + +unify, unify_with_occurs_check :: MonadPlus m => Term -> Term -> m Unifier + +unify = fix unify' + +unify_with_occurs_check = + fix $ \self t1 t2 -> if (t1 `occursIn` t2 || t2 `occursIn` t1) + then fail "occurs check" + else unify' self t1 t2 + where + occursIn t = everything (||) (mkQ False (==t)) + + +unify' _ Wildcard _ = return [] +unify' _ _ Wildcard = return [] +unify' _ (Var v) t = return [(v,t)] +unify' _ t (Var v) = return [(v,t)] +unify' self (Struct a1 ts1) (Struct a2 ts2) | a1 == a2 && same length ts1 ts2 = + unifyList self (zip ts1 ts2) +unify' _ _ _ = mzero + +same :: Eq b => (a -> b) -> a -> a -> Bool +same f x y = f x == f y + +unifyList :: Monad m => (Term -> Term -> m Unifier) -> [(Term, Term)] -> m Unifier +unifyList _ [] = return [] +unifyList unify ((x,y):xys) = do + u <- unify x y + u' <- unifyList unify (map (both (apply u)) xys) + return (u++u') + +both f (x,y) = (f x, f y) + +u1 +++ u2 = simplify $ u1 ++ u2 + +simplify :: Unifier -> Unifier +simplify u = map (second (apply u)) u + + +apply :: Unifier -> Term -> Term +apply = flip $ foldl $ flip substitute + where + substitute (v,t) (Var v') | v == v' = t + substitute s (Struct a ts) = Struct a (map (substitute s) ts) + substitute _ t = t