NanoProlog (empty) → 0.1
raw patch · 5 files changed
+276/−0 lines, 5 filesdep +ListLikedep +basedep +containerssetup-changed
Dependencies added: ListLike, base, containers, uu-parsinglib
Files
- LICENSE +25/−0
- NanoProlog.cabal +36/−0
- Setup.hs +2/−0
- src/Language/Prolog/NanoProlog/Lib.hs +155/−0
- src/Language/Prolog/NanoProlog/Main.hs +58/−0
+ LICENSE view
@@ -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 <organization> 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 <COPYRIGHT HOLDER> 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.+
+ NanoProlog.cabal view
@@ -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
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Language/Prolog/NanoProlog/Lib.hs view
@@ -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
+ src/Language/Prolog/NanoProlog/Main.hs view
@@ -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 ]