Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 36 additions & 5 deletions core/bench/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,13 @@ main :: IO ()
main = defaultMain benchmarks

benchmarks :: [Benchmark]
benchmarks = [ bgroup "clique" [clique n | n <- [5, 10, 25, 40]]
, bgroup "line" [line n | n <- [5, 10, 25, 40]]
, bgroup "loop" [loop n | n <- [50, 100, 500, 1000]]
, bgroup "tight" [tight n | n <- [50, 100, 500, 1000]]
, bgroup "parse" [parse n | n <- [50, 100, 500, 1000]]
benchmarks = [ bgroup "clique" [clique n | n <- [5, 10, 25, 40]]
, bgroup "cliqueText" [cliqueText n | n <- [5, 10, 25, 40]]
, bgroup "line" [line n | n <- [5, 10, 25, 40]]
, bgroup "lineText" [lineText n | n <- [5, 10, 25, 40]]
, bgroup "loop" [loop n | n <- [50, 100, 500, 1000]]
, bgroup "tight" [tight n | n <- [50, 100, 500, 1000]]
, bgroup "parse" [parse n | n <- [50, 100, 500, 1000]]
]

-- | Generate a complete graph of size @n@ and try to find a path from the first node to the last.
Expand Down Expand Up @@ -58,6 +60,21 @@ clique n = do
let Right cfg = pdpConfigRules mempty path
newHandle cfg {maxDepth = 4000}

cliqueText :: Int -> Benchmark
cliqueText n = do
let path = [rls| path(?x, ?y) :- application says edge(?x, ?y).
path(?x, ?z) :- path(?x, ?y), path(?y, ?z). |]
edges = [lit "edge" [val . pack $ show x, val . pack $ show y]
| x <- [1..n]
, y <- [1..n]]
go hdl = bench (show n) $ whnfIO $ do
res <- checkQuery hdl edges "path" [val $ pack "1", val . pack $ show n]
either (error . show) (bool (error "no path found") (pure True)) res

flip env go $ do
let Right cfg = pdpConfigRules mempty path
newHandle cfg {maxDepth = 4000}

-- | Generates a linear sequence of @n@ facts and tries to find a path from the first node to the
-- last. It uses a cons-list shaped @path@ rule. The @application@ assertion looks like this:
--
Expand All @@ -81,6 +98,20 @@ line n = do
let Right cfg = pdpConfigRules mempty path
newHandle cfg {maxDepth = 4000}

lineText :: Int -> Benchmark
lineText n = do
let path = [rls| path(?x, ?y) :- application says edge(?x, ?y).
path(?x, ?z) :- application says edge(?x, ?y), path(?y, ?z). |]
edges = [lit "edge" [val . pack $ show x, val . pack $ show y]
| (x, y) <- zip [1..pred n] [2..n]]
go hdl = bench (show n) $ whnfIO $ do
res <- checkQuery hdl edges "path" [val $ pack "1", val . pack $ show n]
either (error . show) (bool (error "no path found") (pure True)) res

flip env go $ do
let Right cfg = pdpConfigRules mempty path
newHandle cfg {maxDepth = 4000}

-- | Generates a loop of five rules (@e@ implies @d@ implies @c@ implies @b@ implies @a@ implies
-- @e@), each of arity 4 (so that the benchmark exercises the unification code), and then runs a
-- query with @n@ fuel.
Expand Down
1 change: 1 addition & 0 deletions core/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ library:
- deepseq
- filepath
- hashable
- intern
- megaparsec
- mtl
- qq-literals
Expand Down
2 changes: 1 addition & 1 deletion core/src/Language/Avaleryar/ModeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ data ModeError
| FVModeRestricted RawVar
| FVInAssertionPosition RawVar
| FVInRuleHead RawVar
deriving (Eq, Ord, Read, Show)
deriving (Eq, Ord, Show)

instance Pretty ModeError where
pretty (UnboundNativeAssertion assn) = "unbound native assertion: " <> squotes (pretty assn)
Expand Down
2 changes: 1 addition & 1 deletion core/src/Language/Avaleryar/PDP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ data PDPError
| VarInQueryResults TextVar
| ParseError String
| SubmitError SubmitError
deriving (Eq, Ord, Read, Show, Typeable)
deriving (Eq, Ord, Show, Typeable)

instance Exception PDPError

Expand Down
8 changes: 4 additions & 4 deletions core/src/Language/Avaleryar/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Language.Avaleryar.Parser
import Control.Monad (void)
import Data.Bifunctor (first)
import Data.Either (partitionEithers)
import qualified Data.Interned as Interned
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
Expand Down Expand Up @@ -65,9 +66,9 @@ sym = lexeme (T.pack <$> go) <?> "symbol"

value :: Parser Value
value = I <$> L.signed (pure ()) L.decimal
<|> T <$> stringLiteral
<|> T <$> sym -- unquoted symbols
<|> B <$> (string "#t" *> pure True <|> string "#f" *> pure False)
<|> T <$> fmap Interned.intern stringLiteral
<|> T <$> fmap Interned.intern sym -- unquoted symbols
<|> B <$> (string "#t" *> pure True <|> string "#f" *> pure False)

ident :: Parser Text
ident = sym <?> "identifer"
Expand Down Expand Up @@ -183,4 +184,3 @@ qry = qqLiteral queryQQParser 'queryQQParser

fct :: QuasiQuoter
fct = qqLiteral factQQParser 'factQQParser

6 changes: 4 additions & 2 deletions core/src/Language/Avaleryar/Semantics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,8 @@ import Control.Monad.Except
import Control.Monad.State
import Data.Foldable
import qualified Data.HashSet as HashSet
import qualified Data.Interned as Interned
import qualified Data.Interned.Internal.Text as Interned
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
Expand Down Expand Up @@ -349,10 +351,10 @@ compileQuery' :: String -> Query -> Avaleryar (Lit EVar)
compileQuery' assn (Lit (Pred p _) args) = compileQuery assn p args

insertRuleAssertion :: Text -> Map Pred (Lit EVar -> Avaleryar ()) -> RulesDb -> RulesDb
insertRuleAssertion assn rules = RulesDb . Map.insert (T assn) rules . unRulesDb
insertRuleAssertion assn rules = RulesDb . Map.insert (toValue assn) rules . unRulesDb

retractRuleAssertion :: Text -> RulesDb -> RulesDb
retractRuleAssertion assn = RulesDb . Map.delete (T assn) . unRulesDb
retractRuleAssertion assn = RulesDb . Map.delete (toValue assn) . unRulesDb

---------------------

Expand Down
36 changes: 21 additions & 15 deletions core/src/Language/Avaleryar/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -45,11 +45,13 @@ name of the assertion in which @may\/1@ is defined). In brief:

module Language.Avaleryar.Syntax where

import Control.DeepSeq (NFData)
import Control.DeepSeq (NFData(rnf))
import Data.Char (isSpace)
import Data.Function (on)
import Data.Functor.Const (Const(..))
import Data.Hashable (Hashable(hashWithSalt))
import qualified Data.Interned as Interned
import qualified Data.Interned.Internal.Text as Interned
import Data.Map (Map)
import Data.String
import Data.Text (Text)
Expand All @@ -62,11 +64,15 @@ import Text.PrettyPrint.Leijen.Text

data Value
= I Int
| T Text
| T Interned.InternedText
| B Bool
deriving (Eq, Ord, Read, Show, Generic)
deriving (Eq, Ord, Show, Generic)

instance NFData Value where
rnf (I i) = rnf i
rnf (T t) = rnf (Interned.unintern t)
rnf (B b) = rnf b

instance NFData Value
instance Hashable Value

instance IsString Value where
Expand All @@ -75,12 +81,12 @@ instance IsString Value where
instance Pretty Value where
pretty (I n) = pretty n
pretty (B b) = if b then "#t" else "#f"
pretty (T t) = if T.any isSpace t
then pretty (show t) -- want the quotes/escaping
else pretty t -- display as a symbol
pretty (T t) = if T.any isSpace (Interned.unintern t)
then pretty (show $ Interned.unintern t) -- want the quotes/escaping
else pretty (Interned.unintern t) -- display as a symbol

-- | A predicate is identified by its name and arity (i.e., the predicate of the literal @foo(bar, ?baz)@ is @foo/2@)
data Pred = Pred Text Int deriving (Eq, Ord, Read, Show, Generic)
data Pred = Pred Text Int deriving (Eq, Ord, Show, Generic)

instance NFData Pred
instance Hashable Pred
Expand All @@ -92,7 +98,7 @@ instance Pretty Pred where
-- provide a bit of safety by keeping us from crossing various streams (e.g., separating runtime
-- unification variables from raw variables straight out of the parser helps avoid a bit of unwanted
-- variable capture).
data Term v = Val Value | Var v deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
data Term v = Val Value | Var v deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (Term v)
instance Hashable v => Hashable (Term v)
Expand All @@ -103,7 +109,7 @@ instance Pretty v => Pretty (Term v) where

-- | A literal is identified by a 'Pred' and a list of 'Term's, where the arity in the 'Pred' is the
-- same as the length of the list of 'Term's in the argument list.
data Lit v = Lit Pred [Term v] deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
data Lit v = Lit Pred [Term v] deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (Lit v)
instance Hashable v => Hashable (Lit v)
Expand All @@ -117,7 +123,7 @@ lit pn as = Lit (Pred pn (length as)) as

-- | A reference to an assertion may either statically denote a native assertion or appear as a
-- 'Term'.
data ARef v = ARNative Text | ARTerm (Term v) | ARCurrent deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
data ARef v = ARNative Text | ARTerm (Term v) | ARCurrent deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (ARef v)
instance Hashable v => Hashable (ARef v)
Expand All @@ -136,7 +142,7 @@ prettyAssertion assn ps = pretty assn
-- When no assertion appears in the concrete syntax, the parser inserts a reference to the assertion
-- currently being parsed.
data BodyLit v = Says (ARef v) (Lit v)
deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (BodyLit v)
instance Hashable v => Hashable (BodyLit v)
Expand All @@ -146,7 +152,7 @@ instance Pretty v => Pretty (BodyLit v) where

-- | A rule has a head and a body made of 'BodyLit's.
data Rule v = Rule (Lit v) [BodyLit v]
deriving (Eq, Ord, Read, Show, Functor, Foldable, Traversable, Generic)
deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance NFData v => NFData (Rule v)
instance Hashable v => Hashable (Rule v)
Expand Down Expand Up @@ -265,8 +271,8 @@ instance Valuable Value where
fromValue = Just

instance Valuable Text where
toValue = T
fromValue (T a) = Just a
toValue = T . Interned.intern
fromValue (T a) = Just (Interned.unintern a)
fromValue _ = Nothing

instance Valuable Int where
Expand Down
9 changes: 3 additions & 6 deletions core/src/Language/Avaleryar/Testing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ module Language.Avaleryar.Testing

import Data.Bool (bool)
import Data.Foldable (for_, toList)
import qualified Data.Interned as Interned
import qualified Data.Map as Map
import Data.Text (Text, splitOn)
import Data.Void (vacuous)
Expand Down Expand Up @@ -93,9 +94,9 @@ parseTestCase (Directive (Lit (Pred "test" _) (tn:dbs)) tqs) = do
parseTestCase _ = Nothing

parseDb :: (Text, Text) -> Directive -> Maybe TestDb
parseDb (alias, assn) (Directive (Lit (Pred "db" _) [Val (T dbn)]) fs) | assn == dbn =
parseDb (alias, assn) (Directive (Lit (Pred "db" _) [Val (T dbn)]) fs) | Interned.intern assn == dbn =
Just ([(alias, fmap factToRule fs)], mempty)
parseDb (alias, assn) (Directive (Lit (Pred "native" _) [Val (T dbn)]) fs) | assn == dbn =
parseDb (alias, assn) (Directive (Lit (Pred "native" _) [Val (T dbn)]) fs) | Interned.intern assn == dbn =
Just (mempty, mkNativeDb alias $ factsToNative fs)
parseDb _ _ = Nothing

Expand Down Expand Up @@ -207,7 +208,3 @@ runTestFile conf k tf = do
case parsed of
Left err -> pure (Left err)
Right ts -> Right <$> traverse gatherResults ts