format
This commit is contained in:
parent
902fb4e0b5
commit
8dc5cd3c17
@ -1,18 +1,18 @@
|
|||||||
{-# LANGUAGE MultilineStrings #-}
|
{-# LANGUAGE MultilineStrings #-}
|
||||||
|
|
||||||
module Datalog.Parser
|
module Datalog.Parser (
|
||||||
( parseTerm
|
parseTerm,
|
||||||
, parseAtom
|
parseAtom,
|
||||||
, parseRule
|
parseRule,
|
||||||
, parseQuery
|
parseQuery,
|
||||||
, parseProgram
|
parseProgram,
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
|
|
||||||
import Datalog.Syntax
|
|
||||||
import Data.Text (Text)
|
import Data.Text (Text)
|
||||||
import Data.Text qualified as T
|
import Data.Text qualified as T
|
||||||
import Data.Void (Void)
|
import Data.Void (Void)
|
||||||
|
import Datalog.Syntax
|
||||||
import Text.Megaparsec
|
import Text.Megaparsec
|
||||||
import Text.Megaparsec.Char
|
import Text.Megaparsec.Char
|
||||||
import Text.Megaparsec.Char.Lexer qualified as L
|
import Text.Megaparsec.Char.Lexer qualified as L
|
||||||
@ -27,10 +27,11 @@ symbol :: (MonadParsec e Text m) => Text -> m Text
|
|||||||
symbol = L.symbol whitespace
|
symbol = L.symbol whitespace
|
||||||
|
|
||||||
whitespace :: (MonadParsec e Text m) => m ()
|
whitespace :: (MonadParsec e Text m) => m ()
|
||||||
whitespace = L.space
|
whitespace =
|
||||||
space1
|
L.space
|
||||||
(L.skipLineComment "--")
|
space1
|
||||||
(L.skipBlockComment "{-" "-}")
|
(L.skipLineComment "--")
|
||||||
|
(L.skipBlockComment "{-" "-}")
|
||||||
|
|
||||||
parens :: (MonadParsec e Text m) => m a -> m a
|
parens :: (MonadParsec e Text m) => m a -> m a
|
||||||
parens = between (symbol "(") (symbol ")")
|
parens = between (symbol "(") (symbol ")")
|
||||||
@ -50,30 +51,31 @@ parseTerm = parseVar <|> parseCon
|
|||||||
|
|
||||||
parseAtom :: Parser Atom
|
parseAtom :: Parser Atom
|
||||||
parseAtom = do
|
parseAtom = do
|
||||||
rel <- RelId . T.pack <$> lexeme (liftA2 (:) lowerChar (many alphaNumChar))
|
rel <- RelId . T.pack <$> lexeme (liftA2 (:) lowerChar (many alphaNumChar))
|
||||||
args <- parens (parseTerm `sepBy` comma)
|
args <- parens (parseTerm `sepBy` comma)
|
||||||
return (Atom () rel args)
|
return (Atom () rel args)
|
||||||
|
|
||||||
parseQuery :: Parser [Atom]
|
parseQuery :: Parser [Atom]
|
||||||
parseQuery = parseAtom `sepBy` comma
|
parseQuery = parseAtom `sepBy` comma
|
||||||
|
|
||||||
parseFact :: Parser Rule
|
parseFact :: Parser Rule
|
||||||
parseFact = do
|
parseFact = do
|
||||||
headAtom <- parseAtom
|
headAtom <- parseAtom
|
||||||
period
|
period
|
||||||
return (Rule () headAtom [])
|
return (Rule () headAtom [])
|
||||||
|
|
||||||
parseRule :: Parser Rule
|
parseRule :: Parser Rule
|
||||||
parseRule = try parseFact <|> do
|
parseRule =
|
||||||
headAtom <- parseAtom <* symbol ":-"
|
try parseFact <|> do
|
||||||
bodyAtoms <- parseQuery
|
headAtom <- parseAtom <* symbol ":-"
|
||||||
period
|
bodyAtoms <- parseQuery
|
||||||
return (Rule () headAtom bodyAtoms)
|
period
|
||||||
|
return (Rule () headAtom bodyAtoms)
|
||||||
|
|
||||||
parseProgram :: Parser Program
|
parseProgram :: Parser Program
|
||||||
parseProgram = Program () <$> many parseRule
|
parseProgram = Program () <$> many parseRule
|
||||||
|
|
||||||
annotateSrcLoc :: Functor f => Parser (f a) -> Parser (f SrcLoc)
|
annotateSrcLoc :: (Functor f) => Parser (f a) -> Parser (f SrcLoc)
|
||||||
annotateSrcLoc p = do
|
annotateSrcLoc p = do
|
||||||
s <- getSourcePos
|
s <- getSourcePos
|
||||||
res <- p
|
res <- p
|
||||||
@ -81,24 +83,26 @@ annotateSrcLoc p = do
|
|||||||
pure (SrcLoc s f <$ res)
|
pure (SrcLoc s f <$ res)
|
||||||
|
|
||||||
data SrcLoc = SrcLoc
|
data SrcLoc = SrcLoc
|
||||||
{ start :: SourcePos
|
{ start :: SourcePos
|
||||||
, end :: SourcePos
|
, end :: SourcePos
|
||||||
} deriving Show
|
}
|
||||||
|
deriving (Show)
|
||||||
|
|
||||||
test = do
|
test = do
|
||||||
let r = runParser parseProgram "???" prog
|
let r = runParser parseProgram "???" prog
|
||||||
pPrint @IO r
|
pPrint @IO r
|
||||||
|
|
||||||
prog = """
|
prog =
|
||||||
odd(X,Y) :- r(X,Y).
|
"""
|
||||||
odd(X,Y) :- even(X,Z), r(Z,Y).
|
odd(X,Y) :- r(X,Y).
|
||||||
even(X,Y) :- odd(X,Z), r(Z,Y).
|
odd(X,Y) :- even(X,Z), r(Z,Y).
|
||||||
|
even(X,Y) :- odd(X,Z), r(Z,Y).
|
||||||
|
|
||||||
r(0,1).
|
r(0,1).
|
||||||
r(1,2).
|
r(1,2).
|
||||||
r(2,3).
|
r(2,3).
|
||||||
r(3,4).
|
r(3,4).
|
||||||
r(4,5).
|
r(4,5).
|
||||||
|
|
||||||
r(X,Y) :- r(Y,X).
|
r(X,Y) :- r(Y,X).
|
||||||
"""
|
"""
|
||||||
|
|||||||
@ -3,23 +3,23 @@
|
|||||||
module Datalog.Syntax where
|
module Datalog.Syntax where
|
||||||
|
|
||||||
import Data.Char (isUpper)
|
import Data.Char (isUpper)
|
||||||
|
import Data.Set (Set)
|
||||||
|
import Data.Set qualified as Set
|
||||||
import Data.Text (Text)
|
import Data.Text (Text)
|
||||||
import Data.Text qualified as T
|
import Data.Text qualified as T
|
||||||
import Data.Set qualified as Set
|
|
||||||
import Data.Set (Set)
|
|
||||||
|
|
||||||
newtype ConId = ConId Text
|
newtype ConId = ConId Text
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
newtype VarId = VarId Text
|
newtype VarId = VarId Text
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
newtype RelId = RelId Text
|
newtype RelId = RelId Text
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
type Term = Term' ()
|
type Term = Term' ()
|
||||||
data Term' a = Con a ConId | Var a VarId
|
data Term' a = Con a ConId | Var a VarId
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
con :: Text -> Term
|
con :: Text -> Term
|
||||||
con = Con () . ConId
|
con = Con () . ConId
|
||||||
@ -32,64 +32,64 @@ term t = if not (T.null t) && isUpper (T.head t) then var t else con t
|
|||||||
|
|
||||||
type Atom = Atom' ()
|
type Atom = Atom' ()
|
||||||
data Atom' a = Atom a RelId [Term' a]
|
data Atom' a = Atom a RelId [Term' a]
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
atom :: Text -> [Text] -> Atom
|
atom :: Text -> [Text] -> Atom
|
||||||
atom relName args = Atom () (RelId relName) (map term args)
|
atom relName args = Atom () (RelId relName) (map term args)
|
||||||
|
|
||||||
type Rule = Rule' ()
|
type Rule = Rule' ()
|
||||||
data Rule' a = Rule a (Atom' a) [Atom' a]
|
data Rule' a = Rule a (Atom' a) [Atom' a]
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
{-# COMPLETE (:-) #-}
|
{-# COMPLETE (:-) #-}
|
||||||
pattern (:-) :: Atom' a -> [Atom' a] -> Rule' a
|
pattern (:-) :: Atom' a -> [Atom' a] -> Rule' a
|
||||||
pattern a :- b <- Rule _ a b
|
pattern a :- b <- Rule _ a b
|
||||||
|
|
||||||
type Program = Program' ()
|
type Program = Program' ()
|
||||||
data Program' a = Program a [Rule' a]
|
data Program' a = Program a [Rule' a]
|
||||||
deriving (Eq, Ord, Show)
|
deriving (Eq, Ord, Show)
|
||||||
|
|
||||||
class HasConstants a where
|
class HasConstants a where
|
||||||
constants :: a -> Set ConId
|
constants :: a -> Set ConId
|
||||||
|
|
||||||
instance HasConstants (Term' a) where
|
instance HasConstants (Term' a) where
|
||||||
constants t = case t of
|
constants t = case t of
|
||||||
Con _ x -> Set.singleton x
|
Con _ x -> Set.singleton x
|
||||||
Var _ _ -> Set.empty
|
Var _ _ -> Set.empty
|
||||||
|
|
||||||
instance HasConstants a => HasConstants [a] where
|
instance (HasConstants a) => HasConstants [a] where
|
||||||
constants xs = Set.unions (map constants xs)
|
constants xs = Set.unions (map constants xs)
|
||||||
|
|
||||||
instance HasConstants (Atom' a) where
|
instance HasConstants (Atom' a) where
|
||||||
constants (Atom _ _ ts) = constants ts
|
constants (Atom _ _ ts) = constants ts
|
||||||
|
|
||||||
instance HasConstants (Rule' a) where
|
instance HasConstants (Rule' a) where
|
||||||
constants (h :- b) = Set.union (constants h) (constants b)
|
constants (h :- b) = Set.union (constants h) (constants b)
|
||||||
|
|
||||||
instance HasConstants (Program' a) where
|
instance HasConstants (Program' a) where
|
||||||
constants (Program _ rs) = constants rs
|
constants (Program _ rs) = constants rs
|
||||||
|
|
||||||
class Pretty t where
|
class Pretty t where
|
||||||
pretty :: t -> Text
|
pretty :: t -> Text
|
||||||
|
|
||||||
instance Pretty ConId where
|
instance Pretty ConId where
|
||||||
pretty (ConId t) = t
|
pretty (ConId t) = t
|
||||||
|
|
||||||
instance Pretty VarId where
|
instance Pretty VarId where
|
||||||
pretty (VarId t) = t
|
pretty (VarId t) = t
|
||||||
|
|
||||||
instance Pretty RelId where
|
instance Pretty RelId where
|
||||||
pretty (RelId t) = t
|
pretty (RelId t) = t
|
||||||
|
|
||||||
instance Pretty Term where
|
instance Pretty Term where
|
||||||
pretty (Con () conId) = pretty conId
|
pretty (Con () conId) = pretty conId
|
||||||
pretty (Var () varId) = pretty varId
|
pretty (Var () varId) = pretty varId
|
||||||
|
|
||||||
instance Pretty Atom where
|
instance Pretty Atom where
|
||||||
pretty (Atom () relId terms) = pretty relId <> "(" <> T.intercalate "," (map pretty terms) <> ")"
|
pretty (Atom () relId terms) = pretty relId <> "(" <> T.intercalate "," (map pretty terms) <> ")"
|
||||||
|
|
||||||
instance Pretty Rule where
|
instance Pretty Rule where
|
||||||
pretty (h :- []) = pretty h <> "."
|
pretty (h :- []) = pretty h <> "."
|
||||||
pretty (h :- ts) = pretty h <> " :- " <> T.intercalate ", " (map pretty ts) <> "."
|
pretty (h :- ts) = pretty h <> " :- " <> T.intercalate ", " (map pretty ts) <> "."
|
||||||
|
|
||||||
instance Pretty Program where
|
instance Pretty Program where
|
||||||
pretty (Program () rs) = T.unlines (map pretty rs)
|
pretty (Program () rs) = T.unlines (map pretty rs)
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user