diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,25 @@ +Copyright (c) 2011, Jurriën Stutterheim, Robert Kreuzer +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * Neither the name of the nor the + names of its contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + diff --git a/NanoProlog.cabal b/NanoProlog.cabal new file mode 100644 --- /dev/null +++ b/NanoProlog.cabal @@ -0,0 +1,36 @@ +Name: NanoProlog +Version: 0.1 +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 + (@Language.Prolog.Nanoprolog@) which can be run on its + own. It reads a file with definitions, and then prompts + for a goal. All possibe solutions are printed, preceded by + 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 +Stability: Experimental +Category: Language +Build-type: Simple +Cabal-version: >= 1.6 + +Source-repository head + Type: git + Location: https://github.com/norm2782/NanoProlog.git + +Executable nano-prolog + Hs-source-dirs: src + Main-is: Language/Prolog/NanoProlog/Main.hs + + Build-depends: + base >= 4 && < 5 + +Library + Build-Depends: base >= 4.0 && < 5.0, + uu-parsinglib >= 2.7.1, + ListLike == 3.1.*, + containers == 0.4.* + Hs-Source-Dirs: src + Exposed-modules: Language.Prolog.NanoProlog.Lib 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/src/Language/Prolog/NanoProlog/Lib.hs b/src/Language/Prolog/NanoProlog/Lib.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/NanoProlog/Lib.hs @@ -0,0 +1,155 @@ +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +module Language.Prolog.NanoProlog.Lib ( + LowerCase + , Result(..) + , Rule((:<-:)) + , Term(..) + , emptyEnv + , enumerateDepthFirst + , pFun + , pRule + , pTerm + , show' + , solve + , subst + , 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 = None + | Done Env + | ApplyRules [(Rule, Result)] + +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 _ _ = None +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 ] + +-- ** 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 _ (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 + ] + +{- +-- | `enumerateBreadthFirst` is still undefined, and is left as an +-- exercise to the JCU students +enumerateBreadthFirst :: [(String, Rule)] -> [String] -> Result -> [([(String, Rule)], 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'] + +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/Main.hs b/src/Language/Prolog/NanoProlog/Main.hs new file mode 100644 --- /dev/null +++ b/src/Language/Prolog/NanoProlog/Main.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +module Language.Prolog.NanoProlog.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 ]