From d90f2c6a2c1f8281bde77374e30742fbbe723091 Mon Sep 17 00:00:00 2001 From: Joscha Date: Sun, 13 Dec 2020 23:23:59 +0000 Subject: [PATCH] Separate out Stat from Term --- src/Propa/Prolog/Debug.hs | 6 +-- src/Propa/Prolog/Display.hs | 28 ++++++------ src/Propa/Prolog/Parse.hs | 33 +++++++------- src/Propa/Prolog/Types.hs | 42 +++++++++++------- src/Propa/Prolog/Unify.hs | 86 ++++++++++++++++++------------------- 5 files changed, 100 insertions(+), 95 deletions(-) diff --git a/src/Propa/Prolog/Debug.hs b/src/Propa/Prolog/Debug.hs index 1814ad7..b9f1971 100644 --- a/src/Propa/Prolog/Debug.hs +++ b/src/Propa/Prolog/Debug.hs @@ -12,7 +12,7 @@ import Propa.Prolog.Parse import Propa.Prolog.Unify parseAndRun :: T.Text -> T.Text -> IO () -parseAndRun dbText termsText = T.putStrLn $ either id id $ do +parseAndRun dbText statsText = T.putStrLn $ either id id $ do db <- parseDb "" dbText - terms <- parseTerms "" termsText - pure $ T.intercalate "\n" $ map displayResult $ run db terms + stats <- parseStats "" statsText + pure $ T.intercalate "\n" $ map displayResult $ run db stats diff --git a/src/Propa/Prolog/Display.hs b/src/Propa/Prolog/Display.hs index acd15b7..79608b6 100644 --- a/src/Propa/Prolog/Display.hs +++ b/src/Propa/Prolog/Display.hs @@ -28,33 +28,33 @@ displayName name , ("\t", "\\t") ] -displayStat :: T.Text -> [Term T.Text] -> T.Text -displayStat name [] = displayName name -displayStat name args +displayStat :: Stat T.Text -> T.Text +displayStat (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b +displayStat (Stat name []) = displayName name +displayStat (Stat name args) = displayName name <> "(" <> T.intercalate ", " (map displayTerm args) <> ")" displayList :: Term T.Text -> T.Text -displayList (Stat "[|]" [a, b]) = "," <> displayTerm a <> displayList b -displayList (Stat "[]" []) = "]" -displayList t = "|" <> displayTerm t <> "]" +displayList (TStat (Stat "[|]" [a, b])) = "," <> displayTerm a <> displayList b +displayList (TStat (Stat "[]" [])) = "]" +displayList t = "|" <> displayTerm t <> "]" displayTerm :: Term T.Text -> T.Text -displayTerm (Var v) = v -displayTerm (Stat "[|]" [a, b]) = "[" <> displayTerm a <> displayList b -displayTerm (Stat name args) = displayStat name args +displayTerm (TVar v) = v +displayTerm (TStat s) = displayStat s displayTerms :: [Term T.Text] -> T.Text displayTerms terms = T.intercalate ",\n" (map displayTerm terms) <> "." displayDef :: Def T.Text -> T.Text -displayDef (Def name args []) = displayStat name args <> "." -displayDef (Def name args terms) - = displayStat name args +displayDef (Def stat []) = displayStat stat <> "." +displayDef (Def stat stats) + = displayStat stat <> " :-\n" - <> T.intercalate ",\n" (map (\t -> " " <> displayTerm t) terms) + <> T.intercalate ",\n" (map (\t -> " " <> displayStat t) stats) <> "." displayDefs :: [Def T.Text] -> T.Text @@ -64,5 +64,5 @@ displayResult :: Map.Map T.Text (Term T.Text) -> T.Text displayResult = T.intercalate "\n" . map (\(k, v) -> k <> " = " <> displayTerm v) - . filter (\(k, v) -> v /= Var k) + . filter (\(k, v) -> v /= TVar k) . Map.assocs diff --git a/src/Propa/Prolog/Parse.hs b/src/Propa/Prolog/Parse.hs index 004b15e..682d24e 100644 --- a/src/Propa/Prolog/Parse.hs +++ b/src/Propa/Prolog/Parse.hs @@ -1,7 +1,7 @@ {-# LANGUAGE OverloadedStrings #-} module Propa.Prolog.Parse - ( parseTerms + ( parseStats , parseDb ) where @@ -53,23 +53,26 @@ pCons = brackets $ do elems <- pTerm `sepBy1` symbol "," void $ symbol "|" rest <- pTerm - pure $ foldr (\a b -> Stat "[|]" [a, b]) rest elems + pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) rest elems pList :: Parser (Term T.Text) pList = do elems <- brackets $ pTerm `sepBy` symbol "," - pure $ foldr (\a b -> Stat "[|]" [a, b]) (Stat "[]" []) elems + pure $ foldr (\a b -> TStat $ Stat "[|]" [a, b]) (TStat $ Stat "[]" []) elems -pStat :: Parser (T.Text, [Term T.Text]) +pStat :: Parser (Stat T.Text) pStat = do name <- pName terms <- parens (pTerm `sepBy1` symbol ",") <|> pure [] - pure (name, terms) + pure $ Stat name terms + +pStats :: Parser [Stat T.Text] +pStats = (pStat `sepBy1` symbol ",") <* symbol "." pTerm :: Parser (Term T.Text) pTerm - = (Var <$> pVarName) - <|> (uncurry Stat <$> pStat) + = (TVar <$> pVarName) + <|> (TStat <$> pStat) <|> try pCons <|> pList <|> parens pExpr @@ -79,18 +82,14 @@ pExpr = makeExprParser pTerm [ [ binary "=" ] ] where - binary name = InfixL $ (\a b -> Stat name [a, b]) <$ symbol name - -pTerms :: Parser [Term T.Text] -pTerms = (pExpr `sepBy1` symbol ",") <* symbol "." + binary name = InfixL $ (\a b -> TStat $ Stat name [a, b]) <$ symbol name pDef :: Parser (Def T.Text) pDef = do - name <- pName - args <- parens (pExpr `sepBy1` symbol ",") <|> pure [] - terms <- (symbol ":-" *> (pExpr `sepBy1` symbol ",")) <|> pure [] + stat <- pStat + stats <- (symbol ":-" *> (pStat `sepBy1` symbol ",")) <|> pure [] void $ symbol "." - pure $ Def name args terms + pure $ Def stat stats pDefs :: Parser [Def T.Text] pDefs = many pDef @@ -102,8 +101,8 @@ parseHelper p path input = first (T.pack . errorBundlePretty) $ parse (space *> p <* eof) path input -parseTerms :: FilePath -> T.Text -> Either T.Text [Term T.Text] -parseTerms = parseHelper pTerms +parseStats :: FilePath -> T.Text -> Either T.Text [Stat T.Text] +parseStats = parseHelper pStats parseDb :: FilePath -> T.Text -> Either T.Text (Db T.Text) parseDb = parseHelper pDefs diff --git a/src/Propa/Prolog/Types.hs b/src/Propa/Prolog/Types.hs index d526509..485f44b 100644 --- a/src/Propa/Prolog/Types.hs +++ b/src/Propa/Prolog/Types.hs @@ -1,41 +1,51 @@ module Propa.Prolog.Types - ( Term(..) + ( Stat(..) + , Term(..) , Def(..) , Db ) where import qualified Data.Text as T +data Stat a = Stat T.Text [Term a] + deriving (Show, Eq) + +instance Functor Stat where + fmap f (Stat name terms) = Stat name $ fmap (fmap f) terms + +instance Foldable Stat where + foldMap f (Stat _ terms) = foldMap (foldMap f) terms + +instance Traversable Stat where + traverse f (Stat name terms) = Stat name <$> traverse (traverse f) terms + data Term a - = Var a - | Stat T.Text [Term a] + = TVar a + | TStat (Stat a) deriving (Show, Eq) instance Functor Term where - fmap f (Var a) = Var $ f a - fmap f (Stat name args) = Stat name $ fmap (fmap f) args + fmap f (TVar a) = TVar $ f a + fmap f (TStat s) = TStat $ fmap f s instance Foldable Term where - foldMap f (Var a) = f a - foldMap f (Stat _ args) = foldMap (foldMap f) args + foldMap f (TVar a) = f a + foldMap f (TStat s) = foldMap f s instance Traversable Term where - traverse f (Var a) = Var <$> f a - traverse f (Stat name args) = Stat name <$> traverse (traverse f) args + traverse f (TVar a) = TVar <$> f a + traverse f (TStat s) = TStat <$> traverse f s -data Def a = Def T.Text [Term a] [Term a] +data Def a = Def (Stat a) [Stat a] deriving (Show) instance Functor Def where - fmap f (Def dName dArgs dTerms) = Def dName (fmap f <$> dArgs) (fmap f <$> dTerms) + fmap f (Def stat stats) = Def (fmap f stat) (fmap f <$> stats) instance Foldable Def where - foldMap f (Def _ dArgs dTerms) = foldMap (foldMap f) dArgs <> foldMap (foldMap f) dTerms + foldMap f (Def stat stats) = foldMap f stat <> foldMap (foldMap f) stats instance Traversable Def where - traverse f (Def dName dArgs dTerms) - = Def dName - <$> traverse (traverse f) dArgs - <*> traverse (traverse f) dTerms + traverse f (Def stat stats) = Def <$> traverse f stat <*> traverse (traverse f) stats type Db a = [Def a] diff --git a/src/Propa/Prolog/Unify.hs b/src/Propa/Prolog/Unify.hs index e16994f..2caae9f 100644 --- a/src/Propa/Prolog/Unify.hs +++ b/src/Propa/Prolog/Unify.hs @@ -2,7 +2,6 @@ module Propa.Prolog.Unify ( run - , runOne ) where import Control.Monad @@ -36,30 +35,30 @@ data Context = Context { cDb :: Db T.Text , cVarIdx :: Int , cVars :: Map.Map Int Int - , cTerms :: Map.Map Int (T.Text, [Term Int]) + , cStats :: Map.Map Int (Stat Int) } deriving (Show) newContext :: [Def T.Text] -> 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} +bindVar :: Int -> Int -> UniM () +bindVar k v = modify $ \c -> c{cVars = Map.insert k v $ cVars c} -learnTerm :: Int -> T.Text -> [Term Int] -> UniM () -learnTerm k name args = modify $ \c -> c{cTerms = Map.insert k (name, args) $ cTerms c} +bindStat :: Int -> Stat Int -> UniM () +bindStat k s = modify $ \c -> c{cStats = Map.insert k s $ cStats c} -- | Look up a variable, first repeatedly in the var map and then the term map. -- Returns statements unchanged. -- -- If this returns a variable, then that variable is not bound. lookupVar :: Term Int -> UniM (Term Int) -lookupVar (Var v) = do +lookupVar (TVar v) = do c <- get let lastV = follow (cVars c) v - pure $ case cTerms c Map.!? lastV of - Nothing -> Var lastV - Just (name, args) -> Stat name args -lookupVar t@(Stat _ _) = pure t + pure $ case cStats c Map.!? lastV of + Nothing -> TVar lastV + Just s -> TStat s +lookupVar t@(TStat _) = pure t -- | A simple state monad transformer over the list monad for easy backtracking. -- Needs to be changed when implementing cuts. @@ -81,33 +80,34 @@ understand a = do vmap <- varMap a pure (fmap (vmap Map.!) a, vmap) -satisfy :: Term Int -> UniM () -satisfy (Var _) = pure () -satisfy (Stat name args) = do +satisfy :: Stat Int -> UniM () +satisfy s = 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 + (Def dStat dStats, _) <- understand =<< lift (cDb c) + unifyStat s dStat + satisfyStats dStats -satisfyTerms :: [Term Int] -> UniM () -satisfyTerms = traverse_ satisfy +satisfyStats :: [Stat Int] -> UniM () +satisfyStats = traverse_ satisfy + +unifyStat :: Stat Int -> Stat Int -> UniM () +unifyStat (Stat name1 args1) (Stat name2 args2) = do + guard $ name1 == name2 + unifyTerms args1 args2 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 + (TStat s1, TStat s2) -> unifyStat s1 s2 + (TVar v, TStat s) -> bindStat v s + (TStat s, TVar v) -> bindStat v s + (TVar v1, TVar v2) -> bindVar v1 v2 -- The order shouldn't really matter unifyTerms :: [Term Int] -> [Term Int] -> UniM () unifyTerms t1 t2 = do - lift $ guard $ length t1 == length t2 + guard $ length t1 == length t2 sequenceA_ $ zipWith unify t1 t2 -- Figuring out how to display the result of the unification @@ -136,30 +136,26 @@ resolveVars :: Term Int -> UniM (Term Int) resolveVars t = do t2 <- lookupVar t case t2 of - (Var v) -> pure $ Var v - (Stat name args) -> do - args2 <- traverse resolveVars args - pure $ Stat name args2 + (TVar v) -> pure $ TVar v + (TStat (Stat name args)) -> TStat . Stat name <$> traverse resolveVars args --- | Helper type so I can resolve variables in multiple terms simultaneously. -newtype Terms a = Terms { unTerms :: [Term a] } +-- | Helper type so I can resolve variables in multiple statements +-- simultaneously. +newtype Stats a = Stats { unStats :: [Stat a] } -instance Functor Terms where - fmap f (Terms ts) = Terms $ fmap (fmap f) ts +instance Functor Stats where + fmap f (Stats ts) = Stats $ fmap (fmap f) ts -instance Foldable Terms where - foldMap f (Terms ts) = foldMap (foldMap f) ts +instance Foldable Stats where + foldMap f (Stats ts) = foldMap (foldMap f) ts -run :: Db T.Text -> [Term T.Text] -> [Map.Map T.Text (Term T.Text)] -run db terms = map fst $ runStateT helper $ newContext db +run :: Db T.Text -> [Stat T.Text] -> [Map.Map T.Text (Term T.Text)] +run db stats = map fst $ runStateT helper $ newContext db where helper = do - (terms2, vmap) <- understand $ Terms terms - satisfyTerms $ unTerms terms2 - tmap <- traverse (resolveVars . Var) vmap + (stats2, vmap) <- understand $ Stats stats + satisfyStats $ unStats stats2 + tmap <- traverse (resolveVars . TVar) vmap c <- get let naming = findVarNaming vmap (cVars c) $ Map.elems tmap pure $ fmap (naming Map.!) <$> tmap - -runOne :: Db T.Text -> Term T.Text -> [Map.Map T.Text (Term T.Text)] -runOne db term = run db [term]