diff --git a/NanoProlog.cabal b/NanoProlog.cabal --- a/NanoProlog.cabal +++ b/NanoProlog.cabal @@ -1,5 +1,5 @@ Name: NanoProlog -Version: 0.1.3 +Version: 0.2 Synopsis: Very small interpreter for a Prolog-like language Description: This package was developed to demonstrate the ideas behind the Prolog language. It contains a very small interpreter @@ -9,24 +9,24 @@ a tree showing which rules were applied in which order. License: BSD3 license-file: LICENSE -Author: Doaitse Swierstra, Jurrien Stutterheim -Maintainer: Jurrien Stutterheim +Author: Doaitse Swierstra, Jurriën Stutterheim +Maintainer: j.stutterheim@uu.nl Stability: Experimental Category: Language Build-type: Simple -Cabal-version: >= 1.8 +Cabal-version: >= 1.6 +Extra-Source-Files: README, royals.pro Source-repository head Type: git Location: https://github.com/norm2782/NanoProlog.git Executable nano-prolog - Hs-source-dirs: src/Language/Prolog/NanoProlog - Main-is: NanoProlog.hs + Hs-source-dirs: src + Main-is: Main.hs Build-depends: base >= 4 && < 5, - NanoProlog >= 0.1.3, uu-parsinglib >= 2.7.1 Library @@ -35,4 +35,7 @@ ListLike == 3.1.*, containers == 0.4.* Hs-Source-Dirs: src - Exposed-modules: Language.Prolog.NanoProlog.Lib + Exposed-modules: Language.Prolog.NanoProlog.NanoProlog, + Language.Prolog.NanoProlog.Interpreter + Extensions: Rank2Types, FlexibleContexts, TypeSynonymInstances, + FlexibleInstances diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,1 @@ +NanoProlog README goes here. diff --git a/royals.pro b/royals.pro new file mode 100644 --- /dev/null +++ b/royals.pro @@ -0,0 +1,24 @@ +ma(mien,juul). +ma(juul,bea). +ma(bea,alex). +ma(bea,cons). +oma(X,Z):-ma(X,Y),ouder(Y,Z). + +append(nil,X,X). +append(cons(A,X), Y, cons(A,Z)):- append(X,Y,Z) . + +pa(alex,ale). +pa(alex,ama). +pa(alex,ari). +ma(max,ale). +ma(max,ama). +ma(max,ari). + +ouder(X,Y) :- pa(X,Y). +ouder(X,Y) :- ma(X,Y). + +voor(X,Y) :- ouder(X,Y). +voor(X,Y) :- ouder(X,Z), voor(Z,Y). + +plus(zero,X,X). +plus(succ(X), Y, succ(Z)) :- plus(X, Y,Z). diff --git a/src/Language/Prolog/NanoProlog/Interpreter.hs b/src/Language/Prolog/NanoProlog/Interpreter.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/NanoProlog/Interpreter.hs @@ -0,0 +1,53 @@ +module Language.Prolog.NanoProlog.Interpreter where + +import Language.Prolog.NanoProlog.NanoProlog +import Text.ParserCombinators.UU +import System.IO + +-- * Running the Interpreter +-- ** The main interpreter +-- | The `main` program prompt for a file with Prolog rules and call the main +-- interpreter loop +run :: IO () +run = do hSetBuffering stdin LineBuffering + putStrLn "File with rules?" + fn <- getLine + s <- readFile fn + let (rules, errors) = startParse (pList pRule) s + if null errors then do mapM_ print rules + loop rules + else do putStrLn "No rules parsed" + mapM_ print errors + run + +-- | `loop` ask for a goal, and enuartes all solutions found, each preceded by +-- a trace conatining the rules applied in a tree-like fashion +loop :: [Rule] -> IO () +loop rules = do putStrLn "goal? " + s <- getLine + unless (s == "quit") $ + do let (goal, errors) = startParse pFun s + if null errors + then printSolutions (solve rules emptyEnv [("0",goal)]) + else do putStrLn "Some goals were expected:" + mapM_ print errors + loop rules + +-- | `printSolutions` takes the result of a treewalk, which constructs +-- all the proofs, and pairs them with their final +-- substitutions. Alternative approaches in printing are to print the +-- raw proofs, i.e. without applying the final substitution (remove +-- the @subst env@ ). This nicely shows how the intermediate variables +-- come into life. By including the test on the length the facts +-- directly stemming from the data base are not printed. This makes +-- the proofs much shorter, but a bit less complete. +printSolutions :: Result -> IO () +printSolutions result = sequence_ + [ do sequence_ [ putStrLn (prefix ++ " " ++ show (subst env pr)) + | (prefix, pr@(p :<-: pp)) <- reverse proof +-- , length pp >0 + ] + putStr "substitution: " + putStrLn (show' env) + void getLine + | (proof, env) <- enumerateDepthFirst [] result ] diff --git a/src/Language/Prolog/NanoProlog/Lib.hs b/src/Language/Prolog/NanoProlog/Lib.hs deleted file mode 100644 --- a/src/Language/Prolog/NanoProlog/Lib.hs +++ /dev/null @@ -1,158 +0,0 @@ -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} - -module Language.Prolog.NanoProlog.Lib ( - LowerCase - , Result(..) - , Rule((:<-:)) - , Subst(..) - , Taggable(..) - , Term(..) - , emptyEnv - , enumerateDepthFirst - , pFun - , pRule - , pTerm - , pTerms - , show' - , solve - , startParse - , unify - ) where - -import Data.ListLike.Base (ListLike) -import Data.List (intercalate) -import Data.Map (Map) -import qualified Data.Map as M -import Text.ParserCombinators.UU -import Text.ParserCombinators.UU.BasicInstances -import Text.ParserCombinators.UU.Utils - --- * Types -type UpperCase = String -type LowerCase = String - -data Term = Var UpperCase - | Fun LowerCase [Term] - deriving (Eq, Ord) - -data Rule = Term :<-: [Term] - deriving Eq - -class Taggable a where - tag :: Int -> a -> a - -instance Taggable Term where - tag n (Var x) = Var (x ++ show n) - tag n (Fun x xs) = Fun x (tag n xs) - -instance Taggable Rule where - tag n (c :<-: cs) = tag n c :<-: tag n cs - -instance Taggable a => Taggable [a] where - tag n = map (tag n) - -type Env = Map UpperCase Term - -emptyEnv :: Maybe (Map UpperCase t) -emptyEnv = Just M.empty - --- * The Prolog machinery -data Result = Done Env - | ApplyRules [(Rule, Result)] - -type Proofs = [(String, Rule)] - -class Subst t where - subst :: Env -> t -> t - -instance Subst a => Subst [a] where - subst e = map (subst e) - -instance Subst Term where - subst env (Var x) = maybe (Var x) (subst env) (M.lookup x env) - subst env (Fun x cs) = Fun x (subst env cs) - -instance Subst Rule where - subst env (c :<-: cs) = subst env c :<-: subst env cs - -unify :: (Term, Term) -> Maybe Env-> Maybe Env -unify _ Nothing = Nothing -unify (t, u) env@(Just m) = uni (subst m t) (subst m u) - where uni (Var x) y = Just (M.insert x y m) - uni x (Var y) = Just (M.insert y x m) - uni (Fun x xs) (Fun y ys) - | x == y && length xs == length ys = foldr unify env (zip xs ys) - | otherwise = Nothing - -solve :: [Rule] -> Maybe Env -> Int -> [Term] -> Result -solve _ Nothing _ _ = ApplyRules [] -solve _ (Just e) _ [] = Done e -solve rules e n (t:ts) = ApplyRules - [ (rule, solve rules nextenv (n+1) (cs ++ ts)) - | rule@(c :<-: cs) <- tag n rules - , nextenv@(Just _) <- [unify (t, c) e] - ] - --- ** Printing the solutions | `enumerateBreadthFirst` performs a --- depth-first walk over the `Result` tree, while accumulating the --- rules that were applied on the path which was traversed from the --- root to the current node. At a successful leaf this contains the --- full proof. -enumerateDepthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)] -enumerateDepthFirst proofs _ (Done env) = [(proofs, env)] -enumerateDepthFirst proofs (pr:prefixes) (ApplyRules bs) = - [ s | (rule@(c :<-: cs), subTree) <- bs - , let extraPrefixes = take (length cs) (map (\i -> pr ++ "." ++ show i) [1 ..]) - , s <- enumerateDepthFirst ((pr, rule):proofs) (extraPrefixes ++ prefixes) subTree - ] - -{- --- | `enumerateBreadthFirst` is still undefined, and is left as an --- exercise to the JCU students -enumerateBreadthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)] --} - --- | `printEnv` prints a single solution, showing only the variables --- that were introduced in the original goal -show' :: Env -> String -show' env = intercalate ", " . filter (not.null) . map showBdg $ M.assocs env - where showBdg (x, t) | isGlobVar x = x ++ " <- " ++ showTerm t - | otherwise = "" - showTerm t@(Var _) = showTerm (subst env t) - showTerm (Fun f []) = f - showTerm (Fun f ts) = f ++ "(" ++ intercalate ", " (map showTerm ts) ++ ")" - isGlobVar x = head x `elem` ['A'..'Z'] && last x `notElem` ['0'..'9'] - -instance Show Term where - show (Var i) = i - show (Fun i [] ) = i - show (Fun i ts ) = i ++ "(" ++ showCommas ts ++ ")" - -instance Show Rule where - show (t :<-: [] ) = show t ++ "." - show (t :<-: ts ) = show t ++ ":-" ++ showCommas ts ++ "." - -showCommas :: Show a => [a] -> String -showCommas l = intercalate ", " (map show l) - --- ** Parsing Rules and Terms -startParse :: (ListLike s b, Show b) => P (Str b s LineColPos) a -> s - -> (a, [Error LineColPos]) -startParse p inp = parse ((,) <$> p <*> pEnd) - $ createStr (LineColPos 0 0 0) inp - -pTerm, pVar, pFun :: Parser Term -pTerm = pVar <|> pFun -pVar = Var <$> lexeme (pList1 pUpper) -pFun = Fun <$> pLowerCase <*> (pParens pTerms `opt` []) - where pLowerCase :: Parser String - pLowerCase = (:) <$> pLower <*> lexeme (pList (pLetter <|> pDigit)) - -pRule :: Parser Rule -pRule = (:<-:) <$> pFun <*> (pSymbol ":-" *> pTerms `opt` []) <* pDot - -pTerms :: Parser [Term] -pTerms = pListSep pComma pTerm diff --git a/src/Language/Prolog/NanoProlog/NanoProlog.hs b/src/Language/Prolog/NanoProlog/NanoProlog.hs --- a/src/Language/Prolog/NanoProlog/NanoProlog.hs +++ b/src/Language/Prolog/NanoProlog/NanoProlog.hs @@ -3,56 +3,158 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} -module Main where +module Language.Prolog.NanoProlog.NanoProlog ( + LowerCase + , Result(..) + , Rule((:<-:)) + , Subst(..) + , Taggable(..) + , Term(..) + , emptyEnv + , enumerateDepthFirst + , pFun + , pRule + , pTerm + , pTerms + , show' + , solve + , startParse + , unify + ) where -import Language.Prolog.NanoProlog.Lib +import Data.ListLike.Base (ListLike) +import Data.List (intercalate) +import Data.Map (Map) +import qualified Data.Map as M import Text.ParserCombinators.UU -import System.IO +import Text.ParserCombinators.UU.BasicInstances +import Text.ParserCombinators.UU.Utils --- * Running the Interpreter --- ** The main interpreter --- | The `main` program prompt for a file with Prolog rules and call the main --- interpreter loop -main :: IO () -main = do hSetBuffering stdin LineBuffering - putStr "File with rules? " - fn <- getLine - s <- readFile fn - let (rules, errors) = startParse (pList pRule) s - if null errors then do mapM_ print rules - loop rules - else do putStrLn "No rules parsed" - mapM_ print errors - main +-- * Types +type UpperCase = String +type LowerCase = String +type Tag = String --- | `loop` ask for a goal, and enuartes all solutions found, each preceded by --- a trace conatining the rules applied in a tree-like fashion -loop :: [Rule] -> IO () -loop rules = do putStr "goal? " - s <- getLine - unless (s == "quit") $ - do let (goal, errors) = startParse pFun s - if null errors - then printSolutions (solve rules emptyEnv 0 [goal]) - else do putStrLn "Some goals were expected:" - mapM_ print errors - loop rules +data Term = Var UpperCase + | Fun LowerCase [Term] + deriving (Eq, Ord) --- | `printSolutions` takes the result of a treewalk, which constructs --- all the proofs, and pairs them with their final --- substitutions. Alternative approaches in printing are to print the --- raw proofs, i.e. without applying the final substitution (remove --- the @subst env@ ). This nicely shows how the intermediate variables --- come into life. By including the test on the length the facts --- directly stemming from the data base are not printed. This makes --- the proofs much shorter, but a bit less complete. -printSolutions :: Result -> IO () -printSolutions result = sequence_ - [ do sequence_ [ putStrLn (prefix ++ " " ++ show (subst env pr)) - | (prefix, pr@(p :<-: pp)) <- reverse proof --- , length pp >0 - ] - putStr "substitution: " - putStrLn (show' env) - void getLine - | (proof, env) <- enumerateDepthFirst [] ["0"] result ] +type TaggedTerm = (Tag, Term) + +data Rule = Term :<-: [Term] + deriving Eq + +class Taggable a where + tag :: Tag -> a -> a + +instance Taggable Term where + tag n (Var x) = Var (x ++ n) + tag n (Fun x xs) = Fun x (tag n xs) + +instance Taggable Rule where + tag n (c :<-: cs) = tag n c :<-: tag n cs + +instance Taggable a => Taggable [a] where + tag n = map (tag n) + +type Env = Map UpperCase Term + +emptyEnv :: Maybe (Map UpperCase t) +emptyEnv = Just M.empty + +-- * The Prolog machinery +data Result = Done Env + | ApplyRules [(Tag, Rule, Result)] + +type Proofs = [(Tag, Rule)] + +class Subst t where + subst :: Env -> t -> t + +instance Subst a => Subst [a] where + subst e = map (subst e) + +instance Subst Term where + subst env (Var x) = maybe (Var x) (subst env) (M.lookup x env) + subst env (Fun x cs) = Fun x (subst env cs) + +instance Subst Rule where + subst env (c :<-: cs) = subst env c :<-: subst env cs + +unify :: (Term, Term) -> Maybe Env-> Maybe Env +unify _ Nothing = Nothing +unify (t, u) env@(Just m) = uni (subst m t) (subst m u) + where uni (Var x) y = Just (M.insert x y m) + uni x (Var y) = Just (M.insert y x m) + uni (Fun x xs) (Fun y ys) + | x == y && length xs == length ys = foldr unify env (zip xs ys) + | otherwise = Nothing + +solve :: [Rule] -> Maybe Env -> [TaggedTerm] -> Result +solve _ Nothing _ = ApplyRules [] +solve _ (Just e) [] = Done e +solve rules e ((tg,t):ts) = ApplyRules + [ (tg, rule, solve rules nextenv (zip (map (\ n -> tg ++ "." ++ show n) [1..]) cs ++ ts)) + | rule@(c :<-: cs) <- tag tg rules + , nextenv@(Just _) <- [unify (t, c) e] + ] + +-- ** Printing the solutions | `enumerateBreadthFirst` performs a +-- depth-first walk over the `Result` tree, while accumulating the +-- rules that were applied on the path which was traversed from the +-- root to the current node. At a successful leaf this contains the +-- full proof. +enumerateDepthFirst :: Proofs -> Result -> [(Proofs, Env)] +enumerateDepthFirst proofs (Done env) = [(proofs, env)] +enumerateDepthFirst proofs (ApplyRules bs) = + [ s | (tag, rule@(c :<-: cs), subTree) <- bs + , s <- enumerateDepthFirst ((tag, rule):proofs) subTree + ] + +{- +-- | `enumerateBreadthFirst` is still undefined, and is left as an +-- exercise to the JCU students +enumerateBreadthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)] +-} + +-- | `printEnv` prints a single solution, showing only the variables +-- that were introduced in the original goal +show' :: Env -> String +show' env = intercalate ", " . filter (not.null) . map showBdg $ M.assocs env + where showBdg (x, t) | isGlobVar x = x ++ " <- " ++ showTerm t + | otherwise = "" + showTerm t@(Var _) = showTerm (subst env t) + showTerm (Fun f []) = f + showTerm (Fun f ts) = f ++ "(" ++ intercalate ", " (map showTerm ts) ++ ")" + isGlobVar x = head x `elem` ['A'..'Z'] && last x `notElem` ['0'..'9'] + +instance Show Term where + show (Var i) = i + show (Fun i [] ) = i + show (Fun i ts ) = i ++ "(" ++ showCommas ts ++ ")" + +instance Show Rule where + show (t :<-: [] ) = show t ++ "." + show (t :<-: ts ) = show t ++ ":-" ++ showCommas ts ++ "." + +showCommas :: Show a => [a] -> String +showCommas l = intercalate ", " (map show l) + +-- ** Parsing Rules and Terms +startParse :: (ListLike s b, Show b) => P (Str b s LineColPos) a -> s + -> (a, [Error LineColPos]) +startParse p inp = parse ((,) <$> p <*> pEnd) + $ createStr (LineColPos 0 0 0) inp + +pTerm, pVar, pFun :: Parser Term +pTerm = pVar <|> pFun +pVar = Var <$> lexeme (pList1 pUpper) +pFun = Fun <$> pLowerCase <*> (pParens pTerms `opt` []) + where pLowerCase :: Parser String + pLowerCase = (:) <$> pLower <*> lexeme (pList (pLetter <|> pDigit)) + +pRule :: Parser Rule +pRule = (:<-:) <$> pFun <*> (pSymbol ":-" *> pTerms `opt` []) <* pDot + +pTerms :: Parser [Term] +pTerms = pListSep pComma pTerm diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,10 @@ +module Main where + +import Language.Prolog.NanoProlog.Interpreter (run) + +-- * Running the Interpreter +-- ** The main interpreter +-- | The `main` program prompt for a file with Prolog rules and call the main +-- interpreter loop +main :: IO () +main = run