Fix #1213 by unblocking rather than evaluating comparison (#1215)

* Fix #1213 by unblocking rather evaluating comparison

* Fix test error

Author: MatthewDaggitt

vehicle/src/Vehicle/Backend/Loss/Domain.hs

@@ -13,7 +13,7 @@ import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Vehicle.Backend.Loss.Core
-import Vehicle.Backend.Loss.Domain.PurifyAssertion (BlockingReason, tryPurifyAssertion, unblockingActions)
+import Vehicle.Backend.Loss.Domain.PurifyAssertion (tryPurifyAssertion, unblockingActions)
 import Vehicle.Backend.Loss.LossCompilation
 import Vehicle.Backend.Solver.UserVariableElimination.ConstraintSearch (findAllBounds)
 import Vehicle.Compile.Constants.ForcedValue

vehicle/src/Vehicle/Backend/Loss/Domain/PurifyAssertion.hs

@@ -14,6 +14,7 @@ import Control.Applicative (liftA2)
 import Control.Monad (liftM2)
 import Control.Monad.Except (MonadError (..), runExceptT)
 import Vehicle.Compile.Constants.ForcedValue (TensorValueLinearExpr)
+import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.Force
 import Vehicle.Compile.Normalise.RewriteRules (forceAndRewriteTensor)
 import Vehicle.Compile.Normalise.TypedValue
@@ -281,10 +282,6 @@ tryAndUnblock dims expr = do
     Right unblocked -> forIfTreeM unblocked $ \unblockedExpr ->
       compileLinearExpr dims unblockedExpr
 
-data BlockingReason
-  = BlockingNetwork Identifier
-  | BlockingDatasetOrParameter Identifier
-
 unblockingActions ::
   (MonadPurifyAssertion m, MonadError BlockingReason m) =>
   UnblockingActions m
@@ -293,18 +290,19 @@ unblockingActions =
     { unblockRatTensorBoundVar = purifyBoundVar,
       unblockRecordBoundVar = purifyBoundVar,
       unblockNetworkApp = \_ _ ident _ -> throwError $ BlockingNetwork ident,
-      unblockDatasetOrParameter = \ident -> throwError $ BlockingDatasetOrParameter ident
+      unblockDatasetOrParameter = \_ ident -> throwError $ BlockingDatasetOrParameter ident
     }
 
 purifyBoundVar ::
-  (MonadLogger m, MonadReadableTensorBoundContext m) =>
+  (MonadPurifyAssertion m) =>
+  TypeUnblockingFunction (Thunk Builtin) m ->
   Lv ->
-  m (Thunk Builtin)
-purifyBoundVar lv = do
+  m (IfTree (Thunk Builtin) (Thunk Builtin))
+purifyBoundVar unblock lv = do
   (_, maybeChildVars) <- lookupVariableInNestedCtx lv
   case maybeChildVars of
-    Nothing -> return $ Forced $ VBoundVar lv []
-    Just (_tensorVar, sliceVar) -> replaceTensorVariableWithStackedChildren sliceVar
+    Nothing -> return $ IfLeaf $ Forced $ VBoundVar lv []
+    Just (_tensorVar, sliceVar) -> unblock =<< replaceTensorVariableWithStackedChildren sliceVar
 
 --------------------------------------------------------------------------------
 -- Utility functions

vehicle/src/Vehicle/Backend/Loss/LogicCompilation.hs

@@ -6,7 +6,7 @@ module Vehicle.Backend.Loss.LogicCompilation
 where
 
 import Control.Monad (foldM)
-import Control.Monad.Except (MonadError (..))
+import Control.Monad.Except (MonadError (..), runExceptT)
 import Control.Monad.State (MonadState, StateT, execStateT, modify)
 import Data.Map (Map)
 import Data.Map qualified as Map
@@ -17,12 +17,11 @@ import Vehicle.Backend.Loss.Core hiding (lookupLogicField)
 import Vehicle.Backend.Loss.LossCompilation (convertQuantifierlessExprToLoss)
 import Vehicle.Backend.Prelude (DifferentiableLogicID)
 import Vehicle.Compile.Error
-import Vehicle.Compile.Normalise.Builtin
-import Vehicle.Compile.Normalise.Core
 import Vehicle.Compile.Normalise.Force
 import Vehicle.Compile.Normalise.Quote (unnormalise)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print
+import Vehicle.Compile.Unblock (noUnblocking, unblockBoolExpr)
 import Vehicle.Data.Builtin.Interface (Accessor (..))
 import Vehicle.Data.Builtin.Loss (ComparisonOp (..), LogicDirection, LossBuiltin)
 import Vehicle.Data.Builtin.Standard (Builtin)
@@ -153,13 +152,17 @@ calculateLogicDirection ::
   OMap FieldName (Thunk Builtin) ->
   m LogicDirection
 calculateLogicDirection declProv fields = do
-  let trueValue = lookupLogicField TruthityElement fields
-  let falseValue = lookupLogicField FalsityElement fields
-  let args = TensorComparisonArgs (Forced IDimNil) (Forced IDimNil) trueValue falseValue
-  result <- runFreshNameBoundContextT $ evalCompareRatTensor @ForcedValue Le args
-  case result of
-    Evaluated (Forced (IBoolLiteral b)) -> return b
-    _ -> throwError $ UnorderableDifferentiableLogic declProv (mkExpr accessCompareRatTensor (Le, args))
+  let expr = do
+        let trueValue = lookupLogicField TruthityElement fields
+        let falseValue = lookupLogicField FalsityElement fields
+        let args = TensorComparisonArgs (Forced IDimNil) (Forced IDimNil) trueValue falseValue
+        Forced $ mkExpr accessCompareRatTensor (Le, args)
+
+  errorOrResult <- runExceptT $ runFreshNameBoundContextT $ forceThunk =<< unblockBoolExpr noUnblocking expr
+  case errorOrResult of
+    Left blockingErr -> throwError $ UnorderableDifferentiableLogic declProv expr (Left blockingErr)
+    Right (IBoolLiteral b) -> return b
+    Right result -> throwError $ UnorderableDifferentiableLogic declProv expr (Right result)
 
 compileLogicField ::
   (MonadLoss m) =>

vehicle/src/Vehicle/Backend/Solver.hs

@@ -30,6 +30,7 @@ import Vehicle.Compile.Print (prettyFriendly, prettyFriendlyEmptyCtx)
 import Vehicle.Compile.Print.Warning ()
 import Vehicle.Compile.Property (traverseMultiProperty)
 import Vehicle.Compile.Unblock (UnblockingActions (..), unblockBoolExpr)
+import Vehicle.Data.Builtin.Interface (Accessor (..))
 import Vehicle.Data.Builtin.Standard
 import Vehicle.Data.Code.BooleanExpr
 import Vehicle.Data.Code.ForcedValue
@@ -317,10 +318,10 @@ compileQuerySetPartitions globalCtx isPropertyNegated maybePartitions = case may
 topLevelUnblockingActions :: (Monad m) => UnblockingActions m
 topLevelUnblockingActions =
   UnblockingActions
-    { unblockRatTensorBoundVar = developerError "No bound variables should exist at top-level",
-      unblockRecordBoundVar = developerError "No bound variables should exist at top-level",
-      unblockNetworkApp = \_ _ _ -> developerError "Unblocking of constant network functions at top-level not yet supported",
-      unblockDatasetOrParameter = developerError "Should not be unblocking datasets or parameters"
+    { unblockRatTensorBoundVar = \_ _ -> developerError "No bound variables should exist at top-level",
+      unblockRecordBoundVar = \_ _ -> developerError "No bound variables should exist at top-level",
+      unblockNetworkApp = \_ _ ident args -> return $ IfLeaf $ Forced $ VFreeVar ident (mkExpr accessSpine args),
+      unblockDatasetOrParameter = \_ _ -> developerError "Should not be unblocking datasets or parameters"
     }
 
 handlePropertyCompileError ::

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

@@ -38,7 +38,7 @@ import Vehicle.Compile.Unblock qualified as Unblocking
 import Vehicle.Compile.Variable (createUserVar)
 import Vehicle.Data.Builtin.Interface
 import Vehicle.Data.Builtin.Standard
-import Vehicle.Data.Code.BooleanExpr (elimIfTree)
+import Vehicle.Data.Code.BooleanExpr (IfTree, elimIfTree)
 import Vehicle.Data.Code.ForcedValue
 import Vehicle.Data.Code.Interface
 import Vehicle.Data.MaybeTrivial
@@ -271,15 +271,16 @@ unblockingActions =
     { unblockRatTensorBoundVar = unblockQuantifiedBoundVar,
       unblockRecordBoundVar = unblockQuantifiedBoundVar,
       unblockNetworkApp = unblockNetworkApplication,
-      unblockDatasetOrParameter = unexpectedExprError "solver compilation" "dataset or parameter"
+      unblockDatasetOrParameter = \_ _ -> unexpectedExprError "solver compilation" "dataset or parameter"
     }
 
 unblockQuantifiedBoundVar ::
   (MonadQuantifierBody m) =>
+  TypeUnblockingFunction (Thunk Builtin) m ->
   Lv ->
-  m (Thunk Builtin)
-unblockQuantifiedBoundVar lv =
-  replaceTensorVariableWithStackedChildren (SliceVariable lv)
+  m (IfTree (Thunk Builtin) (Thunk Builtin))
+unblockQuantifiedBoundVar unblock lv =
+  unblock =<< replaceTensorVariableWithStackedChildren (SliceVariable lv)
 
 unblockNetworkApplication ::
   (MonadQuantifierBody m) =>

vehicle/src/Vehicle/Backend/Solver/UserVariableElimination/PurifyAssertion.hs

@@ -104,7 +104,7 @@ purifyBoundVar ::
   Lv ->
   PurifyFn m
 purifyBoundVar v actions@UnblockingActions {..} incrDims
-  | incrDims > 0 = purifyExpr actions incrDims =<< unblockRatTensorBoundVar v
+  | incrDims > 0 = unblockRatTensorBoundVar (purifyExpr actions incrDims) v
   | otherwise = return $ IfLeaf $ Forced $ VBoundVar v []
 
 purifyNetworkVar ::

vehicle/src/Vehicle/Compile/Error.hs

@@ -18,6 +18,7 @@ module Vehicle.Compile.Error
     UnboundedIndices,
     ParseLocation,
     MonadCompile,
+    BlockingReason (..),
     compilerDeveloperError,
     unsupportedTensorLikeQuantifier,
   )
@@ -230,7 +231,7 @@ data CompileError
   | UnsupportedLossOperation DeclProvenance (Doc Void)
   | UnableToLiftLogicFieldToTensors DifferentiableLogicID TensorDifferentiableLogicField (BooleanDifferentiableLogicField, Thunk Builtin) NamedBoundCtx (Thunk Builtin)
   | NoQuantifierDomainFound DeclProvenance (UnforcedBinder Builtin) (These (NonEmpty TensorIndices) (NonEmpty TensorIndices))
-  | UnorderableDifferentiableLogic DeclProvenance (ForcedValue Builtin)
+  | UnorderableDifferentiableLogic DeclProvenance (Thunk Builtin) (Either BlockingReason (ForcedValue Builtin))
   | -- ITP backend errors
     UnimplementedFeature Provenance (Doc Void)
   | UnusedMonomorphisableDeclaration Provenance Identifier
@@ -240,6 +241,12 @@ data CompileError
 
 deriving instance Show CompileError
 
+data BlockingReason
+  = BlockingNetwork Identifier
+  | BlockingDatasetOrParameter Identifier
+
+deriving instance Show BlockingReason
+
 --------------------------------------------------------------------------------
 -- Some useful developer errors
 

vehicle/src/Vehicle/Compile/Normalise/Core.hs

@@ -48,11 +48,11 @@ data EvalScheme meta builtin m
   | TypeClassOp
   | None
 
-class (Monad m, HasBuiltinConstructor expr thunk) => NormalisableExpr expr thunk builtin m | thunk -> expr where
+class (Monad m, HasBuiltinConstructor expr thunk, Show (expr builtin)) => NormalisableExpr expr thunk builtin m | thunk -> expr where
   force :: thunk builtin -> m (expr builtin)
   forceApp :: thunk builtin -> [GenericArg (thunk builtin)] -> m (expr builtin)
 
-instance (Monad m) => NormalisableExpr Expr Expr builtin m where
+instance (Monad m, Show builtin) => NormalisableExpr Expr Expr builtin m where
   force = return
   forceApp fun args = return $ normAppList fun args
 

vehicle/src/Vehicle/Compile/Normalise/Force.hs

@@ -112,7 +112,8 @@ instance
 
 -- Merge into `TypedEvalScheme`?
 instance
-  ( MonadNorm builtin m,
+  ( Show meta,
+    MonadNorm builtin m,
     TypedEvalScheme meta builtin m
   ) =>
   NormalisableExpr (GenericForcedValue meta) (GenericThunk meta) builtin m

vehicle/src/Vehicle/Compile/Print/Error.hs

@@ -983,7 +983,7 @@ formatCompileError = \case
           Just
             "declare the logic directly as a record literal."
       }
-  UnorderableDifferentiableLogic (ident, p) value ->
+  UnorderableDifferentiableLogic (ident, p) expr reason ->
     VehicleUserError
       { provenance = Just p,
         problem =
@@ -995,14 +995,21 @@ formatCompileError = \case
             <> line
             <> "in order to work out whether the loss should be maximised or minimised."
             <> line
-            <> "However, Vehicle was unable to establish the truth value of the result:"
-              <+> lineIndent (prettyFriendlyEmptyCtx value),
+            <> "However, Vehicle was unable to establish the truth value of"
+            <> lineIndent (prettyFriendlyEmptyCtx expr)
+            <> line
+            <> "because it could not evaluate" <+> case reason of
+              Right value ->
+                ":"
+                  <+> lineIndent (prettyFriendlyEmptyCtx value)
+              Left (BlockingDatasetOrParameter blockingIdent) -> quotePretty (nameOf blockingIdent)
+              Left (BlockingNetwork blockingIdent) -> quotePretty (nameOf blockingIdent),
         fix =
           Just $
             "ensure that the expression" <+> squotes comp <+> "evaluates to either `true` or `false`."
       }
     where
-      comp = pretty TruthityElement <+> "<=" <+> pretty FalsityElement
+      comp = pretty TruthityElement <+> "<" <+> pretty FalsityElement
 
 datasetDimensionsFix :: Doc a -> Identifier -> FilePath -> Doc a
 datasetDimensionsFix feature ident file =