NanoProlog 0.1.2 → 0.1.3

raw patch · 4 files changed

+104/−100 lines, 4 filesdep +NanoPrologPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: NanoProlog

API changes (from Hackage documentation)

Files

• NanoProlog.cabal +9/−7
• src/Language/Prolog/NanoProlog/Lib.hs +37/−35
• src/Language/Prolog/NanoProlog/NanoProlog.hs +58/−0
• src/Main.hs +0/−58

@@ -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,

@@ -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

@@ -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 ]

@@ -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 ]