diff --git a/NanoProlog.cabal b/NanoProlog.cabal --- a/NanoProlog.cabal +++ b/NanoProlog.cabal @@ -1,5 +1,5 @@ Name: NanoProlog -Version: 0.1.2 +Version: 0.1.3 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,23 +9,25 @@ a tree showing which rules were applied in which order. License: BSD3 license-file: LICENSE -Author: Doaitse Swierstra, Jurriën Stutterheim -Maintainer: Jurriën Stutterheim +Author: Doaitse Swierstra, Jurrien Stutterheim +Maintainer: Jurrien Stutterheim Stability: Experimental Category: Language Build-type: Simple -Cabal-version: >= 1.6 +Cabal-version: >= 1.8 Source-repository head Type: git Location: https://github.com/norm2782/NanoProlog.git Executable nano-prolog - Hs-source-dirs: src - Main-is: Main.hs + Hs-source-dirs: src/Language/Prolog/NanoProlog + Main-is: NanoProlog.hs Build-depends: - base >= 4 && < 5 + base >= 4 && < 5, + NanoProlog >= 0.1.3, + uu-parsinglib >= 2.7.1 Library Build-Depends: base >= 4.0 && < 5.0, diff --git a/src/Language/Prolog/NanoProlog/Lib.hs b/src/Language/Prolog/NanoProlog/Lib.hs --- a/src/Language/Prolog/NanoProlog/Lib.hs +++ b/src/Language/Prolog/NanoProlog/Lib.hs @@ -15,6 +15,7 @@ , pFun , pRule , pTerm + , pTerms , show' , solve , startParse @@ -59,10 +60,11 @@ emptyEnv = Just M.empty -- * The Prolog machinery -data Result = None - | Done Env - | ApplyRules [(Rule, Result)] +data Result = Done Env + | ApplyRules [(Rule, Result)] +type Proofs = [(String, Rule)] + class Subst t where subst :: Env -> t -> t @@ -79,58 +81,59 @@ 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 + 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 _ _ = None +solve _ Nothing _ _ = ApplyRules [] solve _ (Just e) _ [] = Done e solve rules e n (t:ts) = ApplyRules - [ (rule, solve rules (unify (t, c) e) (n+1) (cs ++ ts)) - | rule@(c :<-: cs) <- tag n rules ] + [ (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 :: [(String, Rule)] -> [String] -> Result -> [([(String, Rule)], Env)] +enumerateDepthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)] enumerateDepthFirst proofs _ (Done env) = [(proofs, env)] -enumerateDepthFirst proofs _ None = [] -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 - ] +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 :: [(String, Rule)] -> [String] -> Result -> [([(String, Rule)], Env)] +enumerateBreadthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)] -} -- | `printEnv` prints a single solution, showing only the variables -- that were introduced in the original goal -show' :: Env -> [Char] -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'] +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 ++ ")" + 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 ++ "." + show (t :<-: [] ) = show t ++ "." + show (t :<-: ts ) = show t ++ ":-" ++ showCommas ts ++ "." showCommas :: Show a => [a] -> String showCommas l = intercalate ", " (map show l) @@ -145,9 +148,8 @@ pTerm = pVar <|> pFun pVar = Var <$> lexeme (pList1 pUpper) pFun = Fun <$> pLowerCase <*> (pParens pTerms `opt` []) - where pLowerCase :: Parser String - pLowerCase = (:) <$> pLower - <*> lexeme (pList (pLetter <|> pDigit)) + where pLowerCase :: Parser String + pLowerCase = (:) <$> pLower <*> lexeme (pList (pLetter <|> pDigit)) pRule :: Parser Rule pRule = (:<-:) <$> pFun <*> (pSymbol ":-" *> pTerms `opt` []) <* pDot diff --git a/src/Language/Prolog/NanoProlog/NanoProlog.hs b/src/Language/Prolog/NanoProlog/NanoProlog.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/NanoProlog/NanoProlog.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +module Main where + +import Language.Prolog.NanoProlog.Lib +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 +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 + +-- | `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 + +-- | `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 ] diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 --- a/src/Main.hs +++ /dev/null @@ -1,58 +0,0 @@ -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} - -module Main where - -import Language.Prolog.NanoProlog.Lib -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 -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 - --- | `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 - --- | `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 ]