diff --git a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Error.hs b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Error.hs index 029085e46..9e8873ac5 100644 --- a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Error.hs +++ b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Error.hs @@ -88,7 +88,6 @@ instance Exception ProducedFilesError handleProducedFilesError :: ProducedFilesError -> IO Result handleProducedFilesError ProducedFilesError {..} = do - print stdoutDiff let message = unlines . catMaybes $ [ case stderrDiff of diff --git a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs index cf2b66d0e..09360202b 100644 --- a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs +++ b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs @@ -412,8 +412,6 @@ acceptTestProduced testProduces (IgnoreFiles testIgnores) = do NonEmpty.prependList otherTestSpecsBefore $ NonEmpty.appendList (NonEmpty.singleton acceptTestSpec) otherTestSpecsAfter - liftIO $ putStrLn "Hi2" - liftIO $ print acceptTestSpecsList let acceptTestSpecs = TestSpecs acceptTestSpecsList lift $ writeTestSpecsFile (testDirectory testSpecsFileName) acceptTestSpecs -- Remove the outdated .golden files: diff --git a/vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs b/vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs index 1120eb4d3..17c21c267 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs @@ -75,6 +75,7 @@ instance NoThunks MetaID -- Vehicle.Syntax.AST.Name instance NoThunks Module +instance NoThunks ModulePath instance NoThunks Identifier -- Vehicle.Syntax.AST.Prog diff --git a/vehicle-syntax/src/Vehicle/Syntax/AST/Name.hs b/vehicle-syntax/src/Vehicle/Syntax/AST/Name.hs index 982288ad9..6ae49ce1b 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/AST/Name.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/AST/Name.hs @@ -7,7 +7,7 @@ import Data.Serialize (Serialize) import Data.Serialize.Text () import Data.Text (Text) import GHC.Generics (Generic) -import Prettyprinter (Pretty (..)) +import Prettyprinter (Pretty (..), concatWith, dot, surround) -------------------------------------------------------------------------------- -- Definition @@ -20,6 +20,7 @@ type Name = Text data Module = User | StdLib + | Record Name deriving (Eq, Ord, Show, Generic) instance NFData Module @@ -36,15 +37,37 @@ instance Pretty Module where pretty = \case User -> "User" StdLib -> "StdLib" + Record name -> pretty name + +newtype ModulePath = ModulePath + { modules :: [Module] + } + deriving (Eq, Ord, Show, Generic) + +instance NFData ModulePath + +instance Hashable ModulePath + +instance ToJSON ModulePath + +instance FromJSON ModulePath + +instance Serialize ModulePath + +instance Pretty ModulePath where + pretty (ModulePath m) = concatWith (surround dot) (fmap pretty m) -------------------------------------------------------------------------------- -- Identifiers -data Identifier = Identifier Module Name +data Identifier = Identifier + { modulePath :: ModulePath, + identifierName :: Name + } deriving (Eq, Ord, Show, Generic) instance Pretty Identifier where - pretty (Identifier m s) = pretty m <> "." <> pretty s + pretty (Identifier m s) = pretty m <> dot <> pretty s instance NFData Identifier @@ -61,11 +84,14 @@ instance Serialize Identifier class HasIdentifier a where identifierOf :: a -> Identifier -moduleOf :: Identifier -> Module -moduleOf (Identifier m _) = m +stdlibIdentifier :: Name -> Identifier +stdlibIdentifier = Identifier (ModulePath [StdLib]) + +isUserIdent :: Identifier -> Bool +isUserIdent ident = User `elem` modules (modulePath ident) -identifierName :: Identifier -> Name -identifierName (Identifier _ n) = n +changeName :: Identifier -> Name -> Identifier +changeName Identifier {..} newName = Identifier {identifierName = newName, ..} -------------------------------------------------------------------------------- -- Names diff --git a/vehicle-syntax/src/Vehicle/Syntax/AST/Provenance.hs b/vehicle-syntax/src/Vehicle/Syntax/AST/Provenance.hs index 12bfab0ba..e1f41c3c3 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/AST/Provenance.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/AST/Provenance.hs @@ -18,8 +18,8 @@ import Data.List.NonEmpty (NonEmpty) import Data.List.NonEmpty qualified as NonEmpty import Data.Serialize (Serialize) import GHC.Generics (Generic (..)) -import Prettyprinter (Pretty (..), (<+>)) -import Vehicle.Syntax.AST.Name (Module (..)) +import Prettyprinter (Pretty (..), squotes, (<+>)) +import System.FilePath (takeFileName) import Vehicle.Syntax.Parse.Token -------------------------------------------------------------------------------- @@ -96,10 +96,13 @@ expandRange (l, r) (Range {..}) = data Provenance = Provenance { range :: Range, - modul :: Module + file :: FilePath } deriving (Generic) +noProvenance :: Provenance +noProvenance = Provenance mempty "unknown" + instance Show Provenance where show = const "" @@ -114,9 +117,19 @@ instance Hashable Provenance where instance Serialize Provenance +instance Pretty Provenance where + pretty (Provenance origin file) = "file" <+> squotes (pretty (takeFileName file)) <+> "at" <+> pretty origin + +instance Semigroup Provenance where + Provenance origin1 owner1 <> Provenance origin2 _owner2 = + Provenance (origin1 <> origin2) owner1 + +instance Monoid Provenance where + mempty = noProvenance + -- | Get the provenance for a single token. -tkProvenance :: (IsToken a) => Module -> a -> Provenance -tkProvenance modl tk = Provenance (Range start end) modl +tkProvenance :: (IsToken a) => a -> FilePath -> Provenance +tkProvenance tk = Provenance (Range start end) where start = tkPosition tk end = Position (posLine start) (posColumn start + tkLength tk) @@ -126,7 +139,7 @@ fillInProvenance provenances = do let (starts, ends) = NonEmpty.unzip (fmap getPositions provenances) let start = minimum starts let end = maximum ends - Provenance (Range start end) (modul $ NonEmpty.head provenances) + Provenance (Range start end) (file $ NonEmpty.head provenances) where getPositions :: Provenance -> (Position, Position) getPositions (Provenance (Range start end) _) = (start, end) @@ -134,21 +147,6 @@ fillInProvenance provenances = do expandProvenance :: (Int, Int) -> Provenance -> Provenance expandProvenance w (Provenance range o) = Provenance (expandRange w range) o -instance Pretty Provenance where - pretty (Provenance origin modl) = case modl of - User -> pretty origin - StdLib -> pretty modl <> "," <+> pretty origin - -instance Semigroup Provenance where - Provenance origin1 owner1 <> Provenance origin2 _owner2 = - Provenance (origin1 <> origin2) owner1 - -noProvenance :: Provenance -noProvenance = Provenance mempty User - -instance Monoid Provenance where - mempty = Provenance mempty User - -------------------------------------------------------------------------------- -- Type-classes diff --git a/vehicle-syntax/src/Vehicle/Syntax/BNFC/Elaborate/External.hs b/vehicle-syntax/src/Vehicle/Syntax/BNFC/Elaborate/External.hs index 2c1861094..d8615eba6 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/BNFC/Elaborate/External.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/BNFC/Elaborate/External.hs @@ -12,7 +12,7 @@ where import Control.Monad (foldM_) import Control.Monad.Except (MonadError (..), throwError) -import Control.Monad.Reader (MonadReader (..), runReaderT) +import Control.Monad.Reader (runReaderT) import Data.Bitraversable (bitraverse) import Data.Either (partitionEithers) import Data.List (find) @@ -28,6 +28,8 @@ import Prettyprinter import Vehicle.Syntax.AST qualified as V import Vehicle.Syntax.BNFC.Utils ( MonadElab, + ParseLocation, + getModule, mkProvenance, tokArrow, tokDot, @@ -61,10 +63,10 @@ newtype UnparsedExpr = UnparsedExpr B.Expr -- types and definitions. partiallyElabProg :: (MonadError ParseError m) => - V.Module -> + ParseLocation -> B.Prog -> m PartiallyParsedProg -partiallyElabProg modl (B.Main decls) = flip runReaderT modl $ do +partiallyElabProg file (B.Main decls) = flip runReaderT file $ do V.Main <$> partiallyElabDecls decls partiallyElabDecls :: (MonadElab m) => [B.Decl] -> m [PartiallyParsedDecl] @@ -303,10 +305,10 @@ getTypeOption = \case elaborateDecl :: (MonadError ParseError m) => - V.Module -> + ParseLocation -> PartiallyParsedDecl -> m (V.Decl V.Name V.Builtin) -elaborateDecl modl decl = flip runReaderT modl $ case decl of +elaborateDecl file decl = flip runReaderT file $ case decl of V.DefAbstract p n r t -> V.DefAbstract p n r <$> elabDeclType t V.DefFunction p n b t e -> V.DefFunction p n b <$> elabDeclType t <*> elabDeclBody e @@ -330,10 +332,10 @@ elabDeclBody (UnparsedExpr expr) = case expr of elaborateExpr :: (MonadError ParseError m) => - V.Module -> + ParseLocation -> UnparsedExpr -> m (V.Expr V.Name V.Builtin) -elaborateExpr modl (UnparsedExpr expr) = runReaderT (elabExpr expr) modl +elaborateExpr file (UnparsedExpr expr) = runReaderT (elabExpr expr) file elabExpr :: (MonadElab m) => B.Expr -> m (V.Expr V.Name V.Builtin) elabExpr = \case @@ -391,7 +393,7 @@ elabExpr = \case B.HasMap tk -> builtinTypeClass V.HasMap tk [] B.HasFold tk -> builtinTypeClass V.HasFold tk [] -- NOTE: we reverse the arguments to make it well-typed. - B.Ann e tk t -> freeVar (V.Identifier V.StdLib "typeAnn") tk [t, e] + B.Ann e tk t -> elabExpr (B.App (B.App (B.Var (B.Name (tkLocation tk, "typeAnn"))) (B.ExplicitArg t)) (B.ExplicitArg e)) elabArg :: (MonadElab m) => B.Arg -> m (V.Arg V.Name V.Builtin) elabArg = \case @@ -401,7 +403,7 @@ elabArg = \case elabName :: (MonadElab m) => B.Name -> m V.Identifier elabName n = do - modl <- ask + modl <- getModule return $ V.Identifier modl $ tkSymbol n elabBasicBinder :: (MonadElab m) => Bool -> B.BasicBinder -> m (V.Binder V.Name V.Builtin) @@ -493,11 +495,6 @@ op2 mk t e1 e2 = do let p = V.fillInProvenance (tProv :| [V.provenanceOf ce1, V.provenanceOf ce2]) return $ mk p ce1 ce2 -freeVar :: (MonadElab m, IsToken token) => V.Identifier -> token -> [B.Expr] -> m (V.Expr V.Name V.Builtin) -freeVar b t args = do - tProv <- mkProvenance t - app (V.FreeVar tProv b) <$> traverse elabExpr args - builtin :: (MonadElab m, IsToken token) => V.Builtin -> token -> [B.Expr] -> m (V.Expr V.Name V.Builtin) builtin b t args = do tProv <- mkProvenance t @@ -603,9 +600,9 @@ elabQuantifierIn :: m (V.Expr V.Name V.Builtin) elabQuantifierIn tk q binder container body = do p <- mkProvenance tk - let quantBuiltin = V.FreeVar p $ case q of - V.Forall -> V.Identifier V.StdLib "forallIn" - V.Exists -> V.Identifier V.StdLib "existsIn" + let quantBuiltin = V.BoundVar p $ case q of + V.Forall -> "forallIn" + V.Exists -> "existsIn" binder' <- elabNameBinder False binder container' <- elabExpr container @@ -627,7 +624,7 @@ elabForeach :: m (V.Expr V.Name V.Builtin) elabForeach tk binder body = do p <- mkProvenance tk - let foreachBuiltin = V.FreeVar p (V.Identifier V.StdLib "foreachIndex") + let foreachBuiltin = V.BoundVar p "foreachIndex" binder' <- elabNameBinder False binder body' <- elabExpr body diff --git a/vehicle-syntax/src/Vehicle/Syntax/BNFC/Utils.hs b/vehicle-syntax/src/Vehicle/Syntax/BNFC/Utils.hs index a116598b3..649a02e35 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/BNFC/Utils.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/BNFC/Utils.hs @@ -3,9 +3,9 @@ module Vehicle.Syntax.BNFC.Utils where import Control.Monad.Except (MonadError) -import Control.Monad.Reader (MonadReader (..)) +import Control.Monad.Reader (MonadReader (..), asks) import Data.Text (Text, pack) -import Vehicle.Syntax.AST.Name (Module) +import Vehicle.Syntax.AST.Name (ModulePath) import Vehicle.Syntax.AST.Provenance import Vehicle.Syntax.External.Abs qualified as B import Vehicle.Syntax.Parse.Error (ParseError (..)) @@ -13,16 +13,22 @@ import Vehicle.Syntax.Parse.Token (IsToken, mkToken) type MonadElab m = ( MonadError ParseError m, - MonadReader Module m + MonadReader ParseLocation m ) pattern InferableOption :: Text pattern InferableOption = "infer" +type ParseLocation = (ModulePath, FilePath) + +getModule :: (MonadElab m) => m ModulePath +getModule = asks fst + +getFile :: (MonadElab m) => m FilePath +getFile = asks snd + mkProvenance :: (MonadElab m, IsToken tk) => tk -> m Provenance -mkProvenance tk = do - modl <- ask - return $ tkProvenance modl tk +mkProvenance tk = tkProvenance tk <$> getFile tokType :: Int -> B.Expr tokType l = B.Type (mkToken B.TokType ("Type" <> pack (show l))) diff --git a/vehicle-syntax/src/Vehicle/Syntax/Parse.hs b/vehicle-syntax/src/Vehicle/Syntax/Parse.hs index 9c829ed47..51b1f009d 100644 --- a/vehicle-syntax/src/Vehicle/Syntax/Parse.hs +++ b/vehicle-syntax/src/Vehicle/Syntax/Parse.hs @@ -3,6 +3,7 @@ module Vehicle.Syntax.Parse UnparsedExpr, PartiallyParsedProg, PartiallyParsedDecl, + ParseLocation, readAndParseProg, parseDecl, parseExpr, @@ -14,6 +15,7 @@ import Control.Monad.Except (MonadError (..)) import Data.Text (Text) import Vehicle.Syntax.AST import Vehicle.Syntax.BNFC.Elaborate.External +import Vehicle.Syntax.BNFC.Utils (ParseLocation) import Vehicle.Syntax.Builtin import Vehicle.Syntax.External.Abs qualified as External (Expr, Prog) import Vehicle.Syntax.External.Layout as External (resolveLayout) @@ -24,14 +26,14 @@ import Vehicle.Syntax.Parse.Error (ParseError (..)) -------------------------------------------------------------------------------- -- Interface -readAndParseProg :: (MonadError ParseError m) => Module -> Text -> m PartiallyParsedProg +readAndParseProg :: (MonadError ParseError m) => ParseLocation -> Text -> m PartiallyParsedProg readAndParseProg modul txt = castBNFCError (partiallyElabProg modul) (parseExternalProg txt) -parseDecl :: (MonadError ParseError m) => Module -> PartiallyParsedDecl -> m (Decl Name Builtin) +parseDecl :: (MonadError ParseError m) => ParseLocation -> PartiallyParsedDecl -> m (Decl Name Builtin) parseDecl = elaborateDecl -parseExpr :: (MonadError ParseError m) => Module -> UnparsedExpr -> m (Expr Name Builtin) +parseExpr :: (MonadError ParseError m) => ParseLocation -> UnparsedExpr -> m (Expr Name Builtin) parseExpr = elaborateExpr readExpr :: (MonadError ParseError m) => Text -> m UnparsedExpr diff --git a/vehicle-syntax/vehicle-syntax.cabal b/vehicle-syntax/vehicle-syntax.cabal index 0370d65b0..8afcb3b82 100644 --- a/vehicle-syntax/vehicle-syntax.cabal +++ b/vehicle-syntax/vehicle-syntax.cabal @@ -166,6 +166,7 @@ library , cereal-text >=0.1 && <1 , containers >=0.5 && <1 , deepseq >=1.4 && <2 + , filepath >=1.4 && <2 , hashable >=1.3 && <2 , mtl >=2.2 && <3 , prettyprinter >=1.7 && <2 diff --git a/vehicle/src/Vehicle/Backend/Agda/Compile.hs b/vehicle/src/Vehicle/Backend/Agda/Compile.hs index e36c2e8d6..582bb0c52 100644 --- a/vehicle/src/Vehicle/Backend/Agda/Compile.hs +++ b/vehicle/src/Vehicle/Backend/Agda/Compile.hs @@ -911,7 +911,7 @@ pattern TensorType :: Expr Name Builtin pattern TensorType p tElem tDims <- App - (FreeVar p (Identifier StdLib "Tensor")) + (FreeVar p TensorIdent) [ RelevantExplicitArg _ tElem, IrrelevantExplicitArg _ tDims ] diff --git a/vehicle/src/Vehicle/Backend/LossFunction/TensorCompilation.hs b/vehicle/src/Vehicle/Backend/LossFunction/TensorCompilation.hs index ff022b39b..2f9299af3 100644 --- a/vehicle/src/Vehicle/Backend/LossFunction/TensorCompilation.hs +++ b/vehicle/src/Vehicle/Backend/LossFunction/TensorCompilation.hs @@ -25,7 +25,7 @@ import Vehicle.Data.Builtin.Tensor (TensorBuiltin) import Vehicle.Data.Builtin.Tensor qualified as T import Vehicle.Data.Expr.Normalised import Vehicle.Data.Tensor -import Vehicle.Libraries.StandardLibrary.Definitions (StdLibFunction (StdForeachIndex)) +import Vehicle.Libraries.StandardLibrary.Definitions (StdLibFunction (StdForeachIndex), pattern TensorIdent) import Vehicle.Prelude.Warning import Vehicle.Syntax.Builtin @@ -195,7 +195,7 @@ convertVectorType = \case Nothing -> do declProv <- getDeclProvenance boundCtx <- getNamedBoundCtx (Proxy @MixedLossValue) - let vecType = VFreeVar (Identifier User "Vector") [Arg mempty Explicit Relevant elemType, Arg mempty Explicit Relevant size] + let vecType = VFreeVar TensorIdent [Arg mempty Explicit Relevant elemType, Arg mempty Explicit Relevant size] throwError $ HigherOrderVectors declProv boundCtx vecType elemType _ -> unexpectedExprError currentPass "Vector has incorrect number of arguments" diff --git a/vehicle/src/Vehicle/Compile/Dependency.hs b/vehicle/src/Vehicle/Compile/Dependency.hs index 2d3e2d236..8fe4c889f 100644 --- a/vehicle/src/Vehicle/Compile/Dependency.hs +++ b/vehicle/src/Vehicle/Compile/Dependency.hs @@ -90,7 +90,7 @@ analyseDependenciesAndPrune prog declarationsToCompile = do else do dependencyGraph <- constructGraph prog startingVertices <- forM declarationsToCompile $ \name -> - case vertexFromIdent dependencyGraph (Identifier User name) of + case vertexFromIdent dependencyGraph (Identifier (ModulePath [User]) name) of Just vertex -> return vertex Nothing -> throwError $ MissingPrunedName name diff --git a/vehicle/src/Vehicle/Compile/Error.hs b/vehicle/src/Vehicle/Compile/Error.hs index 688e0c58e..0c07765c1 100644 --- a/vehicle/src/Vehicle/Compile/Error.hs +++ b/vehicle/src/Vehicle/Compile/Error.hs @@ -20,7 +20,7 @@ import Vehicle.Data.Builtin.Tensor import Vehicle.Data.DeBruijn import Vehicle.Data.Expr.Normalised import Vehicle.Data.QuantifiedVariable (UnderConstrainedVariableStatus, UserRationalVariable) -import Vehicle.Syntax.Parse (ParseError) +import Vehicle.Syntax.Parse (ParseError, ParseLocation) import Vehicle.Verify.QueryFormat.Core -------------------------------------------------------------------------------- @@ -37,8 +37,8 @@ type MonadCompile m = data CompileError = DevError (Doc ()) | -- Parse errors - ParseError Module ParseError - | -- Scope checking errors. + ParseError ParseLocation ParseError + | -- Errors thrown by scope checking. UnboundName Provenance Name | DeclarationDeclarationShadowing Provenance Name Identifier | DeclarationBoundShadowing Provenance Name diff --git a/vehicle/src/Vehicle/Compile/Monomorphisation.hs b/vehicle/src/Vehicle/Compile/Monomorphisation.hs index 4fed3c58d..def032e6d 100644 --- a/vehicle/src/Vehicle/Compile/Monomorphisation.hs +++ b/vehicle/src/Vehicle/Compile/Monomorphisation.hs @@ -156,7 +156,7 @@ performMonomorphisation :: performMonomorphisation (p, ident, anns, typ, body) createNewName args = do newIdent <- if createNewName - then Identifier (moduleOf ident) <$> getMonomorphisedName (nameOf ident) args + then changeName ident <$> getMonomorphisedName (nameOf ident) args else return ident (newType, newBody) <- substituteArgsThrough (typ, body, args) tell (Map.singleton (ident, args) newIdent) @@ -278,7 +278,7 @@ removeLiteralCoercions nameJoiner (Main ds) = getVectorCoercion :: Identifier -> Maybe StdLibFunction getVectorCoercion ident = do let typeJoiner = getTypeJoiner nameJoiner - let shortIdent = Identifier (moduleOf ident) $ fst $ Text.breakOn typeJoiner (nameOf ident) + let shortIdent = changeName ident $ fst $ Text.breakOn typeJoiner (nameOf ident) findStdLibFunction shortIdent updateBuiltin :: Decl Ix Builtin -> BuiltinUpdate m Ix Builtin Builtin diff --git a/vehicle/src/Vehicle/Compile/Print/Error.hs b/vehicle/src/Vehicle/Compile/Print/Error.hs index 3a04dc5cc..7fe86916d 100644 --- a/vehicle/src/Vehicle/Compile/Print/Error.hs +++ b/vehicle/src/Vehicle/Compile/Print/Error.hs @@ -52,7 +52,7 @@ data VehicleError instance Pretty VehicleError where pretty (UError (UserError p prob probFix)) = unAnnotate $ - "Error at" + "Error in" <+> pretty p <> ":" <+> prob @@ -1090,24 +1090,24 @@ instance MeaningfulError CompileError where Left err -> errorInSubsystemMessage "locate the original source of the non-linearity" err Right source -> case source of LinearTimesLinear opProv lhs rhs -> - "In particular the multiplication at" + "In particular the multiplication in" <+> pretty opProv <+> "involves" <> prettyLinearityProvenance lhs "left hand side of the multiplication" <> "and" <> prettyLinearityProvenance rhs "right hand side of the multiplication" DivideByLinear opProv rhs -> - "In particular the division at" + "In particular the division in" <+> pretty opProv <+> "involves" <> prettyLinearityProvenance rhs "denominator of the division" PowLinearBase opProv lhs -> - "In particular the power at" + "In particular the power in" <+> pretty opProv <+> "involves" <> prettyLinearityProvenance lhs "base of the power" PowLinearExponent opProv lhs -> - "In particular the power at" + "In particular the power in" <+> pretty opProv <+> "involves" <> prettyLinearityProvenance lhs "exponent of the power" @@ -1319,7 +1319,7 @@ prettyPolarityProvenance topQuantifierProv topQuantifier bottomQuantifierProvena go :: Quantifier -> PolarityProvenance -> [Doc a] go q = \case QuantifierProvenance p -> - ["the inner quantifier is the" <+> quotePretty q <+> "located at" <+> pretty p] + ["the inner quantifier is the" <+> quotePretty q <+> "located in" <+> pretty p] NegateProvenance p pp -> transform p ("the" <+> quotePretty Not) : go (neg q) pp LHSImpliesProvenance p pp -> @@ -1330,7 +1330,7 @@ prettyPolarityProvenance topQuantifierProv topQuantifier bottomQuantifierProvena surround p (prettyAuxiliaryFunctionProvenance position) : go q pp where surround p x = - "which is" <+> x <+> "at" <+> pretty p + "which is" <+> x <+> "in" <+> pretty p transform p x = surround p ("turned into" <+> prettyQuantifierArticle q <+> "by" <+> x) @@ -1339,7 +1339,7 @@ prettyPolarityProvenance topQuantifierProv topQuantifier bottomQuantifierProvena finalLine = "which alternates with the outer" <+> quotePretty topQuantifier - <+> "at" + <+> "in" <+> pretty topQuantifierProv prettyLinearityProvenance :: forall a. LinearityProvenance -> Doc a -> Doc a @@ -1349,11 +1349,11 @@ prettyLinearityProvenance lp location = go :: LinearityProvenance -> [Doc a] go = \case QuantifiedVariableProvenance p v -> - ["the quantified variable" <+> quotePretty v <+> "introduced at" <+> pretty p] + ["the quantified variable" <+> quotePretty v <+> "introduced in" <+> pretty p] NetworkOutputProvenance p networkName -> - ["the output of network" <+> squotes (pretty networkName) <+> "at" <+> pretty p] + ["the output of network" <+> squotes (pretty networkName) <+> "in" <+> pretty p] LinFunctionProvenance p pp position -> - (prettyAuxiliaryFunctionProvenance position <+> "at" <+> pretty p) : go pp + (prettyAuxiliaryFunctionProvenance position <+> "in" <+> pretty p) : go pp finalLine :: Doc a finalLine = "which is used in the" <+> location diff --git a/vehicle/src/Vehicle/Compile/Simplify.hs b/vehicle/src/Vehicle/Compile/Simplify.hs index 5cd810355..62d486358 100644 --- a/vehicle/src/Vehicle/Compile/Simplify.hs +++ b/vehicle/src/Vehicle/Compile/Simplify.hs @@ -54,7 +54,7 @@ instance Simplify (Expr Name Builtin) where normAppList (Builtin p (BuiltinConstructor (LVec n))) [ firstArg, - Arg p Explicit Relevant (FreeVar p (Identifier StdLib ("<" <> n2 <> " more>"))), + Arg p Explicit Relevant (FreeVar p (stdlibIdentifier ("<" <> n2 <> " more>"))), lastArg ] where diff --git a/vehicle/src/Vehicle/Compile/Type.hs b/vehicle/src/Vehicle/Compile/Type.hs index ac4cedbf9..397189927 100644 --- a/vehicle/src/Vehicle/Compile/Type.hs +++ b/vehicle/src/Vehicle/Compile/Type.hs @@ -154,7 +154,7 @@ typeCheckFunction p ident anns typ body = do else do -- Otherwise if not a property then generalise over unsolved meta-variables. checkedDecl1 <- - if moduleOf ident == User + if isUserIdent ident then addAuxiliaryInputOutputConstraints substDecl else return substDecl logUnsolvedUnknowns (Just substDecl) Nothing diff --git a/vehicle/src/Vehicle/Data/Builtin/Linearity/Core.hs b/vehicle/src/Vehicle/Data/Builtin/Linearity/Core.hs index 8da122dfc..4d3945046 100644 --- a/vehicle/src/Vehicle/Data/Builtin/Linearity/Core.hs +++ b/vehicle/src/Vehicle/Data/Builtin/Linearity/Core.hs @@ -159,7 +159,7 @@ instance ConvertableBuiltin LinearityBuiltin S.Builtin where convertBuiltin p = \case BuiltinConstructor c -> Builtin p (S.BuiltinConstructor c) BuiltinFunction f -> Builtin p (S.BuiltinFunction f) - b -> FreeVar p $ Identifier StdLib (layoutAsText $ pretty b) + b -> FreeVar p $ stdlibIdentifier (layoutAsText $ pretty b) instance PrintableBuiltin LinearityBuiltin where isCoercion = const False diff --git a/vehicle/src/Vehicle/Data/Builtin/Polarity/Core.hs b/vehicle/src/Vehicle/Data/Builtin/Polarity/Core.hs index d2500cc24..d2e02321e 100644 --- a/vehicle/src/Vehicle/Data/Builtin/Polarity/Core.hs +++ b/vehicle/src/Vehicle/Data/Builtin/Polarity/Core.hs @@ -169,7 +169,7 @@ instance ConvertableBuiltin PolarityBuiltin S.Builtin where convertBuiltin p = \case BuiltinConstructor c -> Builtin p (S.BuiltinConstructor c) BuiltinFunction f -> Builtin p (S.BuiltinFunction f) - b -> FreeVar p $ Identifier StdLib (layoutAsText $ pretty b) + b -> FreeVar p $ stdlibIdentifier (layoutAsText $ pretty b) instance PrintableBuiltin PolarityBuiltin where isCoercion = const False diff --git a/vehicle/src/Vehicle/Data/Expr/Normalised.hs b/vehicle/src/Vehicle/Data/Expr/Normalised.hs index bf3b5f48b..906b6ed8a 100644 --- a/vehicle/src/Vehicle/Data/Expr/Normalised.hs +++ b/vehicle/src/Vehicle/Data/Expr/Normalised.hs @@ -97,7 +97,7 @@ cheatEnvToValues = fmap envEntryToValue where envEntryToValue :: EnvEntry closure builtin -> Value closure builtin envEntryToValue (binder, value) = do - let ident = Identifier StdLib (fromMaybe "_" (nameOf binder) <> " =") + let ident = stdlibIdentifier (fromMaybe "_" (nameOf binder) <> " =") VFreeVar ident [explicit value] type FreeEnv closure builtin = Map Identifier (VDecl closure builtin) diff --git a/vehicle/src/Vehicle/Data/Expr/Standard.hs b/vehicle/src/Vehicle/Data/Expr/Standard.hs index 8a7c57c9f..1a08ec21e 100644 --- a/vehicle/src/Vehicle/Data/Expr/Standard.hs +++ b/vehicle/src/Vehicle/Data/Expr/Standard.hs @@ -127,7 +127,7 @@ substArgs e args = normAppList e args -- | Use to convert builtins for printing that have no representation in the -- standard `Builtin` type. cheatConvertBuiltin :: Provenance -> Doc a -> Expr var builtin -cheatConvertBuiltin p b = FreeVar p $ Identifier StdLib (layoutAsText b) +cheatConvertBuiltin p b = FreeVar p $ stdlibIdentifier (layoutAsText b) convertExprBuiltins :: forall builtin1 builtin2 var. diff --git a/vehicle/src/Vehicle/Libraries/StandardLibrary/Definitions.hs b/vehicle/src/Vehicle/Libraries/StandardLibrary/Definitions.hs index 61833bfd1..cef7c7b1a 100644 --- a/vehicle/src/Vehicle/Libraries/StandardLibrary/Definitions.hs +++ b/vehicle/src/Vehicle/Libraries/StandardLibrary/Definitions.hs @@ -11,7 +11,9 @@ import Vehicle.Syntax.AST import Vehicle.Syntax.Builtin pattern TensorIdent :: Identifier -pattern TensorIdent = Identifier StdLib "Tensor" +pattern TensorIdent <- Identifier (ModulePath [StdLib]) "Tensor" + where + TensorIdent = Identifier (ModulePath [StdLib]) "Tensor" data StdLibFunction = StdTypeAnn @@ -61,7 +63,7 @@ instance Pretty StdLibFunction where instance Hashable StdLibFunction instance HasIdentifier StdLibFunction where - identifierOf f = Identifier StdLib $ pack $ show f + identifierOf f = stdlibIdentifier $ pack $ show f stdLibFunctions :: Map Name StdLibFunction stdLibFunctions = Map.fromList $ fmap (\f -> (pack $ show f, f)) [minBound .. maxBound] diff --git a/vehicle/src/Vehicle/TypeCheck.hs b/vehicle/src/Vehicle/TypeCheck.hs index 68bee9eea..70255beac 100644 --- a/vehicle/src/Vehicle/TypeCheck.hs +++ b/vehicle/src/Vehicle/TypeCheck.hs @@ -51,7 +51,7 @@ typeCheck loggingSettings options@TypeCheckOptions {..} = runCompileMonad loggin -------------------------------------------------------------------------------- -- Useful functions that apply to multiple compiler passes -parseAndTypeCheckExpr :: (MonadIO m, MonadCompile m) => Text -> m (Expr Ix Builtin) +parseAndTypeCheckExpr :: (MonadIO m, MonadCompile m) => (FilePath, Text) -> m (Expr Ix Builtin) parseAndTypeCheckExpr expr = do standardLibraryProg <- loadLibrary standardLibrary freeCtx <- createFreeCtx [standardLibraryProg] @@ -60,10 +60,11 @@ parseAndTypeCheckExpr expr = do typedExpr <- typeCheckExpr standardBuiltinInstances freeCtx scopedExpr convertBackToStandardBuiltin typedExpr -parseExprText :: (MonadCompile m) => Text -> m (Expr Name Builtin) -parseExprText txt = - case runExcept (parseExpr User =<< readExpr txt) of - Left err -> throwError $ ParseError User err +parseExprText :: (MonadCompile m) => (FilePath, Text) -> m (Expr Name Builtin) +parseExprText (file, txt) = do + let location = (ModulePath [User], file) + case runExcept (parseExpr location =<< readExpr txt) of + Left err -> throwError $ ParseError location err Right expr -> return expr typeCheckUserProg :: @@ -79,7 +80,7 @@ typeCheckUserProg TypeCheckOptions {..} = do -- not load networks and datasets from disk. typeCheckProgram :: (MonadIO m, MonadCompile m) => - Module -> + ParseLocation -> Imports -> SpecificationText -> m (Prog Ix Builtin) @@ -98,22 +99,22 @@ typeCheckOrLoadProg :: Imports -> FilePath -> m (Prog Ix Builtin) -typeCheckOrLoadProg modul imports specificationFile = do +typeCheckOrLoadProg modl imports specificationFile = do spec <- readSpecification specificationFile interfaceFileResult <- readObjectFile specificationFile spec case interfaceFileResult of Just result -> return result Nothing -> do - result <- typeCheckProgram modul imports spec + result <- typeCheckProgram (ModulePath [modl], specificationFile) imports spec writeObjectFile specificationFile spec result return result -parseProgText :: (MonadCompile m) => Module -> Text -> m (Prog Name Builtin) -parseProgText modul txt = do - case runExcept (readAndParseProg modul txt) of - Left err -> throwError $ ParseError modul err - Right prog -> case traverseDecls (parseDecl modul) prog of - Left err -> throwError $ ParseError modul err +parseProgText :: (MonadCompile m) => ParseLocation -> Text -> m (Prog Name Builtin) +parseProgText location txt = do + case runExcept (readAndParseProg location txt) of + Left err -> throwError $ ParseError location err + Right prog -> case traverseDecls (parseDecl location) prog of + Left err -> throwError $ ParseError location err Right prog' -> return prog' loadLibrary :: (MonadIO m, MonadCompile m) => Library -> m (Prog Ix Builtin) diff --git a/vehicle/tests/golden/compile/issue699/MarabouQueries.err.golden b/vehicle/tests/golden/compile/issue699/MarabouQueries.err.golden index ea5eb865c..5c3639698 100644 --- a/vehicle/tests/golden/compile/issue699/MarabouQueries.err.golden +++ b/vehicle/tests/golden/compile/issue699/MarabouQueries.err.golden @@ -1,7 +1,7 @@ -Error at Line 33, Columns 1-7: The property 'robust' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the division at Line 15, Columns 42-43 involves - 1. the output of network 'classifier' at Line 9, Columns 1-11 - 2. which is returned as an output of the function 'scaler' at Line 34, Columns 10-22 +Error in file 'spec.vcl' at Line 33, Columns 1-7: The property 'robust' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the division in file 'spec.vcl' at Line 15, Columns 42-43 involves + 1. the output of network 'classifier' in file 'spec.vcl' at Line 9, Columns 1-11 + 2. which is returned as an output of the function 'scaler' in file 'spec.vcl' at Line 34, Columns 10-22 3. which is used in the denominator of the division Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/compile/issue700/MarabouQueries.err.golden b/vehicle/tests/golden/compile/issue700/MarabouQueries.err.golden index 10f3b2277..d59e7a7c8 100644 --- a/vehicle/tests/golden/compile/issue700/MarabouQueries.err.golden +++ b/vehicle/tests/golden/compile/issue700/MarabouQueries.err.golden @@ -1,6 +1,6 @@ -Error at Line 7, Columns 1-13: The property 'robustAround' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the division at Line 8, Columns 29-30 involves - 1. the output of network 'classifier' at Line 4, Columns 1-11 +Error in file 'spec.vcl' at Line 7, Columns 1-13: The property 'robustAround' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the division in file 'spec.vcl' at Line 8, Columns 29-30 involves + 1. the output of network 'classifier' in file 'spec.vcl' at Line 4, Columns 1-11 2. which is used in the denominator of the division Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/argument/missingDeclaration/Marabou.err.golden b/vehicle/tests/golden/error/argument/missingDeclaration/Marabou.err.golden index 2bdf9b8f4..1698c0a1d 100644 --- a/vehicle/tests/golden/error/argument/missingDeclaration/Marabou.err.golden +++ b/vehicle/tests/golden/error/argument/missingDeclaration/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 0, Columns 0-0: Was asked to compile declaration 'property' but no declaration exists with that name in the specification. +Error in file 'unknown' at Line 0, Columns 0-0: Was asked to compile declaration 'property' but no declaration exists with that name in the specification. Fix: check the spelling of 'property' or that the right specification is being used. diff --git a/vehicle/tests/golden/error/dataset/invalidContainerType/TypeCheck.err.golden b/vehicle/tests/golden/error/dataset/invalidContainerType/TypeCheck.err.golden index c57cf01a1..20b796e0e 100644 --- a/vehicle/tests/golden/error/dataset/invalidContainerType/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/dataset/invalidContainerType/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 1-16: The type of @dataset 'trainingDataset': +Error in file 'invalidContainerType.vcl' at Line 2, Columns 1-16: The type of @dataset 'trainingDataset': Nat is not supported. Only the following types are allowed for datasets: List, Vector, Tensor diff --git a/vehicle/tests/golden/error/dataset/invalidElementType/TypeCheck.err.golden b/vehicle/tests/golden/error/dataset/invalidElementType/TypeCheck.err.golden index b36e38a7a..c7e2d44d3 100644 --- a/vehicle/tests/golden/error/dataset/invalidElementType/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/dataset/invalidElementType/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 1-16: The type of @dataset 'trainingDataset': +Error in file 'invalidElementType.vcl' at Line 2, Columns 1-16: The type of @dataset 'trainingDataset': List (Nat -> Nat) is not supported as it has elements of an unsupported type: Nat -> Nat diff --git a/vehicle/tests/golden/error/dataset/mismatchedDimensionSize/Marabou.err.golden b/vehicle/tests/golden/error/dataset/mismatchedDimensionSize/Marabou.err.golden index c4563da55..1bbe2eb5a 100644 --- a/vehicle/tests/golden/error/dataset/mismatchedDimensionSize/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/mismatchedDimensionSize/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 3, Columns 1-16: Mismatch in the size of the first dimension of dataset 'trainingDataset'. +Error in file 'mismatchedDimensionSize.vcl' at Line 3, Columns 1-16: Mismatch in the size of the first dimension of dataset 'trainingDataset'. According to the specification it should be '5' but was actually found to be '4' when reading 'dataset-nat-4.idx'. Fix: change the dimensions of 'trainingDataset' in the specification or check that 'dataset-nat-4.idx' is in the format you were expecting. diff --git a/vehicle/tests/golden/error/dataset/mismatchedDimensions/Marabou.err.golden b/vehicle/tests/golden/error/dataset/mismatchedDimensions/Marabou.err.golden index bf1bf4f6a..6ac8d2a0d 100644 --- a/vehicle/tests/golden/error/dataset/mismatchedDimensions/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/mismatchedDimensions/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 3, Columns 1-16: Mismatch in the dimensions of dataset 'trainingDataset'. +Error in file 'mismatchedDimensions.vcl' at Line 3, Columns 1-16: Mismatch in the dimensions of dataset 'trainingDataset'. According to the specification it should be 2-dimensional but was actually found to be 1-dimensional when reading 'dataset-nat-4.idx'. Fix: change the dimensions of 'trainingDataset' in the specification or check that 'dataset-nat-4.idx' is in the format you were expecting. diff --git a/vehicle/tests/golden/error/dataset/mismatchedType/Marabou.err.golden b/vehicle/tests/golden/error/dataset/mismatchedType/Marabou.err.golden index cf5ce4525..93334a833 100644 --- a/vehicle/tests/golden/error/dataset/mismatchedType/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/mismatchedType/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. +Error in file 'mismatchedType.vcl' at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. Expected elements of type 'Nat' but found elements of type 'Rat' when reading 'dataset-rat-4.idx'. Fix: change the type of 'trainingDataset' in the specification or check that 'dataset-rat-4.idx' is in the format you were expecting. diff --git a/vehicle/tests/golden/error/dataset/missingDataset/Marabou.err.golden b/vehicle/tests/golden/error/dataset/missingDataset/Marabou.err.golden index 1bddab794..a0203f7c6 100644 --- a/vehicle/tests/golden/error/dataset/missingDataset/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/missingDataset/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 3, Columns 1-16: The following exception occured when trying to read the file provided for dataset 'trainingDataset': +Error in file 'missingDataset.vcl' at Line 3, Columns 1-16: The following exception occured when trying to read the file provided for dataset 'trainingDataset': non-existent.idx: openBinaryFile: does not exist (No such file or directory) diff --git a/vehicle/tests/golden/error/dataset/negativeNat/Marabou.err.golden b/vehicle/tests/golden/error/dataset/negativeNat/Marabou.err.golden index 7a1eff80c..640883fba 100644 --- a/vehicle/tests/golden/error/dataset/negativeNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/negativeNat/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. +Error in file 'negativeNat.vcl' at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. Expected elements of type 'Nat' but found value '-1' when reading 'dataset-int-4.idx'. Fix: change the type of 'trainingDataset' in the specification or check that 'dataset-int-4.idx' is in the format you were expecting. diff --git a/vehicle/tests/golden/error/dataset/notProvided/Marabou.err.golden b/vehicle/tests/golden/error/dataset/notProvided/Marabou.err.golden index c52bdaa14..33c90be7f 100644 --- a/vehicle/tests/golden/error/dataset/notProvided/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/notProvided/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 3, Columns 1-16: No file was provided for the dataset 'trainingDataset'. +Error in file 'notProvided.vcl' at Line 3, Columns 1-16: No file was provided for the dataset 'trainingDataset'. Fix: provide it via the command line using '--dataset trainingDataset:FILEPATH' diff --git a/vehicle/tests/golden/error/dataset/tooBigIndex/Marabou.err.golden b/vehicle/tests/golden/error/dataset/tooBigIndex/Marabou.err.golden index b91a18a93..43df0ec6d 100644 --- a/vehicle/tests/golden/error/dataset/tooBigIndex/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/tooBigIndex/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. +Error in file 'tooBigIndex.vcl' at Line 3, Columns 1-16: Mismatch in the type of elements of dataset 'trainingDataset'. Expected elements of type 'Index 3' but found value '3' when reading 'dataset-nat-4.idx'. Fix: change the type of 'trainingDataset' in the specification or check that 'dataset-nat-4.idx' is in the format you were expecting. diff --git a/vehicle/tests/golden/error/dataset/unsupportedFormat/Marabou.err.golden b/vehicle/tests/golden/error/dataset/unsupportedFormat/Marabou.err.golden index 38458d24c..a33ed092c 100644 --- a/vehicle/tests/golden/error/dataset/unsupportedFormat/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/unsupportedFormat/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 3, Columns 1-16: The '.blerp' format of the file provided for the dataset 'trainingDataset' is not currently supported by Vehicle. +Error in file 'unsupportedFormat.vcl' at Line 3, Columns 1-16: The '.blerp' format of the file provided for the dataset 'trainingDataset' is not currently supported by Vehicle. Fix: use one of the supported formats [ .idx ] , or open an issue on Github (https://github.com/vehicle-lang/vehicle/issues/) to discuss adding support. diff --git a/vehicle/tests/golden/error/dataset/variableDimensions/Marabou.err.golden b/vehicle/tests/golden/error/dataset/variableDimensions/Marabou.err.golden index cda99e400..8565d3251 100644 --- a/vehicle/tests/golden/error/dataset/variableDimensions/Marabou.err.golden +++ b/vehicle/tests/golden/error/dataset/variableDimensions/Marabou.err.golden @@ -1,4 +1,4 @@ -Error at Line 5, Columns 1-16: The type of @parameter 'trainingDataset': +Error in file 'variableDimensions.vcl' at Line 5, Columns 1-16: The type of @parameter 'trainingDataset': Tensor Nat [if f [0] ! 0 > 0 then 2 else 3] which reduces to: Vector Nat (if f [0.0] ! 0 > 0.0 then 2 else 3) diff --git a/vehicle/tests/golden/error/inferableParameter/unsupportedType/TypeCheck.err.golden b/vehicle/tests/golden/error/inferableParameter/unsupportedType/TypeCheck.err.golden index b26e52418..34d0f8e9c 100644 --- a/vehicle/tests/golden/error/inferableParameter/unsupportedType/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/inferableParameter/unsupportedType/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 1-2: The type of @parameter 'n': +Error in file 'unsupportedType.vcl' at Line 2, Columns 1-2: The type of @parameter 'n': Rat is not supported. Inferable parameters must be of type 'Nat'. Fix: either change the type of 'n' or make the parameter non-inferable and provide the value manually. diff --git a/vehicle/tests/golden/error/linearity/nonLinearIfCondition/Marabou.err.golden b/vehicle/tests/golden/error/linearity/nonLinearIfCondition/Marabou.err.golden index 2c470e93a..d7bd04d72 100644 --- a/vehicle/tests/golden/error/linearity/nonLinearIfCondition/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/nonLinearIfCondition/Marabou.err.golden @@ -1,9 +1,9 @@ -Error at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 6, Columns 30-31 involves - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 +Error in file 'spec.vcl' at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 6, Columns 30-31 involves + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the left hand side of the multiplication and - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/quadraticFunInput/Marabou.err.golden b/vehicle/tests/golden/error/linearity/quadraticFunInput/Marabou.err.golden index 3c3dfead9..22e79bf97 100644 --- a/vehicle/tests/golden/error/linearity/quadraticFunInput/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/quadraticFunInput/Marabou.err.golden @@ -1,11 +1,11 @@ -Error at Line 8, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 5, Columns 14-15 involves - 1. the quantified variable 'x' introduced at Line 9, Columns 13-20 - 2. which is used as an input to the function 'square' at Line 9, Columns 27-33 +Error in file 'spec.vcl' at Line 8, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 5, Columns 14-15 involves + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 9, Columns 13-20 + 2. which is used as an input to the function 'square' in file 'spec.vcl' at Line 9, Columns 27-33 3. which is used in the left hand side of the multiplication and - 1. the quantified variable 'x' introduced at Line 9, Columns 13-20 - 2. which is used as an input to the function 'square' at Line 9, Columns 27-33 + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 9, Columns 13-20 + 2. which is used as an input to the function 'square' in file 'spec.vcl' at Line 9, Columns 27-33 3. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/quadraticFunOutput/Marabou.err.golden b/vehicle/tests/golden/error/linearity/quadraticFunOutput/Marabou.err.golden index 31d12c3fe..ad170bc1e 100644 --- a/vehicle/tests/golden/error/linearity/quadraticFunOutput/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/quadraticFunOutput/Marabou.err.golden @@ -1,11 +1,11 @@ -Error at Line 8, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 5, Columns 14-15 involves - 1. the output of network 'f' at Line 2, Columns 1-2 - 2. which is used as an input to the function 'square' at Line 9, Columns 24-30 +Error in file 'spec.vcl' at Line 8, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 5, Columns 14-15 involves + 1. the output of network 'f' in file 'spec.vcl' at Line 2, Columns 1-2 + 2. which is used as an input to the function 'square' in file 'spec.vcl' at Line 9, Columns 24-30 3. which is used in the left hand side of the multiplication and - 1. the output of network 'f' at Line 2, Columns 1-2 - 2. which is used as an input to the function 'square' at Line 9, Columns 24-30 + 1. the output of network 'f' in file 'spec.vcl' at Line 2, Columns 1-2 + 2. which is used as an input to the function 'square' in file 'spec.vcl' at Line 9, Columns 24-30 3. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/quadraticInput/Marabou.err.golden b/vehicle/tests/golden/error/linearity/quadraticInput/Marabou.err.golden index 240abc17f..253ba81c4 100644 --- a/vehicle/tests/golden/error/linearity/quadraticInput/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/quadraticInput/Marabou.err.golden @@ -1,9 +1,9 @@ -Error at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 6, Columns 29-30 involves - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 +Error in file 'spec.vcl' at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 6, Columns 29-30 involves + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the left hand side of the multiplication and - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/quadraticInputOutput/Marabou.err.golden b/vehicle/tests/golden/error/linearity/quadraticInputOutput/Marabou.err.golden index 5c66cdb3d..b626c2d3e 100644 --- a/vehicle/tests/golden/error/linearity/quadraticInputOutput/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/quadraticInputOutput/Marabou.err.golden @@ -1,9 +1,9 @@ -Error at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 6, Columns 36-37 involves - 1. the output of network 'f' at Line 2, Columns 1-2 +Error in file 'spec.vcl' at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 6, Columns 36-37 involves + 1. the output of network 'f' in file 'spec.vcl' at Line 2, Columns 1-2 2. which is used in the left hand side of the multiplication and - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/quadraticTensorInputLookup/Marabou.err.golden b/vehicle/tests/golden/error/linearity/quadraticTensorInputLookup/Marabou.err.golden index e008c6c3a..ab128c5a2 100644 --- a/vehicle/tests/golden/error/linearity/quadraticTensorInputLookup/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/quadraticTensorInputLookup/Marabou.err.golden @@ -1,9 +1,9 @@ -Error at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the multiplication at Line 6, Columns 24-25 involves - 1. the quantified variable 'x' introduced at Line 6, Columns 12-13 +Error in file 'spec.vcl' at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the multiplication in file 'spec.vcl' at Line 6, Columns 24-25 involves + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 12-13 2. which is used in the left hand side of the multiplication and - 1. the quantified variable 'x' introduced at Line 6, Columns 12-13 + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 12-13 2. which is used in the right hand side of the multiplication Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/linearity/reciprocalInput/Marabou.err.golden b/vehicle/tests/golden/error/linearity/reciprocalInput/Marabou.err.golden index 26931e9d4..e43fd5ba9 100644 --- a/vehicle/tests/golden/error/linearity/reciprocalInput/Marabou.err.golden +++ b/vehicle/tests/golden/error/linearity/reciprocalInput/Marabou.err.golden @@ -1,6 +1,6 @@ -Error at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. -In particular the division at Line 6, Columns 29-30 involves - 1. the quantified variable 'x' introduced at Line 6, Columns 13-20 +Error in file 'spec.vcl' at Line 5, Columns 1-2: The property 'p' contains a non-linear constraint which is not supported by the Marabou query format. +In particular the division in file 'spec.vcl' at Line 6, Columns 29-30 involves + 1. the quantified variable 'x' introduced in file 'spec.vcl' at Line 6, Columns 13-20 2. which is used in the denominator of the division Fix: try rewriting the specification to avoid the non-linearity. diff --git a/vehicle/tests/golden/error/network/notAFunction/TypeCheck.err.golden b/vehicle/tests/golden/error/network/notAFunction/TypeCheck.err.golden index 7bdabb70c..6f70b8325 100644 --- a/vehicle/tests/golden/error/network/notAFunction/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/network/notAFunction/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 5-8: The type of @network 'f': +Error in file 'notAFunction.vcl' at Line 2, Columns 5-8: The type of @network 'f': Rat is not supported as it is not a function. Fix: Only networks of the following types are allowed: diff --git a/vehicle/tests/golden/error/other-verifier/quantifiedNat/Marabou.err.golden b/vehicle/tests/golden/error/other-verifier/quantifiedNat/Marabou.err.golden index 959441b28..d4c0ca562 100644 --- a/vehicle/tests/golden/error/other-verifier/quantifiedNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/other-verifier/quantifiedNat/Marabou.err.golden @@ -1,4 +1,4 @@ -Error at Line 3, Columns 5-11: unable to work out a valid type for the overloaded expression 'forall'. +Error in file 'quantifiedNat.vcl' at Line 3, Columns 5-11: unable to work out a valid type for the overloaded expression 'forall'. Type checking has deduced that it is of type: (Nat -> Bool) -> Bool but 'forall' has only the following valid types: diff --git a/vehicle/tests/golden/error/other-verifier/quantifiedVectorNat/Marabou.err.golden b/vehicle/tests/golden/error/other-verifier/quantifiedVectorNat/Marabou.err.golden index 29cc3e125..7cfa9f6cc 100644 --- a/vehicle/tests/golden/error/other-verifier/quantifiedVectorNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/other-verifier/quantifiedVectorNat/Marabou.err.golden @@ -1,4 +1,4 @@ -Error at Line 3, Columns 5-11: unable to work out a valid type for the overloaded expression 'forall'. +Error in file 'quantifiedVectorNat.vcl' at Line 3, Columns 5-11: unable to work out a valid type for the overloaded expression 'forall'. Type checking has deduced that it is of type: (Vector Nat 2 -> Bool) -> Bool but 'forall' has only the following valid types: diff --git a/vehicle/tests/golden/error/parameter/givenDefinition/TypeCheck.err.golden b/vehicle/tests/golden/error/parameter/givenDefinition/TypeCheck.err.golden index e973cfa42..3061c5ed3 100644 --- a/vehicle/tests/golden/error/parameter/givenDefinition/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parameter/givenDefinition/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-8: The declaration 'epsilon' should not have a definition as it has been marked with a '@parameter' annotation. +Error in file 'spec.vcl' at Line 2, Columns 1-8: The declaration 'epsilon' should not have a definition as it has been marked with a '@parameter' annotation. Fix: either remove the definition for 'epsilon' or remove the '@parameter' annotation. diff --git a/vehicle/tests/golden/error/parameter/invalidIndex/Marabou.err.golden b/vehicle/tests/golden/error/parameter/invalidIndex/Marabou.err.golden index e2df5bf76..b2f5e6867 100644 --- a/vehicle/tests/golden/error/parameter/invalidIndex/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/invalidIndex/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. +Error in file 'invalidIndex.vcl' at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. Expected something of type 'Index 5' but was provided the value '5'. Fix: either change the size of the index or ensure the value provided is in the range '0...4' (inclusive). diff --git a/vehicle/tests/golden/error/parameter/invalidIndex/invalidNat/Marabou.err.golden b/vehicle/tests/golden/error/parameter/invalidIndex/invalidNat/Marabou.err.golden index f9e3928ab..30453980c 100644 --- a/vehicle/tests/golden/error/parameter/invalidIndex/invalidNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/invalidIndex/invalidNat/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. +Error in file 'invalidNat.vcl' at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. Expected something of type 'Nat' but was provided the value '-5'. Fix: either change the type of 'n' or ensure the value provided is non-negative. diff --git a/vehicle/tests/golden/error/parameter/invalidNat/Marabou.err.golden b/vehicle/tests/golden/error/parameter/invalidNat/Marabou.err.golden index f9e3928ab..30453980c 100644 --- a/vehicle/tests/golden/error/parameter/invalidNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/invalidNat/Marabou.err.golden @@ -1,3 +1,3 @@ -Error at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. +Error in file 'invalidNat.vcl' at Line 2, Columns 1-2: Mismatch in the type of parameter 'n'. Expected something of type 'Nat' but was provided the value '-5'. Fix: either change the type of 'n' or ensure the value provided is non-negative. diff --git a/vehicle/tests/golden/error/parameter/notProvided/Marabou.err.golden b/vehicle/tests/golden/error/parameter/notProvided/Marabou.err.golden index d80a39165..067dbca09 100644 --- a/vehicle/tests/golden/error/parameter/notProvided/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/notProvided/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-2: No value was provided for the parameter 'n'. +Error in file 'notProvided.vcl' at Line 2, Columns 1-2: No value was provided for the parameter 'n'. Fix: provide it via the command line using '--parameter n:VALUE' diff --git a/vehicle/tests/golden/error/parameter/unparseableBool/Marabou.err.golden b/vehicle/tests/golden/error/parameter/unparseableBool/Marabou.err.golden index 54cb40086..6c356dd9a 100644 --- a/vehicle/tests/golden/error/parameter/unparseableBool/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/unparseableBool/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-2: The value 'x' provided for parameter 'b' could not be parsed as a 'Bool'. +Error in file 'unparseableBool.vcl' at Line 2, Columns 1-2: The value 'x' provided for parameter 'b' could not be parsed as a 'Bool'. Fix: either change the type of 'b' in the specification or change the value provided. diff --git a/vehicle/tests/golden/error/parameter/unparseableIndex/Marabou.err.golden b/vehicle/tests/golden/error/parameter/unparseableIndex/Marabou.err.golden index 7ad9062ed..77c176b34 100644 --- a/vehicle/tests/golden/error/parameter/unparseableIndex/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/unparseableIndex/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-2: The value '~' provided for parameter 'n' could not be parsed as an 'Index'. +Error in file 'unparseableIndex.vcl' at Line 2, Columns 1-2: The value '~' provided for parameter 'n' could not be parsed as an 'Index'. Fix: either change the type of 'n' in the specification or change the value provided. diff --git a/vehicle/tests/golden/error/parameter/unparseableNat/Marabou.err.golden b/vehicle/tests/golden/error/parameter/unparseableNat/Marabou.err.golden index 25821584b..83969396d 100644 --- a/vehicle/tests/golden/error/parameter/unparseableNat/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/unparseableNat/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-2: The value '~' provided for parameter 'n' could not be parsed as a 'Nat'. +Error in file 'unparseableNat.vcl' at Line 2, Columns 1-2: The value '~' provided for parameter 'n' could not be parsed as a 'Nat'. Fix: either change the type of 'n' in the specification or change the value provided. diff --git a/vehicle/tests/golden/error/parameter/unparseableRat/Marabou.err.golden b/vehicle/tests/golden/error/parameter/unparseableRat/Marabou.err.golden index 8c52935da..2bcf9e969 100644 --- a/vehicle/tests/golden/error/parameter/unparseableRat/Marabou.err.golden +++ b/vehicle/tests/golden/error/parameter/unparseableRat/Marabou.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-2: The value '~' provided for parameter 'r' could not be parsed as a 'Rat'. +Error in file 'unparseableRat.vcl' at Line 2, Columns 1-2: The value '~' provided for parameter 'r' could not be parsed as a 'Rat'. Fix: either change the type of 'r' in the specification or change the value provided. diff --git a/vehicle/tests/golden/error/parameter/unsupportedType/TypeCheck.err.golden b/vehicle/tests/golden/error/parameter/unsupportedType/TypeCheck.err.golden index f441fe996..0e08a1e83 100644 --- a/vehicle/tests/golden/error/parameter/unsupportedType/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parameter/unsupportedType/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 1-2: The type of @parameter 'n': +Error in file 'unsupportedType.vcl' at Line 2, Columns 1-2: The type of @parameter 'n': Nat -> Nat is not supported. Only the following types are allowed for parameters: Bool, Index, Nat, Rat diff --git a/vehicle/tests/golden/error/parsing/annotationWithNoDeclaration/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/annotationWithNoDeclaration/TypeCheck.err.golden index 1336b866f..3cd050e6a 100644 --- a/vehicle/tests/golden/error/parsing/annotationWithNoDeclaration/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/annotationWithNoDeclaration/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 1, Columns 1-10: unattached annotation '@property' +Error in file 'annotationWithNoDeclaration.vcl' at Line 1, Columns 1-10: unattached annotation '@property' Fix: either attach the annotation to a declaration or remove it entirely diff --git a/vehicle/tests/golden/error/parsing/functionNotGivenBody/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/functionNotGivenBody/TypeCheck.err.golden index 59c363a6f..65ffebea7 100644 --- a/vehicle/tests/golden/error/parsing/functionNotGivenBody/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/functionNotGivenBody/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 1, Columns 1-5: no definition provided for the declaration 'test'. +Error in file 'spec.vcl' at Line 1, Columns 1-5: no definition provided for the declaration 'test'. Fix: either provide a definition for 'test' or mark it as an external resource by adding an appropriate annotation, i.e. @network, @dataset or @parameter. diff --git a/vehicle/tests/golden/error/parsing/functionWithMismatchedNames/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/functionWithMismatchedNames/TypeCheck.err.golden index c04f449fd..f9f4d7cfc 100644 --- a/vehicle/tests/golden/error/parsing/functionWithMismatchedNames/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/functionWithMismatchedNames/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 1, Columns 1-6: mismatch in function declaration names: 'test1' and 'test2'. +Error in file 'functionWithMismatchedNames.vcl' at Line 1, Columns 1-6: mismatch in function declaration names: 'test1' and 'test2'. Fix: ensure the function definition has the same name as the declaration it follows. diff --git a/vehicle/tests/golden/error/parsing/invalidAnnotationParameter/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/invalidAnnotationParameter/TypeCheck.err.golden index 95ba15e24..970e1db73 100644 --- a/vehicle/tests/golden/error/parsing/invalidAnnotationParameter/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/invalidAnnotationParameter/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 1, Columns 12-17: unknown option 'valid' for '@parameter' annotation. +Error in file 'invalidAnnotationParameter.vcl' at Line 1, Columns 12-17: unknown option 'valid' for '@parameter' annotation. Fix: did you mean 'infer'? diff --git a/vehicle/tests/golden/error/parsing/invalidAnnotationParameterValue/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/invalidAnnotationParameterValue/TypeCheck.err.golden index 21956d643..a8fd4e4bb 100644 --- a/vehicle/tests/golden/error/parsing/invalidAnnotationParameterValue/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/invalidAnnotationParameterValue/TypeCheck.err.golden @@ -1 +1 @@ -Error at Line 1, Columns 20-23: unable to parse the value 'xsd' for option 'infer' +Error in file 'invalidAnnotationParameterValue.vcl' at Line 1, Columns 20-23: unable to parse the value 'xsd' for option 'infer' diff --git a/vehicle/tests/golden/error/parsing/missingVariablesLambda/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/missingVariablesLambda/TypeCheck.err.golden index d05c4b313..a064e2ca6 100644 --- a/vehicle/tests/golden/error/parsing/missingVariablesLambda/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/missingVariablesLambda/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 9-10: expected at least one variable name after '\' +Error in file 'missingVariablesLambda.vcl' at Line 2, Columns 9-10: expected at least one variable name after '\' Fix: add one or more names after '\' diff --git a/vehicle/tests/golden/error/parsing/multipleResources/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/multipleResources/TypeCheck.err.golden index ba707cf0e..8e4f9faea 100644 --- a/vehicle/tests/golden/error/parsing/multipleResources/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/multipleResources/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 3, Columns 1-5: abstract declaration 'test' cannot simulataneously be annotated with both '@dataset' and '@parameter'. +Error in file 'spec.vcl' at Line 3, Columns 1-5: abstract declaration 'test' cannot simulataneously be annotated with both '@dataset' and '@parameter'. Fix: remove one of annotations. diff --git a/vehicle/tests/golden/error/parsing/unchainableOrdersEqualsEquals/TypeCheck.err.golden b/vehicle/tests/golden/error/parsing/unchainableOrdersEqualsEquals/TypeCheck.err.golden index ac85cf71e..3743af8a6 100644 --- a/vehicle/tests/golden/error/parsing/unchainableOrdersEqualsEquals/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/parsing/unchainableOrdersEqualsEquals/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 15-17: cannot chain '<=' and '>=' +Error in file 'unchainableOrdersEqualsEquals.vcl' at Line 2, Columns 15-17: cannot chain '<=' and '>=' Fix: split chained orders into a conjunction diff --git a/vehicle/tests/golden/error/polarity/alternating/Marabou.err.golden b/vehicle/tests/golden/error/polarity/alternating/Marabou.err.golden index 3e5595afc..26009013a 100644 --- a/vehicle/tests/golden/error/polarity/alternating/Marabou.err.golden +++ b/vehicle/tests/golden/error/polarity/alternating/Marabou.err.golden @@ -1,5 +1,5 @@ -Error at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. +Error in file 'alternating.vcl' at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. In particular: - 1. the inner quantifier is the 'exists' located at Line 6, Columns 16-22 - 2. which alternates with the outer 'forall' at Line 6, Columns 5-11 + 1. the inner quantifier is the 'exists' located in file 'alternating.vcl' at Line 6, Columns 16-22 + 2. which alternates with the outer 'forall' in file 'alternating.vcl' at Line 6, Columns 5-11 Fix: try simplifying the specification to avoid the alternating quantifiers. diff --git a/vehicle/tests/golden/error/polarity/alternatingFun/Marabou.err.golden b/vehicle/tests/golden/error/polarity/alternatingFun/Marabou.err.golden index 1772d5aca..4989c3245 100644 --- a/vehicle/tests/golden/error/polarity/alternatingFun/Marabou.err.golden +++ b/vehicle/tests/golden/error/polarity/alternatingFun/Marabou.err.golden @@ -1,6 +1,6 @@ -Error at Line 8, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. +Error in file 'alternatingFun.vcl' at Line 8, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. In particular: - 1. the inner quantifier is the 'exists' located at Line 0 Column 0 - Line 5 Column 23 - 2. which is which is returned as an output of the function 'existential' at Line 9, Columns 24-35 - 3. which alternates with the outer 'forall' at Line 9, Columns 5-11 + 1. the inner quantifier is the 'exists' located in file 'alternatingFun.vcl' at Line 0 Column 0 - Line 5 Column 23 + 2. which is which is returned as an output of the function 'existential' in file 'alternatingFun.vcl' at Line 9, Columns 24-35 + 3. which alternates with the outer 'forall' in file 'alternatingFun.vcl' at Line 9, Columns 5-11 Fix: try simplifying the specification to avoid the alternating quantifiers. diff --git a/vehicle/tests/golden/error/polarity/alternatingImplies/Marabou.err.golden b/vehicle/tests/golden/error/polarity/alternatingImplies/Marabou.err.golden index 3e6e0aa39..e7e3f1299 100644 --- a/vehicle/tests/golden/error/polarity/alternatingImplies/Marabou.err.golden +++ b/vehicle/tests/golden/error/polarity/alternatingImplies/Marabou.err.golden @@ -1,6 +1,6 @@ -Error at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. +Error in file 'alternatingImplies.vcl' at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. In particular: - 1. the inner quantifier is the 'forall' located at Line 6, Columns 17-23 - 2. which is turned into an 'exists' by being on the LHS of the '=>' at Line 6, Columns 42-44 - 3. which alternates with the outer 'forall' at Line 6, Columns 5-11 + 1. the inner quantifier is the 'forall' located in file 'alternatingImplies.vcl' at Line 6, Columns 17-23 + 2. which is turned into an 'exists' by being on the LHS of the '=>' in file 'alternatingImplies.vcl' at Line 6, Columns 42-44 + 3. which alternates with the outer 'forall' in file 'alternatingImplies.vcl' at Line 6, Columns 5-11 Fix: try simplifying the specification to avoid the alternating quantifiers. diff --git a/vehicle/tests/golden/error/polarity/alternatingNeg/Marabou.err.golden b/vehicle/tests/golden/error/polarity/alternatingNeg/Marabou.err.golden index 1df67df3e..b01aa9239 100644 --- a/vehicle/tests/golden/error/polarity/alternatingNeg/Marabou.err.golden +++ b/vehicle/tests/golden/error/polarity/alternatingNeg/Marabou.err.golden @@ -1,6 +1,6 @@ -Error at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. +Error in file 'alternatingNeg.vcl' at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. In particular: - 1. the inner quantifier is the 'forall' located at Line 6, Columns 21-27 - 2. which is turned into an 'exists' by the 'not' at Line 6, Columns 16-19 - 3. which alternates with the outer 'forall' at Line 6, Columns 5-11 + 1. the inner quantifier is the 'forall' located in file 'alternatingNeg.vcl' at Line 6, Columns 21-27 + 2. which is turned into an 'exists' by the 'not' in file 'alternatingNeg.vcl' at Line 6, Columns 16-19 + 3. which alternates with the outer 'forall' in file 'alternatingNeg.vcl' at Line 6, Columns 5-11 Fix: try simplifying the specification to avoid the alternating quantifiers. diff --git a/vehicle/tests/golden/error/polarity/alternatingNegNeg/Marabou.err.golden b/vehicle/tests/golden/error/polarity/alternatingNegNeg/Marabou.err.golden index 4de924f52..5d018cf6d 100644 --- a/vehicle/tests/golden/error/polarity/alternatingNegNeg/Marabou.err.golden +++ b/vehicle/tests/golden/error/polarity/alternatingNegNeg/Marabou.err.golden @@ -1,7 +1,7 @@ -Error at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. +Error in file 'alternatingNegNeg.vcl' at Line 5, Columns 1-2: The property 'p' contains alternating 'forall' and 'exists' quantifiers which is not supported by the Marabou query format. In particular: - 1. the inner quantifier is the 'exists' located at Line 6, Columns 26-32 - 2. which is turned into a 'forall' by the 'not' at Line 6, Columns 21-24 - 3. which is turned into an 'exists' by the 'not' at Line 6, Columns 16-19 - 4. which alternates with the outer 'forall' at Line 6, Columns 5-11 + 1. the inner quantifier is the 'exists' located in file 'alternatingNegNeg.vcl' at Line 6, Columns 26-32 + 2. which is turned into a 'forall' by the 'not' in file 'alternatingNegNeg.vcl' at Line 6, Columns 21-24 + 3. which is turned into an 'exists' by the 'not' in file 'alternatingNegNeg.vcl' at Line 6, Columns 16-19 + 4. which alternates with the outer 'forall' in file 'alternatingNegNeg.vcl' at Line 6, Columns 5-11 Fix: try simplifying the specification to avoid the alternating quantifiers. diff --git a/vehicle/tests/golden/error/property/invalidType/TypeCheck.err.golden b/vehicle/tests/golden/error/property/invalidType/TypeCheck.err.golden index 329066464..ca929224f 100644 --- a/vehicle/tests/golden/error/property/invalidType/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/property/invalidType/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 1-2: The type of @property 'p': +Error in file 'invalidType.vcl' at Line 2, Columns 1-2: The type of @property 'p': Rat is not supported. Only the following types are allowed for '@property's: Bool, Vector Bool n, Tensor Bool ns diff --git a/vehicle/tests/golden/error/property/noDefinition/TypeCheck.err.golden b/vehicle/tests/golden/error/property/noDefinition/TypeCheck.err.golden index 0188501d4..430f08776 100644 --- a/vehicle/tests/golden/error/property/noDefinition/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/property/noDefinition/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 1-5: missing definition for property 'test'. +Error in file 'spec.vcl' at Line 2, Columns 1-5: missing definition for property 'test'. Fix: add a definition for 'test' . diff --git a/vehicle/tests/golden/error/scoping/freeBoundShadowing/TypeCheck.err.golden b/vehicle/tests/golden/error/scoping/freeBoundShadowing/TypeCheck.err.golden index 106821f33..97016ce64 100644 --- a/vehicle/tests/golden/error/scoping/freeBoundShadowing/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/scoping/freeBoundShadowing/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 4, Columns 1-2: multiple declarations found with the name 'f' +Error in file 'spec.vcl' at Line 4, Columns 1-2: multiple declarations found with the name 'f' Fix: remove or rename the duplicate definitions diff --git a/vehicle/tests/golden/error/scoping/freeFreeShadowing/TypeCheck.err.golden b/vehicle/tests/golden/error/scoping/freeFreeShadowing/TypeCheck.err.golden index d786166db..fc249f8e5 100644 --- a/vehicle/tests/golden/error/scoping/freeFreeShadowing/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/scoping/freeFreeShadowing/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 5, Columns 3-4: cannot re-use the name 'f' as a local variable because there is already a declaration with that name. +Error in file 'spec.vcl' at Line 5, Columns 3-4: cannot re-use the name 'f' as a local variable because there is already a declaration with that name. Fix: rename either the original declaration or this variable diff --git a/vehicle/tests/golden/error/scoping/unboundName/TypeCheck.err.golden b/vehicle/tests/golden/error/scoping/unboundName/TypeCheck.err.golden index 5db7ba057..0585c1b08 100644 --- a/vehicle/tests/golden/error/scoping/unboundName/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/scoping/unboundName/TypeCheck.err.golden @@ -1 +1 @@ -Error at Line 2, Columns 5-6: The name 'x' is not in scope +Error in file 'spec.vcl' at Line 2, Columns 5-6: The name 'x' is not in scope diff --git a/vehicle/tests/golden/error/typing/incorrectTensorLength/TypeCheck.err.golden b/vehicle/tests/golden/error/typing/incorrectTensorLength/TypeCheck.err.golden index 7eaf12598..51ef012e1 100644 --- a/vehicle/tests/golden/error/typing/incorrectTensorLength/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/typing/incorrectTensorLength/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 10-11: unable to work out a valid type for the overloaded expression '[1]'. +Error in file 'incorrectTensorLength.vcl' at Line 2, Columns 10-11: unable to work out a valid type for the overloaded expression '[1]'. Type checking has deduced that it is of type: forallT {A} . Vector A 1 -> ?4 A but '[1]' has only the following valid types: diff --git a/vehicle/tests/golden/error/typing/indexOutOfBoundsConcrete/TypeCheck.err.golden b/vehicle/tests/golden/error/typing/indexOutOfBoundsConcrete/TypeCheck.err.golden index 18771fdcc..562c16987 100644 --- a/vehicle/tests/golden/error/typing/indexOutOfBoundsConcrete/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/typing/indexOutOfBoundsConcrete/TypeCheck.err.golden @@ -1 +1 @@ -Error at Line 2, Columns 21-22: the value '1' is too big to be used as an index of size '1'. +Error in file 'indexOutOfBoundsConcrete.vcl' at Line 2, Columns 21-22: the value '1' is too big to be used as an index of size '1'. diff --git a/vehicle/tests/golden/error/typing/indexOutOfBoundsUnknown/TypeCheck.err.golden b/vehicle/tests/golden/error/typing/indexOutOfBoundsUnknown/TypeCheck.err.golden index c4ab32351..81afdb4bd 100644 --- a/vehicle/tests/golden/error/typing/indexOutOfBoundsUnknown/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/typing/indexOutOfBoundsUnknown/TypeCheck.err.golden @@ -1 +1 @@ -Error at Line 2, Columns 21-22: unable to determine if '1' is a valid index of size 'n'. +Error in file 'indexOutOfBoundsUnknown.vcl' at Line 2, Columns 21-22: unable to determine if '1' is a valid index of size 'n'. diff --git a/vehicle/tests/golden/error/typing/intAsNat/TypeCheck.err.golden b/vehicle/tests/golden/error/typing/intAsNat/TypeCheck.err.golden index 535af8ce7..f4d660cb2 100644 --- a/vehicle/tests/golden/error/typing/intAsNat/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/typing/intAsNat/TypeCheck.err.golden @@ -1,4 +1,4 @@ -Error at Line 2, Columns 7-8: unable to work out a valid type for the overloaded expression '-'. +Error in file 'intAsNat.vcl' at Line 2, Columns 7-8: unable to work out a valid type for the overloaded expression '-'. Type checking has deduced that it is of type: ?3 -> Nat but '-' has only the following valid types: diff --git a/vehicle/tests/golden/error/typing/unsolvedMeta/TypeCheck.err.golden b/vehicle/tests/golden/error/typing/unsolvedMeta/TypeCheck.err.golden index a5e62ce4a..ed75b0ceb 100644 --- a/vehicle/tests/golden/error/typing/unsolvedMeta/TypeCheck.err.golden +++ b/vehicle/tests/golden/error/typing/unsolvedMeta/TypeCheck.err.golden @@ -1,2 +1,2 @@ -Error at Line 2, Columns 8-14: insufficient information to find a valid type for the overloaded expression 'forall'. +Error in file 'unsolvedMeta.vcl' at Line 2, Columns 8-14: insufficient information to find a valid type for the overloaded expression 'forall'. Fix: try adding more type annotations