From 37c1307d545a6f4147eb43a1a8e2bccbd487e75d Mon Sep 17 00:00:00 2001 From: Joscha Date: Fri, 11 Dec 2020 16:50:39 +0000 Subject: [PATCH] Implement prolog-style unification --- app/Main.hs | 13 +--- src/Props/Prolog.hs | 154 +++++++++++++++++++++++++++++++++++++------- 2 files changed, 133 insertions(+), 34 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 3eacdac..f7090c2 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,15 +1,4 @@ module Main where -import Data.Void - -import Props.Lambda.Term - -yCombinator :: Term Void String String -yCombinator = Lambda "f" - (App - (Lambda "x" (App (Var 1) (App (Var 0) (Var 0)))) - (Lambda "x" (App (Var 1) (App (Var 0) (Var 0)))) - ) - main :: IO () -main = print yCombinator +main = putStrLn "Hello world!" diff --git a/src/Props/Prolog.hs b/src/Props/Prolog.hs index 80faa2b..3ca4234 100644 --- a/src/Props/Prolog.hs +++ b/src/Props/Prolog.hs @@ -1,33 +1,143 @@ module Props.Prolog where import Control.Monad +import Data.Foldable -import qualified Data.Map as Map +import Control.Monad.Trans.Class +import Control.Monad.Trans.State +import qualified Data.Map as Map +import qualified Data.Set as Set -data Term - = Variable String - | Statement String [Term] +data Term a + = Var a + | Stat String [Term a] deriving (Show) -type VarMap = Map.Map String Term +instance Functor Term where + fmap f (Var a) = Var $ f a + fmap f (Stat name args) = Stat name $ fmap (fmap f) args -lookupTerm :: VarMap -> Term -> Term -lookupTerm _ t@(Statement _ _) = t -lookupTerm env t@(Variable s) = case env Map.!? s of - Nothing -> t - Just t' -> lookupTerm env t' +instance Foldable Term where + foldMap f (Var a) = f a + foldMap f (Stat _ args) = foldMap (foldMap f) args -unifyStatements :: String -> [Term] -> String -> [Term] -> VarMap -> [VarMap] -unifyStatements a as b bs env = do - guard $ a == b - guard $ length as == length bs - foldr (>=>) pure (zipWith unify as bs) env +instance Traversable Term where + traverse f (Var a) = Var <$> f a + traverse f (Stat name args) = Stat name <$> traverse (traverse f) args -unify :: Term -> Term -> VarMap -> [VarMap] -unify t1 t2 env = case (lookupTerm env t1, lookupTerm env t2) of - (Statement a as, Statement b bs) -> unifyStatements a as b bs env - (Variable a, b) -> [Map.insert a b env] - (a, Variable b) -> [Map.insert b a env] +data Def a = Def String [Term a] [Term a] + deriving (Show) -unify' :: Term -> Term -> [VarMap] -unify' t1 t2 = unify t1 t2 Map.empty +instance Functor Def where + fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms) + +instance Foldable Def where + foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms + +instance Traversable Def where + traverse f (Def dName dArgs dTerms) + = Def dName + <$> traverse (traverse f) dArgs + <*> traverse (traverse f) dTerms + +data Context = Context + { cDb :: [Def String] + , cVarIdx :: Int + , cVars :: Map.Map Int Int + , cTerms :: Map.Map Int (String, [Term Int]) + } deriving (Show) + +newContext :: [Def String] -> Context +newContext db = Context db 0 Map.empty Map.empty + +learnVar :: Int -> Int -> UniM () +learnVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c} + +learnTerm :: Int -> String -> [Term Int] -> UniM () +learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c} + +-- | Look up a variable, first in the var map and then the term map. Returns +-- statements unchanged. +-- +-- If this returns a variable, then that variable is unbound. +lookupVar :: Term Int -> UniM (Term Int) +lookupVar t@(Stat _ _) = pure t +lookupVar t@(Var v) = do + c <- get + case cVars c Map.!? v of + Just v' -> lookupVar (Var v') + Nothing -> pure $ case cTerms c Map.!? v of + Nothing -> t + Just (name, args) -> Stat name args + +-- | A simple state monad transformer over the list monad for easy backtracking. +-- Needs to be changed when implementing cuts. +type UniM = StateT Context [] + +-- | A faster version of 'nub'. +fastNub :: (Ord a) => [a] -> [a] +fastNub = Set.toList . Set.fromList + +varMap :: (Foldable a) => a String -> UniM (Map.Map String Int) +varMap a = do + c <- get + let i = cVarIdx c + vars = fastNub $ toList a + vmap = Map.fromList $ zip vars [i..] + put c{cVarIdx = i + Map.size vmap} + pure vmap + +-- | Convert a definition's variables to unique integers that are not already in +-- use in the current context. +understand :: (Functor a, Foldable a) => a String -> UniM (a Int, Map.Map String Int) +understand a = do + vmap <- varMap a + pure (fmap (vmap Map.!) a, vmap) + +satisfy :: Term Int -> UniM () +satisfy (Var _) = undefined +satisfy (Stat name args) = do + c <- get + (Def dName dArgs dTerms, _) <- understand =<< lift (cDb c) + lift $ guard $ name == dName -- Not sure if 'lift' is really necessary + unifyTerms args dArgs + satisfyTerms dTerms + +satisfyTerms :: [Term Int] -> UniM () +satisfyTerms = traverse_ satisfy + +unify :: Term Int -> Term Int -> UniM () +unify t1 t2 = do + t1' <- lookupVar t1 + t2' <- lookupVar t2 + case (t1', t2') of + (Stat name1 args1, Stat name2 args2) -> do + lift $ guard $ name1 == name2 + unifyTerms args1 args2 + (Var v1, Stat name2 args2) -> learnTerm v1 name2 args2 + (Stat name1 args1, Var v2) -> learnTerm v2 name1 args1 + (Var v1, Var v2) -> learnVar v1 v2 -- The order shouldn't really matter + +unifyTerms :: [Term Int] -> [Term Int] -> UniM () +unifyTerms t1 t2 = do + lift $ guard $ length t1 == length t2 + sequenceA_ $ zipWith unify t1 t2 + +run :: Term String -> UniM (Map.Map String (Term Int)) +run t = do + (t2, vmap) <- understand t + satisfy t2 + traverse (lookupVar . Var) vmap + +exampleDb :: [Def String] +exampleDb = + [ Def "food" [Stat "burger" []] [] + , Def "food" [Stat "sandwich" []] [] + , Def "meal" [Var "X"] [Stat "food" [Var "X"]] + ] + +burgerIsMeal :: Term String +burgerIsMeal = Stat "meal" [Stat "burger" []] + +whatIsMeal :: Term String +whatIsMeal = Stat "meal" [Var "X"]