NanoProlog 0.2.2 → 0.2.3
raw patch · 4 files changed
+50/−36 lines, 4 filesnew-uploader
Files
- NanoProlog.cabal +5/−2
- src/Language/Prolog/NanoProlog/Interpreter.hs +1/−1
- src/Language/Prolog/NanoProlog/NanoProlog.hs +40/−33
- tc.pro +4/−0
NanoProlog.cabal view
@@ -1,5 +1,5 @@ Name: NanoProlog-Version: 0.2.2+Version: 0.2.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@@ -7,6 +7,9 @@ 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.+ .+ The file @royals.pro@ contains a description of part of the Dutch royal family, whereas the file + @tc.pro@ shows unification at work in a very small type inferencer. License: BSD3 license-file: LICENSE Author: Doaitse Swierstra, Jurriën Stutterheim@@ -15,7 +18,7 @@ Category: Language Build-type: Simple Cabal-version: >= 1.6-Extra-Source-Files: README, royals.pro+Extra-Source-Files: README, royals.pro, tc.pro Source-repository head Type: git
src/Language/Prolog/NanoProlog/Interpreter.hs view
@@ -51,6 +51,6 @@ | (prefix, pr) <- reverse proof ] putStr "substitution: "- putStrLn (show' env)+ putStrLn (show env) void getLine | (proof, env) <- enumerateDepthFirst [] result ]
src/Language/Prolog/NanoProlog/NanoProlog.hs view
@@ -18,7 +18,6 @@ , pRule , pTerm , pTerms- , show' , solve , startParse , unify@@ -43,8 +42,7 @@ type TaggedTerm = (Tag, Term) -data Rule = Term :<-: [Term]- deriving Eq+data Rule = Term :<-: [Term] deriving Eq class Taggable a where tag :: Tag -> a -> a@@ -59,12 +57,17 @@ instance Taggable a => Taggable [a] where tag n = map (tag n) -type Env = Map UpperCase Term+newtype Env = Env {fromEnv :: Map UpperCase Term} -emptyEnv :: Maybe (Map UpperCase t)-emptyEnv = Just M.empty+emptyEnv :: Maybe Env+emptyEnv = Just (Env M.empty) -- * The Prolog machinery+-- The result type contains a search tree, where the branches represent an application of a rule, and the +-- leaves succesful results. Successes are represented by their corresponding substitution.+-- A branch is represented by the tag used to loabel the rule that was applied, by the rule that was applied, +-- and by the ``continution'' of the search.+ data Result = Done Env | ApplyRules [(Tag, Rule, Result)] @@ -77,7 +80,7 @@ subst e = map (subst e) instance Subst Term where- subst env (Var x) = maybe (Var x) (subst env) (M.lookup x env)+ subst env (Var x) = maybe (Var x) (subst env) (M.lookup x (fromEnv env)) subst env (Fun x cs) = Fun x (subst env cs) instance Subst Rule where@@ -85,17 +88,17 @@ matches :: (Term, Term) -> Maybe Env -> Maybe Env matches _ Nothing = Nothing-matches (t, u) env@(Just m) = match(subst m t) u- where match (Var x) y = Just (M.insert x y m)+matches (t, u) env@(Just e@(Env m)) = match(subst e t) u+ where match (Var x) y = Just . Env $ M.insert x y m match (Fun x xs) (Fun y ys) | x == y && length xs == length ys = foldr matches env (zip xs ys) match _ _ = Nothing 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)+unify (t, u) env@(Just e@(Env m)) = uni (subst e t) (subst e u)+ where uni (Var x) y = Just (Env (M.insert x y m))+ uni x (Var y) = Just (Env (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@@ -123,25 +126,24 @@ {- -- | `enumerateBreadthFirst` is still undefined, and is left as an--- exercise to the JCU students+-- exercise to the students enumerateBreadthFirst :: Proofs -> 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 Env where+ show e@(Env env) = intercalate ", " . filter (not.null) . map showBdg $ M.assocs env+ where showBdg (x, t) | isGlobVar x = x ++ " <- " ++ show(subst e t) + | otherwise = ""+ 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 "->" [f,a]) = "(" ++ show f ++ ")" ++ " -> " ++ show a + show (Fun "[]" [l]) = "[" ++ show l ++ "]"+ show (Fun i ts ) = i ++ "(" ++ showCommas ts ++ ")" instance Show Rule where show (t :<-: [] ) = show t ++ "."@@ -151,23 +153,28 @@ 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 :: (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 pSepDot :: Parser String -> Parser [String]-pSepDot p = (:) <$> p <*> pFoldr list_alg ((:) <$> pDot <*> p)+pSepDot p = (:) <$> p <*> pList ((:) <$> pDot <*> p) -pTerm, pVar, pFun :: Parser Term-pTerm = pVar <|> pFun-pVar = Var <$> lexeme ((++) <$> pList1 pUpper <*> (concat <$> pSepDot (pList1 pDigit) <|> pure []))-pFun = Fun <$> pLowerCase <*> (pParens pTerms `opt` [])+pTerm, pFactor, pVar, pFun :: Parser Term+pTerm = pChainr ((\ f a -> Fun "->" [f, a]) <$ pToken "->") pFactor+pFactor = pVar+ <|> pFun+ <|> pParens pTerm++pVar = Var <$> lexeme ((++) <$> pList1 pUpper <*> (concat <$> pSepDot (pList1 pDigit) `opt` []))+pFun = Fun <$> pLowerCase <*> (pParens pTerms `opt` [])+ <|> Fun "[]" <$> pBrackets ((:[]) <$> pTerm) where pLowerCase :: Parser String- pLowerCase = (:) <$> pLower <*> lexeme (pList (pLetter <|> pDigit))+ pLowerCase = lexeme ((:) <$> pLower <*> pList (pLetter <|> pDigit)) pRule :: Parser Rule pRule = (:<-:) <$> pFun <*> (pSymbol ":-" *> pTerms `opt` []) <* pDot pTerms :: Parser [Term]-pTerms = pListSep pComma pTerm+pTerms = pList1Sep pComma pTerm
+ tc.pro view
@@ -0,0 +1,4 @@+wellTyped(map,(A->B)->([A]->[B])).+wellTyped(foldr,(A->B->B)->B->[A]->B).+wellTyped(ap(F,V),A):-wellTyped(F, B->A), wellTyped(V,B).+