From 252124ecb4a591bc7f46c12c6b784f5ee343cdc9 Mon Sep 17 00:00:00 2001 From: Ken Friis Larsen Date: Tue, 27 Oct 2009 09:33:10 +0100 Subject: [PATCH] Model solution --- miniprolog.hs | 212 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 212 insertions(+) create mode 100644 miniprolog.hs diff --git a/miniprolog.hs b/miniprolog.hs new file mode 100644 index 0000000..019ff67 --- /dev/null +++ b/miniprolog.hs @@ -0,0 +1,212 @@ +import Text.ParserCombinators.Parsec +import Data.List (nub) +import Control.Monad +import Control.Monad.State +--import Control.Monad.Trans + +---------------------------------------------------------------------- +-- Abstract Syntax Tree +---------------------------------------------------------------------- + + +type Goal = [Term] +type Program = Clauses +type Clauses = [Clause] +type Clause = (Term, Terms) -- head and body +data Term = Var Variable + | Comp Ident [Term] + deriving (Eq, Show, Read) +type Terms = [Term] +type Ident = String +type Variable = String + +---------------------------------------------------------------------- +-- Parser +---------------------------------------------------------------------- + +ctok c = (try(spaces >> char c) >> spaces) +stok s = (try(spaces >> string s) >> spaces) + +goal :: Parser Goal +goal = do stok "?-" + ts <- terms + ctok '.' + return ts + +program :: Parser Program +program = many clause + +clause :: Parser Clause +clause = do t <- term + body <- option [] + (stok ":-" >> terms) + ctok '.' + return (t, body) + +term :: Parser Term +term = (variable >>= return . Var) + <|> literal + <|> list + +terms :: Parser Terms +terms = sepBy1 term (ctok ',') + +literal :: Parser Term +literal = do id <- ident + option (Comp id []) + (parens terms >>= return . Comp id) + +parens :: Parser p -> Parser p +parens p = between (ctok '(') (ctok ')') p + +list :: Parser Term +list = between (ctok '[') (ctok ']') + (option emptyListTerm listTerms) + +listTerms = + do heads <- terms + tail <- option emptyListTerm + (ctok '|' >> term) + return (foldr cons tail heads) + +emptyListTerm = Comp "[]" [] + +cons h t = Comp "." [h,t] + +ident :: Parser Ident +ident = (do c <- lower + cs <- many (alphaNum <|> char '_') + return (c:cs)) "identifier" + +variable :: Parser Variable +variable = (do c <- upper <|> char '_' + cs <- many (alphaNum <|> char '_') + return (c:cs)) "variable" + + +---------------------------------------------------------------------- +-- Interpreter +---------------------------------------------------------------------- + +type Unifier = [(Variable, Term)] + +occur :: Variable -> Term -> Bool +occur v (Var x) = v == x +occur v (Comp _ ms) = any (occur v) ms + +subs :: Unifier -> Term -> Term +subs u t@(Var x) = maybe t id (lookup x u) +subs u (Comp n ts) = Comp n (map (subs u) ts) + +unify :: Term -> Term -> Maybe Unifier +unify (Var x) (Var y) = if x < y then return [(y, Var x)] + else return [(x, Var y)] +unify (Var x) t | not(x `occur` t) = return [(x, t)] +unify t v@(Var _) = unify v t +unify (Comp m ms) (Comp n ns) | m == n = unifyList ms ns +unify _ _ = Nothing + +unifyList (t : ts) (r : rs) = + do u1 <- unify t r + u2 <- unifyList (map (subs u1) ts) (map (subs u1) rs) + return $ u1 ++ u2 +unifyList [] [] = Just [] +unifyList _ _ = Nothing + +variables ts = nub $ varsList ts + where vars (Var x) = [x] + vars (Comp _ ts) = varsList ts + varsList ts = [ v | t <- ts, v <- vars t] + +data TreeState = TS {next :: Int} + +nextVar x = do st <- get + let n = next st + put $ st{next = n+1} + return $ "_" ++ show n ++ "_" ++ x + +freshSub vs = + do sub <- mapM freshVar vs + return $ sub + where freshVar v = do v' <- nextVar v + return $ (v, Var v') + +fresh (head, body) = + do let vars = variables(head:body) + sub <- freshSub vars + return (subs sub head, map (subs sub) body) + +freshen bound (tc, tb) = (subs sub tc, map (subs sub) tb) + where vars = variables(tc : tb) + sub = [ (v, Var $ nextVar 0 v) | v <- vars, v `notElem` bound] + nextVar i v = let v' = "_" ++ show i ++ "_" ++ v in + if v' `elem` bound then nextVar (i+1) v + else v' + +data SearchTree = Solution [(Variable, Term)] + | Node Goal [SearchTree] + deriving (Eq, Show, Read) + +solve :: Program -> Goal -> [SearchTree] +solve _ [Comp "_report" args] = return $ Solution sol + where sol = map (\ (Comp "=" [Comp v [], t]) -> (v, t)) args +solve prog g@(t1 : ts) = return $ Node g trees + where treesC = do c <- prog + let (tc, tsc) = freshen (variables g) c + case unify tc t1 of + Just u -> do + let g' = map (subs u) $ tsc ++ ts + solve prog g' + Nothing -> [] + trees = treesC + +{- Failed attempt at using StateT monad transformer + +-- Back-Tracking-State +type BTS a = StateT TreeState [] a + +solve :: Program -> Goal -> BTS SearchTree +solve _ [Comp "_report" args] = return $ Solution sol + where sol = map (\ (Comp "=" [Comp v [], t]) -> (v, t)) args +solve prog g@(t1 : ts) = + do c <- lift prog + (tc, tsc) <- fresh c + case unify tc t1 of + Just u -> do + let g' = map (subs u) $ tsc ++ ts + t <- solve prog g' + return $ Node g' [t] + Nothing -> lift [] + +makeTree prog goal = Node goal trees + where trees = evalStateT (solve prog goal) initialState + initialState = TS 0 +-} + +makeTopTree prog goal = Node goal $ solve prog reportGoal + where reportVars = map (\ v -> Comp "=" [Comp v [], Var v]) vars + vars = variables goal + reportGoal = goal ++ [Comp "_report" reportVars] + + + +testSibling = + do Right p <- parseFromFile program "siblings.pl" + let Right g = parse goal "" "?- sibling(homer, X)." + return $ makeTopTree p g + +testNats = + do Right p <- parseFromFile program "nats.pl" + let Right g = parse goal "" "?- natlist(X)." + return $ makeTopTree p g + +-- Depth first +dfs (Solution sols) = [sols] +dfs (Node g st) = [ s | t <- st, s <- dfs t] + +-- Breath first +bfs t = trav [t] + where trav [] = [] + trav ((Solution x) : q) = x : trav q + trav ((Node _ st) : q) = trav (q ++ st) +