diff --git a/prolog.cabal b/prolog.cabal --- a/prolog.cabal +++ b/prolog.cabal @@ -1,18 +1,13 @@ Name: prolog -Version: 0.1 +Version: 0.3.2 Synopsis: A Prolog interpreter written in Haskell. -Description: A Prolog interpreter written in Haskell. +Description: A Prolog interpreter written in Haskell. Implements a subset of the Prolog language. License: PublicDomain Author: Matthias Bartsch -Maintainer: bartsch@cs.uni-bonn.de -Homepage: https://github.com/Erdwolf/prolog +Maintainer: Marcel Fourné (haskell@marcelfourne.de) Category: Language Build-type: Simple -Cabal-version: >=1.6 - -Source-repository head - type: git - location: git://github.com/Erdwolf/prolog.git +Cabal-version: >=1.10 Library Exposed-modules: Language.Prolog @@ -27,14 +22,19 @@ IsString Quote Hs-Source-Dirs: src + Default-Language: Haskell98 Build-depends: base >=4 && <5, parsec >= 3.1.1, syb >= 0.3, mtl >= 2.0.1.0, - containers >=0.4 && <0.5, + containers, template-haskell, th-lift >=0.5.3, transformers >=0.2.2.0 + +source-repository head + type: git + location: https://github.com/mfourne/prolog diff --git a/src/Database.hs b/src/Database.hs --- a/src/Database.hs +++ b/src/Database.hs @@ -10,7 +10,7 @@ where import Data.Map (Map) -import qualified Data.Map as Map +import qualified Data.Map.Strict as Map import Syntax @@ -28,7 +28,7 @@ hasPredicate sig (DB index) = Map.member sig index createDB clauses emptyPredicates = DB $ - foldr (\clause -> Map.insertWith' (++) (signature (lhs clause)) [clause]) + foldr (\clause -> Map.insertWith (++) (signature (lhs clause)) [clause]) (Map.fromList [ (signature (Struct name []), []) | name <- emptyPredicates ]) clauses diff --git a/src/Interpreter.hs b/src/Interpreter.hs --- a/src/Interpreter.hs +++ b/src/Interpreter.hs @@ -11,7 +11,7 @@ import Control.Monad.Error import Data.Maybe (isJust) import Data.Generics (everywhere, mkT) -import Control.Applicative ((<$>),(<*>),(<$),(<*), Applicative(..)) +import Control.Applicative ((<$>),(<*>),(<$),(<*), Applicative(..), Alternative) import Data.List (sort, nub) import Syntax @@ -44,9 +44,6 @@ , 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 @@ -58,8 +55,6 @@ , 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]) @@ -78,6 +73,7 @@ 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 "div" [t1, t2]) = div <$> eval t1 <*> eval t2 eval (Struct "-" [t]) = negate <$> eval t eval _ = mzero @@ -109,13 +105,13 @@ trace x = lift (trace x) -newtype Trace m a = Trace { withTrace :: m a } deriving (Functor, Monad, MonadError e) +newtype Trace m a = Trace { withTrace :: m a } deriving (Functor, Applicative, Monad, MonadError e) trace_ label x = trace (label++":\t"++show x) class Monad m => MonadGraphGen m where - createConnections :: Unifier -> [Goal] -> [Branch] -> m () + createConnections :: Branch -> [Branch] -> [Branch] -> m () markSolution :: Unifier -> m () markCutBranches :: Stack -> m () @@ -125,32 +121,34 @@ markCutBranches = lift . markCutBranches -newtype NoGraphT m a = NoGraphT {runNoGraphT :: m a} deriving (Monad, Functor, MonadFix, MonadPlus, Applicative, MonadError e) +newtype NoGraphT m a = NoGraphT {runNoGraphT :: m a} deriving (Monad, Functor, MonadFix, Alternative, 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 () + markSolution _ = NoGraphT $ return () + markCutBranches _ = NoGraphT $ return () -type Stack = [(Unifier, [Goal], [Branch])] -type Branch = (Unifier, [Goal]) +type Stack = [(Branch, [Branch])] +type Branch = (Path, Unifier, [Goal]) +type Path = [Integer] -- Used for generating graph output +root = [] :: Path 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? +resolve_ program goals = map cleanup <$> runReaderT (resolve' 1 (root, [], 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 + resolve' depth (path, usf, []) stack = do trace "=== yield solution ===" trace_ "Depth" depth trace_ "Unif." usf @@ -158,52 +156,76 @@ markSolution usf (cleanup usf:) <$> backtrack depth stack - resolve' depth usf (Cut n:gs) stack = do + resolve' depth (path, 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)] + createConnections (path, usf, Cut n:gs) [(1:path,[],[])] [(1:path, usf, gs)] markCutBranches (take n stack) - resolve' depth usf gs (drop n stack) - resolve' depth usf goals@(Struct "asserta" [fact]:gs) stack = do + resolve' depth (1:path, usf, gs) (drop n stack) + resolve' depth (path, 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)] + createConnections (path, usf, goals) [(1:path,[],[])] [(1:path, usf, gs)] - local (asserta fact) $ resolve' depth usf gs stack - resolve' depth usf goals@(Struct "assertz" [fact]:gs) stack = do + local (asserta fact) $ resolve' depth (1:path, usf, gs) stack + resolve' depth (path, 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)] + createConnections (path, usf, goals) [(1:path,[],[])] [(1:path, usf, gs)] - local (assertz fact) $ resolve' depth usf gs stack - resolve' depth usf goals@(Struct "retract" [t]:gs) stack = do + local (assertz fact) $ resolve' depth (1:path, usf, gs) stack + resolve' depth (path, 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)] + createConnections (path, usf, goals) [(1:path,[],[])] [(1:path, 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 + (fact:_) -> local (abolish fact) $ resolve' depth (1:path, usf, gs) stack + resolve' depth (path, usf, goals@(nextGoal@(Struct "=" [l,r]):gs)) stack = do + -- This special case is here to avoid introducing unnecessary + -- variables that occur when applying "X=X." as a rule. + trace "=== resolve' (=/2) ===" + trace_ "Depth" depth + trace_ "Unif." usf + trace_ "Goals" goals + mapM_ (trace_ "Stack") stack + + let bs = [ (1:path,u,[]) | u <- unify l r ] + let branches = do + (p,u,[]) <- bs + let u' = usf +++ u + gs' = map (apply u') gs + gs'' = everywhere (mkT shiftCut) gs' + return (p, u', gs'') + + createConnections (path, usf, nextGoal:gs) bs branches + + choose depth (path,usf,gs) branches stack + + where + shiftCut (Cut n) = Cut (succ n) + shiftCut t = t + resolve' depth (path, usf, nextGoal:gs) stack = do trace "=== resolve' ===" trace_ "Depth" depth trace_ "Unif." usf @@ -212,43 +234,46 @@ let sig = signature nextGoal whenPredicateIsUnknown sig $ do throwError $ strMsg $ "Unknown predicate: " ++ show sig - branches <- getBranches + bs <- getProtoBranches -- Branch generation happens in two phases so visualizers can pick what to display. + let branches = do + (p, u, newGoals) <- bs + let u' = usf +++ u + let gs' = map (apply u') $ newGoals ++ gs + let gs'' = everywhere (mkT shiftCut) gs' + return (p, u', gs'') - createConnections usf (nextGoal:gs) branches + createConnections (path, usf, nextGoal:gs) bs branches - choose depth usf gs branches stack + choose depth (path,usf,gs) branches stack where - getBranches = do + getProtoBranches = do clauses <- asks (getClauses nextGoal) return $ do - clause <- renameVars clauses + (i,clause) <- zip [1..] $ 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'') + return (i:path, u, rhs clause (map snd u)) + 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 + choose depth _ [] stack = backtrack depth stack + choose depth (path,u,gs) ((path',u',gs'):alts) stack = do trace "=== choose ===" trace_ "Depth" depth trace_ "Unif." u trace_ "Goals" gs - mapM_ (trace_ "Alt.") ((u',gs'):alts) + mapM_ (trace_ "Alt.") ((path',u',gs'):alts) mapM_ (trace_ "Stack") stack - resolve' (succ depth) u' gs' ((u,gs,alts) : stack) + resolve' (succ depth) (path',u',gs') (((path,u,gs),alts) : stack) backtrack _ [] = do trace "=== give up ===" return (fail "Goal cannot be resolved!") - backtrack depth ((u,gs,alts):stack) = do + backtrack depth (((path,u,gs),alts):stack) = do trace "=== backtrack ===" - choose (pred depth) u gs alts stack + choose (pred depth) (path,u,gs) alts stack diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -92,7 +92,7 @@ charWs c = char c <* whitespace -operatorNames = [ ";", ",", "<", "=..", "=:=", "=<", "=", ">=", ">", "\\=", "is", "*", "+", "-", "\\", "mod", "\\+" ] +operatorNames = [ ";", ",", "<", "=..", "=:=", "=<", "=", ">=", ">", "\\=", "is", "*", "+", "-", "\\", "mod", "div", "\\+" ] variable = (Wildcard <$ try (char '_' <* notFollowedBy (alphaNum <|> char '_'))) <|> Var <$> vname diff --git a/src/Quote.hs b/src/Quote.hs --- a/src/Quote.hs +++ b/src/Quote.hs @@ -9,6 +9,7 @@ import Language.Haskell.TH.Lift (deriveLiftMany) import Language.Haskell.TH.Quote (QuasiQuoter(..)) import Text.Parsec (parse, eof, ParsecT) +import Text.Parsec.String (Parser) import Data.Generics (extQ, typeOf, Data) import Prolog ( Term(..), VariableName, Clause(..), Goal @@ -26,14 +27,15 @@ c = prologQuasiQuoter clause "clause" pl = prologQuasiQuoter program "program" +prologQuasiQuoter :: (Data a, Lift a) => Parser a -> String -> QuasiQuoter 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!") + , 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 :: (Data a, Lift a) => Parser 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.") @@ -56,7 +58,7 @@ fail "Clauses using Haskell functions are not quasi-quotable." -parsePrologPat :: (Data a, Lift a) => ParsecT [Char] () Identity a -> String -> String -> Q Pat +parsePrologPat :: (Data a, Lift a) => Parser 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 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -92,8 +92,9 @@ 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 +prettyPrint _ _ (Cut _) = "!" +--prettyPrint _ _ ((==cut)->True) = "!" +--prettyPrint _ _ (Cut n) = "!^" ++ show n spaced s = let h = head s @@ -115,7 +116,7 @@ instance Show VariableName where show (VariableName 0 v) = v - show (VariableName i v) = show i ++ "#" ++ v + show (VariableName i v) = v ++ "#" ++ show i instance Show Clause where show (Clause lhs [] ) = show $ show lhs @@ -146,6 +147,7 @@ , map infixL ["+", "-", "\\"] , [ infixL "*"] , [ infixL "mod" ] + , [ infixL "div" ] , [ prefix "-" ] , [ prefix "$" ] -- used for quasi quotation ] diff --git a/src/Unifier.hs b/src/Unifier.hs --- a/src/Unifier.hs +++ b/src/Unifier.hs @@ -5,18 +5,19 @@ ) where -import Control.Monad (MonadPlus, mzero) -import Control.Arrow (second) -import Data.Function (fix) -import Data.Generics (everything, mkQ) +import Control.Arrow (second) +import Control.Monad (mzero) +import Control.Monad.Fail (MonadFail) +import Data.Function (fix) +import Data.Generics (everything, mkQ) -import Syntax +import Syntax type Unifier = [Substitution] type Substitution = (VariableName, Term) -unify, unify_with_occurs_check :: MonadPlus m => Term -> Term -> m Unifier +unify, unify_with_occurs_check :: MonadFail m => Term -> Term -> m Unifier unify = fix unify' @@ -34,7 +35,7 @@ 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 +unify' _ _ _ = fail "unify'" same :: Eq b => (a -> b) -> a -> a -> Bool same f x y = f x == f y @@ -57,6 +58,6 @@ 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 + substitute (v,t) (Var v') | v == v' = t + substitute s (Struct a ts) = Struct a (map (substitute s) ts) + substitute _ t = t