forked from norm2782/NanoProlog
/
NanoProlog.hs
166 lines (135 loc) · 5.13 KB
/
NanoProlog.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
module Language.Prolog.NanoProlog.NanoProlog (
Env
, LowerCase
, Result(..)
, Rule((:<-:))
, Subst(..)
, Taggable(..)
, Term(..)
, emptyEnv
, enumerateDepthFirst
, pFun
, pRule
, pTerm
, pTerms
, show'
, solve
, 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
type Tag = String
data Term = Var UpperCase
| Fun LowerCase [Term]
deriving (Eq, Ord)
type TaggedTerm = (Tag, Term)
data Rule = Term :<-: [Term]
deriving Eq
class Taggable a where
tag :: Tag -> a -> a
instance Taggable Term where
tag n (Var x) = Var (x ++ 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 = Done Env
| ApplyRules [(Tag, Rule, Result)]
type Proofs = [(Tag, Rule)]
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 -> [TaggedTerm] -> Result
solve _ Nothing _ = ApplyRules []
solve _ (Just e) [] = Done e
solve rls e ((tg,t):ts) = ApplyRules
[ let tagged = map (\n -> tg ++ "." ++ show n) ([1..] :: [Int])
result' = solve rls nextenv (zip tagged cs ++ ts)
in (tg, rule, result')
| rule@(c :<-: cs) <- tag tg rls
, 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 :: Proofs -> Result -> [(Proofs, Env)]
enumerateDepthFirst proofs (Done env) = [(proofs, env)]
enumerateDepthFirst proofs (ApplyRules bs) =
[ s | (tag', rule, subTree) <- bs
, s <- enumerateDepthFirst ((tag', rule):proofs) subTree
]
{-
-- | `enumerateBreadthFirst` is still undefined, and is left as an
-- exercise to the JCU 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 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
pSepDot :: Parser String -> Parser [String]
pSepDot p = (:) <$> p <*> pFoldr list_alg ((:) <$> 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` [])
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