diff --git a/core/bench/Main.hs b/core/bench/Main.hs index 8da6ec1..e93950c 100644 --- a/core/bench/Main.hs +++ b/core/bench/Main.hs @@ -5,6 +5,7 @@ module Main where +import Control.Monad.Except import Criterion.Main import Data.Bool import Data.Text (pack) @@ -55,7 +56,7 @@ clique n = do either (error . show) (bool (error "no path found") (pure True)) res flip env go $ do - let Right cfg = pdpConfigRules mempty path + Right cfg <- runExceptT $ 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 @@ -78,7 +79,7 @@ line n = do either (error . show) (bool (error "no path found") (pure True)) res flip env go $ do - let Right cfg = pdpConfigRules mempty path + Right cfg <- runExceptT $ pdpConfigRules mempty path newHandle cfg {maxDepth = 4000} -- | Generates a loop of five rules (@e@ implies @d@ implies @c@ implies @b@ implies @a@ implies @@ -96,7 +97,7 @@ loop n = do either (error . show) (bool (pure True) (error "loop shouldn't succeed")) res flip env go $ do - let Right cfg = pdpConfigRules mempty rules + Right cfg <- runExceptT $ pdpConfigRules mempty rules newHandle cfg {maxDepth = n} -- | As 'loop', but with arity 0 rules. This should be a better measure of the overhead of the @@ -110,7 +111,7 @@ tight n = do either (error . show) (bool (pure True) (error "tight shouldn't succeed")) res flip env go $ do - let Right cfg = pdpConfigRules mempty rules + Right cfg <- runExceptT $ pdpConfigRules mempty rules newHandle cfg {maxDepth = n} -- | Generates @n@ rules, pretty prints them, then times how long it takes to parse them. The text diff --git a/core/package.yaml b/core/package.yaml index b29def6..47b817d 100644 --- a/core/package.yaml +++ b/core/package.yaml @@ -30,11 +30,11 @@ tests: - hspec - hspec-core - - HUnit - - QuickCheck - containers - directory - filepath + - HUnit + - QuickCheck - text benchmarks: @@ -46,5 +46,6 @@ benchmarks: - avaleryar - criterion - - wl-pprint-text + - mtl - text + - wl-pprint-text diff --git a/core/src/Language/Avaleryar/PDP.hs b/core/src/Language/Avaleryar/PDP.hs index 488ba34..62b23be 100644 --- a/core/src/Language/Avaleryar/PDP.hs +++ b/core/src/Language/Avaleryar/PDP.hs @@ -76,7 +76,7 @@ runPDP' :: PDP a -> PDPConfig -> IO a runPDP' pdp conf = runPDP pdp conf >>= either (error . show) pure runAva :: Avaleryar a -> PDP (AvaResults a) -runAva = runAvaWith id +runAva = runAvaWith pure -- | Run an 'Avaleryar' computation inside a 'PDP', configured according to the latter's -- 'PDPConfig'. The caller is given an opportunity to muck with the 'RulesDb' with which the @@ -86,15 +86,16 @@ runAva = runAvaWith id -- NB: The system assertion from the config is added to the the rule database after the caller's -- mucking function has done its business to ensure that the caller can't sneakily override the -- @system@ assertion with their own. -runAvaWith :: (RulesDb -> RulesDb) -> Avaleryar a -> PDP (AvaResults a) +runAvaWith :: (RulesDb -> IO RulesDb) -> Avaleryar a -> PDP (AvaResults a) runAvaWith f ma = avaResults <$> runDetailedWith f ma -runDetailedWith :: (RulesDb -> RulesDb) -> Avaleryar a -> PDP (DetailedResults a) +runDetailedWith :: (RulesDb -> IO RulesDb) -> Avaleryar a -> PDP (DetailedResults a) runDetailedWith f ma = do PDPConfig {..} <- askConfig -- do 'f' *before* inserting the system assertion, to make sure the caller can't override it! - rdb <- insertRuleAssertion "system" systemAssertion . f <$> getRulesDb - liftIO $ runAvaleryar' maxDepth maxAnswers (Db (f rdb) nativeAssertions) ma + rdb <- (insertRuleAssertion "system" systemAssertion) <$> (liftIO . f =<< getRulesDb) + rdb' <- liftIO $ f rdb + liftIO $ runAvaleryar' maxDepth maxAnswers (Db rdb' nativeAssertions) ma -- is this exactly what I just said not to do ^ ? checkRules :: [Rule RawVar] -> PDP () @@ -122,7 +123,8 @@ submitFile assn path facts = checkSubmit facts >> unsafeSubmitFile assn path unsafeSubmitAssertion :: Text -> [Rule RawVar] -> PDP () unsafeSubmitAssertion assn rules = do checkRules rules - modifyRulesDb $ insertRuleAssertion assn (compileRules assn $ fmap (fmap unRawVar) rules) + compiledRules <- liftIO $ compileRules assn $ fmap (fmap unRawVar) rules + modifyRulesDb $ insertRuleAssertion assn compiledRules -- | TODO: ergonomics, protect "system", etc. @@ -162,8 +164,10 @@ testQuery :: [Fact] -> Query -> PDP () testQuery facts (Lit (Pred p _) as) = queryPretty facts p as -- | Insert an @application@ assertion into a 'RulesDb' providing the given facts. -insertApplicationAssertion :: [Fact] -> RulesDb -> RulesDb -insertApplicationAssertion = insertRuleAssertion "application" . compileRules "application" . fmap factToRule +insertApplicationAssertion :: [Fact] -> RulesDb -> IO RulesDb +insertApplicationAssertion facts ruleDB = do + rules <- compileRules "application" $ fmap factToRule facts + pure $ insertRuleAssertion "application" rules ruleDB nativeModes :: NativeDb -> Map Text (Map Pred ModedLit) nativeModes = fmap (fmap nativeSig) . unNativeDb @@ -176,22 +180,25 @@ stripPathPrefix pfx path = maybe path id $ stripPrefix pfx path -- NB: The given file is parsed as the @system@ assertion regardless of its filename, which is -- almost guaranteed to be what you want. -pdpConfig :: NativeDb -> FilePath -> IO (Either PDPError PDPConfig) -pdpConfig db fp = runExceptT $ do +pdpConfig :: NativeDb -> FilePath -> ExceptT PDPError IO PDPConfig +pdpConfig db fp = do sys <- ExceptT . liftIO . fmap (first ParseError . coerce) $ parseFile fp ExceptT . pure . first ModeError $ modeCheck (nativeModes db) sys - pure $ PDPConfig (compileRules "system" $ fmap (fmap unRawVar) sys) db Nothing 50 10 + rules <- liftIO $ compileRules "system" $ fmap (fmap unRawVar) sys + pure $ PDPConfig rules db Nothing 50 10 -pdpConfigText :: NativeDb -> Text -> Either PDPError PDPConfig +pdpConfigText :: NativeDb -> Text -> ExceptT PDPError IO PDPConfig pdpConfigText db text = do - sys <- first ParseError . coerce $ parseText "system" text - first ModeError $ modeCheck (nativeModes db) sys - pure $ PDPConfig (compileRules "system" $ fmap (fmap unRawVar) sys) db Nothing 50 10 + sys <- liftEither . first ParseError . coerce $ parseText "system" text + liftEither . first ModeError $ modeCheck (nativeModes db) sys + rules <- liftIO $ compileRules "system" $ fmap (fmap unRawVar) sys + pure $ PDPConfig rules db Nothing 50 10 -pdpConfigRules :: NativeDb -> [Rule RawVar] -> Either PDPError PDPConfig +pdpConfigRules :: NativeDb -> [Rule RawVar] -> ExceptT PDPError IO PDPConfig pdpConfigRules db sys = do - first ModeError $ modeCheck (nativeModes db) sys - pure $ PDPConfig (compileRules "system" $ fmap (fmap unRawVar) sys) db Nothing 50 10 + liftEither . first ModeError $ modeCheck (nativeModes db) sys + rules <- liftIO $ compileRules "system" $ fmap (fmap unRawVar) sys + pure $ PDPConfig rules db Nothing 50 10 demoNativeDb :: NativeDb @@ -204,7 +211,7 @@ demoNativeDb = mkNativeDb "base" preds , mkNativePred "lines" $ fmap Solely . T.lines] demoConfig :: IO (Either PDPError PDPConfig) -demoConfig = fmap addSubmit <$> pdpConfig demoNativeDb "system.ava" +demoConfig = runExceptT (addSubmit <$> pdpConfig demoNativeDb "system.ava") where addSubmit conf = conf { submitQuery = Just [qry| may(submit) |]} -- Everyone: Alec, why not just use lenses? diff --git a/core/src/Language/Avaleryar/Semantics.hs b/core/src/Language/Avaleryar/Semantics.hs index 7a0b24b..a23b707 100644 --- a/core/src/Language/Avaleryar/Semantics.hs +++ b/core/src/Language/Avaleryar/Semantics.hs @@ -5,6 +5,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -70,6 +71,7 @@ import Control.DeepSeq (NFData) import Control.Monad.Except import Control.Monad.State import Data.Foldable +import Data.IORef import Data.Map (Map) import qualified Data.Map as Map import Data.String @@ -135,9 +137,10 @@ loadNative n p = getsRT (unNativeDb . nativeDb . db) >>= alookup n >>= alookup p -- | Runtime state for 'Avaleryar' computations. data RT = RT - { env :: Env -- ^ The accumulated substitution - , epoch :: Epoch -- ^ A counter for generating fresh variables - , db :: Db -- ^ The database of compiled predicates + { env :: !Env -- ^ The accumulated substitution + , epoch :: !Epoch -- ^ A counter for generating fresh variables + , db :: !Db -- ^ The database of compiled predicates + , cacheVersion :: !Int -- ^ Used to invalide cache when adding and removing rules. } deriving (Generic) -- | Allegedly more-detailed results from an 'Avaleryar' computation. A more ergonomic type is @@ -184,7 +187,7 @@ runAvaleryar' :: Int -> Int -> Db -> Avaleryar a -> IO (DetailedResults a) runAvaleryar' d b db ava = do start <- getMonotonicTime res <- runM' (Just d) (Just b) - . flip evalStateT (RT mempty 0 db) + . flip evalStateT (RT mempty 0 db 0) . unAvaleryar $ ava end <- getMonotonicTime case res of @@ -253,6 +256,22 @@ resolve (assn `Says` l@(Lit p as)) = do resolver l Lit p <$> traverse subst as +-- | Just like resolve, except that Instead of looking up the resolver every +-- time, it is cached inside an IORef. The cached value is invalidated by +-- incrementing cacheVersion, and is done whenever the rules change. +resolveAndCache :: IORef (Int, Lit EVar -> Avaleryar ()) -> Goal -> Avaleryar (Lit EVar) +resolveAndCache ref goal@(assn `Says` l@(Lit p as)) = do + currentVer <- getsRT cacheVersion + resolver <- liftIO (readIORef ref) >>= \case + (resVer, res) | currentVer == resVer -> do + yield' $ pure res + _ -> do + res <- yield' $ loadResolver assn p + liftIO $ writeIORef ref (currentVer, res) + pure res + + yield' $ resolver l + Lit p <$> traverse subst as -- | A slightly safer version of @'zipWithM_' 'unifyTerm'@ that ensures its argument lists are the -- same length. @@ -264,24 +283,28 @@ unifyArgs _ _ = empty -- | NB: 'compilePred' doesn't look at the 'Pred' for any of the given rules, it assumes it was -- given a query that applies, and that the rules it was handed are all for the same predicate. -- This is not the function you want. FIXME: Suck less -compilePred :: [Rule TextVar] -> Lit EVar -> Avaleryar () -compilePred rules (Lit _ qas) = do - rt@RT {..} <- getRT - putRT rt {epoch = succ epoch} - let rules' = fmap (EVar epoch) <$> rules - go (Rule (Lit _ has) body) = do - unifyArgs has qas - traverse_ resolve body - msum $ go <$> rules' +compilePred :: [Rule TextVar] -> IO (Lit EVar -> Avaleryar ()) +compilePred rules = do + let makeCaches (Rule _lit body) = traverse (const $ newIORef (-1, \_ -> pure ())) body + cachess :: [[IORef (Int, Lit EVar -> Avaleryar ())]] <- traverse makeCaches rules + pure $ \(Lit _ qas) -> do + rt@RT {..} <- getRT + putRT rt {epoch = succ epoch} + let rules' = fmap (EVar epoch) <$> rules + go caches (Rule (Lit _ has) body) = do + unifyArgs has qas + traverse_ (uncurry resolveAndCache) (zip caches body) + msum $ uncurry go <$> zip cachess rules' -- | Turn a list of 'Rule's into a map from their names to code that executes them. -- -- Substitutes the given assertion for references to 'ARCurrent' in the bodies of the rules. This -- is somewhat gross, and needs to be reexamined in the fullness of time. -compileRules :: Text -> [Rule TextVar] -> Map Pred (Lit EVar -> Avaleryar ()) -compileRules assn rules = - fmap compilePred $ Map.fromListWith (++) [(p, [emplaceCurrentAssertion assn r]) - | r@(Rule (Lit p _) _) <- rules] +compileRules :: Text -> [Rule TextVar] -> IO (Map Pred (Lit EVar -> Avaleryar ())) +compileRules assn rules = do + let rulesMap = Map.fromListWith (++) [ (p, [emplaceCurrentAssertion assn r]) + | r@(Rule (Lit p _) _) <- rules ] + fmap Map.fromList . traverse (\(p, rs) -> (p,) <$> compilePred rs) $ Map.toList rulesMap emplaceCurrentAssertion :: Text -> Rule v -> Rule v emplaceCurrentAssertion assn (Rule l b) = Rule l (go <$> b) diff --git a/core/src/Language/Avaleryar/Testing.hs b/core/src/Language/Avaleryar/Testing.hs index 3297a0c..ff9dd85 100644 --- a/core/src/Language/Avaleryar/Testing.hs +++ b/core/src/Language/Avaleryar/Testing.hs @@ -92,26 +92,26 @@ parseTestCase (Directive (Lit (Pred "test" _) (tn:dbs)) tqs) = do pure TestCase {..} parseTestCase _ = Nothing -parseDb :: (Text, Text) -> Directive -> Maybe TestDb +parseDb :: (Text, Text) -> Directive -> IO (Maybe TestDb) parseDb (alias, assn) (Directive (Lit (Pred "db" _) [Val (T dbn)]) fs) | assn == dbn = - Just ([(alias, fmap factToRule fs)], mempty) + pure $ Just ([(alias, fmap factToRule fs)], mempty) parseDb (alias, assn) (Directive (Lit (Pred "native" _) [Val (T dbn)]) fs) | assn == dbn = - Just (mempty, mkNativeDb alias $ factsToNative fs) -parseDb _ _ = Nothing + Just . (mempty,) . mkNativeDb alias <$> factsToNative fs +parseDb _ _ = pure Nothing -- Have to group up all the facts to pass to 'compilePred' or else they won't succeed more than once -- (i.e., @native(stuff) may(read), may(write).@ can't succeed on both @may@s without this annoying -- grouping pass. -- -- TODO: The fake mode might be too strong, in which case we'd need some other plan? -factsToNative :: [Fact] -> [NativePred] -factsToNative fs = [NativePred (compilePred rs) (modeFor p) | (p, rs) <- Map.toList preds] +factsToNative :: [Fact] -> IO [NativePred] +factsToNative fs = sequence [NativePred <$> compilePred rs <*> pure (modeFor p) | (p, rs) <- Map.toList preds] where preds = Map.fromListWith (<>) [(p, [factToRule f]) | f@(Lit p _) <- fs] modeFor p@(Pred _ n) = Lit p (replicate n (Var outMode)) -dbForTestCase :: [Directive] -> TestCase -> TestDb +dbForTestCase :: [Directive] -> TestCase -> IO TestDb dbForTestCase dirs TestCase {..} = foldMap go testAssns - where go p = maybe mempty id $ foldMap (parseDb p) dirs + where go p = maybe mempty id <$> foldMap (parseDb p) dirs -- | Find assertions used by the 'Test' that aren't available in its 'TestDb'. -- @@ -180,10 +180,10 @@ withTestHandle conf k t@(Test _ (assns, ndb)) = do withTestHandle_ :: PDPConfig -> (PDPHandle -> IO ()) -> Test -> IO TestResults withTestHandle_ p k t = fst <$> withTestHandle p k t -extractTests :: [Directive] -> [Test] -extractTests dirs = go <$> cases +extractTests :: [Directive] -> IO [Test] +extractTests dirs = sequence (go <$> cases) where cases = foldMap (toList . parseTestCase) dirs - go tc = Test tc $ dbForTestCase dirs tc + go tc = Test tc <$> dbForTestCase dirs tc -- | Turn a 'Rule' that's really a fact into a 'Fact' in fact. Hideously unsafe if you don't -- already know for sure it'll succeed. This function really shouldn't escape this module. @@ -198,7 +198,7 @@ appAssertion :: Test -> [Fact] appAssertion = fmap ruleToFact . concat . lookup "application" . fst . testDb parseTestFile :: FilePath -> IO (Either String [Test]) -parseTestFile fp = fmap (extractTests . fst) <$> parseFile' fp +parseTestFile fp = either (pure . Left) (fmap Right . extractTests . fst) =<< parseFile' fp runTestFile :: PDPConfig -> (PDPHandle -> IO ()) -> FilePath -> IO (Either String [(Text, TestResults)]) runTestFile conf k tf = do @@ -207,7 +207,3 @@ runTestFile conf k tf = do case parsed of Left err -> pure (Left err) Right ts -> Right <$> traverse gatherResults ts - - - - diff --git a/repl/src/Language/Avaleryar/Repl.hs b/repl/src/Language/Avaleryar/Repl.hs index fef5a35..929bbcd 100644 --- a/repl/src/Language/Avaleryar/Repl.hs +++ b/repl/src/Language/Avaleryar/Repl.hs @@ -10,6 +10,7 @@ module Language.Avaleryar.Repl where import Control.Applicative +import Control.Monad.Except import Control.Monad.Reader import Data.Containers.ListUtils (nubOrd) import Data.Foldable @@ -59,7 +60,7 @@ repl conf = replWithHandle conf mempty main :: IO () main = do Args {..} <- execParser (info parseArgs mempty) - conf <- pdpConfig demoNativeDb systemAssn >>= either diePretty pure + conf <- runExceptT (pdpConfig demoNativeDb systemAssn) >>= either diePretty pure let loadAssns h = for_ otherAssns $ either diePretty pure <=< unsafeSubmitFile h Nothing displayResults = traverse_ $ either putStrLn (traverse_ $ uncurry putTestResults)