diff --git a/.github/workflows/build-vehicle.yml b/.github/workflows/build-vehicle.yml index f180714d7..f77900be2 100644 --- a/.github/workflows/build-vehicle.yml +++ b/.github/workflows/build-vehicle.yml @@ -26,6 +26,17 @@ jobs: project-file: "cabal.project.ghc-9.4.8" extra-args: "" include: + # Build with GHC 9.8.1 + - os: + name: Linux + type: ubuntu-latest + haskell: + ghc: + version: "9.8.1" + cabal: + version: "3.10.2.1" + project-file: "cabal.project.ghc-9.8.1" + extra-args: "" # Build with GHC 9.6.4 - os: name: Linux diff --git a/cabal.project.ghc-9.2.8 b/cabal.project.ghc-9.2.8 index c962c76c0..7d05f01d9 100644 --- a/cabal.project.ghc-9.2.8 +++ b/cabal.project.ghc-9.2.8 @@ -1,4 +1,4 @@ --- Cabal project configuration file for GHC 9.2.7 +-- Cabal project configuration file for GHC 9.2.8 -- -- See `cabal.project` for details. diff --git a/cabal.project.ghc-9.4.8 b/cabal.project.ghc-9.4.8 index c58654f45..cf0fc4b5f 100644 --- a/cabal.project.ghc-9.4.8 +++ b/cabal.project.ghc-9.4.8 @@ -1,4 +1,5 @@ --- Cabal project configuration file for GHC 9.4.4 + +-- Cabal project configuration file for GHC 9.4.8 -- -- See `cabal.project` for details. diff --git a/cabal.project.ghc-9.6.4 b/cabal.project.ghc-9.6.4 index a5bd23f94..eae6fb21f 100644 --- a/cabal.project.ghc-9.6.4 +++ b/cabal.project.ghc-9.6.4 @@ -1,4 +1,4 @@ --- Cabal project configuration file for GHC 9.6.1 +-- Cabal project configuration file for GHC 9.6.4 -- -- See `cabal.project` for details. diff --git a/cabal.project.ghc-9.8.1 b/cabal.project.ghc-9.8.1 new file mode 100644 index 000000000..f1d971670 --- /dev/null +++ b/cabal.project.ghc-9.8.1 @@ -0,0 +1,5 @@ +-- Cabal project configuration file for GHC 9.8.1 +-- +-- See `cabal.project` for details. + +import: cabal.project diff --git a/cabal.project.ghc-9.8.1.freeze b/cabal.project.ghc-9.8.1.freeze new file mode 100644 index 000000000..1817ffe9d --- /dev/null +++ b/cabal.project.ghc-9.8.1.freeze @@ -0,0 +1,142 @@ +active-repositories: hackage.haskell.org:merge +constraints: any.BNFC ==2.9.5, + any.Cabal ==3.10.2.1, + any.Cabal-syntax ==3.10.2.0, + any.Diff ==0.4.1, + any.Glob ==0.10.2, + any.OneTuple ==0.4.1.1, + any.QuickCheck ==2.14.3, + QuickCheck -old-random +templatehaskell, + any.StateVar ==1.2.2, + any.aeson ==2.2.1.0, + aeson +ordered-keymap, + any.aeson-pretty ==0.8.10, + aeson-pretty -lib-only, + any.alex ==3.5.0.0, + any.ansi-terminal ==0.11.5, + ansi-terminal -example +win32-2-13-1, + any.ansi-terminal-types ==0.11.5, + any.array ==0.5.6.0, + any.assoc ==1.1, + assoc +tagged, + any.attoparsec ==0.14.4, + attoparsec -developer, + any.attoparsec-aeson ==2.2.0.1, + any.base ==4.19.0.0, + any.base-compat ==0.13.1, + any.base-orphans ==0.9.1, + any.bifunctors ==5.6.1, + bifunctors +tagged, + any.binary ==0.8.9.1, + any.bytestring ==0.11.5.3, + any.call-stack ==0.4.0, + any.cereal ==0.5.8.3, + cereal -bytestring-builder, + any.cereal-text ==0.1.0.2, + any.cmdargs ==0.10.22, + cmdargs +quotation -testprog, + any.colour ==2.3.6, + any.comonad ==5.0.8, + comonad +containers +distributive +indexed-traversable, + any.containers ==0.6.8, + any.contravariant ==1.5.5, + contravariant +semigroups +statevar +tagged, + any.data-default ==0.7.1.1, + any.data-default-class ==0.1.2.0, + any.data-default-instances-containers ==0.0.1, + any.data-default-instances-dlist ==0.0.1, + any.data-default-instances-old-locale ==0.0.1, + any.data-fix ==0.3.2, + any.deepseq ==1.5.0.0, + any.directory ==1.3.8.1, + any.distributive ==0.6.2.1, + distributive +semigroups +tagged, + any.dlist ==1.0, + dlist -werror, + any.exceptions ==0.10.7, + any.file-embed ==0.0.15.0, + any.filepath ==1.4.200.1, + filepath -cpphs, + any.generically ==0.1.1, + any.ghc-bignum ==1.3, + any.ghc-boot-th ==9.8.1, + any.ghc-prim ==0.11.0, + any.gitrev ==1.3.1, + any.happy ==1.20.1.1, + any.hashable ==1.4.3.0, + hashable +integer-gmp -random-initial-seed, + any.hsc2hs ==0.68.10, + hsc2hs -in-ghc-tree, + any.indexed-traversable ==0.1.3, + any.indexed-traversable-instances ==0.1.1.2, + any.integer-conversion ==0.1.0.1, + any.integer-logarithms ==1.0.3.1, + integer-logarithms -check-bounds +integer-gmp, + any.linkedhashmap ==0.4.0.0, + any.mnist-idx ==0.1.3.2, + any.mtl ==2.3.1, + any.network-uri ==2.6.4.2, + any.old-locale ==1.0.0.7, + any.optparse-applicative ==0.18.1.0, + optparse-applicative +process, + any.parsec ==3.1.17.0, + any.pretty ==1.1.3.6, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.prettyprinter-ansi-terminal ==1.1.3, + any.primitive ==0.9.0.0, + any.process ==1.6.18.0, + any.random ==1.2.1.1, + any.regex-base ==0.94.0.2, + any.regex-tdfa ==1.3.2.2, + regex-tdfa +doctest -force-o2, + any.rts ==1.0.2, + any.scientific ==0.3.7.0, + scientific -bytestring-builder -integer-simple, + any.semialign ==1.3, + semialign +semigroupoids, + any.semigroupoids ==6.0.0.1, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.split ==0.2.5, + any.splitmix ==0.1.0.5, + splitmix -optimised-mixer, + any.sscript ==0.1.0.2, + any.stm ==2.5.2.1, + any.strict ==0.5, + any.string-qq ==0.0.5, + any.system-cxx-std-lib ==1.0, + any.tagged ==0.8.8, + tagged +deepseq +transformers, + any.tasty ==1.4.3, + tasty +unix, + any.tasty-hunit ==0.10.1, + any.template-haskell ==2.21.0.0, + any.temporary ==1.3, + any.terminal-progress-bar ==0.4.2, + any.terminal-size ==0.3.4, + any.text ==2.1, + text -developer +simdutf, + any.text-iso8601 ==0.1, + any.text-short ==0.1.5, + text-short -asserts, + any.th-abstraction ==0.6.0.0, + any.th-compat ==0.1.4, + any.these ==1.2, + any.time ==1.12.2, + any.time-compat ==1.9.6.1, + time-compat -old-locale, + any.transformers ==0.6.1.0, + any.transformers-compat ==0.7.2, + transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, + any.unix ==2.8.5.0, + unix -os-string, + any.unordered-containers ==0.2.20, + unordered-containers -debug, + any.uuid-types ==1.0.5.1, + any.vector ==0.13.1.0, + vector +boundschecks -internalchecks -unsafechecks -wall, + any.vector-stream ==0.1.0.1, + vehicle -ghc-debug -nothunks -optimise-heavily -release-build, + vehicle-syntax -ghc-debug -nothunks -optimise-heavily, + any.witherable ==0.4.2 +index-state: hackage.haskell.org 2024-01-12T12:48:28Z 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 1afab82b0..7ff51aa15 100644 --- a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs +++ b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs @@ -8,7 +8,7 @@ module Test.Tasty.Golden.Executable.Runner where -import Control.Exception (assert, throw) +import Control.Exception (throw) import Control.Monad (unless, when) import Control.Monad.Catch (MonadCatch (..), MonadMask, MonadThrow, handle) import Control.Monad.IO.Class (MonadIO) @@ -345,7 +345,7 @@ acceptTestProduced testProduces (IgnoreFiles testIgnores) = do let testSpecsList = toList testSpecs let thisTestIndices = List.findIndices ((== testName) . testSpecName) testSpecsList -- There should be EXACTLY ONE test named testSpecName: - thisTestIndex <- assert (length thisTestIndices == 1) (return $ head thisTestIndices) + thisTestIndex <- maybe (error $ "No unique test named '" <> testName <> "'") (return . fst) (List.uncons thisTestIndices) let (otherTestSpecsBefore, thisTestSpecAndOtherTestSpecsAfter) = List.splitAt thisTestIndex testSpecsList let (thisTestSpec, otherTestSpecsAfter) = fromMaybe (error $ printf "Could not find test named '%s'" testName) $ diff --git a/tasty-golden-executable/tasty-golden-executable.cabal b/tasty-golden-executable/tasty-golden-executable.cabal index f8f714738..37e276930 100644 --- a/tasty-golden-executable/tasty-golden-executable.cabal +++ b/tasty-golden-executable/tasty-golden-executable.cabal @@ -50,7 +50,7 @@ library Test.Tasty.Golden.Executable.TestSpecs build-depends: - , aeson >=2.1.1 && <2.2 + , aeson >=2.1.1 && <2.3 , aeson-pretty >=0.8.9 && <0.9 , array >=0.5.4 && <0.6 , base >=4.13 && <5 diff --git a/vehicle-syntax/vehicle-syntax.cabal b/vehicle-syntax/vehicle-syntax.cabal index 69c509609..7d1f2a1d1 100644 --- a/vehicle-syntax/vehicle-syntax.cabal +++ b/vehicle-syntax/vehicle-syntax.cabal @@ -152,18 +152,18 @@ library Vehicle.Syntax.Internal.Print build-depends: - , aeson ^>=2.1.1 - , array >=0.5 && <1 - , base >=4 && <5 - , cereal >=0.5 && <1 - , cereal-text >=0.1 && <1 - , containers >=0.5 && <1 - , deepseq >=1.4 && <2 - , hashable >=1.3 && <2 - , mtl >=2.2 && <3 - , prettyprinter >=1.7 && <2 - , text >=1.2 && <3 - , these >=1.0 && <2 + , aeson >=2.1.1 && <2.3 + , array >=0.5 && <1 + , base >=4 && <5 + , cereal >=0.5 && <1 + , cereal-text >=0.1 && <1 + , containers >=0.5 && <1 + , deepseq >=1.4 && <2 + , hashable >=1.3 && <2 + , mtl >=2.2 && <3 + , prettyprinter >=1.7 && <2 + , text >=1.2 && <3 + , these >=1.0 && <2 build-tool-depends: , alex:alex >=3.2 diff --git a/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs b/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs index 764199d92..764de6e0c 100644 --- a/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs +++ b/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs @@ -69,7 +69,9 @@ preprocessLogicalOperators logic = traverse (traverseBuiltinsM builtinUpdateFunc builtinUpdateFunction p1 p2 b args = do maybeUpdatedExpr <- case b of S.BuiltinFunction S.Not -> case compileNot logic of - TryToEliminate -> Just <$> lowerNot p2 (argExpr $ head args) + TryToEliminate -> case args of + [arg] -> Just <$> lowerNot p2 (argExpr arg) + _ -> compilerDeveloperError "Found partially applied Not" UnaryNot {} -> return Nothing _ -> return Nothing diff --git a/vehicle/src/Vehicle/Backend/Queries/Error.hs b/vehicle/src/Vehicle/Backend/Queries/Error.hs index e77ea7c66..c7e8f2b59 100644 --- a/vehicle/src/Vehicle/Backend/Queries/Error.hs +++ b/vehicle/src/Vehicle/Backend/Queries/Error.hs @@ -28,11 +28,10 @@ diagnoseNonLinearity queryFormat prog propertyProv@(propertyIdentifier, _) = do <+> quotePretty propertyIdentifier <> line - Main typedDecls <- typeCheckWithSubsystem mempty handleUnexpectedError prog + subTypedProg <- typeCheckWithSubsystem mempty handleUnexpectedError prog -- Extract and diagnose the type. - let property = head $ filter (\decl -> identifierOf decl == propertyIdentifier) typedDecls - let propertyType = typeOf property + propertyType <- findDeclType propertyIdentifier subTypedProg case propertyType of LinearityExpr _ (NonLinear source) -> do throwError $ UnsupportedNonLinearConstraint queryFormat propertyProv (Right source) @@ -56,11 +55,10 @@ diagnoseAlternatingQuantifiers queryFormat prog propertyProv@(propertyIdentifier <+> quotePretty propertyIdentifier <> line - Main typedDecls <- typeCheckWithSubsystem mempty handleUnexpectedError prog + subTypedProg <- typeCheckWithSubsystem mempty handleUnexpectedError prog -- Extract and diagnose the type. - let property = head $ filter (\decl -> identifierOf decl == propertyIdentifier) typedDecls - let propertyType = typeOf property + propertyType <- findDeclType propertyIdentifier subTypedProg case propertyType of PolarityExpr _ (MixedSequential q p pp2) -> do throwError $ UnsupportedAlternatingQuantifiers queryFormat propertyProv (Right (q, p, pp2)) @@ -69,3 +67,10 @@ diagnoseAlternatingQuantifiers queryFormat prog propertyProv@(propertyIdentifier handleUnexpectedError :: (MonadCompile m) => CompileError -> m a handleUnexpectedError err = throwError $ UnsupportedAlternatingQuantifiers queryFormat propertyProv (Left err) + +findDeclType :: (MonadCompile m) => Identifier -> Prog Ix builtin -> m (Expr Ix builtin) +findDeclType ident (Main decls) = do + let candidates = filter (\decl -> identifierOf decl == ident) decls + case candidates of + [property] -> return $ typeOf property + _ -> compilerDeveloperError $ "Could not find property" <+> quotePretty ident <+> "in program after subtyping." diff --git a/vehicle/src/Vehicle/Compile/Error/Message.hs b/vehicle/src/Vehicle/Compile/Error/Message.hs index 35fdfc303..adb65d412 100644 --- a/vehicle/src/Vehicle/Compile/Error/Message.hs +++ b/vehicle/src/Vehicle/Compile/Error/Message.hs @@ -204,9 +204,9 @@ instance MeaningfulError CompileError where <+> quotePretty annotationName <+> "annotation.", fix = - if null suggestions - then Nothing - else Just $ "did you mean" <+> quotePretty (head suggestions) <> "?" + case suggestions of + [] -> Nothing + (s : _) -> Just $ "did you mean" <+> quotePretty s <> "?" } InvalidAnnotationOptionValue p parameterName parameterValue -> UError $ @@ -421,7 +421,9 @@ instance MeaningfulError CompileError where <> line <> indent 2 deducedType <> line - <> "but" <+> originExpr <+> "has only the following valid types:" + <> "but" + <+> originExpr + <+> "has only the following valid types:" <> line <> indent 2 (vsep (fmap calculateCandidateType candidates)), fix = Nothing @@ -1245,13 +1247,15 @@ supportedNetworkTypeDescription = errorInSubsystemMessage :: Doc a -> CompileError -> Doc a errorInSubsystemMessage task err = line - <> "Unfortunately while trying to" <+> task + <> "Unfortunately while trying to" + <+> task <> "," <+> "the following error was encountered:" <> line <> indent 2 (pretty (details err)) <> line - <> "Please report this as an issue on Github" <+> parens githubIssues + <> "Please report this as an issue on Github" + <+> parens githubIssues <> line githubIssues :: Doc a diff --git a/vehicle/src/Vehicle/Compile/Simplify.hs b/vehicle/src/Vehicle/Compile/Simplify.hs index 9d3f1ae7e..e5e149bc9 100644 --- a/vehicle/src/Vehicle/Compile/Simplify.hs +++ b/vehicle/src/Vehicle/Compile/Simplify.hs @@ -48,18 +48,29 @@ instance Simplify (Expr Name Builtin) where shortenVec = mapBuiltins $ \p1 p2 b args -> case b of - BuiltinConstructor (LVec n) - | length args > 5 -> - normAppList - p1 - (Builtin p2 (BuiltinConstructor (LVec n))) - [ head args, - Arg p2 Explicit Relevant (FreeVar p2 (Identifier StdLib ("<" <> n2 <> " more>"))), - last args - ] - where - n2 = Text.pack $ show $ length args - 2 + BuiltinConstructor (LVec n) -> case getHeadMidTail args of + Just (firstArg, numberOfMiddleAgs, lastArg) + | numberOfMiddleAgs > 3 -> + normAppList + p1 + (Builtin p2 (BuiltinConstructor (LVec n))) + [ firstArg, + Arg p2 Explicit Relevant (FreeVar p2 (Identifier StdLib ("<" <> n2 <> " more>"))), + lastArg + ] + where + n2 = Text.pack $ show $ length args - 2 + _ -> normAppList p1 (Builtin p2 b) args _ -> normAppList p1 (Builtin p2 b) args + where + getHeadMidTail :: forall a. [a] -> Maybe (a, Int, a) + getHeadMidTail [] = Nothing + getHeadMidTail (x : xs) = go 0 xs + where + go :: Int -> [a] -> Maybe (a, Int, a) + go _ [] = Nothing + go l [e] = Just (x, l, e) + go l (_ : ys) = go (l + 1) ys instance Simplify (Binder Name Builtin) where uninsert = fmap uninsert diff --git a/vehicle/src/Vehicle/Data/LinearExpr.hs b/vehicle/src/Vehicle/Data/LinearExpr.hs index 18f7d86b8..07b0f04ab 100644 --- a/vehicle/src/Vehicle/Data/LinearExpr.hs +++ b/vehicle/src/Vehicle/Data/LinearExpr.hs @@ -83,7 +83,8 @@ foldTensor :: forall a. (Rational -> a) -> ([a] -> a) -> RationalTensor -> a foldTensor mkValue mkVec (RationalTensor dims value) = go dims (Vector.toList value) where go :: TensorDimensions -> [Rational] -> a - go [] xs = mkValue (head xs) + go [] [x] = mkValue x + go [] _xs = developerError "Mis-sized tensor. Expected a single element." go (_d : ds) xs = do let inputVarIndicesChunks = chunksOf (product ds) xs let elems = fmap (go ds) inputVarIndicesChunks diff --git a/vehicle/src/Vehicle/Verify/Specification/Status.hs b/vehicle/src/Vehicle/Verify/Specification/Status.hs index b1259013f..f4f10875e 100644 --- a/vehicle/src/Vehicle/Verify/Specification/Status.hs +++ b/vehicle/src/Vehicle/Verify/Specification/Status.hs @@ -92,7 +92,8 @@ prettyUserVariableAssignment (OriginalUserVariable {..}, variableValue) = pretty userTensorVarName <> ":" <+> pretty variableValue assignmentToExpr :: TensorDimensions -> [Rational] -> Expr Ix Builtin -assignmentToExpr [] xs = RatLiteral mempty (toRational (head xs)) +assignmentToExpr [] [x] = RatLiteral mempty (toRational x) +assignmentToExpr [] _ = developerError "Malformed tensor" assignmentToExpr (dim : dims) xs = do let vecConstructor = Builtin mempty (BuiltinConstructor $ LVec dim) let inputVarIndicesChunks = chunksOf (product dims) xs diff --git a/vehicle/tests/unit/Vehicle/Test/Unit/Compile/CommandLine.hs b/vehicle/tests/unit/Vehicle/Test/Unit/Compile/CommandLine.hs index 53a419aef..ee25ec579 100644 --- a/vehicle/tests/unit/Vehicle/Test/Unit/Compile/CommandLine.hs +++ b/vehicle/tests/unit/Vehicle/Test/Unit/Compile/CommandLine.hs @@ -17,6 +17,7 @@ import Vehicle.CommandLine ) import Vehicle.Prelude ( Pretty (pretty), + developerError, indent, layoutAsString, line, @@ -181,7 +182,9 @@ verifyTests = parserTest :: String -> String -> Options -> TestTree parserTest name command expected = testCase name $ do - let args = tail $ words command + let args = case words command of + (_ : as) -> as + _ -> developerError "Malformed command. Commands must start with 'vehicle'" let result = execParserPure defaultPrefs commandLineOptionsParserInfo args case result of diff --git a/vehicle/vehicle.cabal b/vehicle/vehicle.cabal index 12a655375..851c26f69 100644 --- a/vehicle/vehicle.cabal +++ b/vehicle/vehicle.cabal @@ -266,7 +266,7 @@ library autogen-modules: Paths_vehicle build-depends: - , aeson >=2.1.1 && <2.2 + , aeson >=2.1.1 && <2.3 , aeson-pretty >=0.8.9 && <0.9 , ansi-terminal >=0.6 && <1 , base >=4.13 && <5