Skip to content

Commit 7040e96

Browse files
laurenpudzpre-commit-ci[bot]MatthewDaggitt
authored
Use record information in compiler reporting (#1143)
* set up reporting and compilation step * back to existing functionality * basic functionality with hardcoded var name * add variable for quantified variable name * use hsep instead of vsep * Add tests, only counterexamle bar showing errors * fix/add comments * precommit * rearrange userVariableAssignmentType * update with dev and fix * restructure userVariableAssignment * Add type to bounds error * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci * reset tests * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci * format and update .plan files with compilation step * add comma between fields in bounds message * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci * refactor * make recordAssignment list and fields nonEmpty * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci * refactor bounds error * Minor refactorings --------- Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com> Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>
1 parent 085ba91 commit 7040e96

26 files changed

Lines changed: 356 additions & 91 deletions

File tree

‎ChangeLog.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,10 @@
1616
reduceOr e xs -> reduceOr xs (if 0D returns False)
1717
```
1818

19+
* Added new @tensor annotations that can be attached to record definitions. These allow tensors to be
20+
written as named records thereby avoiding the need to declare and use indices to reference rows of the
21+
tensor. See documentation for further details and see `examples/windController-newStyle` for a worked example.
22+
1923
* Added the operators:
2024
```
2125
^ : Tensor Real ds -> Real -> Tensor Real ds

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

Lines changed: 14 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -13,29 +13,25 @@ import Data.Maybe (maybeToList)
1313
import Data.Proxy (Proxy (..))
1414
import System.Directory (createDirectoryIfMissing)
1515
import Vehicle.Backend.Solver.QueryCompilation (compilePartitionsToQueries)
16-
import Vehicle.Backend.Solver.UserVariableElimination (eliminateExistless, eliminateExists)
16+
import Vehicle.Backend.Solver.UserVariableElimination (eliminateExistless, eliminateExists, eliminateExistsRecord)
1717
import Vehicle.Backend.Solver.UserVariableElimination.Core
1818
import Vehicle.Backend.Solver.UserVariableElimination.Error
1919
import Vehicle.Compile.Error
2020
import Vehicle.Compile.ExpandResources (expandResources)
2121
import Vehicle.Compile.ExpandResources.Core
2222
import Vehicle.Compile.LiftIf (unfoldIf)
23-
import Vehicle.Compile.LowerNot (lowerNot, negateRatTensorQuantifierBody)
23+
import Vehicle.Compile.LowerNot (lowerNot, negateRatTensorQuantifierBody, negateRecordQuantifierBody)
2424
import Vehicle.Compile.Normalise.NBE
25-
import Vehicle.Compile.Normalise.Quote
2625
import Vehicle.Compile.Prelude
2726
import Vehicle.Compile.Print (prettyFriendly, prettyFriendlyEmptyCtx)
2827
import Vehicle.Compile.Print.Warning ()
2928
import Vehicle.Compile.Property (traverseMultiProperty)
3029
import Vehicle.Compile.Unblock (UnblockingActions (..), unblockBoolExpr)
3130
import Vehicle.Data.Builtin.Standard
32-
import Vehicle.Data.Builtin.Standard.Scoping (constructFromTensorFreeVar, constructTensorisableDims)
3331
import Vehicle.Data.Code.BooleanExpr
34-
import Vehicle.Data.Code.DSL
3532
import Vehicle.Data.Code.Interface
3633
import Vehicle.Data.Code.TypedView
3734
import Vehicle.Data.Code.Value
38-
import Vehicle.Data.DSL
3935
import Vehicle.Data.MaybeTrivial (MaybeTrivial (..), andTrivial, orTrivial)
4036
import Vehicle.Data.Variable.Bound.Context.Name
4137
import Vehicle.Data.Variable.Bound.Context.Tensor
@@ -202,14 +198,16 @@ compileQueries expr = do
202198
-- Base cases --
203199
----------------
204200
VBoolLiteral b -> return $ Trivial b
205-
VQuantifyRatTensor (Exists, args) -> compileQuantifiedQuerySet False args
201+
VQuantifyRatTensor (Exists, args) -> compileQuantifiedQuerySet False (Left args)
202+
VQuantifyRecord (Exists, args) -> compileQuantifiedQuerySet False (Right args)
206203
VQuantifyRatTensor (Forall, args) -> do
207204
logDebug MaxDetail $ "negate" <+> pretty Forall
208205
negatedArgs <- negateRatTensorQuantifierBody args
209-
compileQuantifiedQuerySet True negatedArgs
210-
VQuantifyRecord (q, args) -> do
211-
wrappedBinderArgs <- wrapQuantifyRecord args
212-
compileQueries (fromBoolValue $ VQuantifyRatTensor (q, wrappedBinderArgs))
206+
compileQuantifiedQuerySet True (Left negatedArgs)
207+
VQuantifyRecord (Forall, args) -> do
208+
logDebug MaxDetail $ "negate" <+> pretty Forall
209+
negatedArgs <- negateRecordQuantifierBody args
210+
compileQuantifiedQuerySet True (Right negatedArgs)
213211
---------------------
214212
-- Recursive cases --
215213
---------------------
@@ -242,53 +240,16 @@ compileQueries expr = do
242240
compileQuantifiedQuerySet ::
243241
(MonadPropertyStructure m, MonadSupply QueryID m, MonadStdIO m, MonadError CompileError m) =>
244242
Bool ->
245-
QuantifyRatTensorArgs (Value Builtin) (Closure Builtin) ->
243+
Either (QuantifyRatTensorArgs (Value Builtin) (Closure Builtin)) (QuantifyRecordArgs (Value Builtin) (Closure Builtin)) ->
246244
m (Property QueryMetaData)
247245
compileQuantifiedQuerySet isPropertyNegated args =
248246
logCompilerSection2 MaxDetail "compilation of query set" $ do
249-
(maybePartitions, globalCtx) <- runStateT (eliminateExists args) emptyGlobalCtx
247+
let action = case args of
248+
Left tensorArgs -> eliminateExists tensorArgs
249+
Right recordArgs -> eliminateExistsRecord recordArgs
250+
(maybePartitions, globalCtx) <- runStateT action emptyGlobalCtx
250251
compileQuerySetPartitions globalCtx isPropertyNegated maybePartitions
251252

252-
-- | Takes a record quantifier and wraps the binder & body in a tensor quantifier
253-
-- e.g. given Pair has fields { a : Real, b : Real }
254-
-- forall (r : Pair) . (body)
255-
-- becomes
256-
-- forall (_t0 : tensor Real [2]) . (body (_PairFromTensor _t0))
257-
wrapQuantifyRecord ::
258-
( MonadPropertyStructure m,
259-
MonadSupply QueryID m,
260-
MonadStdIO m,
261-
MonadFreeContext Builtin m
262-
) =>
263-
QuantifyRecordArgs (Value Builtin) (Closure Builtin) ->
264-
m (QuantifyRatTensorArgs (Value Builtin) (Closure Builtin))
265-
wrapQuantifyRecord QuantifyRecordArgs {..} = do
266-
namedCtx <- getNameContext
267-
recordTypeIdent <- case toTypeValue quantifyRecordType of
268-
VFreeTypeVar v _spine -> pure v
269-
_ -> developerError "Record binder is not of expected format."
270-
271-
-- Construct \r -> body from binder and body in record quantifier args
272-
recordQLam <- unnormaliseInCtx $ VLam quantifyRecordBinder quantifyRecordBody
273-
fields <- getRecordFields recordTypeIdent
274-
let shape = constructTensorisableDims fields
275-
let dims = mkDims shape
276-
277-
-- Build tensor binder with appropriate dims and type for record
278-
let Closure boundEnv _body = quantifyRecordBody
279-
tensorType <- eval namedCtx boundEnv $ fromDSL mempty $ tTensor tRat (toDSL dims)
280-
normalisedDims <- eval namedCtx boundEnv dims
281-
let tensorBinder = mkExplicitBinder tensorType (Just (mempty, getFreshTensorBinderName namedCtx))
282-
283-
let tensorBoundVar = explicit $ BoundVar mempty 0
284-
recordTypeProv <- getRecordProvenance recordTypeIdent
285-
-- Construct _PairFromTensor _t0
286-
let fromTensorExpr = App (constructFromTensorFreeVar recordTypeIdent recordTypeProv) [tensorBoundVar]
287-
288-
-- Construct body (_PairFromTensor _t0)
289-
let nestedBody = App recordQLam [Arg Explicit Relevant fromTensorExpr]
290-
return $ QuantifyRatTensorArgs normalisedDims tensorBinder (Closure boundEnv nestedBody)
291-
292253
-- | We only need this because we can't evaluate networks in the compiler.
293254
compileUnquantifiedQuerySet ::
294255
(MonadPropertyStructure m, MonadSupply QueryID m, MonadStdIO m, MonadError CompileError m) =>

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

Lines changed: 65 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
{- HLINT ignore "Use fewer imports" -}
22
module Vehicle.Backend.Solver.UserVariableElimination
33
( eliminateExists,
4+
eliminateExistsRecord,
45
eliminateExistless,
6+
compileBoolExpr,
57
)
68
where
79

@@ -12,6 +14,7 @@ import Control.Monad.Except (MonadError (..))
1214
import Control.Monad.Reader (MonadReader (..), asks)
1315
import Control.Monad.State (MonadState (..))
1416
import Control.Monad.Writer (MonadWriter (..), WriterT (..))
17+
import Data.Map qualified as Map
1518
import Vehicle.Backend.Solver.UserVariableElimination.Core
1619
import Vehicle.Backend.Solver.UserVariableElimination.EliminateExists (eliminateQuantifiedVariable)
1720
import Vehicle.Backend.Solver.UserVariableElimination.LinearExpr (LinearityError (..), compileLinearAssertion)
@@ -22,6 +25,7 @@ import Vehicle.Compile.ExpandResources.Core (lookupNetworkInfo)
2225
import Vehicle.Compile.LiftIf (unfoldIf)
2326
import Vehicle.Compile.LowerNot (lowerNot)
2427
import Vehicle.Compile.Normalise.NBE
28+
import Vehicle.Compile.Normalise.Quote (unnormaliseInCtx)
2529
import Vehicle.Compile.Prelude
2630
import Vehicle.Compile.Print (prettyVerbose)
2731
import Vehicle.Compile.Resource
@@ -30,19 +34,77 @@ import Vehicle.Compile.Unblock qualified as Unblocking
3034
import Vehicle.Compile.Variable (createUserVar)
3135
import Vehicle.Data.Builtin.Interface.Normalise (evalAtTensor, unoptimisedEvalReduceAndTensor)
3236
import Vehicle.Data.Builtin.Standard
33-
import Vehicle.Data.Builtin.Standard.Scoping (constructFromTensorFreeVar, constructToTensorFreeVar)
37+
import Vehicle.Data.Builtin.Standard.Scoping (constructFromTensorFreeVar, constructTensorisableDims, constructToTensorFreeVar)
3438
import Vehicle.Data.Code.BooleanExpr (elimIfTree)
39+
import Vehicle.Data.Code.DSL
3540
import Vehicle.Data.Code.Interface
3641
import Vehicle.Data.Code.TypedView
3742
import Vehicle.Data.Code.Value
43+
import Vehicle.Data.DSL (fromDSL, toDSL)
3844
import Vehicle.Data.MaybeTrivial
39-
import Vehicle.Data.Variable.Bound.Context.Name (getNameContext, prettyFriendlyInCtx)
45+
import Vehicle.Data.Variable.Bound.Context.Name (getFreshTensorBinderName, getNameContext, prettyFriendlyInCtx)
4046
import Vehicle.Data.Variable.Bound.Context.Tensor (replaceTensorVariableWithStackedChildren)
4147
import Vehicle.Data.Variable.Bound.Level
48+
import Vehicle.Data.Variable.Free.Context (getRecordFieldNames, getRecordFields, getRecordProvenance)
4249
import Vehicle.Verify.Core
4350
import Vehicle.Verify.QueryFormat (QueryFormat (..), supportsStrictInequalities)
51+
import Vehicle.Verify.Specification (CompilationStep (..))
4452
import Prelude hiding (Applicative (..))
4553

54+
eliminateExistsRecord ::
55+
(MonadQueryStructure m) =>
56+
QuantifyRecordArgs (Value Builtin) (Closure Builtin) ->
57+
m (MaybeTrivial Partitions)
58+
eliminateExistsRecord args = do
59+
(wrappedBinderArgs, step) <- wrapQuantifyRecord args
60+
maybePartitions <- eliminateExists wrappedBinderArgs
61+
62+
return $ case maybePartitions of
63+
Trivial b -> Trivial b
64+
NonTrivial (Partitions m) ->
65+
NonTrivial (Partitions (Map.mapKeys ([step] ++) m))
66+
67+
-- | Takes a record quantifier and wraps the binder & body in a tensor quantifier
68+
-- e.g. given Pair has fields { a : Real, b : Real }
69+
-- forall (r : Pair) . (body)
70+
-- becomes
71+
-- forall (_t0 : tensor Real [2]) . (body (_PairFromTensor _t0))
72+
wrapQuantifyRecord ::
73+
(MonadQueryStructure m) =>
74+
QuantifyRecordArgs (Value Builtin) (Closure Builtin) ->
75+
m (QuantifyRatTensorArgs (Value Builtin) (Closure Builtin), CompilationStep)
76+
wrapQuantifyRecord QuantifyRecordArgs {..} = do
77+
namedCtx <- getNameContext
78+
recordTypeIdent <- case toTypeValue quantifyRecordType of
79+
VFreeTypeVar v _spine -> pure v
80+
_ -> developerError "Record binder is not of expected format."
81+
82+
-- Construct \r -> body from binder and body in record quantifier args
83+
recordQLam <- unnormaliseInCtx $ VLam quantifyRecordBinder quantifyRecordBody
84+
fields <- getRecordFields recordTypeIdent
85+
let shape = constructTensorisableDims fields
86+
let dims = mkDims shape
87+
88+
-- Build tensor binder with appropriate dims and type for record
89+
let Closure boundEnv _body = quantifyRecordBody
90+
tensorType <- eval namedCtx boundEnv $ fromDSL mempty $ tTensor tRat (toDSL dims)
91+
normalisedDims <- eval namedCtx boundEnv dims
92+
let tensorBinderName = getFreshTensorBinderName namedCtx
93+
let tensorBinder = mkExplicitBinder tensorType (Just (mempty, tensorBinderName))
94+
95+
let tensorBoundVar = explicit $ BoundVar mempty 0
96+
recordTypeProv <- getRecordProvenance recordTypeIdent
97+
-- Construct _PairFromTensor _t0
98+
let fromTensorExpr = App (constructFromTensorFreeVar recordTypeIdent recordTypeProv) [tensorBoundVar]
99+
100+
-- Construct body (_PairFromTensor _t0)
101+
let nestedBody = App recordQLam [Arg Explicit Relevant fromTensorExpr]
102+
let ratTensorArgs = QuantifyRatTensorArgs normalisedDims tensorBinder (Closure boundEnv nestedBody)
103+
104+
fieldNames <- getRecordFieldNames recordTypeIdent
105+
let name = getBinderName quantifyRecordBinder
106+
return (ratTensorArgs, ConvertQuantifiedTensorLike tensorBinderName name fieldNames)
107+
46108
eliminateExists ::
47109
(MonadQueryStructure m) =>
48110
QuantifyRatTensorArgs (Value Builtin) (Closure Builtin) ->
@@ -111,8 +173,7 @@ compileBoolExpr expr = do
111173
VAnd (TensorOp2Args _dims x y) -> andTrivial andPartitions <$> compileBoolExpr x <*> compileBoolExpr y
112174
VOr (TensorOp2Args _dims x y) -> orTrivial orPartitions <$> compileBoolExpr x <*> compileBoolExpr y
113175
VQuantifyRatTensor (Exists, args) -> eliminateExists args
114-
-- TODO: RECORD SUPPORT
115-
VQuantifyRecord (Exists, _args) -> compilerDeveloperError "Non top-level record quantifiers are not supported yet"
176+
VQuantifyRecord (Exists, args) -> eliminateExistsRecord args
116177
---------------------
117178
-- Recursive cases --
118179
---------------------

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

Lines changed: 38 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Control.Monad.Except (ExceptT, MonadError (..), runExceptT)
77
import Data.Bifunctor (Bifunctor (..))
88
import Data.Coerce (coerce)
99
import Data.Foldable (foldlM)
10+
import Data.List (delete)
1011
import Data.List.NonEmpty (NonEmpty (..))
1112
import Data.List.NonEmpty qualified as NonEmpty
1213
import Data.Map (Map)
@@ -20,7 +21,7 @@ import Vehicle.Compile.Print (prettyFriendly)
2021
import Vehicle.Data.Assertion (InequalityRelation (..))
2122
import Vehicle.Data.Bound
2223
import Vehicle.Data.Code.LinearExpr (LinearExpr, evaluateExpr)
23-
import Vehicle.Data.Tensor (RatTensor, at, mapTensor, shapeOf, stack, zipWithTensor, pattern ZeroDimTensor)
24+
import Vehicle.Data.Tensor (RatTensor, at, mapTensor, shapeOf, stack, unstack, zipWithTensor, pattern ZeroDimTensor)
2425
import Vehicle.Data.Variable.Bound.Context.Name.Core
2526
import Vehicle.Data.Variable.Bound.Level
2627
import Vehicle.Verify.Core
@@ -44,8 +45,34 @@ reconstructUserVars variables (Reconstruction steps) networkVariableAssignment =
4445
let assignment = createInitialAssignment queryVariableMap networkVariableAssignment
4546
alteredAssignment <- foldlM (applyReconstructionStep vehicleVariableCtx) assignment steps
4647
finalAssignment <- createFinalAssignment vehicleVariableCtx userVariables alteredAssignment
47-
logDebug MidDetail $ "User variables:" <> lineIndent (pretty finalAssignment)
48-
return finalAssignment
48+
recordSubstAssignment <- reconstructRecords finalAssignment steps
49+
logDebug MidDetail $ "User variables:" <> lineIndent (pretty recordSubstAssignment)
50+
return recordSubstAssignment
51+
52+
reconstructRecords ::
53+
(MonadLogger m) =>
54+
UserVariableAssignment ->
55+
[CompilationStep] ->
56+
m UserVariableAssignment
57+
reconstructRecords existingAssignment steps = do
58+
foldlM checkStep existingAssignment steps
59+
where
60+
checkStep (UserVariableAssignment assignments) step = do
61+
case step of
62+
ConvertQuantifiedTensorLike tensorName recordName fieldNames -> do
63+
tensorValues <- case Map.lookup tensorName (Map.fromList assignments) of
64+
Just (TensorValue v) -> pure v
65+
_ -> developerError "No assignment found"
66+
tensorIndices <- case NonEmpty.nonEmpty (unstack tensorValues) of
67+
Just xs -> pure xs
68+
_ -> developerError "Values must be present for tensor assignment"
69+
70+
let fields = NonEmpty.zip fieldNames tensorIndices
71+
let assignment = (recordName, RecordValue fields)
72+
let newMap = delete (tensorName, TensorValue tensorValues) assignments ++ [assignment]
73+
74+
return $ UserVariableAssignment newMap
75+
_ -> return $ UserVariableAssignment assignments
4976

5077
--------------------------------------------------------------------------------
5178
-- Mixed variable assignments
@@ -81,6 +108,13 @@ applyReconstructionStep ctx assignment step = do
81108
SolveEquality nestedVar eq -> reconstructTensorViaEquality nestedVar eq
82109
SolveInequalities var solution -> reconstructRationalViaFourierMotzkin var solution
83110
ReconstructTensorVariable var depth -> reconstructTensorFromConstituents ctx var depth
111+
-- do nothing if we have convertTensorLike
112+
-- TODO: this is not nice at all, maybe we need to store the compilationStep
113+
-- differently or convert a different way?
114+
ConvertQuantifiedTensorLike {} -> \varAssignment ->
115+
case NonEmpty.nonEmpty (Map.toList varAssignment) of
116+
Just a -> pure a
117+
Nothing -> developerError "Variable assignment list should not be empty"
84118
newValues <- handleMissingError ctx (errorOrValueFn assignment)
85119

86120
logDebugM MidDetail $ do
@@ -209,7 +243,7 @@ createFinalAssignment ::
209243
m UserVariableAssignment
210244
createFinalAssignment vehicleVariables userVariables assignment = do
211245
let userVariableValues = mapMaybe isUserVar $ Map.toList assignment
212-
return $ UserVariableAssignment userVariableValues
246+
return $ UserVariableAssignment (map (second TensorValue) userVariableValues)
213247
where
214248
isUserVar :: (SliceVariable, RatTensor) -> Maybe (Name, RatTensor)
215249
isUserVar (var, value) =

‎vehicle/src/Vehicle/Compile/ExpandResources/Network.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ module Vehicle.Compile.ExpandResources.Network
44
where
55

66
import Control.Monad.Except (MonadError (..))
7+
import Data.List.NonEmpty qualified as NonEmpty
78
import Data.Map qualified as Map
89
import Vehicle.Compile.Error
910
import Vehicle.Compile.ExpandResources.Core
@@ -62,7 +63,7 @@ getNetworkType decl networkType = case normalised networkType of
6263
fieldNames <- getRecordFieldNames ident
6364
fields <- getRecordFields ident
6465
let shape = constructTensorisableDims fields
65-
return $ RecordIOType $ NetworkRecordType NetworkRatType ident shape fieldNames
66+
return $ RecordIOType $ NetworkRecordType NetworkRatType ident shape $ NonEmpty.toList fieldNames
6667
_ -> typingError
6768

6869
tensorDimensions :: InputOrOutput -> VType Builtin -> m TensorShape

‎vehicle/src/Vehicle/Compile/LowerNot.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
module Vehicle.Compile.LowerNot
22
( lowerNot,
33
negateRatTensorQuantifierBody,
4+
negateRecordQuantifierBody,
45
)
56
where
67

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -617,6 +617,8 @@ instance
617617
prettyUsing @restVar (toSliceVar var, ctx)
618618
<+> "->"
619619
<+> pretty d
620+
ConvertQuantifiedTensorLike _tensorName recordName _fields ->
621+
"Convert" <+> pretty recordName <+> "to record"
620622

621623
instance
622624
(PrettyUsing restVar (variable `In` ctx)) =>

0 commit comments

Comments
 (0)