Improved performance of compilation to queries

CONTRIBUTING.md

@@ -164,7 +164,7 @@ There are three test suites for the Vehicle compiler:
 The standard command to test the Vehicle compiler runs the unit and the compiler tests:
 
 ```sh
-cabal test unit-tests golden-tests --test-show-details=always --test-option=--color=always --test-option=--num-threads=1
+cabal test unit-tests golden-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1
 ```
 
 This command is run on GitHub Actions whenever changes are pushed to Vehicle the default branch or an open pull request—see [build-vehicle.yml](./.github/workflows/build-vehicle.yml).
@@ -198,7 +198,7 @@ All 155 tests passed (12.33s)
 Test suite golden-tests: PASS
 ```
 
-The option `--test-show-details=always` asks the testing framework to print some details about the tests it is running, and `--test-option=--color=always` asks it to use colour. If you omit these options, the output is much less verbose, and looks like:
+The option `--test-show-details=streaming` asks the testing framework to print some live details about the tests it is running, and `--test-option=--color=always` asks it to use colour. If you omit these options, the output is much less verbose, and looks like:
 
 ```
 Running 1 test suites...
@@ -254,7 +254,7 @@ The unit tests test properties of the internals of Vehicle, _e.g._, of the Vehic
 Run the following command:
 
 ```sh
-cabal test unit-tests --test-show-details=always --test-option=--color=always --test-option=--num-threads=1
+cabal test unit-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1
 ```
 
 You can use `--test-option="--vehicle-logging X"` to set the logging level, where `X` is one of `NoDetail`, `MinDetail`, `MidDetail`, or `MaxDetail`. The logging levels can be found by running `vehicle --help`.
@@ -268,7 +268,7 @@ The golden tests test properties of the compiler as a whole, by running it with
 Run the following command:
 
 ```sh
-cabal test golden-tests --test-show-details=always --test-option=--color=always --test-option=--num-threads=1
+cabal test golden-tests --test-show-details=streaming --test-option=--color=always --test-option=--num-threads=1
 ```
 
 These tests are specified in `test.json` files in [tests/golden](./vehicle/tests/golden/), _e.g._, [windController/test.json](./vehicle/tests/golden/compile/windController/test.json):

vehicle/src/Vehicle/Backend/Queries.hs

@@ -128,7 +128,7 @@ compilePropertyDecl ::
   Maybe FilePath ->
   m (Name, MultiProperty ())
 compilePropertyDecl prog propertyData@(_, _, _, declProv@(ident, _), _) expr outputLocation = do
-  logCompilerPass MinDetail ("property" <+> quotePretty ident) $ do
+  logCompilerPass MinDetail ("found property" <+> quotePretty ident) $ do
     normalisedExpr <- normaliseInEmptyEnv expr
     multiProperty <-
       compileMultiProperty propertyData outputLocation normalisedExpr
@@ -156,16 +156,12 @@ compileMultiProperty multiPropertyMetaData outputLocation = go []
     go :: TensorIndices -> WHNFValue Builtin -> m (MultiProperty ())
     go indices expr = case expr of
       VVecLiteral es -> do
-        let es' = zip [0 :: QueryID ..] es
+        let es' = zip [0 :: Int ..] es
         MultiProperty <$> traverse (\(i, e) -> go (i : indices) (argExpr e)) es'
       _ -> do
         let propertyMetaData@PropertyMetaData {..} = updateMetaData multiPropertyMetaData indices
-        let logFunction =
-              if null indices
-                then id
-                else logCompilerPass MinDetail ("property" <+> quotePretty propertyAddress)
         flip runReaderT propertyMetaData $ do
-          logFunction $ do
+          logCompilerPass MinDetail ("property" <+> quotePretty propertyAddress) $ do
             compileSingleProperty outputLocation expr
             return $ SingleProperty propertyAddress ()
 

vehicle/src/Vehicle/Backend/Queries/PostProcessing.hs

@@ -6,6 +6,7 @@ where
 
 import Control.Monad (foldM, forM, unless, when)
 import Control.Monad.Reader (MonadReader (..))
+import Control.Monad.State (get)
 import Data.Either (partitionEithers)
 import Data.LinkedHashMap qualified as LinkedHashMap
 import Data.List.NonEmpty (NonEmpty (..))
@@ -31,17 +32,16 @@ import Vehicle.Verify.Variable
 -- Main entry point
 
 convertPartitionsToQueries ::
-  (MonadPropertyStructure m) =>
-  GlobalCtx ->
+  (MonadQueryStructure m) =>
   Partitions ->
   m (DisjunctAll (MetaNetwork, UserVariableReconstruction, QueryContents))
-convertPartitionsToQueries globalCtx partitions = do
+convertPartitionsToQueries partitions = do
   allQueries <- forM (partitionsToDisjuncts partitions) $ \(userVarSol, assertionTree) -> do
-    networkVarAssertions <- convertToNetworkRatVarAssertions globalCtx assertionTree
+    networkVarAssertions <- convertToNetworkRatVarAssertions assertionTree
     let dnfTree = exprToDNF networkVarAssertions
     forM dnfTree $ \conjuncts -> do
       -- Calculate meta network
-      (metaNetwork, newConjuncts) <- calculateMetaNetwork globalCtx conjuncts
+      (metaNetwork, newConjuncts) <- calculateMetaNetwork conjuncts
       -- Compile queries to particular format
       let contents = prettifyQueryContents (variables metaNetwork) newConjuncts
       -- Return the result
@@ -70,11 +70,10 @@ compileQueryToFormat (metaNetwork, userVars, contents@QueryContents {..}) = do
 
 convertToNetworkRatVarAssertions ::
   forall m.
-  (MonadCompile m) =>
-  GlobalCtx ->
+  (MonadQueryStructure m) =>
   AssertionTree ->
   m (BooleanExpr QueryAssertion)
-convertToNetworkRatVarAssertions globalCtx = go
+convertToNetworkRatVarAssertions = go
   where
     go :: BooleanExpr Assertion -> m (BooleanExpr QueryAssertion)
     go = \case
@@ -85,7 +84,7 @@ convertToNetworkRatVarAssertions globalCtx = go
     convert :: Assertion -> m (BooleanExpr QueryAssertion)
     convert = \case
       TensorEq tensorEquality -> do
-        rationalEqualities <- reduceTensorEquality globalCtx tensorEquality
+        rationalEqualities <- reduceTensorEquality tensorEquality
         let assertions = fmap (Query . RationalEq) rationalEqualities
         go $ Conjunct $ ConjunctAll (NonEmpty.fromList assertions)
       RationalEq (RationalEquality expr) ->
@@ -143,11 +142,11 @@ data ReindexingState = ReindexingState
 
 calculateMetaNetwork ::
   forall m f.
-  (MonadCompile m, Traversable f) =>
-  GlobalCtx ->
+  (MonadQueryStructure m, Traversable f) =>
   f QueryAssertion ->
   m (MetaNetwork, f QueryAssertion)
-calculateMetaNetwork ctx queries = do
+calculateMetaNetwork queries = do
+  ctx <- get
   -- First calculate the set of network applications actually used in the query
   let referencedVars = foldMap queryAssertionVariables queries
   let networkApps = snd <$> LinkedHashMap.toList (networkApplications ctx)

vehicle/src/Vehicle/Backend/Queries/UserVariableElimination.hs

@@ -7,18 +7,18 @@ where
 
 -- Needed as Applicative is exported by Prelude in GHC 9.6 and above.
 import Control.Applicative (Applicative (..))
-import Control.Monad (unless, when)
+import Control.Monad (when)
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Reader (MonadReader (..))
-import Control.Monad.State (MonadState (..), StateT (..))
+import Control.Monad.State (MonadState (..), evalStateT)
 import Control.Monad.Writer (MonadWriter, WriterT (..))
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Vehicle.Backend.Queries.PostProcessing (convertPartitionsToQueries)
 import Vehicle.Backend.Queries.UserVariableElimination.Core
 import Vehicle.Backend.Queries.UserVariableElimination.EliminateExists (eliminateExists)
 import Vehicle.Backend.Queries.UserVariableElimination.EliminateNot (eliminateNot)
-import Vehicle.Backend.Queries.UserVariableElimination.Unblocking (tryUnblockBool)
+import Vehicle.Backend.Queries.UserVariableElimination.Unblocking
 import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.NBE
 import Vehicle.Compile.Prelude
@@ -94,12 +94,13 @@ compileQuantifiedQuerySet ::
 compileQuantifiedQuerySet isPropertyNegated binder env body = do
   let subsectionDoc = "compilation of set of quantified queries:" <+> prettyFriendlyEmptyCtx (VExists [] binder env body)
   logCompilerPass MaxDetail subsectionDoc $ do
-    (maybePartitions, globalCtx) <- runStateT (compileExists binder env body) emptyGlobalCtx
-    case maybePartitions of
-      Trivial b -> return $ Trivial (b `xor` isPropertyNegated)
-      NonTrivial partitions -> do
-        queries <- convertPartitionsToQueries globalCtx partitions
-        return $ NonTrivial $ Query $ QuerySet isPropertyNegated queries
+    flip evalStateT emptyGlobalCtx $ do
+      maybePartitions <- compileExists binder env body
+      case maybePartitions of
+        Trivial b -> return $ Trivial (b `xor` isPropertyNegated)
+        NonTrivial partitions -> do
+          queries <- convertPartitionsToQueries partitions
+          return $ NonTrivial $ Query $ QuerySet isPropertyNegated queries
 
 -- | We only need this because we can't evaluate networks in the compiler.
 compileUnquantifiedQuerySet ::
@@ -109,14 +110,15 @@ compileUnquantifiedQuerySet ::
 compileUnquantifiedQuerySet value = do
   let subsectionDoc = "compilation of set of unquantified queries:" <+> prettyFriendlyEmptyCtx value
   logCompilerPass MaxDetail subsectionDoc $ do
-    ((maybePartitions, globalCtx), equalities) <- runWriterT (runStateT (compileBoolExpr value) emptyGlobalCtx)
-    (networkEqPartitions, _) <- runStateT (networkEqualitiesToPartition equalities) globalCtx
-    let equalitiesPartition = andTrivial andPartitions maybePartitions networkEqPartitions
-    case equalitiesPartition of
-      Trivial b -> return $ Trivial b
-      NonTrivial partitions -> do
-        queries <- convertPartitionsToQueries globalCtx partitions
-        return $ NonTrivial $ Query $ QuerySet False queries
+    flip evalStateT emptyGlobalCtx $ do
+      (maybePartitions, equalities) <- runWriterT $ do (compileBoolExpr value)
+      networkEqPartitions <- networkEqualitiesToPartition equalities
+      let equalitiesPartition = andTrivial andPartitions maybePartitions networkEqPartitions
+      case equalitiesPartition of
+        Trivial b -> return $ Trivial b
+        NonTrivial partitions -> do
+          queries <- convertPartitionsToQueries partitions
+          return $ NonTrivial $ Query $ QuerySet False queries
 
 -- | Attempts to compile an arbitrary expression of type `Bool` down to a tree
 -- of assertions implicitly existentially quantified by a set of network
@@ -130,9 +132,9 @@ compileBoolExpr expr = case expr of
   -- Base cases --
   ----------------
   VBoolLiteral b -> return $ Trivial b
-  VOrder OrderRat op e1 e2 -> tryUnblockBool expr compileBoolExpr (compileRationalAssertion (ordToAssertion op) e1 e2)
-  VEqual EqRat e1 e2 -> tryUnblockBool expr compileBoolExpr (compileRationalAssertion eqToAssertion e1 e2)
-  VVectorEqualFull spine@(VVecEqArgs e1 e2) -> tryUnblockBool expr compileBoolExpr (compileTensorAssertion spine e1 e2)
+  VOrder OrderRat op _ _ -> tryPurifyAssertion expr compileBoolExpr (compileRationalAssertion (ordToAssertion op))
+  VEqual EqRat _ _ -> tryPurifyAssertion expr compileBoolExpr (compileRationalAssertion eqToAssertion)
+  VVectorEqualFull (VVecEqSpine t1 t2 n s _ _) -> tryPurifyAssertion expr compileBoolExpr (compileTensorAssertion [t1, t2, n, s])
   VForall {} -> throwError catchableUnsupportedAlternatingQuantifiersError
   ---------------------
   -- Recursive cases --
@@ -144,7 +146,7 @@ compileBoolExpr expr = case expr of
   VAnd x y -> andTrivial andPartitions <$> compileBoolExpr x <*> compileBoolExpr y
   VOr x y -> orTrivial orPartitions <$> compileBoolExpr x <*> compileBoolExpr y
   VExists _ binder env body -> compileExists binder env body
-  _ -> tryUnblockBool expr compileBoolExpr (compilerDeveloperError "Could not unblock bool expr")
+  _ -> compileBoolExpr =<< unblockBoolExpr expr
 
 eliminateIf :: WHNFValue QueryBuiltin -> WHNFValue QueryBuiltin -> WHNFValue QueryBuiltin -> WHNFValue QueryBuiltin
 eliminateIf c x y = VOr (VAnd c x) (VAnd (VNot c) y)
@@ -157,7 +159,7 @@ eliminateNotEqualRat ::
 eliminateNotEqualRat x y = do
   PropertyMetaData {..} <- ask
   if supportsStrictInequalities queryFormat
-    then return $ VOr (VOrder OrderRat Le x y) (VOrder OrderRat Le y x)
+    then return $ VOr (VOrderRat Le x y) (VOrderRat Le y x)
     else throwError $ UnsupportedInequality (queryFormatID queryFormat) propertyProvenance
 
 eliminateNotVectorEqual ::
@@ -221,13 +223,13 @@ compileTensorAssertion ::
   WHNFValue QueryBuiltin ->
   WHNFValue QueryBuiltin ->
   m (MaybeTrivial Partitions)
-compileTensorAssertion spine x y = do
+compileTensorAssertion spinePrefix x y = do
   x' <- compileTensorLinearExpr x
   y' <- compileTensorLinearExpr y
   let maybeAssertion = liftA2 tensorEqToAssertion x' y'
   case maybeAssertion of
     Just assertion -> return $ mkTrivialPartition assertion
-    Nothing -> compileBoolExpr =<< appStdlibDef StdEqualsVector spine
+    Nothing -> compileBoolExpr =<< appStdlibDef StdEqualsVector (spinePrefix <> (Arg mempty Explicit Relevant <$> [x, y]))
 
 compileTensorLinearExpr ::
   forall m.
@@ -299,7 +301,6 @@ compileExists binder env body = do
     -- performance as the search for constraints will find them first.)
     networkEqPartitions <- networkEqualitiesToPartition networkInputEqualities
     let finalPartitions = andTrivial andPartitions partitions networkEqPartitions
-    logDebug MaxDetail $ pretty finalPartitions
 
     -- Solve for the user variable.
     eliminateExists finalPartitions userVar
@@ -351,10 +352,14 @@ checkUserVariableType binder = go (typeOf binder)
 
 networkEqualitiesToPartition :: (MonadQueryStructure m) => [WHNFValue Builtin] -> m (MaybeTrivial Partitions)
 networkEqualitiesToPartition networkEqualities = do
+  logDebugM MaxDetail $ do
+    networkEqDocs <- traverse prettyFriendlyInCtx networkEqualities
+    return $ line <> "Generated network equalities:" <> line <> indent 2 (vsep networkEqDocs)
+
   (partitions, newNetworkEqualities) <- runWriterT (compileBoolExpr (foldr VAnd (VBoolLiteral True) networkEqualities))
-  unless (null newNetworkEqualities) $
-    compilerDeveloperError "New network equalities generated when compiling network equalities."
-  return partitions
+  if (null newNetworkEqualities)
+    then return partitions
+    else andTrivial andPartitions partitions <$> networkEqualitiesToPartition newNetworkEqualities
 
 -- (mkSinglePartition (mempty, conjunct equalities))
 --------------------------------------------------------------------------------