Cache resolve results

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

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

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?

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)

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
-
-
-
-

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)