copilot-language 3.7 → 4.8
raw patch · 32 files changed
Files
- CHANGELOG +124/−8
- copilot-language.cabal +47/−12
- src/Copilot.hs +0/−14
- src/Copilot/Language.hs +3/−16
- src/Copilot/Language/Analyze.hs +32/−47
- src/Copilot/Language/Error.hs +0/−2
- src/Copilot/Language/Interpret.hs +8/−13
- src/Copilot/Language/Operators/Array.hs +63/−24
- src/Copilot/Language/Operators/BitWise.hs +8/−2
- src/Copilot/Language/Operators/Boolean.hs +0/−6
- src/Copilot/Language/Operators/Cast.hs +1/−27
- src/Copilot/Language/Operators/Constant.hs +0/−7
- src/Copilot/Language/Operators/Eq.hs +0/−6
- src/Copilot/Language/Operators/Extern.hs +0/−6
- src/Copilot/Language/Operators/Integral.hs +0/−6
- src/Copilot/Language/Operators/Label.hs +0/−6
- src/Copilot/Language/Operators/Local.hs +0/−6
- src/Copilot/Language/Operators/Mux.hs +0/−8
- src/Copilot/Language/Operators/Ord.hs +0/−6
- src/Copilot/Language/Operators/Projection.hs +38/−0
- src/Copilot/Language/Operators/Propositional.hs +4/−7
- src/Copilot/Language/Operators/Struct.hs +79/−9
- src/Copilot/Language/Operators/Temporal.hs +0/−5
- src/Copilot/Language/Prelude.hs +0/−4
- src/Copilot/Language/Reify.hs +18/−20
- src/Copilot/Language/Spec.hs +20/−38
- src/Copilot/Language/Stream.hs +3/−33
- src/System/Mem/StableName/Dynamic.hs +7/−8
- src/System/Mem/StableName/Map.hs +0/−2
- tests/Main.hs +18/−0
- tests/Test/Copilot/Language/Reify.hs +782/−0
- tests/Test/Extra.hs +31/−0
CHANGELOG view
@@ -1,3 +1,119 @@+2026-07-07+ * Version bump (4.8). (#745)++2026-05-07+ * Version bump (4.7.1). (#730)++2026-03-07+ * Version bump (4.7). (#714)++2026-01-07+ * Version bump (4.6.1). (#705)+ * Relax version constraint on containers. (#603)++2025-11-07+ * Version bump (4.6). (#679)++2025-09-07+ * Version bump (4.5.1). (#666)++2025-07-07+ * Version bump (4.5). (#642)++2025-05-07+ * Version bump (4.4). (#618)++2025-03-07+ * Version bump (4.3). (#604)+ * Fix typo in documentation. (#587)+ * Record how a Property's underlying proposition is quantified. (#254)+ * Remove deprecated function Copilot.Language.Operators.Array.(.!!).+ (#599)++2025-01-07+ * Version bump (4.2). (#577)+ * Bump upper version constraint on containers. (#570)++2024-11-07+ * Version bump (4.1). (#561)+ * Reject duplicate externs in properties and theorems. (#536)+ * Standardize changelog format. (#550)++2024-09-07+ * Version bump (4.0). (#532)+ * Add support for array updates. (#36)++2024-07-07+ * Version bump (3.20). (#522)+ * Remove deprecated function Copilot.Language.Spec.forall. (#518)+ * Add support for struct field updates. (#520)++2024-05-07+ * Version bump (3.19.1). (#512)++2024-03-07+ * Version bump (3.19). (#504)++2024-01-07+ * Version bump (3.18.1). (#493)++2024-01-07+ * Version bump (3.18). (#487)+ * Add type annotation to help type inference engine. (#469)+ * Rename forall to forAll. (#470)++2023-11-07+ * Version bump (3.17). (#466)++2023-09-07+ * Version bump (3.16.1). (#455)++2023-07-07+ * Version bump (3.16). (#448)+ * Move Copilot.Language.Stream.Arg to Copilot.Language.Spec. (#446)++2023-05-07+ * Version bump (3.15). (#438)+ * Remove outdated comment about pretty-printer. (#428)++2023-03-07+ * Version bump (3.14). (#422)+ * Remove function Copilot.Language.prettyPrint. (#412)+ * Adjust to work with GHC 9.4. (#423)++2023-01-07+ * Version bump (3.13). (#406)++2022-11-07+ * Version bump (3.12). (#389)+ * Use pretty-printer from copilot-prettyprinter. (#383)++2022-09-07+ * Version bump (3.11). (#376)+ * Deprecate prettyPrint. (#362)+ * Reimplement DynStableName without unsafeCoerce. (#262)+ * Use interpreter from copilot-interpreter. (#361)+ * Remove unnecessary type constraints. (#369)++2022-07-07+ * Version bump (3.10). (#356)+ * Fix error in test case generation; enable CLI args in tests. (#337)+ * Remove duplicated compiler option. (#328)+ * Adjust imports due to deprecation. (#330)+ * Fix typos in Copilot.Language.Interpret. (#331)+ * Update repo info in cabal file. (#333)++2022-05-06+ * Version bump (3.9). (#320)+ * Compliance with style guide (partial). (#316)++2022-03-07+ * Version bump (3.8). (#298)+ * Introduce testing infrastructure. (#271)+ * Remove deprecated module Copilot. (#291)+ * Remove deprecated type StructArg. (#290)+ * Mark package as uncurated to avoid modification. (#288)+ 2022-01-07 * Version bump (3.7). (#287) * Bring back externF. (#261)@@ -33,12 +149,12 @@ * Completed the documentation. (#112) 2020-05-07- * Version bump (3.2).- * Fixed the reverse order of triggers (#114).- * Update description, bug-reports, changelog fields in cabal file- (#116).- * Bump ghc-prim version bounds (#122).+ * Version bump (3.2). (#65)+ * Fixed the reverse order of triggers. (#114)+ * Update description, bug-reports, changelog fields in cabal file.+ (#116)+ * Bump ghc-prim version bounds. (#122) -2019-11-22 Ivan Perez <ivan.perez@nianet.org>- * Version bump (3.1).- * Remove ExternFun (#118).+2019-11-22+ * Version bump (3.1). (#46)+ * Remove ExternFun. (#118)
copilot-language.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language-version: 3.7+version: 4.8 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description:@@ -25,26 +25,28 @@ build-type: Simple extra-source-files: README.md, CHANGELOG +x-curation: uncurated+ source-repository head type: git location: https://github.com/Copilot-Language/copilot.git- subdir: lib/copilot-language+ subdir: copilot-language library default-language: Haskell2010 hs-source-dirs: src- build-depends: base >= 4.9 && < 5+ build-depends: base >= 4.9 && < 5 - , array >= 0.5 && < 0.6- , containers >= 0.4 && < 0.7- , data-reify >= 0.6 && < 0.7- , mtl >= 2.0 && < 3+ , array >= 0.5 && < 0.6+ , containers >= 0.4 && < 0.9+ , data-reify >= 0.6 && < 0.7+ , mtl >= 2.0 && < 3 - , copilot-core >= 3.7 && < 3.8- , copilot-theorem >= 3.7 && < 3.8+ , copilot-core >= 4.8 && < 4.9+ , copilot-interpreter >= 4.8 && < 4.9+ , copilot-theorem >= 4.8 && < 4.9 - exposed-modules: Copilot- , Copilot.Language+ exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise , Copilot.Language.Operators.Boolean , Copilot.Language.Operators.Propositional@@ -59,6 +61,7 @@ , Copilot.Language.Operators.Ord , Copilot.Language.Operators.Temporal , Copilot.Language.Operators.Array+ , Copilot.Language.Operators.Projection , Copilot.Language.Operators.Struct , Copilot.Language.Prelude , Copilot.Language.Reify@@ -70,5 +73,37 @@ , System.Mem.StableName.Map , Copilot.Language.Error ghc-options:- -fwarn-tabs+ -Wall++test-suite unit-tests+ type:+ exitcode-stdio-1.0++ main-is:+ Main.hs++ other-modules:+ Test.Copilot.Language.Reify+ Test.Extra++ build-depends:+ base+ , HUnit+ , QuickCheck+ , pretty+ , test-framework+ , test-framework-hunit+ , test-framework-quickcheck2++ , copilot-core+ , copilot-interpreter+ , copilot-language++ hs-source-dirs:+ tests++ default-language:+ Haskell2010++ ghc-options: -Wall
− src/Copilot.hs
@@ -1,14 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE Safe #-}--module Copilot- {-# DEPRECATED "This module is deprecated." #-}- ( module Copilot.Language- ) where--import Copilot.Language----------------------------------------------------------------------------------
src/Copilot/Language.hs view
@@ -1,12 +1,9 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Main Copilot language export file. -- -- This is mainly a meta-module that re-exports most definitions in this--- library. It also provides a default pretty printer that prints a--- specification to stdout.+-- library. {-# LANGUAGE Safe #-} @@ -40,8 +37,8 @@ , arg , prop , theorem- , forall, exists- , prettyPrint+ , forAll+ , exists ) where import Data.Int hiding (Int)@@ -49,7 +46,6 @@ import Copilot.Core (Name, Typed) import Copilot.Core.Type import Copilot.Core.Type.Array-import qualified Copilot.Core.PrettyPrint as PP import Copilot.Language.Error import Copilot.Language.Interpret import Copilot.Language.Operators.Boolean@@ -70,12 +66,3 @@ import Copilot.Language.Prelude import Copilot.Language.Spec import Copilot.Language.Stream (Stream)-------------------------------------------------------------------------------------- | Transform a high-level Copilot Language specification into a low-level--- Copilot Core specification and pretty-print it to stdout.-prettyPrint :: Spec -> IO ()-prettyPrint e = fmap PP.prettyPrint (reify e) >>= putStr----------------------------------------------------------------------------------
src/Copilot/Language/Analyze.hs view
@@ -1,10 +1,8 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} -- | Copilot specification sanity check.@@ -16,9 +14,10 @@ import Copilot.Core (DropIdx) import qualified Copilot.Core as C-import Copilot.Language.Stream (Stream (..), Arg (..))+import Copilot.Language.Stream (Stream (..)) import Copilot.Language.Spec import Copilot.Language.Error (badUsage)+import Copilot.Theorem.Prove (UProof) import Data.List (groupBy) import Data.IORef@@ -29,8 +28,6 @@ import Control.Monad (when, foldM_, foldM) import Control.Exception (Exception, throw) ---------------------------------------------------------------------------------- -- | Exceptions or kinds of errors in Copilot specifications that the analysis -- implemented is able to detect. data AnalyzeException@@ -57,7 +54,7 @@ show NestedArray = badUsage $ "An external function cannot take another external function or external array as an argument. Try defining a stream, and using the stream values in the other definition." show TooMuchRecursion = badUsage $- "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition. Likely, you have accidently defined a circular stream, such as 'x = x'. Another possibility is you have defined a a polymorphic function with type constraints that references other streams. For example,\n\n nats :: (Typed a, Num a) => Stream a\n nats = [0] ++ nats + 1\n\nis not allowed. Make the definition monomorphic, or add a level of indirection, like \n\n nats :: (Typed a, Num a) => Stream a\n nats = n\n where n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression. You can try shrinking the expression by using local variables. It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language."+ "You have exceeded the limit of " ++ show maxRecursion ++ " recursive calls in a stream definition. Likely, you have accidently defined a circular stream, such as 'x = x'. Another possibility is you have defined a a polymorphic function with type constraints that references other streams. For example,\n\n nats :: (Typed a, Num a) => Stream a\n nats = [0] ++ nats + 1\n\nis not allowed. Make the definition monomorphic, or add a level of indirection, like \n\n nats :: (Typed a, Num a) => Stream a\n nats = n\n where\n n = [0] ++ n + 1\n\nFinally, you may have intended to generate a very large expression. You can try shrinking the expression by using local variables. It all else fails, you can increase the maximum size of ecursive calls by modifying 'maxRecursion' in copilot-language." show InvalidField = badUsage $ "A struct can only take external variables, arrays, or other structs as fields." show (DifferentTypes name) = badUsage $@@ -77,13 +74,9 @@ maxRecursion :: Int maxRecursion = 100000 ---------------------------------------------------------------------------------- -- | An environment that contains the nodes visited. type Env = Map () ---------------------------------------------------------------------------------- -- | Analyze a Copilot specification and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -96,8 +89,6 @@ mapM_ (analyzeProperty refStreams) (map fst $ theorems $ runSpec spec) specExts refStreams spec >>= analyzeExts ---------------------------------------------------------------------------------- -- | Analyze a Copilot trigger and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -109,31 +100,27 @@ analyzeTriggerArg :: Arg -> IO () analyzeTriggerArg (Arg e) = analyzeExpr refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot observer and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeObserver :: IORef Env -> Observer -> IO () analyzeObserver refStreams (Observer _ e) = analyzeExpr refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot property and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'. analyzeProperty :: IORef Env -> Property -> IO ()-analyzeProperty refStreams (Property _ e) = analyzeExpr refStreams e----------------------------------------------------------------------------------+analyzeProperty refStreams (Property _ p) =+ -- Soundness note: it is OK to call `extractProp` here to drop the quantifier+ -- from the proposition `p`, as the analysis does not depend on what the+ -- quantifier is.+ analyzeExpr refStreams (extractProp p) data SeenExtern = NoExtern | SeenFun | SeenArr | SeenStruct ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream and report any errors detected. -- -- This function can fail with one of the exceptions in 'AnalyzeException'.@@ -165,8 +152,6 @@ go seenExt nodes' e3 Label _ e -> go seenExt nodes' e ---------------------------------------------------------------------------------- -- | Detect whether the given stream name has already been visited. -- -- This function throws a 'ReferentialCycle' exception if the second argument@@ -178,16 +163,12 @@ Just () -> throw ReferentialCycle Nothing -> return () ---------------------------------------------------------------------------------- -- | Check that the level of recursion is not above the max recursion allowed. mapCheck :: IORef Env -> IO Bool mapCheck refStreams = do ref <- readIORef refStreams return $ getSize ref > maxRecursion ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream append and report any errors detected. analyzeAppend :: IORef Env -> DynStableName -> Stream a -> b@@ -200,8 +181,6 @@ modifyIORef refStreams $ M.insert dstn () f refStreams e ---------------------------------------------------------------------------------- -- | Analyze a Copilot stream drop and report any errors detected. -- -- This function can fail if the drop is exercised over a stream that is not an@@ -214,12 +193,9 @@ | otherwise = return () analyzeDrop _ _ = throw DropAppliedToNonAppend ---------------------------------------------------------------------------------- -- Analyzing external variables. We check that every reference to an external -- variable has the same type, and for external functions, they have the same -- typed arguments.--------------------------------------------------------------------------------- -- | An environment to store external variables, arrays, functions and structs, -- so that we can check types in the expression---e.g., if we declare the same@@ -231,8 +207,6 @@ , externStructArgs :: [(String, [C.SimpleType])] } ---------------------------------------------------------------------------------- -- | Make sure external variables, functions, arrays, and structs are correctly -- typed. analyzeExts :: ExternEnv -> IO ()@@ -296,15 +270,19 @@ (head grp) -- should be typesafe, since this is from groupBy grp ---------------------------------------------------------------------------------- -- | Obtain all the externs in a specification. specExts :: IORef Env -> Spec' a -> IO ExternEnv specExts refStreams spec = do- env <- foldM triggerExts- (ExternEnv [] [] [] [])- (triggers $ runSpec spec)- foldM observerExts env (observers $ runSpec spec)+ env0 <- foldM triggerExts+ (ExternEnv [] [] [] [])+ (triggers $ runSpec spec)+ env1 <- foldM observerExts+ env0+ (observers $ runSpec spec)+ env2 <- foldM propertyExts+ env1+ (properties $ runSpec spec)+ foldM theoremExts env2 (theorems $ runSpec spec) where observerExts :: ExternEnv -> Observer -> IO ExternEnv@@ -316,6 +294,17 @@ foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'') env' args + propertyExts :: ExternEnv -> Property -> IO ExternEnv+ propertyExts env (Property _ p) =+ -- Soundness note: it is OK to call `extractProp` here to drop the+ -- quantifier from the proposition `p`. This is because we are simply+ -- gathering externs from `p`, and the presence of externs does not depend+ -- on what the quantifier is.+ collectExts refStreams (extractProp p) env++ theoremExts :: ExternEnv -> (Property, UProof) -> IO ExternEnv+ theoremExts env (p, _) = propertyExts env p+ -- | Obtain all the externs in a stream. collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv collectExts refStreams stream_ env_ = do@@ -348,11 +337,7 @@ go nodes env'' e3 Label _ e -> go nodes env e ---------------------------------------------------------------------------------- -- | Return the simple C type representation of the type of the values carried -- by a stream. getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)----------------------------------------------------------------------------------
src/Copilot/Language/Error.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-}
src/Copilot/Language/Interpret.hs view
@@ -1,28 +1,27 @@-{- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc. -}+-- Copyright (c) 2011 National Institute of Aerospace / Galois, Inc. --- | This module implements two interpreters, which may be used to simulated or--- executed Copilot specifications on a computer to understand their behavior--- to debug possible errors.+-- | This module implements two interpreters, which may be used to simulate or+-- execute Copilot specifications on a computer to understand their behavior to+-- debug possible errors. -- -- The interpreters included vary in how the present the results to the user. -- One of them uses a format (csv) that may be more machine-readable, while the -- other uses a format that may be easier for humans to read. -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs, FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Safe #-} module Copilot.Language.Interpret ( csv , interpret ) where -import qualified Copilot.Core.Interpret as I+import qualified Copilot.Interpret as I import Copilot.Language.Spec (Spec) import Copilot.Language.Reify ---------------------------------------------------------------------------------- -- | Simulate a number of steps of a given specification, printing the results -- in a table in comma-separated value (CSV) format. csv :: Integer -> Spec -> IO ()@@ -30,8 +29,6 @@ putStrLn "Note: CSV format does not output observers." interpret' I.CSV i spec ---------------------------------------------------------------------------------- -- | Simulate a number of steps of a given specification, printing the results -- in a table in readable format. --@@ -46,5 +43,3 @@ interpret' format i spec = do coreSpec <- reify spec putStrLn $ I.interpret format (fromIntegral i) coreSpec----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Array.hs view
@@ -1,37 +1,76 @@-{-# LANGUAGE Safe #-}--{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeFamilies #-}+-- The following warning is disabled due to a necessary instance of Projectable+-- defined in this module.+{-# OPTIONS_GHC -fno-warn-orphans #-} -- | Combinators to deal with streams carrying arrays. module Copilot.Language.Operators.Array- ( (.!!)+ ( (!)+ , (!!)+ , (=:)+ , (=$) ) where -import Copilot.Core ( Typed- , Op2 (Index)- , typeOf- , Array- , InnerType- , Flatten)-import Copilot.Language.Stream (Stream (..))--import Data.Word (Word32)-import GHC.TypeLits (KnownNat)+import Copilot.Core (Array, Op2 (Index),+ Op3 (UpdateArray), Typed, typeOf)+import Copilot.Language.Operators.Projection (Projectable(..))+import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------+import Data.Word (Word32)+import GHC.TypeLits (KnownNat)+import Prelude hiding ((!!)) -- | Create a stream that carries an element of an array in another stream. -- -- This function implements a projection of the element of an array at a given -- position, over time. For example, if @s@ is a stream of type @Stream (Array--- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd+-- '5 Word8)@, then @s ! 3@ has type @Stream Word8@ and contains the 3rd -- element (starting from zero) of the arrays in @s@ at any point in time.-(.!!) :: ( KnownNat n- , t' ~ InnerType t- , Flatten t t'- , Typed t- , Typed t'- ) => Stream (Array n t) -> Stream Word32 -> Stream t-arr .!! n = Op2 (Index typeOf) arr n+(!) :: (KnownNat n, Typed t)+ => Stream (Array n t) -> Stream Word32 -> Stream t+arr ! n = Op2 (Index typeOf) arr n ---------------------------------------------------------------------------------+-- | Pair a stream with an element accessor, without applying it to obtain the+-- value of the element.+--+-- This function is needed to refer to an element accessor when the goal is to+-- update the element value, not just to read it.+(!!) :: Stream (Array n t)+ -> Stream Word32+ -> Projection (Array n t) (Stream Word32) t+(!!) = ProjectionA++-- | Update a stream of arrays.++-- This is an orphan instance; we suppress the warning that GHC would+-- normally produce with a GHC option at the top.+instance (KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t where++ -- | A projection of an element of a stream of arrays.+ data Projection (Array n t) (Stream Word32) t =+ ProjectionA (Stream (Array n t)) (Stream Word32)++ -- | Create a stream where an element of an array has been updated with+ -- values from another stream.+ --+ -- For example, if an array has two elements of type @Int32@, and @s@ is a+ -- stream of such array type (@Stream (Array 2 Int32)@), and $v0$ is a stream+ -- of type @Int32@, then @s !! 0 =: v0@ has type @Stream (Array 2 Int32)@ and+ -- contains arrays where the value of the first element of each array is that+ -- of @v0@ at each point in time, and the value of the second element in the+ -- array is the same it had in @s@.+ (=:) (ProjectionA s ix) v = Op3 (UpdateArray typeOf) s ix v++ -- | Create a stream where an element of an array has been updated by+ -- applying a stream function to it.+ --+ -- For example, if an array has two elements of type @Int32@, and @s@ is a+ -- stream of such array type (@Stream (Array 2 Int32)@), and $f$ is function+ -- of type @Stream Int32 -> Stream Int32@, then @s !! 0 =$ f@ has type+ -- @Stream (Array 2 Int32)@ and contains arrays where the value of the first+ -- element of each array is that of @f (s ! 0)@ at each point in time, and+ -- the value of the second element in the array is the same it had in @s@.+ (=$) (ProjectionA s ix) op = Op3 (UpdateArray typeOf) s ix (op (s ! ix))
src/Copilot/Language/Operators/BitWise.hs view
@@ -1,7 +1,6 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE Safe #-} {-# OPTIONS_GHC -fno-warn-orphans #-}@@ -18,7 +17,12 @@ import qualified Copilot.Core as Core import Copilot.Language.Stream import qualified Prelude as P++#if MIN_VERSION_base(4,17,0)+import Data.Bits hiding ((.>>.), (.<<.))+#else import Data.Bits+#endif -- | Instance of the 'Bits' class for 'Stream's. --@@ -38,9 +42,11 @@ bit = P.error "tbd: bit" popCount = P.error "tbd: popCount" +#if !MIN_VERSION_base(4,17,0) -- | See 'xor'. (.^.) :: Bits a => a -> a -> a (.^.) = xor -- Avoid redefinition of the Operators.Boolean xor+#endif -- | Shifting values of a stream to the left. (.<<.) :: (Bits a, Typed a, Typed b, P.Integral b)
src/Copilot/Language/Operators/Boolean.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} @@ -21,8 +19,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | A stream that contains the constant value 'True'. true :: Stream Bool true = constant True@@ -64,5 +60,3 @@ -- | Apply the implication ('==>') operator to two boolean streams, point-wise. (==>) :: Stream Bool -> Stream Bool -> Stream Bool x ==> y = not x || y----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Cast.hs view
@@ -1,9 +1,7 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-} -- | Type-safe casting operators. module Copilot.Language.Operators.Cast@@ -16,8 +14,6 @@ import Data.Int import Data.Word ---------------------------------------------------------------------------------- -- | Class to capture casting between types for which it can be performed -- safely. class Cast a b where@@ -30,16 +26,12 @@ -- | Perform an unsafe cast from @Stream a@ to @Stream b@. unsafeCast :: (Typed a, Typed b) => Stream a -> Stream b ---------------------------------------------------------------------------------- -- | Cast a boolean stream to a stream of numbers, producing 1 if the -- value at a point in time is 'True', and 0 otherwise. castBool :: (Eq a, Num a, Typed a) => Stream Bool -> Stream a castBool (Const bool) = Const $ if bool then 1 else 0 castBool x = Op3 (C.Mux typeOf) x 1 0 ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Bool Bool where cast = id@@ -84,15 +76,11 @@ instance Cast Bool Int64 where cast = castBool ---------------------------------------------------------------------------------- -- | Cast a stream carrying numbers to an integral using 'fromIntegral'. castIntegral :: (Integral a, Typed a, Num b, Typed b) => Stream a -> Stream b castIntegral (Const x) = Const (fromIntegral x) castIntegral x = Op1 (C.Cast typeOf typeOf) x ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word8 Word8 where cast = castIntegral@@ -121,8 +109,6 @@ instance Cast Word8 Int64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word16 Word16 where cast = castIntegral@@ -143,8 +129,6 @@ instance Cast Word16 Int64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word32 Word32 where cast = castIntegral@@ -157,14 +141,10 @@ instance Cast Word32 Int64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Word64 Word64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int8 Int8 where cast = castIntegral@@ -181,8 +161,6 @@ instance Cast Int8 Int64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int16 Int16 where cast = castIntegral@@ -195,8 +173,6 @@ instance Cast Int16 Int64 where cast = castIntegral ---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int32 Int32 where cast = castIntegral@@ -204,8 +180,6 @@ -- | Cast number to bigger type. instance Cast Int32 Int64 where cast = castIntegral---------------------------------------------------------------------------------- -- | Identity casting. instance Cast Int64 Int64 where
src/Copilot/Language/Operators/Constant.hs view
@@ -1,10 +1,7 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} - -- | Primitives to build constant streams. module Copilot.Language.Operators.Constant ( constant@@ -27,14 +24,10 @@ import Data.Word import Data.Int ---------------------------------------------------------------------------------- -- | Create a constant stream that is equal to the given argument, at any -- point in time. constant :: Typed a => a -> Stream a constant = Const---------------------------------------------------------------------------------- -- | Create a constant stream carrying values of type 'Bool' that is equal to -- the given argument, at any point in time.
src/Copilot/Language/Operators/Eq.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} @@ -16,8 +14,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | Compare two streams point-wise for equality. -- -- The output stream contains the value True at a point in time if both@@ -33,5 +29,3 @@ (/=) :: (P.Eq a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) /= (Const y) = Const (x P./= y) x /= y = Op2 (Core.Ne typeOf) x y----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Extern.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Primitives to build streams connected to external variables. @@ -26,8 +24,6 @@ import Data.Word import Data.Int ---------------------------------------------------------------------------------- -- | Create a stream populated by an external global variable. -- -- The Copilot compiler does not check that the type is correct. If the list@@ -41,8 +37,6 @@ -> Maybe [a] -- ^ Values to be used exclusively for testing/simulation. -> Stream a extern = Extern---------------------------------------------------------------------------------- -- | Create a stream carrying values of type Bool, populated by an external -- global variable.
src/Copilot/Language/Operators/Integral.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Integral class operators applied point-wise on streams. @@ -22,8 +20,6 @@ import qualified Prelude as P import Data.List (foldl', replicate) ---------------------------------------------------------------------------------- -- | Apply the 'Prelude.div' operation to two streams, point-wise. div :: (Typed a, P.Integral a) => Stream a -> Stream a -> Stream a (Const 0) `div` _ = Const 0@@ -51,5 +47,3 @@ (Const 2) ^ y = (Const 1) .<<. y x ^ (Const y) = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x) _ ^ _ = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant. (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Label.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Label a stream with additional information. @@ -13,8 +11,6 @@ import Copilot.Core (Typed) import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------- -- | This function allows you to label a stream with a tag, which can be used -- by different backends to provide additional information either in error -- messages or in the generated code (e.g., for traceability purposes).@@ -24,5 +20,3 @@ -- is used in the code generated is a decision specific to each backend. label :: (Typed a) => String -> Stream a -> Stream a label = Label----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Local.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Let expressions. --@@ -18,8 +16,6 @@ import Copilot.Core (Typed) import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------- -- | Let expressions. -- -- Create a stream that results from applying a stream to a function on@@ -33,5 +29,3 @@ -- @ local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b local = Local----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Mux.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} @@ -17,16 +15,12 @@ import Copilot.Language.Stream import Prelude () ---------------------------------------------------------------------------------- -- | Convenient synonym for 'ifThenElse'. mux :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a mux (Const True) t _ = t mux (Const False) _ f = f mux b t f = Op3 (Core.Mux typeOf) b t f ---------------------------------------------------------------------------------- -- | If-then-else applied point-wise to three streams (a condition stream, a -- then-branch stream, and an else-branch stream). --@@ -35,5 +29,3 @@ -- that time, otherwise it contains the value in the third stream. ifThenElse :: Typed a => Stream Bool -> Stream a -> Stream a -> Stream a ifThenElse = mux----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Ord.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} @@ -18,8 +16,6 @@ import Copilot.Language.Stream import qualified Prelude as P ---------------------------------------------------------------------------------- -- | Compare two streams point-wise for order. -- -- The output stream contains the value True at a point in time if the@@ -55,5 +51,3 @@ (>) :: (P.Ord a, Typed a) => Stream a -> Stream a -> Stream Bool (Const x) > (Const y) = Const (x P.> y) x > y = Op2 (Core.Gt typeOf) x y----------------------------------------------------------------------------------
+ src/Copilot/Language/Operators/Projection.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE TypeFamilies #-}+-- | Interface to access portions of a larger data structure.+--+-- Default operations to access elements from structs and arrays (e.g., a field+-- of a struct, an element of an array) allow obtaining the values of those+-- elements, but not modifying.+--+-- This module defines a common interface to manipulate portions of a larger+-- data structure. We define the interface in a generic way, using a type+-- class with two operations: one to set the value of the sub-element, and+-- one to update the value of such element applying a stream function.+module Copilot.Language.Operators.Projection+ ( Projectable (..) )+ where++import Copilot.Language.Stream (Stream)++infixl 8 =:+infixl 8 =$++-- | Common interface to manipulate portions of a larger data structure.+--+-- A projectable d s t means that it is possible to manipulate a sub-element s+-- of type t carried in a stream of type d.+class Projectable d s t | d s -> t where++ -- | Unapplied projection or element access on a type.+ data Projection d s t++ -- | Modify the value of a sub-element of a type in a stream of elements+ -- of that type.+ (=:) :: Projection d s t -> Stream t -> Stream d++ -- | Update the value of a sub-element of a type in a stream of elements of+ -- that type, by applying a function on streams.+ (=$) :: Projection d s t -> (Stream t -> Stream t) -> Stream d
src/Copilot/Language/Operators/Propositional.hs view
@@ -1,8 +1,9 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe, FlexibleInstances, GADTs, MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-} -- | Implement negation over quantified extensions of boolean streams. --@@ -16,8 +17,6 @@ import Copilot.Theorem ---------------------------------------------------------------------------------- -- | A proposition that can be negated. class Negatable a b where -- | Negate a proposition.@@ -30,5 +29,3 @@ -- | Negation of a universally quantified proposition. instance Negatable (Prop Universal) (Prop Existential) where not (Forall p) = Exists $ B.not p----------------------------------------------------------------------------------
src/Copilot/Language/Operators/Struct.hs view
@@ -1,17 +1,47 @@-{-# LANGUAGE Safe #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeFamilies #-}+-- The following warning is disabled due to a necessary instance of Projectable+-- defined in this module.+{-# OPTIONS_GHC -fno-warn-orphans #-} -- | Combinators to deal with streams carrying structs.+--+-- We support two kinds of operations on structs: reading the fields of structs+-- and modifying the fields of structs.+--+-- To obtain the values of field @x@ of a struct @s@, you can just write:+--+-- @+-- expr = s # x+-- @+--+-- If you want to update it, use instead a double hash to refer to the field.+-- You can either update the field:+--+-- @+-- expr = s ## x =: 75+-- @+--+-- To update it by applying a function to it, for example, the function that+-- updates a stream by one unit, just do:+--+-- @+-- expr = s ## x =$ (+1)+-- @ module Copilot.Language.Operators.Struct- ( (#)+ ( Projectable(..)+ , (#)+ , (##) ) where import Copilot.Core.Type import Copilot.Core.Operators-import Copilot.Language.Stream (Stream (..))--import GHC.TypeLits (KnownSymbol)+import Copilot.Language.Operators.Projection+import Copilot.Language.Stream (Stream (..)) ---------------------------------------------------------------------------------+import GHC.TypeLits (KnownSymbol) -- | Create a stream that carries a field of a struct in another stream. --@@ -20,8 +50,48 @@ -- of type @Word8@, and @s@ is a stream of type @Stream T@, then @s # t2@ has -- type @Stream Word8@ and contains the values of the @t2@ field of the structs -- in @s@ at any point in time.-(#) :: (KnownSymbol s, Typed t, Typed a, Struct a)- => Stream a -> (a -> Field s t) -> Stream t+(#) :: (KnownSymbol f, Typed t, Typed s, Struct s)+ => Stream s -> (s -> Field f t) -> Stream t (#) s f = Op1 (GetField typeOf typeOf f) s ---------------------------------------------------------------------------------+-- | Pair a stream with a field accessor, without applying it to obtain the+-- value of the field.+--+-- This function is needed to refer to a field accessor when the goal is to+-- update the field value, not just to read it.+(##) :: (KnownSymbol f, Typed t, Typed s, Struct s)+ => Stream s -> (s -> Field f t) -> Projection s (s -> Field f t) t+(##) = ProjectionS++-- | Update a stream of structs.++-- This is an orphan instance; we suppress the warning that GHC would+-- normally produce with a GHC option at the top.+instance (KnownSymbol f, Typed s, Typed t, Struct s)+ => Projectable s (s -> Field f t) t+ where++ -- | A projection of a field of a stream of structs.+ data Projection s (s -> Field f t) t = ProjectionS (Stream s) (s -> Field f t)++ -- | Create a stream where the field of a struct has been updated with values+ -- from another stream.+ --+ -- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@+ -- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and+ -- $sT1$ is a stream of type @Int32@ then @s ## t2 =: sT1@ has type @Stream+ -- T@ and contains structs where the value of @t1@ is that of @sT1@ and the+ -- value of @t2@ is the value that the same field had in @s@, at any point in+ -- time.+ (=:) (ProjectionS s f) v = Op2 (UpdateField typeOf typeOf f) s v++ -- | Create a stream where the field of a struct has been updated by applying+ -- a function to it.+ --+ -- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@+ -- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and $f$+ -- is a function from @Stream Int32 -> Stream Int32@ then @s ## t2 =$ f@ has+ -- type @Stream T@ and contains structs where the value of @t1@ is that of+ -- @f@ applied to the original value of @t1@ in @s@, and the value of @t2@ is+ -- the value that the same field had in @s@, at any point in time.+ (=$) (ProjectionS s f) op = Op2 (UpdateField typeOf typeOf f) s (op (s # f))
src/Copilot/Language/Operators/Temporal.hs view
@@ -1,8 +1,5 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- - {-# LANGUAGE Safe #-} -- | Temporal stream transformations.@@ -15,8 +12,6 @@ import Copilot.Language.Prelude import Copilot.Language.Stream import Prelude ()---------------------------------------------------------------------------------- infixr 1 ++
src/Copilot/Language/Prelude.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Reexports 'Prelude' from package "base" hiding identifiers redefined by -- Copilot.@@ -31,5 +29,3 @@ , cycle , take )----------------------------------------------------------------------------------
src/Copilot/Language/Reify.hs view
@@ -1,12 +1,12 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Transform a Copilot Language specification into a Copilot Core -- specification. -{-# LANGUAGE Safe #-}-{-# LANGUAGE ExistentialQuantification, Rank2Types #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Safe #-} module Copilot.Language.Reify ( reify@@ -18,7 +18,7 @@ import Copilot.Language.Analyze (analyze) import Copilot.Language.Error (impossible) import Copilot.Language.Spec-import Copilot.Language.Stream (Stream (..), Arg (..))+import Copilot.Language.Stream (Stream (..)) import Copilot.Theorem.Prove @@ -28,7 +28,6 @@ import System.Mem.StableName.Map (Map) import qualified System.Mem.StableName.Map as M import Control.Monad (liftM, unless)--------------------------------------------------------------------------------- -- | Transform a Copilot Language specification into a Copilot Core -- specification.@@ -58,8 +57,6 @@ return cspec ---------------------------------------------------------------------------------- -- | Transform a Copilot observer specification into a Copilot Core -- observer specification. {-# INLINE mkObserver #-}@@ -76,8 +73,6 @@ , Core.observerExpr = w , Core.observerExprType = typeOf } ---------------------------------------------------------------------------------- -- | Transform a Copilot trigger specification into a Copilot Core -- trigger specification. {-# INLINE mkTrigger #-}@@ -102,8 +97,6 @@ w <- mkExpr refMkId refStreams refMap e return $ Core.UExpr typeOf w ---------------------------------------------------------------------------------- -- | Transform a Copilot property specification into a Copilot Core -- property specification. {-# INLINE mkProperty #-}@@ -113,13 +106,22 @@ -> IORef [Core.Stream] -> Property -> IO Core.Property-mkProperty refMkId refStreams refMap (Property name guard) = do- w1 <- mkExpr refMkId refStreams refMap guard+mkProperty refMkId refStreams refMap (Property name p) = do+ p' <- mkProp refMkId refStreams refMap p return Core.Property { Core.propertyName = name- , Core.propertyExpr = w1 }+ , Core.propertyProp = p' } ---------------------------------------------------------------------------------+-- | Transform a Copilot proposition into a Copilot Core proposition.+mkProp :: IORef Int+ -> IORef (Map Core.Id)+ -> IORef [Core.Stream]+ -> Prop a+ -> IO Core.Prop+mkProp refMkId refStreams refMap prop =+ case prop of+ Forall e -> Core.Forall <$> mkExpr refMkId refStreams refMap e+ Exists e -> Core.Exists <$> mkExpr refMkId refStreams refMap e -- | Transform a Copilot stream expression into a Copilot Core expression. {-# INLINE mkExpr #-}@@ -210,8 +212,6 @@ w <- mkExpr refMkId refStreams refMap e return $ (name, Core.UExpr typeOf w) ---------------------------------------------------------------------------------- -- | Transform a Copilot stream expression into a Copilot Core stream -- expression. {-# INLINE mkStream #-}@@ -256,8 +256,6 @@ , Core.streamExpr = w , Core.streamExprType = typeOf } return id---------------------------------------------------------------------------------- -- | Create a fresh, unused 'Id'. mkId :: IORef Int -> IO Id
src/Copilot/Language/Spec.hs view
@@ -1,11 +1,9 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} -- | Copilot specifications consistute the main declaration of Copilot modules. --@@ -24,11 +22,13 @@ , Trigger (..) , trigger, triggers , arg+ , Arg(..) , Property (..) , Prop (..) , prop, properties , theorem, theorems- , forall, exists+ , forAll+ , exists , extractProp , Universal, Existential ) where@@ -43,8 +43,6 @@ import Copilot.Theorem.Prove ---------------------------------------------------------------------------------- -- | A specification is a list of declarations of triggers, observers, -- properties and theorems. --@@ -68,8 +66,6 @@ -- can be used in subsequent actions. type Spec' a = Writer [SpecItem] a ---------------------------------------------------------------------------------- -- | Return the complete list of declarations inside a 'Spec' or 'Spec''. -- -- The word run in this function is unrelated to running the underlying@@ -78,8 +74,6 @@ runSpec :: Spec' a -> [SpecItem] runSpec = execWriter ---------------------------------------------------------------------------------- -- | Filter a list of spec items to keep only the observers. observers :: [SpecItem] -> [Observer] observers =@@ -120,8 +114,6 @@ TheoremItem p -> p : ls _ -> ls ---------------------------------------------------------------------------------- -- | An item of a Copilot specification. data SpecItem = ObserverItem Observer@@ -129,15 +121,11 @@ | PropertyItem Property | TheoremItem (Property, UProof) ---------------------------------------------------------------------------------- -- | An observer, representing a stream that we observe during execution at -- every sample. data Observer where Observer :: Typed a => String -> Stream a -> Observer ---------------------------------------------------------------------------------- -- | Define a new observer as part of a specification. This allows someone to -- print the value at every iteration during interpretation. Observers do not -- have any functionality outside the interpreter.@@ -148,15 +136,11 @@ -> Spec observer name e = tell [ObserverItem $ Observer name e] ---------------------------------------------------------------------------------- -- | A trigger, representing a function we execute when a boolean stream becomes -- true at a sample. data Trigger where Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger ---------------------------------------------------------------------------------- -- | Define a new trigger as part of a specification. A trigger declares which -- external function, or handler, will be called when a guard defined by a -- boolean stream becomes true.@@ -166,14 +150,10 @@ -> Spec trigger name e args = tell [TriggerItem $ Trigger name e args] ---------------------------------------------------------------------------------- -- | A property, representing a boolean stream that is existentially or -- universally quantified over time. data Property where- Property :: String -> Stream Bool -> Property----------------------------------------------------------------------------------+ Property :: String -> Prop a -> Property -- | A proposition, representing the quantification of a boolean streams over -- time.@@ -182,41 +162,41 @@ Exists :: Stream Bool -> Prop Existential -- | Universal quantification of boolean streams over time.-forall :: Stream Bool -> Prop Universal-forall = Forall+forAll :: Stream Bool -> Prop Universal+forAll = Forall -- | Existential quantification of boolean streams over time. exists :: Stream Bool -> Prop Existential exists = Exists -- | Extract the underlying stream from a quantified proposition.+--+-- Think carefully before using this function, as this function will remove the+-- quantifier from a proposition. Universally quantified streams usually require+-- separate treatment from existentially quantified ones, so carelessly using+-- this function to remove quantifiers can result in hard-to-spot soundness+-- bugs. extractProp :: Prop a -> Stream Bool extractProp (Forall p) = p extractProp (Exists p) = p ---------------------------------------------------------------------------------- -- | A proposition, representing a boolean stream that is existentially or -- universally quantified over time, as part of a specification. -- -- This function returns, in the monadic context, a reference to the -- proposition. prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)-prop name e = tell [PropertyItem $ Property name (extractProp e)]+prop name e = tell [PropertyItem $ Property name e] >> return (PropRef name) ---------------------------------------------------------------------------------- -- | A theorem, or proposition together with a proof. -- -- This function returns, in the monadic context, a reference to the -- proposition. theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)-theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]+theorem name e (Proof p) = tell [TheoremItem (Property name e, p)] >> return (PropRef name) ---------------------------------------------------------------------------------- -- | Construct a function argument from a stream. -- -- 'Arg's can be used to pass arguments to handlers or trigger functions, to@@ -227,4 +207,6 @@ arg :: Typed a => Stream a -> Arg arg = Arg ---------------------------------------------------------------------------------+-- | Wrapper to use 'Stream's as arguments to triggers.+data Arg where+ Arg :: Typed a => Stream a -> Arg
src/Copilot/Language/Stream.hs view
@@ -1,18 +1,14 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -- | Abstract syntax for streams and operators. -{-# LANGUAGE Safe #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Safe #-} module Copilot.Language.Stream ( Stream (..)- , Arg (..)- , StructArg (..) , Copilot.Language.Stream.ceiling , Copilot.Language.Stream.floor , Copilot.Language.Stream.atan2@@ -24,8 +20,6 @@ import Copilot.Language.Prelude import qualified Prelude as P ---------------------------------------------------------------------------------- -- | A stream in Copilot is an infinite succession of values of the same type. -- -- Streams can be built using simple primities (e.g., 'Const'), by applying@@ -53,30 +47,15 @@ => Core.Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d Label :: Typed a => String -> Stream a -> Stream a ------------------------------------------------------------------------------------- | Wrapper to use 'Stream's as arguments to triggers.-data Arg where- Arg :: Typed a => Stream a -> Arg--data StructArg = StructArg { name_ :: String, arg' :: Arg }-{-# DEPRECATED StructArg "StructArg is deprecated" #-}----------------------------------------------------------------------------------- -- | Dummy instance in order to make 'Stream' an instance of 'Num'. instance Show (Stream a) where show _ = "Stream" ---------------------------------------------------------------------------------- -- | Dummy instance in order to make 'Stream' an instance of 'Num'. instance P.Eq (Stream a) where (==) = badUsage "'Prelude.(==)' isn't implemented for streams!" (/=) = badUsage "'Prelude.(/=)' isn't implemented for streams!" ---------------------------------------------------------------------------------- -- | Streams carrying numbers are instances of 'Num', and you can apply to them -- the 'Num' functions, point-wise. instance (Typed a, P.Eq a, Num a) => Num (Stream a) where@@ -104,8 +83,6 @@ fromInteger = Const . fromInteger ---------------------------------------------------------------------------------- -- | Streams carrying fractional numbers are instances of 'Fractional', and you can -- apply to them the 'Fractional' functions, point-wise. @@ -119,8 +96,6 @@ fromRational = Const . fromRational ---------------------------------------------------------------------------------- -- | Streams carrying floating point numbers are instances of 'Floating', and -- you can apply to them the 'Floating' functions, point-wise. @@ -146,8 +121,6 @@ atanh = Op1 (Core.Atanh typeOf) acosh = Op1 (Core.Acosh typeOf) ---------------------------------------------------------------------------------- -- | Point-wise application of @ceiling@ to a stream. -- -- Unlike the Haskell variant of this function, this variant takes and returns@@ -179,9 +152,6 @@ -- qualified to use this function. floor :: (Typed a, RealFrac a) => Stream a -> Stream a floor = Op1 (Core.Floor typeOf)----------------------------------------------------------------------------------- -- | Point-wise application of @atan2@ to the values of two streams. --
src/System/Mem/StableName/Dynamic.hs view
@@ -1,8 +1,7 @@--------------------------------------------------------------------------------- -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.--------------------------------------------------------------------------------- -{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE Safe #-} module System.Mem.StableName.Dynamic ( DynStableName(..)@@ -10,19 +9,19 @@ , makeDynStableName ) where -import System.Mem.StableName (StableName, makeStableName, hashStableName)-import Unsafe.Coerce (unsafeCoerce) -- XXX Not safe!+import System.Mem.StableName (StableName, eqStableName, makeStableName,+ hashStableName) -newtype DynStableName = DynStableName (StableName ())+data DynStableName = forall a . DynStableName (StableName a) makeDynStableName :: a -> IO DynStableName makeDynStableName x = do stn <- makeStableName x- return (DynStableName (unsafeCoerce stn))+ return (DynStableName stn) hashDynStableName :: DynStableName -> Int hashDynStableName (DynStableName sn) = hashStableName sn instance Eq DynStableName where- DynStableName sn1 == DynStableName sn2 = sn1 == sn2+ DynStableName sn1 == DynStableName sn2 = eqStableName sn1 sn2
src/System/Mem/StableName/Map.hs view
@@ -1,6 +1,4 @@--------------------------------------------------------------------------------- -- Most of this code is taken from 'http://github.com/ekmett/stable-maps'.--------------------------------------------------------------------------------- {-# LANGUAGE Safe #-}
+ tests/Main.hs view
@@ -0,0 +1,18 @@+-- | Test copilot-language.+module Main where++-- External imports+import Test.Framework (Test, defaultMain)++-- Internal imports+import qualified Test.Copilot.Language.Reify++-- | Run all unit tests on copilot-language.+main :: IO ()+main = defaultMain tests++-- | All unit tests in copilot-language.+tests :: [Test.Framework.Test]+tests =+ [ Test.Copilot.Language.Reify.tests+ ]
+ tests/Test/Copilot/Language/Reify.hs view
@@ -0,0 +1,782 @@+{-# LANGUAGE ExistentialQuantification #-}+-- | Test copilot-language:Copilot.Language.Reify.+--+-- The gist of this evaluation is in 'SemanticsP' and 'checkSemanticsP' which+-- evaluates an expression using Copilot's evaluator and compares it against+-- its expected meaning.+module Test.Copilot.Language.Reify where++-- External imports+import Data.Bits (Bits, complement, shiftL, shiftR,+ xor, (.&.), (.|.))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Maybe (fromMaybe)+import Data.Typeable (Typeable)+import Data.Word (Word16, Word32, Word64, Word8)+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.QuickCheck (Arbitrary, Gen, Property,+ arbitrary, chooseInt, elements,+ forAll, forAllShow, frequency,+ oneof, suchThat)+import Test.QuickCheck.Monadic (monadicIO, run)++-- Internal imports: library modules being tested+import Copilot.Language (Typed)+import qualified Copilot.Language.Operators.BitWise as Copilot+import qualified Copilot.Language.Operators.Boolean as Copilot+import qualified Copilot.Language.Operators.Constant as Copilot+import qualified Copilot.Language.Operators.Eq as Copilot+import qualified Copilot.Language.Operators.Integral as Copilot+import qualified Copilot.Language.Operators.Mux as Copilot+import qualified Copilot.Language.Operators.Ord as Copilot+import Copilot.Language.Reify (reify)+import Copilot.Language.Spec (Spec, observer)+import Copilot.Language.Stream (Stream)+import qualified Copilot.Language.Stream as Copilot++-- Internal imports: functions needed to test after reification+import Copilot.Interpret.Eval (ExecTrace (interpObservers), ShowType (Haskell),+ eval)++-- Internal imports: auxiliary functions+import Test.Extra (apply1, apply2, apply3)++-- * Constants++-- | Max length of the traces being tested.+maxTraceLength :: Int+maxTraceLength = 200++-- | All unit tests for copilot-language:Copilot.Language.Reify.+tests :: Test.Framework.Test+tests =+ testGroup "Copilot.Language.Reify"+ [ testProperty "eval Stream" testEvalExpr ]++-- * Individual tests++-- | Test for expression evaluation.+testEvalExpr :: Property+testEvalExpr =+ forAll (chooseInt (0, maxTraceLength)) $ \steps ->+ forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair ->+ monadicIO $ run (checkSemanticsP steps [] pair)++-- * Random generators++-- ** Random SemanticsP generators++-- | An arbitrary expression, paired with its expected meaning.+--+-- See the function 'checkSemanticsP' to evaluate the pair.+arbitrarySemanticsP :: Gen SemanticsP+arbitrarySemanticsP = oneof+ [ SemanticsP <$> (arbitraryBoolExpr :: Gen (Semantics Bool))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryFloatingExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryFloatingExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryRealFracExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryRealFracExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryRealFloatExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryRealFloatExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryFractionalExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryFractionalExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Bool))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word64))+ ]++-- ** Random Stream generators++-- | An arbitrary constant expression of any type, paired with its expected+-- meaning.+arbitraryConst :: (Arbitrary t, Typed t)+ => Gen (Stream t, [t])+arbitraryConst = (\v -> (Copilot.constant v, repeat v)) <$> arbitrary++-- | Generator for constant boolean streams, paired with their expected+-- meaning.+arbitraryBoolOp0 :: Gen (Stream Bool, [Bool])+arbitraryBoolOp0 = elements+ [ (Copilot.false, repeat False)+ , (Copilot.true, repeat True)+ ]++-- | An arbitrary boolean expression, paired with its expected meaning.+arbitraryBoolExpr :: Gen (Stream Bool, [Bool])+arbitraryBoolExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, arbitraryBoolOp0)++ , (5, apply1 <$> arbitraryBoolOp1 <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryBoolOp2+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Int8, [Int8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Int16, [Int16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Int32, [Int32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Int64, [Int64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Word8, [Word8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Word16, [Word16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Word32, [Word32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Stream Word64, [Word64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int8, [Int8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int16, [Int16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int32, [Int32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int64, [Int64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word8, [Word8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word16, [Word16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word32, [Word32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word64, [Word64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int8, [Int8])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int16, [Int16])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int32, [Int32])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Int64, [Int64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word8, [Word8])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word16, [Word16])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word32, [Word32])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Stream Word64, [Word64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryFloatingExpr+ <*> (arbitraryFloatingExpr :: Gen (Stream Float, [Float])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryFloatingExpr+ <*> (arbitraryFloatingExpr :: Gen (Stream Double, [Double])))++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)+ ]++-- | An arbitrary numeric expression, paired with its expected meaning.+arbitraryNumExpr :: (Arbitrary t, Typed t, Num t, Eq t)+ => Gen (Stream t, [t])+arbitraryNumExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryNumExpr)++ , (2, apply2 <$> arbitraryNumOp2 <*> arbitraryNumExpr <*> arbitraryNumExpr)++ , (2, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryNumExpr+ <*> arbitraryNumExpr)+ ]++-- | An arbitrary floating point expression, paired with its expected meaning.+arbitraryFloatingExpr :: (Arbitrary t, Typed t, Floating t, Eq t)+ => Gen (Stream t, [t])+arbitraryFloatingExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryFloatingOp1 <*> arbitraryFloatingExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFloatingExpr)++ , (2, apply2 <$> arbitraryFloatingOp2+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)++ , (2, apply2 <$> arbitraryNumOp2+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)+ ]++-- | An arbitrary realfrac expression, paired with its expected meaning.+arbitraryRealFracExpr :: (Arbitrary t, Typed t, RealFrac t)+ => Gen (Stream t, [t])+arbitraryRealFracExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryRealFracOp1 <*> arbitraryRealFracExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryRealFracExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryRealFracExpr+ <*> arbitraryRealFracExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryRealFracExpr+ <*> arbitraryRealFracExpr)+ ]++-- | An arbitrary realfloat expression, paired with its expected meaning.+arbitraryRealFloatExpr :: (Arbitrary t, Typed t, RealFloat t)+ => Gen (Stream t, [t])+arbitraryRealFloatExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryRealFloatExpr)++ , (5, apply2 <$> arbitraryRealFloatOp2+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)+ ]++-- | An arbitrary fractional expression, paired with its expected meaning.+--+-- We add the constraint Eq because we sometimes need to make sure numbers are+-- not zero.+arbitraryFractionalExpr :: (Arbitrary t, Typed t, Fractional t, Eq t)+ => Gen (Stream t, [t])+arbitraryFractionalExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryFractionalOp1 <*> arbitraryFractionalExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFractionalExpr)++ , (2, apply2 <$> arbitraryFractionalOp2+ <*> arbitraryFractionalExpr+ <*> arbitraryFractionalExprNonZero)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryFractionalExpr+ <*> arbitraryFractionalExpr)+ ]+ where++ -- Generator for fractional expressions that are never zero.+ --+ -- The list is infinite, so this generator checks up to maxTraceLength+ -- elements.+ arbitraryFractionalExprNonZero = arbitraryFractionalExpr+ `suchThat` (notElem 0 . take maxTraceLength . snd)++-- | An arbitrary integral expression, paired with its expected meaning.+--+-- We add the constraint Eq because we sometimes need to make sure numbers are+-- not zero.+arbitraryIntegralExpr :: (Arbitrary t, Typed t, Integral t, Eq t)+ => Gen (Stream t, [t])+arbitraryIntegralExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryIntegralExpr)++ , (2, apply2 <$> arbitraryNumOp2+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExpr)++ , (2, apply2 <$> arbitraryIntegralOp2+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExprNonZero)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExpr)+ ]+ where++ -- Generator for integral expressions that are never zero.+ --+ -- The list is infinite, so this generator checks up to maxTraceLength+ -- elements.+ arbitraryIntegralExprNonZero = arbitraryIntegralExpr+ `suchThat` (notElem 0 . take maxTraceLength . snd)++-- | An arbitrary Bits expression, paired with its expected meaning.+arbitraryBitsExpr :: (Arbitrary t, Typed t, Bits t)+ => Gen (Stream t, [t])+arbitraryBitsExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryBitsOp1 <*> arbitraryBitsExpr)++ , (2, apply2 <$> arbitraryBitsOp2+ <*> arbitraryBitsExpr+ <*> arbitraryBitsExpr)++ , (2, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBitsExpr <*> arbitraryBitsExpr)+ ]++-- | An arbitrary expression for types that are instances of Bits and Integral,+-- paired with its expected meaning.+arbitraryBitsIntegralExpr :: (Arbitrary t, Typed t, Bits t, Integral t)+ => Gen (Stream t, [t])+arbitraryBitsIntegralExpr =+ -- We use frequency instead of oneof because the random expression+ -- generator seems to generate expressions that are too large and the+ -- test fails due to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryBitsIntegralExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExpr)++ , (5, apply2 <$> arbitraryBitsIntegralOp2+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExprConstPos)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExpr)+ ]+ where++ -- Generator for constant bit integral expressions that, when converted to+ -- type 't', result in a positive number. We use a constant generator, as+ -- opposed to a generator based on the more comprehensive+ -- arbitraryBitsIntegralExpr, because the latter runs out of memory easily+ -- when nested and filtered with suchThat.+ arbitraryBitsIntegralExprConstPos =+ (\v -> (Copilot.constant v, repeat v)) <$> intThatFits+ where+ -- In this context:+ --+ -- intThatFits :: Gen t+ intThatFits =+ suchThat arbitrary ((> 0) . (\x -> (fromIntegral x) :: Int))++-- ** Operators++-- *** Op 1++-- | Generator for arbitrary boolean operators with arity 1, paired with their+-- expected meaning.+arbitraryBoolOp1 :: Gen (Stream Bool -> Stream Bool, [Bool] -> [Bool])+arbitraryBoolOp1 = elements+ [ (Copilot.not, fmap not)+ ]++-- | Generator for arbitrary numeric operators with arity 1, paired with their+-- expected meaning.+arbitraryNumOp1 :: (Typed t, Num t, Eq t)+ => Gen (Stream t -> Stream t, [t] -> [t])+arbitraryNumOp1 = elements+ [ (abs, fmap abs)+ , (signum, fmap signum)+ ]++-- | Generator for arbitrary floating point operators with arity 1, paired with+-- their expected meaning.+arbitraryFloatingOp1 :: (Typed t, Floating t, Eq t)+ => Gen (Stream t -> Stream t, [t] -> [t])+arbitraryFloatingOp1 = elements+ [ (exp, fmap exp)+ , (sqrt, fmap sqrt)+ , (log, fmap log)+ , (sin, fmap sin)+ , (tan, fmap tan)+ , (cos, fmap cos)+ , (asin, fmap asin)+ , (atan, fmap atan)+ , (acos, fmap acos)+ , (sinh, fmap sinh)+ , (tanh, fmap tanh)+ , (cosh, fmap cosh)+ , (asinh, fmap asinh)+ , (atanh, fmap atanh)+ , (acosh, fmap acosh)+ ]++-- | Generator for arbitrary realfrac operators with arity 1, paired with their+-- expected meaning.+arbitraryRealFracOp1 :: (Typed t, RealFrac t)+ => Gen (Stream t -> Stream t, [t] -> [t])+arbitraryRealFracOp1 = elements+ [ (Copilot.ceiling, fmap (fromIntegral . idI . ceiling))+ , (Copilot.floor, fmap (fromIntegral . idI . floor))+ ]+ where+ -- Auxiliary function to help the compiler determine which integral type+ -- the result of ceiling must be converted to. An Integer ensures that the+ -- result fits and there is no loss of precision due to the intermediate+ -- casting.+ idI :: Integer -> Integer+ idI = id++-- | Generator for arbitrary fractional operators with arity 1, paired with+-- their expected meaning.+arbitraryFractionalOp1 :: (Typed t, Fractional t, Eq t)+ => Gen (Stream t -> Stream t, [t] -> [t])+arbitraryFractionalOp1 = elements+ [ (recip, fmap recip)+ ]++-- | Generator for arbitrary bitwise operators with arity 1, paired with their+-- expected meaning.+arbitraryBitsOp1 :: (Typed t, Bits t)+ => Gen (Stream t -> Stream t, [t] -> [t])+arbitraryBitsOp1 = elements+ [ (complement, fmap complement)+ ]++-- *** Op 2++-- | Generator for arbitrary boolean operators with arity 2, paired with their+-- expected meaning.+arbitraryBoolOp2 :: Gen ( Stream Bool -> Stream Bool -> Stream Bool+ , [Bool] -> [Bool] -> [Bool]+ )+arbitraryBoolOp2 = elements+ [ ((Copilot.&&), zipWith (&&))+ , ((Copilot.||), zipWith (||))+ , ((Copilot.==>), zipWith (\x y -> not x || y))+ , ((Copilot.xor), zipWith (\x y -> (x || y) && not (x && y)))+ ]++-- | Generator for arbitrary numeric operators with arity 2, paired with their+-- expected meaning.+arbitraryNumOp2 :: (Typed t, Num t, Eq t)+ => Gen (Stream t -> Stream t -> Stream t, [t] -> [t] -> [t])+arbitraryNumOp2 = elements+ [ ((+), zipWith (+))+ , ((-), zipWith (-))+ , ((*), zipWith (*))+ ]++-- | Generator for arbitrary integral operators with arity 2, paired with their+-- expected meaning.+arbitraryIntegralOp2 :: (Typed t, Integral t)+ => Gen ( Stream t -> Stream t -> Stream t+ , [t] -> [t] -> [t]+ )+arbitraryIntegralOp2 = elements+ [ (Copilot.mod, zipWith mod)+ , (Copilot.div, zipWith quot)+ ]++-- | Generator for arbitrary fractional operators with arity 2, paired with+-- their expected meaning.+arbitraryFractionalOp2 :: (Typed t, Fractional t, Eq t)+ => Gen ( Stream t -> Stream t -> Stream t+ , [t] -> [t] -> [t]+ )+arbitraryFractionalOp2 = elements+ [ ((/), zipWith (/))+ ]++-- | Generator for arbitrary floating point operators with arity 2, paired with+-- their expected meaning.+arbitraryFloatingOp2 :: (Typed t, Floating t, Eq t)+ => Gen ( Stream t -> Stream t -> Stream t+ , [t] -> [t] -> [t]+ )+arbitraryFloatingOp2 = elements+ [ ((**), zipWith (**))+ , (logBase, zipWith logBase)+ ]++-- | Generator for arbitrary floating point operators with arity 2, paired with+-- their expected meaning.+arbitraryRealFloatOp2 :: (Typed t, RealFloat t)+ => Gen ( Stream t -> Stream t -> Stream t+ , [t] -> [t] -> [t]+ )+arbitraryRealFloatOp2 = elements+ [ (Copilot.atan2, zipWith atan2)+ ]++-- | Generator for arbitrary equality operators with arity 2, paired with their+-- expected meaning.+arbitraryEqOp2 :: (Typed t, Eq t)+ => Gen ( Stream t -> Stream t -> Stream Bool+ , [t] -> [t] -> [Bool]+ )+arbitraryEqOp2 = elements+ [ ((Copilot.==), zipWith (==))+ , ((Copilot./=), zipWith (/=))+ ]++-- | Generator for arbitrary ordering operators with arity 2, paired with their+-- expected meaning.+arbitraryOrdOp2 :: (Typed t, Ord t)+ => Gen ( Stream t -> Stream t -> Stream Bool+ , [t] -> [t] -> [Bool]+ )+arbitraryOrdOp2 = elements+ [ ((Copilot.<=), zipWith (<=))+ , ((Copilot.<), zipWith (<))+ , ((Copilot.>=), zipWith (>=))+ , ((Copilot.>), zipWith (>))+ ]++-- | Generator for arbitrary bitwise operators with arity 2, paired with their+-- expected meaning.+arbitraryBitsOp2 :: (Typed t, Bits t)+ => Gen (Stream t -> Stream t -> Stream t, [t] -> [t] -> [t])+arbitraryBitsOp2 = elements+ [ ((.&.), zipWith (.&.))+ , ((.|.), zipWith (.|.))+ , (xor, zipWith xor)+ ]++-- | Generator for arbitrary bit shifting operators with arity 2, paired with+-- their expected meaning.+--+-- This generator is a bit more strict in its type signature than the+-- underlying bit-shifting operators being tested, since it enforces both the+-- value being manipulated and the value that indicates how much to shift by to+-- have the same type.+arbitraryBitsIntegralOp2 :: (Typed t, Bits t, Integral t)+ => Gen ( Stream t -> Stream t -> Stream t+ , [t] -> [t] -> [t]+ )+arbitraryBitsIntegralOp2 = elements+ [ ((Copilot..<<.), zipWith (\x y -> shiftL x (fromIntegral y)))+ , ((Copilot..>>.), zipWith (\x y -> shiftR x (fromIntegral y)))+ ]++-- *** Op 3++-- | Generator for if-then-else operator (with arity 3), paired with its+-- expected meaning.+--+-- Although this is constant and there is nothing arbitrary, we use the same+-- structure and naming convention as with others for simplicity.+arbitraryITEOp3 :: (Arbitrary t, Typed t)+ => Gen ( Stream Bool -> Stream t -> Stream t -> Stream t+ , [Bool] -> [t] -> [t] -> [t]+ )+arbitraryITEOp3 = return+ (Copilot.mux, zipWith3 (\x y z -> if x then y else z))++-- * Semantics++-- | Type that pairs an expression with its meaning as an infinite stream.+type Semantics t = (Stream t, [t])++-- | A phantom semantics pair is an existential type that encloses an+-- expression and its expected meaning as an infinite list of values.+--+-- It is needed by the arbitrary expression generator, to create a+-- heterogeneous list.+data SemanticsP = forall t+ . (Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t)+ => SemanticsP+ { semanticsPair :: (Stream t, [t])+ }++-- | Show function for test triplets that limits the accompanying list+-- to a certain length.+semanticsShowK :: Int -> SemanticsP -> String+semanticsShowK steps (SemanticsP (expr, exprList)) =+ show ("Cannot show stream", take steps exprList)++-- | Check that the expression in the semantics pair is evaluated to the given+-- list, up to a number of steps.+--+-- Some operations will overflow and return NaN. Because comparing any NaN+-- will, as per IEEE 754, always fail (i.e., return False), we handle that+-- specific case by stating that the test succeeds if any expected values+-- is NaN.+checkSemanticsP :: Int -> [a] -> SemanticsP -> IO Bool+checkSemanticsP steps _streams (SemanticsP (expr, exprList)) = do+ -- Spec with just one observer of one expression.+ --+ -- Because SemanticsP is an existential type, we need to help GHC figure+ -- out the type of spec.+ let spec :: Spec+ spec = observer testObserverName expr++ -- Reified stream (low-level)+ llSpec <- reify spec++ let trace = eval Haskell steps llSpec++ -- Limit expectation to the number of evaluation steps.+ let expectation = take steps exprList++ -- Obtain the results by looking up the observer in the spec+ -- and parsing the results into Haskell values.+ let resultValues = fmap readResult results+ results = lookupWithDefault testObserverName []+ $ interpObservers trace++ return $ any isNaN' expectation || resultValues == expectation++ where++ -- Fixed name for the observer. Used to obtain the result from the+ -- trace. It should be the only observer in the trace.+ testObserverName :: String+ testObserverName = "res"++ -- | Is NaN with Eq requirement only.+ isNaN' :: Eq a => a -> Bool+ isNaN' x = x /= x++-- * Auxiliary++-- | Read a Haskell value from the output of the evaluator.+readResult :: Read a => String -> a+readResult = read . readResult'+ where+ readResult' :: String -> String+ readResult' "false" = "False"+ readResult' "true" = "True"+ readResult' s = s++-- | Variant of 'lookup' with an additional default value returned when the key+-- provided is not found in the map.+lookupWithDefault :: Ord k => k -> v -> [(k, v)] -> v+lookupWithDefault k def = fromMaybe def . lookup k
+ tests/Test/Extra.hs view
@@ -0,0 +1,31 @@+-- | Auxiliary testing helper functions.+module Test.Extra where++-- External imports+import Control.Arrow ((***))++-- * Function application++-- | Apply a tuple with two functions to a tuple of arguments.+apply1 :: (a1 -> b1, a2 -> b2) -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with arguments+ -> (b1, b2) -- ^ Pair with results+apply1 = uncurry (***)++-- | Apply a tuple with two functions on two arguments to their tupled+-- arguments.+apply2 :: (a1 -> b1 -> c1, a2 -> b2 -> c2) -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with first arguments+ -> (b1, b2) -- ^ Pair with second arguments+ -> (c1, c2) -- ^ Pair with results+apply2 fs = apply1 . apply1 fs++-- | Apply a tuple with two functions on three arguments to their tupled+-- arguments.+apply3 :: (a1 -> b1 -> c1 -> d1, a2 -> b2 -> c2 -> d2)+ -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with first arguments+ -> (b1, b2) -- ^ Pair with second arguments+ -> (c1, c2) -- ^ Pair with third arguments+ -> (d1, d2) -- ^ Pair with results+apply3 fs = apply2 . apply1 fs