Commit 0ee4b41e authored by Paul Ogris's avatar Paul Ogris
Browse files

Remove choices that are guarded by an #instance

Since those variables are going to be assumptions, we do not want them
to be derived.
parent ea50a6d0
......@@ -7,6 +7,8 @@ module Language.LARS
, Head(..)
, BodyElement(..)
, SignedAtom(..)
, Signature(..)
, matchSignature
,
-- * Pretty Printing
......@@ -25,6 +27,7 @@ module Language.LARS
, head_
, bodyElement
, program
, sig
)
where
......@@ -42,15 +45,32 @@ import Data.List.NonEmpty ( NonEmpty
, fromList
)
import qualified Data.Text as T
import qualified Text.Megaparsec.Char as P
import qualified Text.PrettyPrint.Leijen.Text as PP
import qualified Text.Megaparsec.Char.Lexer as L
newtype Statement = StmtRule Rule
data Statement
= StmtRule Rule
| StmtInstance Signature
deriving (Eq, Show, Ord, Read)
instance Pretty Statement where
pretty (StmtRule r) = PP.pretty r
pretty (StmtInstance s) = "#instance" <+> PP.pretty s <> PP.dot
data Signature = Signature Text Int
deriving (Eq, Show, Ord, Read)
matchSignature :: Atom -> Signature -> Bool
matchSignature a (Signature k 0) = a == k
matchSignature a (Signature k n) =
let (pre, args) = T.breakOn "(" a
commas = T.length $ T.filter (== ',') args
in pre == k && commas == n - 1
instance Pretty Signature where
pretty (Signature t i) = PP.textStrict t <> "/" <> PP.pretty i
type Atom = Text
......@@ -191,6 +211,12 @@ openBrace = symbol "{"
closeBrace :: Parser Text
closeBrace = symbol "}"
slash :: Parser Text
slash = symbol "/"
instanceDirective :: Parser Text
instanceDirective = symbol "#instance"
signedAtom :: Parser SignedAtom
signedAtom = try (negation *> (Negative <$> atom)) <|> (Positive <$> atom)
......@@ -205,7 +231,15 @@ relation = lexeme $ do
pure $ a <> b
stmt :: Parser Statement
stmt = StmtRule <$> rule
stmt = (StmtInstance <$> inst) <|> (StmtRule <$> rule)
where inst = do
_ <- instanceDirective
s <- sig
_ <- dot
pure s
sig :: Parser Signature
sig = Signature <$> takeWhileP Nothing (/= '/') <*> (slash *> L.decimal)
program :: Parser [Statement]
program = some stmt
......@@ -3,9 +3,11 @@ module Relax where
import Language.LARS
import Data.Maybe ( mapMaybe )
import Data.Foldable ( toList )
import Control.Monad ( guard )
relax :: [Statement] -> [Statement]
relax = map normalRules . concatMap splitChoices . filter (not . isConstraint)
relax stmts =
map normalRules . concatMap splitChoices . filter (not . isConstraint) $ stmts
where
normalRules (StmtRule (Rule h@HeadAtom{} bs)) =
StmtRule (Rule h (mapMaybe removeNegation bs))
......@@ -14,13 +16,21 @@ relax = map normalRules . concatMap splitChoices . filter (not . isConstraint)
splitChoices (StmtRule (Rule (HeadChoice _ hs cs _) bs)) = map StmtRule $ do
h <- toList hs
let bs' = map (BodyAtom . Positive) cs <> bs
guard $ all (not . matchSignature h) instances
pure $ Rule (HeadAtom h) bs'
splitChoices x = [x]
isConstraint (StmtRule (Rule HeadFalse _)) = True
isConstraint _ = False
isConstraint _ = False
instances = instanceSigs stmts
removeNegation :: BodyElement -> Maybe BodyElement
removeNegation (BodyAtom (Negative _)) = Nothing
removeNegation (BodyAtom (Positive x)) = Just (BodyAtom (Positive x))
removeNegation (BodyRelation r ) = Just (BodyRelation r)
removeNegation (BodyAtom (Negative _)) = Nothing
removeNegation (BodyAtom (Positive x)) = Just (BodyAtom (Positive x))
removeNegation (BodyRelation r ) = Just (BodyRelation r)
instanceSigs :: [Statement] -> [Signature]
instanceSigs [] = []
instanceSigs (StmtInstance s : xs) = s : instanceSigs xs
instanceSigs (_ : xs) = instanceSigs xs
1 { a(X) : b(X) } 1 :- choice.
choice.
b(1..5).
#instance a/1.
......@@ -15,6 +15,20 @@ spec :: Spec
spec = parallel $ do
describe "LARS Pretty Printing" pprint
describe "LARS Parsing" parser
describe "Functions" funs
funs :: Spec
funs = describe "matchSignature" $ do
it "Matches foo/0 and foo" $
matchSignature "foo" (Signature "foo" 0) `shouldBe` True
it "Matches foo/1 and foo(A)" $
matchSignature "foo(A)" (Signature "foo" 1) `shouldBe` True
it "Does not match foo/2 and foo(A)" $
matchSignature "foo(A)" (Signature "foo" 2) `shouldBe` False
it "Does not match foo/0 and foo(a,b)" $
matchSignature "foo(a,b)" (Signature "foo" 0) `shouldBe` False
it "Matches quux_bar/3 and quux_bar(1,2,X)" $
matchSignature "quux_bar(1,2,X)" (Signature "quux_bar" 3) `shouldBe` True
pprint :: Spec
pprint = parallel $ do
......@@ -67,6 +81,12 @@ pprint = parallel $ do
it "pretty prints constraints"
$ prettyOneLine (Rule HeadFalse [BodyAtom (Positive "a")])
`shouldBe` ":- a."
it "pretty prints signatures"
$ prettyOneLine (Signature "foo" 3)
`shouldBe` "foo/3"
it "pretty prints instance statements"
$ prettyOneLine (StmtInstance (Signature "quux" 2))
`shouldBe` "#instance quux/2."
parser :: Spec
parser = parallel $ do
......@@ -115,3 +135,9 @@ parser = parallel $ do
it "parses aggregates"
$ parse bodyElement "" "#count { a(X) : b(X) }"
`shouldParse` BodyRelation "#count { a(X) : b(X) }"
it "parses signatures" $ parse sig "" "foo/3" `shouldParse` Signature
"foo"
3
it "parses instance directives"
$ parse stmt "" "#instance someSig/3."
`shouldParse` StmtInstance (Signature "someSig" 3)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment