Implement blocking of vector operations using postulates (#746)

Author: MatthewDaggitt

Diff for: vehicle-syntax/src/Vehicle/Syntax/AST.hs

@@ -13,4 +13,5 @@ import Vehicle.Syntax.AST.Name as X
 import Vehicle.Syntax.AST.Prog as X
 import Vehicle.Syntax.AST.Provenance as X
 import Vehicle.Syntax.AST.Relevance as X
+import Vehicle.Syntax.AST.Type as X
 import Vehicle.Syntax.AST.Visibility as X

Diff for: vehicle-syntax/src/Vehicle/Syntax/AST/Binder.hs

@@ -10,6 +10,7 @@ import GHC.Generics (Generic)
 import Vehicle.Syntax.AST.Name (HasName (..), Name)
 import Vehicle.Syntax.AST.Provenance (HasProvenance (..), Provenance)
 import Vehicle.Syntax.AST.Relevance (HasRelevance (..), Relevance (..))
+import Vehicle.Syntax.AST.Type
 import Vehicle.Syntax.AST.Visibility (HasVisibility (..), Visibility (..))
 
 --------------------------------------------------------------------------------
@@ -111,6 +112,9 @@ instance HasRelevance (GenericBinder expr) where
 instance HasName (GenericBinder expr) (Maybe Name) where
   nameOf = nameOf . binderNamingForm
 
+instance HasType (GenericBinder expr) expr where
+  typeOf = binderValue
+
 --------------------------------------------------------------------------------
 -- Binders
 

Diff for: vehicle-syntax/src/Vehicle/Syntax/AST/Decl.hs

@@ -7,6 +7,7 @@ import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..))
 import Vehicle.Syntax.AST.Name
 import Vehicle.Syntax.AST.Provenance
+import Vehicle.Syntax.AST.Type
 
 --------------------------------------------------------------------------------
 -- Declarations
@@ -45,6 +46,11 @@ instance HasIdentifier (GenericDecl expr) where
 instance HasName (GenericDecl expr) Name where
   nameOf = nameOf . identifierOf
 
+instance HasType (GenericDecl expr) expr where
+  typeOf = \case
+    DefAbstract _ _ _ t -> t
+    DefFunction _ _ _ t _ -> t
+
 bodyOf :: GenericDecl expr -> Maybe expr
 bodyOf = \case
   DefFunction _ _ _ _ e -> Just e
@@ -124,6 +130,10 @@ isExternalResourceSort = \case
   ParameterDef {} -> True
   PostulateDef -> False
 
+convertToPostulate :: GenericDecl expr -> GenericDecl expr
+convertToPostulate d =
+  DefAbstract (provenanceOf d) (identifierOf d) PostulateDef (typeOf d)
+
 --------------------------------------------------------------------------------
 -- Annotations options
 

Diff for: vehicle-syntax/src/Vehicle/Syntax/AST/Type.hs

@@ -0,0 +1,7 @@
+module Vehicle.Syntax.AST.Type where
+
+--------------------------------------------------------------------------------
+-- HasType
+
+class HasType expr typ | expr -> typ where
+  typeOf :: expr -> typ

Diff for: vehicle-syntax/vehicle-syntax.cabal

@@ -113,6 +113,7 @@ library
     Vehicle.Syntax.AST.Prog
     Vehicle.Syntax.AST.Provenance
     Vehicle.Syntax.AST.Relevance
+    Vehicle.Syntax.AST.Type
     Vehicle.Syntax.AST.Visibility
     Vehicle.Syntax.BNFC.Delaborate.External
     Vehicle.Syntax.BNFC.Delaborate.Internal

Diff for: vehicle/src/Vehicle/Backend/Queries.hs

@@ -127,7 +127,7 @@ compilePropertyDecl ::
   m (Name, MultiProperty ())
 compilePropertyDecl prog queryFormat networkCtx queryFreeCtx p ident expr outputLocation = do
   logCompilerPass MinDetail ("property" <+> quotePretty ident) $ do
-    normalisedExpr <- eval (mkNBEOptions vectorStructureOperations) emptyEnv expr
+    normalisedExpr <- whilePreservingOperations vectorOperations $ normaliseInEmptyEnv expr
 
     let computeProperty = compileMultiProperty queryFormat networkCtx queryFreeCtx p ident outputLocation normalisedExpr
 

Diff for: vehicle/src/Vehicle/Backend/Queries/QuerySetStructure.hs

@@ -2,13 +2,15 @@ module Vehicle.Backend.Queries.QuerySetStructure
   ( UnreducedAssertion,
     compileSetQueryStructure,
     eliminateNot,
-    vectorStructureOperations,
+    whilePreservingOperations,
     isVectorEquals,
+    vectorOperations,
   )
 where
 
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Reader (MonadReader (..), ReaderT (..))
+import Data.Data (Proxy (..))
 import Data.HashSet qualified as HashSet (fromList, intersection, null)
 import Data.Map qualified as Map (keysSet)
 import Data.Set (Set)
@@ -127,8 +129,8 @@ type MonadQueryStructure m =
 
 -- | The set of vector operations that we sometimes want to avoid normalising
 -- out in the property for efficiency reasons.
-vectorStructureOperations :: Set StdLibFunction
-vectorStructureOperations =
+vectorOperations :: Set StdLibFunction
+vectorOperations =
   Set.fromList
     [ StdAddVector,
       StdSubVector,
@@ -138,15 +140,22 @@ vectorStructureOperations =
 
 -- | The set of finite quantifier operations that we sometimes want to avoid normalising
 -- out in the property for efficiency reasons.
-finiteQuantifierFunctions :: Set StdLibFunction
-finiteQuantifierFunctions =
+finiteQuantifierOperations :: Set StdLibFunction
+finiteQuantifierOperations =
   Set.fromList
     [ StdForallIndex,
       StdExistsIndex
     ]
 
-queryStructureNBEOptions :: NBEOptions
-queryStructureNBEOptions = mkNBEOptions (vectorStructureOperations <> finiteQuantifierFunctions)
+vectorLikeOperations :: Set StdLibFunction
+vectorLikeOperations = vectorOperations <> finiteQuantifierOperations
+
+-- | Alter the normalisation monads so that builtin vector operations are
+-- temporarily converted to postulates and therefore do not evaluate.
+whilePreservingOperations :: (MonadNorm Builtin m) => Set StdLibFunction -> m a -> m a
+whilePreservingOperations funcs = do
+  let operations = Set.map identifierOf funcs
+  locallyAdjustCtx (Proxy @Builtin) (alterKeys operations convertToPostulate)
 
 compileBoolExpr ::
   forall m.
@@ -220,7 +229,7 @@ compileBoolExpr = go False
             Just (Just exprWithoutIf) -> do
               logDebug MaxDetail $ "If-lifted to:" <+> prettyFriendly (WithContext exprWithoutIf ctx)
               let env = variableCtxToEnv quantifiedVariables
-              normExprWithoutIf <- reeval defaultNBEOptions env exprWithoutIf
+              normExprWithoutIf <- renormalise env exprWithoutIf
               logDebug MaxDetail $ "Normalised to:" <+> prettyFriendly (WithContext normExprWithoutIf ctx)
               go True quantifiedVariables normExprWithoutIf
           decrCallDepth
@@ -321,9 +330,11 @@ compileFiniteQuantifier quantifiedVariables q quantSpine binder env body = do
       return $ Right (mempty, Query foldedExpr, mempty)
     else do
       logDebug MaxDetail $ "Unfolding finite quantifier:" <+> pretty q <+> prettyVerbose binder
-      quantImplementation <- lookupIdentValueInEnv defaultNBEOptions env (fromFiniteQuantifier q)
+      quantImplementation <- lookupIdentValueInEnv noAbstractFreeVarInterpretation env (fromFiniteQuantifier q)
       let quantifierExpr = VFiniteQuantifierSpine quantSpine binder env body
-      normResult <- evalApp queryStructureNBEOptions quantImplementation quantifierExpr
+      normResult <-
+        whilePreservingOperations vectorLikeOperations $
+          normaliseApp quantImplementation quantifierExpr
       compileBoolExpr quantifiedVariables normResult
 
 -- | This is a sound, inexpensive, but incomplete, check for whether
@@ -375,7 +386,7 @@ compileInfiniteQuantifier quantifiedVariables binder env body = do
 
         -- First of all optimistically try not to normalise the quantified variable.
         let optimisticEnv = extendEnvWithBound binder env
-        optimisiticBody <- eval queryStructureNBEOptions optimisticEnv body
+        optimisiticBody <- whilePreservingOperations vectorLikeOperations $ normaliseInEnv optimisticEnv body
 
         let unreducedPassDoc = "Trying without reducing dimensions of" <+> variableDoc
         optimisticResult <-
@@ -398,7 +409,7 @@ compileInfiniteQuantifier quantifiedVariables binder env body = do
 
             let updatedQuantifiedVars = newQuantifiedVariables <> quantifiedVariables
 
-            normBody <- eval queryStructureNBEOptions newEnv body
+            normBody <- whilePreservingOperations vectorLikeOperations $ normaliseInEnv newEnv body
 
             let reducedPassDoc = "Compiling while reducing dimensions of" <+> quotePretty variableName
             normalisedResult <-

Diff for: vehicle/src/Vehicle/Backend/Queries/UserVariableElimination.hs

@@ -33,7 +33,7 @@ import Vehicle.Backend.Queries.Variable
 import Vehicle.Compile.Context.Free (MonadFreeContext)
 import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.Builtin (evalMul)
-import Vehicle.Compile.Normalise.NBE (defaultNBEOptions, reeval)
+import Vehicle.Compile.Normalise.NBE (renormalise)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print (prettyVerbose)
 import Vehicle.Compile.Type.Subsystem.Standard
@@ -408,7 +408,7 @@ substituteReducedVariablesThroughSolutions partialEnv solutions solvedVariablePo
   where
     f :: (UserVariable, WHNFValue Builtin) -> WHNFEnv Builtin -> m (WHNFEnv Builtin)
     f (var, solution) env = do
-      normalisedSolution <- reeval defaultNBEOptions env solution
+      normalisedSolution <- renormalise env solution
       let errorMsg = developerError $ "Environment index missing for solved variable" <+> quotePretty var
       let index = unIx $ fromMaybe errorMsg $ Map.lookup var solvedVariablePositions
       let newEntry = mkDefaultEnvEntry (layoutAsText $ pretty var) (Defined normalisedSolution)
@@ -493,7 +493,7 @@ compileReducedAssertion ::
   m (MaybeTrivial (BooleanExpr SolvableAssertion))
 compileReducedAssertion _originalVariables variables variableSubstEnv assertion = do
   -- First normalise the expression under the new environment of reduced variables
-  normExpr <- reeval defaultNBEOptions variableSubstEnv assertion
+  normExpr <- renormalise variableSubstEnv assertion
 
   -- Then extract the relation and arguments
   splitAssertions <- splitUpAssertions False normExpr
@@ -546,7 +546,7 @@ compileReducedAssertion _originalVariables variables variableSubstEnv assertion
         Just Nothing -> compilerDeveloperError $ "Cannot lift 'if' over" <+> prettyVerbose expr
         Just (Just exprWithoutIf) -> do
           let env = variableCtxToEnv variableCtx
-          normExprWithoutIf <- reeval defaultNBEOptions env exprWithoutIf
+          normExprWithoutIf <- renormalise env exprWithoutIf
           splitUpAssertions True normExprWithoutIf
 
     reduceAssertion ::

Diff for: vehicle/src/Vehicle/Compile/Context/Free/Class.hs

@@ -1,7 +1,7 @@
 module Vehicle.Compile.Context.Free.Class where
 
 import Control.Monad.Reader (ReaderT (..), mapReaderT)
-import Control.Monad.State (StateT, mapStateT)
+import Control.Monad.State (StateT (..), mapStateT)
 import Control.Monad.Writer
 import Data.Data (Proxy (..))
 import Vehicle.Compile.Context.Bound
@@ -19,22 +19,27 @@ import Vehicle.Data.BuiltinInterface (HasStandardData)
 class (PrintableBuiltin builtin, HasStandardData builtin, MonadCompile m) => MonadFreeContext builtin m where
   addDeclToContext :: Decl Ix builtin -> m a -> m a
   getFreeCtx :: Proxy builtin -> m (FreeCtx builtin)
+  locallyAdjustCtx :: Proxy builtin -> (FreeCtx builtin -> FreeCtx builtin) -> m a -> m a
 
 instance (Monoid w, MonadFreeContext builtin m) => MonadFreeContext builtin (WriterT w m) where
   addDeclToContext = mapWriterT . addDeclToContext
   getFreeCtx = lift . getFreeCtx
+  locallyAdjustCtx p = mapWriterT . locallyAdjustCtx p
 
 instance (MonadFreeContext builtin m) => MonadFreeContext builtin (ReaderT w m) where
   addDeclToContext = mapReaderT . addDeclToContext
   getFreeCtx = lift . getFreeCtx
+  locallyAdjustCtx p = mapReaderT . locallyAdjustCtx p
 
 instance (MonadFreeContext builtin m) => MonadFreeContext builtin (StateT w m) where
   addDeclToContext = mapStateT . addDeclToContext
   getFreeCtx = lift . getFreeCtx
+  locallyAdjustCtx p = mapStateT . locallyAdjustCtx p
 
 instance (MonadFreeContext builtin m) => MonadFreeContext builtin (BoundContextT builtin m) where
   addDeclToContext = mapBoundContextT . addDeclToContext
   getFreeCtx = lift . getFreeCtx
+  locallyAdjustCtx p = mapBoundContextT . locallyAdjustCtx p
 
 --------------------------------------------------------------------------------
 -- Operations

Diff for: vehicle/src/Vehicle/Compile/Context/Free/Instance.hs

@@ -81,3 +81,7 @@ instance
     local updateCtx (unFreeContextT cont)
 
   getFreeCtx _ = FreeContextT ask
+
+  locallyAdjustCtx _ f x =
+    FreeContextT $
+      local f (unFreeContextT x)