diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,13 @@ +2023-01-07 + * Version bump (3.13). (#406) + * Implement missing cases of type equality for arrays and structs. + (#400) + +2022-12-27 + * Remove Copilot.Core.External. (#391) + * Fix bug in definition of simpleType for Int8. (#393) + * Hide module Copilot.Core.Type.Show. (#392) + 2022-11-07 * Version bump (3.12). (#389) * Deprecate Copilot.Core.PrettyPrinter. (#383) diff --git a/copilot-core.cabal b/copilot-core.cabal --- a/copilot-core.cabal +++ b/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 3.12 +version: 3.13 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. @@ -43,14 +43,12 @@ build-depends: base >= 4.9 && < 5, - pretty >= 1.0 && < 1.2, - dlist + pretty >= 1.0 && < 1.2 exposed-modules: Copilot.Core Copilot.Core.Expr - Copilot.Core.External Copilot.Core.Interpret Copilot.Core.Interpret.Eval Copilot.Core.Operators @@ -58,7 +56,6 @@ Copilot.Core.Type Copilot.Core.Type.Array Copilot.Core.Type.Equality - Copilot.Core.Type.Show Copilot.Core.PrettyPrint Copilot.Core.PrettyDot @@ -66,7 +63,7 @@ Copilot.Core.Error Copilot.Core.Interpret.Render - Copilot.Core.Type.ShowInternal + Copilot.Core.Type.Show test-suite unit-tests type: @@ -77,11 +74,8 @@ other-modules: Test.Extra - Test.Copilot.Core.External - Test.Copilot.Core.Interpret.Eval Test.Copilot.Core.Type Test.Copilot.Core.Type.Array - Test.Copilot.Core.Type.Show build-depends: base diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs --- a/src/Copilot/Core.hs +++ b/src/Copilot/Core.hs @@ -1,10 +1,5 @@ {-# LANGUAGE Safe #-} --- The following warning is enabled in this module so that the import of --- Copilot.Core.External does not give rise to a warning. It can be removed --- when that module is removed from the implementation. -{-# OPTIONS_GHC -fno-warn-deprecations #-} - -- | -- Description: Intermediate representation for Copilot specifications. -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. @@ -27,7 +22,6 @@ -- ("Copilot.Core.PrettyPrint"). module Copilot.Core ( module Copilot.Core.Expr - , module Copilot.Core.External , module Copilot.Core.Operators , module Copilot.Core.Spec , module Copilot.Core.Type @@ -43,7 +37,6 @@ -- Internal imports import Copilot.Core.Expr -import Copilot.Core.External -- See GHC flag enabled above import Copilot.Core.Operators import Copilot.Core.Spec import Copilot.Core.Type diff --git a/src/Copilot/Core/External.hs b/src/Copilot/Core/External.hs deleted file mode 100644 --- a/src/Copilot/Core/External.hs +++ /dev/null @@ -1,78 +0,0 @@ --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. - -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE Trustworthy #-} - --- | Internal Copilot Core representation of Copilot externs. -module Copilot.Core.External - {-# DEPRECATED "This module is deprecated in Copilot 3.10." #-} - ( ExtVar (..) - , externVars - ) where - -import Copilot.Core.Expr -import Copilot.Core.Type -import Copilot.Core.Spec -import Data.DList (DList, empty, singleton, append, concat, toList) -import Data.List (nubBy) -import Prelude hiding (all, concat, foldr) - -import Data.Typeable (Typeable) - --- | An extern variable declaration, together with the type of the underlying --- extern. -data ExtVar = ExtVar - { externVarName :: Name - , externVarType :: UType } - --- | List of all externs used in a specification. -externVars :: Spec -> [ExtVar] -externVars = nubBy eqExt . toList . all externVarsExpr - where - eqExt :: ExtVar -> ExtVar -> Bool - eqExt ExtVar { externVarName = name1 } ExtVar { externVarName = name2 } = - name1 == name2 - --- | Extract all externs used in a Copilot expression. -externVarsExpr :: Expr a -> DList ExtVar -externVarsExpr e0 = case e0 of - Const _ _ -> empty - Drop _ _ _ -> empty - Local _ _ _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 - Var _ _ -> empty - ExternVar t name _ -> singleton (ExtVar name (UType t)) - Op1 _ e -> externVarsExpr e - Op2 _ e1 e2 -> externVarsExpr e1 `append` externVarsExpr e2 - Op3 _ e1 e2 e3 -> externVarsExpr e1 `append` - externVarsExpr e2 `append` - externVarsExpr e3 - Label _ _ e -> externVarsExpr e - --- | Extract all expressions used in an untyped Copilot expression. -externVarsUExpr :: UExpr -> DList ExtVar -externVarsUExpr UExpr { uExprExpr = e } = externVarsExpr e - --- | Apply a function to all expressions in a specification, concatenating the --- results. -all :: (forall a . Expr a -> DList b) -> Spec -> DList b -all f spec = - concat (fmap (allStream) (specStreams spec)) `append` - concat (fmap allTrigger (specTriggers spec)) `append` - concat (fmap allObserver (specObservers spec)) - - where - - allStream - Stream { streamExpr = e } = f e - - allTrigger - Trigger - { triggerGuard = e - , triggerArgs = args } = f e `append` concat (fmap allUExpr args) - - allUExpr - (UExpr _ e1) = f e1 - - allObserver - Observer { observerExpr = e } = f e diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs --- a/src/Copilot/Core/Interpret.hs +++ b/src/Copilot/Core/Interpret.hs @@ -17,7 +17,7 @@ import Copilot.Core import Copilot.Core.Interpret.Eval import Copilot.Core.Interpret.Render -import Copilot.Core.Type.ShowInternal (ShowType(..)) +import Copilot.Core.Type.Show (ShowType (..)) -- | Output format for the results of a Copilot spec interpretation. data Format = Table | CSV diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs --- a/src/Copilot/Core/Interpret/Eval.hs +++ b/src/Copilot/Core/Interpret/Eval.hs @@ -16,14 +16,13 @@ , ShowType (..) ) where -import Copilot.Core (Expr (..), Field (..), Id, Name, - Observer (..), Op1 (..), Op2 (..), - Op3 (..), Spec, Stream (..), - Trigger (..), Type (Struct), UExpr (..), - arrayelems, specObservers, specStreams, - specTriggers) -import Copilot.Core.Error (badUsage) -import Copilot.Core.Type.ShowInternal (ShowType (..), showWithType) +import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..), + Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..), + Trigger (..), Type (Struct), UExpr (..), + arrayelems, specObservers, specStreams, + specTriggers) +import Copilot.Core.Error (badUsage) +import Copilot.Core.Type.Show (ShowType (..), showWithType) import Prelude hiding (id) import qualified Prelude as P diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs --- a/src/Copilot/Core/PrettyDot.hs +++ b/src/Copilot/Core/PrettyDot.hs @@ -12,7 +12,7 @@ ) where import Copilot.Core -import Copilot.Core.Type.ShowInternal (showWithType, ShowType(..), showType) +import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse) diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs --- a/src/Copilot/Core/PrettyPrint.hs +++ b/src/Copilot/Core/PrettyPrint.hs @@ -13,7 +13,7 @@ import Copilot.Core import Copilot.Core.Error (impossible) -import Copilot.Core.Type.ShowInternal (showWithType, ShowType(..), showType) +import Copilot.Core.Type.Show (showWithType, ShowType(..), showType) import Prelude hiding (id, (<>)) import Text.PrettyPrint.HughesPJ import Data.List (intersperse) diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs --- a/src/Copilot/Core/Type.hs +++ b/src/Copilot/Core/Type.hs @@ -6,6 +6,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- The following flag is disabled in this module so that the import of @@ -46,9 +47,10 @@ import Data.List (intercalate) import Data.Proxy (Proxy (..)) import Data.Type.Equality as DE -import Data.Typeable (Typeable, typeRep) +import Data.Typeable (Typeable, eqT, typeRep) import Data.Word (Word16, Word32, Word64, Word8) -import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, symbolVal) +import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, sameNat, + symbolVal) -- Internal imports import Copilot.Core.Type.Array (Array) @@ -147,6 +149,21 @@ testEquality Word64 Word64 = Just DE.Refl testEquality Float Float = Just DE.Refl testEquality Double Double = Just DE.Refl + testEquality (Array t1) (Array t2) = + testArrayEquality t1 t2 + where + testArrayEquality :: forall n1 a1 n2 a2. + (KnownNat n1, KnownNat n2) + => Type a1 + -> Type a2 + -> Maybe (Array n1 a1 :~: Array n2 a2) + testArrayEquality ty1 ty2 + | Just DE.Refl <- sameNat (Proxy :: Proxy n1) (Proxy :: Proxy n2) + , Just DE.Refl <- testEquality ty1 ty2 + = Just DE.Refl + | otherwise + = Nothing + testEquality (Struct _) (Struct _) = eqT testEquality _ _ = Nothing -- | A simple, monomorphic representation of types that facilitates putting @@ -200,7 +217,7 @@ instance Typed Int8 where typeOf = Int8 - simpleType _ = SBool + simpleType _ = SInt8 instance Typed Int16 where typeOf = Int16 diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs --- a/src/Copilot/Core/Type/Show.hs +++ b/src/Copilot/Core/Type/Show.hs @@ -1,11 +1,77 @@ --- Copyright © 2011 National Institute of Aerospace / Galois, Inc. +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Safe #-} --- | Show Copilot Core types and typed values. +-- | +-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. +-- +-- Show Copilot Core types and typed values. module Copilot.Core.Type.Show - {-# DEPRECATED "This module is deprecated in Copilot 3.10." #-} - ( showWithType - , ShowType(..) - , showType - ) where + ( showWithType + , ShowType (..) + , showType + ) + where -import Copilot.Core.Type.ShowInternal (ShowType (..), showType, showWithType) +-- Internal imports +import Copilot.Core.Type (Type (..)) + +-- | Target language for showing a typed value. Used to adapt the +-- representation of booleans. +data ShowType = C | Haskell + +-- | Show a value. The representation depends on the type and the target +-- language. Booleans are represented differently depending on the backend. +showWithType :: ShowType -> Type a -> a -> String +showWithType showT t x = + case showT of + C -> case t of + Bool -> if x then "1" else "0" + _ -> sw + Haskell -> case t of + Bool -> if x then "true" else "false" + _ -> sw + where + sw = case showWit t of + ShowWit -> show x + +-- | Show Copilot Core type. +showType :: Type a -> String +showType t = + case t of + Bool -> "Bool" + Int8 -> "Int8" + Int16 -> "Int16" + Int32 -> "Int32" + Int64 -> "Int64" + Word8 -> "Word8" + Word16 -> "Word16" + Word32 -> "Word32" + Word64 -> "Word64" + Float -> "Float" + Double -> "Double" + Array t -> "Array " ++ showType t + Struct t -> "Struct" + +-- * Auxiliary show instance + +-- | Witness datatype for showing a value, used by 'showWithType'. +data ShowWit a = Show a => ShowWit + +-- | Turn a type into a show witness. +showWit :: Type a -> ShowWit a +showWit t = + case t of + Bool -> ShowWit + Int8 -> ShowWit + Int16 -> ShowWit + Int32 -> ShowWit + Int64 -> ShowWit + Word8 -> ShowWit + Word16 -> ShowWit + Word32 -> ShowWit + Word64 -> ShowWit + Float -> ShowWit + Double -> ShowWit + Array t -> ShowWit + Struct t -> ShowWit diff --git a/src/Copilot/Core/Type/ShowInternal.hs b/src/Copilot/Core/Type/ShowInternal.hs deleted file mode 100644 --- a/src/Copilot/Core/Type/ShowInternal.hs +++ /dev/null @@ -1,77 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE Safe #-} - --- | --- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. --- --- Show Copilot Core types and typed values. -module Copilot.Core.Type.ShowInternal - ( showWithType - , ShowType (..) - , showType - ) - where - --- Internal imports -import Copilot.Core.Type (Type (..)) - --- | Target language for showing a typed value. Used to adapt the --- representation of booleans. -data ShowType = C | Haskell - --- | Show a value. The representation depends on the type and the target --- language. Booleans are represented differently depending on the backend. -showWithType :: ShowType -> Type a -> a -> String -showWithType showT t x = - case showT of - C -> case t of - Bool -> if x then "1" else "0" - _ -> sw - Haskell -> case t of - Bool -> if x then "true" else "false" - _ -> sw - where - sw = case showWit t of - ShowWit -> show x - --- | Show Copilot Core type. -showType :: Type a -> String -showType t = - case t of - Bool -> "Bool" - Int8 -> "Int8" - Int16 -> "Int16" - Int32 -> "Int32" - Int64 -> "Int64" - Word8 -> "Word8" - Word16 -> "Word16" - Word32 -> "Word32" - Word64 -> "Word64" - Float -> "Float" - Double -> "Double" - Array t -> "Array " ++ showType t - Struct t -> "Struct" - --- * Auxiliary show instance - --- | Witness datatype for showing a value, used by 'showWithType'. -data ShowWit a = Show a => ShowWit - --- | Turn a type into a show witness. -showWit :: Type a -> ShowWit a -showWit t = - case t of - Bool -> ShowWit - Int8 -> ShowWit - Int16 -> ShowWit - Int32 -> ShowWit - Int64 -> ShowWit - Word8 -> ShowWit - Word16 -> ShowWit - Word32 -> ShowWit - Word64 -> ShowWit - Float -> ShowWit - Double -> ShowWit - Array t -> ShowWit - Struct t -> ShowWit diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -5,11 +5,8 @@ import Test.Framework (Test, defaultMain) -- Internal library modules being tested -import qualified Test.Copilot.Core.External -import qualified Test.Copilot.Core.Interpret.Eval import qualified Test.Copilot.Core.Type import qualified Test.Copilot.Core.Type.Array -import qualified Test.Copilot.Core.Type.Show -- | Run all unit tests on copilot-core. main :: IO () @@ -18,9 +15,6 @@ -- | All unit tests in copilot-core. tests :: [Test.Framework.Test] tests = - [ Test.Copilot.Core.External.tests - , Test.Copilot.Core.Interpret.Eval.tests - , Test.Copilot.Core.Type.tests + [ Test.Copilot.Core.Type.tests , Test.Copilot.Core.Type.Array.tests - , Test.Copilot.Core.Type.Show.tests ] diff --git a/tests/Test/Copilot/Core/External.hs b/tests/Test/Copilot/Core/External.hs deleted file mode 100644 --- a/tests/Test/Copilot/Core/External.hs +++ /dev/null @@ -1,47 +0,0 @@ --- The following warning is enabled in this module so that the import of --- Copilot.Core.External does not give rise to a warning. -{-# OPTIONS_GHC -fno-warn-deprecations #-} - --- | Test copilot-core:Copilot.Core.External. -module Test.Copilot.Core.External where - --- External imports -import Data.List (sort) -import Test.Framework (Test, testGroup) -import Test.Framework.Providers.HUnit (testCase) -import Test.HUnit (assertBool) - --- Internal imports: library modules being tested -import Copilot.Core.Expr (Expr (ExternVar, Op1)) -import Copilot.Core.External (externVarName, externVars) -import Copilot.Core.Operators (Op1 (Abs, Sign)) -import Copilot.Core.Spec (Spec (..), Stream (..)) -import Copilot.Core.Type (Type (Int64)) - --- | All unit tests for copilot-core:Copilot.Core.External. -tests :: Test.Framework.Test -tests = - testGroup "Copilot.Core.External" - [ testCase "externVars" testExternVarsFind - ] - --- * Individual tests - --- | Test that 'externVars' will find an extern in a spec. -testExternVarsFind :: IO () -testExternVarsFind = do - -- A simple stream and a nested stream - let s1 = Stream 1 [] (ExternVar Int64 "z" Nothing) Int64 - s2 = Stream 2 [] s2Expr Int64 - s2Expr = Op1 (Abs Int64) - $ Op1 (Sign Int64) - $ ExternVar Int64 "y" Nothing - - -- Calculate the expected external vars in a spec - let res = sort $ map externVarName $ externVars $ Spec [s1, s2] [] [] [] - - -- Compare result with the expectation - let success = [ "y", "z" ] == res - assertBool - "The function externVars could not find the expected externs" - success diff --git a/tests/Test/Copilot/Core/Interpret/Eval.hs b/tests/Test/Copilot/Core/Interpret/Eval.hs deleted file mode 100644 --- a/tests/Test/Copilot/Core/Interpret/Eval.hs +++ /dev/null @@ -1,789 +0,0 @@ -{-# LANGUAGE ExistentialQuantification #-} --- The following warning is disabled in this module so that the import of --- Copilot.Core.Type.Show does not give rise to a warning. -{-# OPTIONS_GHC -fno-warn-deprecations #-} - --- | Test copilot-core:Copilot.Core.Interpret.Eval. --- --- 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.Core.Interpret.Eval where - --- External imports -import Data.Bits (Bits, complement, shiftL, shiftR, - xor, (.&.), (.|.)) -import Data.Int (Int16, Int32, Int64, Int8) -import Data.List (lookup) -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, - getPositive, oneof, suchThat, - vectorOf) -import Text.PrettyPrint.HughesPJ (render) - --- Internal imports: library modules being tested -import Copilot.Core.Expr (Expr (Const, Drop, Op1, Op2, Op3), - UExpr (UExpr)) -import Copilot.Core.Interpret.Eval (ExecTrace (interpObservers), eval) -import Copilot.Core.Operators (Op1 (..), Op2 (..), Op3 (..)) -import Copilot.Core.PrettyPrint (ppExpr) -import Copilot.Core.Spec (Observer (..), Spec (..), Stream (Stream)) -import Copilot.Core.Type (Typed (typeOf)) -import Copilot.Core.Type.Show (ShowType (Haskell), showType) - --- 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-core:Copilot.Core.Interpret.Eval. -tests :: Test.Framework.Test -tests = - testGroup "Copilot.Core.Interpret.Eval" - [ testProperty "eval Expr" testEvalExpr - , testProperty "eval Expr with Drop" testEvalExprWithDrop - ] - --- * Individual tests - --- | Test for expression evaluation. -testEvalExpr :: Property -testEvalExpr = - forAll (chooseInt (0, maxTraceLength)) $ \steps -> - forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair -> - checkSemanticsP steps [] pair - --- | Test for expression evaluation with a drop. -testEvalExprWithDrop :: Property -testEvalExprWithDrop = - forAll (chooseInt (0, maxTraceLength)) $ \steps -> - forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair -> - forAllShow (arbitraryDrop pair) (semanticsShowK steps . snd) $ \(str, sem) -> - checkSemanticsP steps [str] sem - --- * 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)) - ] - --- | Generate an arbitrary drop by taking an expression, adding a number of --- elements to it, and then dropping some. -arbitraryDrop :: SemanticsP -> Gen (Stream, SemanticsP) -arbitraryDrop (SemanticsP (expr, meaning)) = do - -- Randomly generate a list of elements - prependLength <- getPositive <$> arbitrary - buffer <- vectorOf prependLength arbitrary - - -- Build the stream with the buffer - let streamId = 0 - stream = Stream streamId buffer expr typeOf - - -- Select how many elements to drop from the stream (up to the length of the - -- buffer) - dropLength <- chooseInt (0, prependLength) - - -- Build a drop expression that drops those many elements, paired with its - -- meaning. - let expr' = Drop typeOf (fromIntegral dropLength) streamId - meaning' = drop dropLength buffer ++ meaning - - return (stream, SemanticsP (expr', meaning')) - --- ** Random Expr generators - --- | An arbitrary constant expression of any type, paired with its expected --- meaning. -arbitraryConst :: (Arbitrary t, Typed t) - => Gen (Expr t, [t]) -arbitraryConst = (\v -> (Const typeOf v, repeat v)) <$> arbitrary - --- | An arbitrary boolean expression, paired with its expected meaning. -arbitraryBoolExpr :: Gen (Expr 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, apply1 <$> arbitraryBoolOp1 <*> arbitraryBoolExpr) - - , (1, apply2 <$> arbitraryBoolOp2 - <*> arbitraryBoolExpr - <*> arbitraryBoolExpr) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBoolExpr - <*> arbitraryBoolExpr) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Int8, [Int8]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Int16, [Int16]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Int32, [Int32]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Int64, [Int64]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Word8, [Word8]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Word16, [Word16]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Word32, [Word32]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryBitsExpr - <*> (arbitraryBitsExpr :: Gen (Expr Word64, [Word64]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32]))) - - , (1, apply2 <$> arbitraryEqOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryNumExpr - <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryFloatingExpr - <*> (arbitraryFloatingExpr :: Gen (Expr Float, [Float]))) - - , (1, apply2 <$> arbitraryOrdOp2 - <*> arbitraryFloatingExpr - <*> (arbitraryFloatingExpr :: Gen (Expr Double, [Double]))) - - , (1, apply3 <$> arbitraryITEOp3 - <*> arbitraryBoolExpr - <*> arbitraryBoolExpr - <*> arbitraryBoolExpr) - ] - --- | An arbitrary numeric expression, paired with its expected meaning. -arbitraryNumExpr :: (Arbitrary t, Typed t, Num t) - => Gen (Expr 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) - => Gen (Expr 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 (Expr 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 (Expr 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 (Expr 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 (Expr 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 (Expr 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 (Expr 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 -> (Const typeOf 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 (Expr Bool -> Expr Bool, [Bool] -> [Bool]) -arbitraryBoolOp1 = elements - [ (Op1 Not, fmap not) - ] - --- | Generator for arbitrary numeric operators with arity 1, paired with their --- expected meaning. -arbitraryNumOp1 :: (Typed t, Num t) - => Gen (Expr t -> Expr t, [t] -> [t]) -arbitraryNumOp1 = elements - [ (Op1 (Abs typeOf), fmap abs) - , (Op1 (Sign typeOf), fmap signum) - ] - --- | Generator for arbitrary floating point operators with arity 1, paired with --- their expected meaning. -arbitraryFloatingOp1 :: (Typed t, Floating t) - => Gen (Expr t -> Expr t, [t] -> [t]) -arbitraryFloatingOp1 = elements - [ (Op1 (Exp typeOf), fmap exp) - , (Op1 (Sqrt typeOf), fmap sqrt) - , (Op1 (Log typeOf), fmap log) - , (Op1 (Sin typeOf), fmap sin) - , (Op1 (Tan typeOf), fmap tan) - , (Op1 (Cos typeOf), fmap cos) - , (Op1 (Asin typeOf), fmap asin) - , (Op1 (Atan typeOf), fmap atan) - , (Op1 (Acos typeOf), fmap acos) - , (Op1 (Sinh typeOf), fmap sinh) - , (Op1 (Tanh typeOf), fmap tanh) - , (Op1 (Cosh typeOf), fmap cosh) - , (Op1 (Asinh typeOf), fmap asinh) - , (Op1 (Atanh typeOf), fmap atanh) - , (Op1 (Acosh typeOf), fmap acosh) - ] - --- | Generator for arbitrary realfrac operators with arity 1, paired with their --- expected meaning. -arbitraryRealFracOp1 :: (Typed t, RealFrac t) - => Gen (Expr t -> Expr t, [t] -> [t]) -arbitraryRealFracOp1 = elements - [ (Op1 (Ceiling typeOf), fmap (fromIntegral . idI . ceiling)) - , (Op1 (Floor typeOf), 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) - => Gen (Expr t -> Expr t, [t] -> [t]) -arbitraryFractionalOp1 = elements - [ (Op1 (Recip typeOf), fmap recip) - ] - --- | Generator for arbitrary bitwise operators with arity 1, paired with their --- expected meaning. -arbitraryBitsOp1 :: (Typed t, Bits t) - => Gen (Expr t -> Expr t, [t] -> [t]) -arbitraryBitsOp1 = elements - [ (Op1 (BwNot typeOf), fmap complement) - ] - --- *** Op 2 - --- | Generator for arbitrary boolean operators with arity 2, paired with their --- expected meaning. -arbitraryBoolOp2 :: Gen ( Expr Bool -> Expr Bool -> Expr Bool - , [Bool] -> [Bool] -> [Bool] - ) -arbitraryBoolOp2 = elements - [ (Op2 And, zipWith (&&)) - , (Op2 Or, zipWith (||)) - ] - --- | Generator for arbitrary numeric operators with arity 2, paired with their --- expected meaning. -arbitraryNumOp2 :: (Typed t, Num t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryNumOp2 = elements - [ (Op2 (Add typeOf), zipWith (+)) - , (Op2 (Sub typeOf), zipWith (-)) - , (Op2 (Mul typeOf), zipWith (*)) - ] - --- | Generator for arbitrary integral operators with arity 2, paired with their --- expected meaning. -arbitraryIntegralOp2 :: (Typed t, Integral t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryIntegralOp2 = elements - [ (Op2 (Mod typeOf), zipWith mod) - , (Op2 (Div typeOf), zipWith quot) - ] - --- | Generator for arbitrary fractional operators with arity 2, paired with --- their expected meaning. -arbitraryFractionalOp2 :: (Typed t, Fractional t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryFractionalOp2 = elements - [ (Op2 (Fdiv typeOf), zipWith (/)) - ] - --- | Generator for arbitrary floating point operators with arity 2, paired with --- their expected meaning. -arbitraryFloatingOp2 :: (Typed t, Floating t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryFloatingOp2 = elements - [ (Op2 (Pow typeOf), zipWith (**)) - , (Op2 (Logb typeOf), zipWith logBase) - ] - --- | Generator for arbitrary floating point operators with arity 2, paired with --- their expected meaning. -arbitraryRealFloatOp2 :: (Typed t, RealFloat t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryRealFloatOp2 = elements - [ (Op2 (Atan2 typeOf), zipWith atan2) - ] - --- | Generator for arbitrary equality operators with arity 2, paired with their --- expected meaning. -arbitraryEqOp2 :: (Typed t, Eq t) - => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool]) -arbitraryEqOp2 = elements - [ (Op2 (Eq typeOf), zipWith (==)) - , (Op2 (Ne typeOf), zipWith (/=)) - ] - --- | Generator for arbitrary ordering operators with arity 2, paired with their --- expected meaning. -arbitraryOrdOp2 :: (Typed t, Ord t) - => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool]) -arbitraryOrdOp2 = elements - [ (Op2 (Le typeOf), zipWith (<=)) - , (Op2 (Lt typeOf), zipWith (<)) - , (Op2 (Ge typeOf), zipWith (>=)) - , (Op2 (Gt typeOf), zipWith (>)) - ] - --- | Generator for arbitrary bitwise operators with arity 2, paired with their --- expected meaning. -arbitraryBitsOp2 :: (Typed t, Bits t) - => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryBitsOp2 = elements - [ (Op2 (BwAnd typeOf), zipWith (.&.)) - , (Op2 (BwOr typeOf), zipWith (.|.)) - , (Op2 (BwXor typeOf), 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 (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t]) -arbitraryBitsIntegralOp2 = elements - [ (Op2 (BwShiftL typeOf typeOf), zipWith (\x y -> shiftL x (fromIntegral y))) - , (Op2 (BwShiftR typeOf typeOf), 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 ( Expr Bool -> Expr t -> Expr t -> Expr t - , [Bool] -> [t] -> [t] -> [t] - ) -arbitraryITEOp3 = return - (Op3 (Mux typeOf), 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 = (Expr 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 :: (Expr 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 (showType ty, render $ ppExpr expr, take steps exprList) - - where - - -- Type of the expression. The type is enforced by _u below. - ty = typeOf - - -- We want to show the type. To help GHC determine that the type t is the - -- same as the expression's (expr), we use an UExpr, which has an - -- additional constraint. This definition serves no other purpose than to - -- help enforce that constraint. - _u = UExpr ty expr - --- | 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 -> [Stream] -> SemanticsP -> Bool -checkSemanticsP steps streams (SemanticsP (expr, exprList)) = - any isNaN' expectation || resultValues == expectation - where - -- Limit expectation to the number of evaluation steps. - expectation = take steps exprList - - -- Obtain the results by looking up the observer in the spec - -- and parsing the results into Haskell values. - resultValues = fmap readResult results - results = lookupWithDefault testObserverName [] - $ interpObservers trace - - -- Spec with just one observer of one expression. - trace = eval Haskell steps spec - spec = Spec streams observers [] [] - observers = [Observer testObserverName expr typeOf] - - -- 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 diff --git a/tests/Test/Copilot/Core/Type.hs b/tests/Test/Copilot/Core/Type.hs --- a/tests/Test/Copilot/Core/Type.hs +++ b/tests/Test/Copilot/Core/Type.hs @@ -4,17 +4,19 @@ -- External imports import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) -import Test.QuickCheck (Property, elements, forAllBlind, - shuffle, (==>)) +import Test.QuickCheck (Gen, Property, elements, + forAllBlind, shuffle, (==>)) -- Internal imports: library modules being tested -import Copilot.Core.Type (SimpleType (..)) +import Copilot.Core.Type (SimpleType (..), Type(..), simpleType) -- | All unit tests for copilot-core:Copilot.Core.Type. tests :: Test.Framework.Test tests = testGroup "Copilot.Core.Type" - [ testProperty "reflexivity of equality of simple types" + [ testProperty "simpleType preserves inequality" + testSimpleTypesInequality + , testProperty "reflexivity of equality of simple types" testSimpleTypesEqualityReflexive , testProperty "symmetry of equality of simple types" testSimpleTypesEqualitySymmetric @@ -23,6 +25,35 @@ , testProperty "uniqueness of equality of simple types" testSimpleTypesEqualityUniqueness ] + +-- | Test that the function simpleTypes preserves inequality, that is, it +-- returns different values for different types. This test is limited; we do +-- not test structs or arrays. +testSimpleTypesInequality :: Property +testSimpleTypesInequality = forAllBlind twoDiffTypes $ \(t1, t2) -> + t1 /= t2 + where + twoDiffTypes :: Gen (SimpleType, SimpleType) + twoDiffTypes = do + shuffled <- shuffle diffTypes + case shuffled of + (t1:t2:_) -> return (t1, t2) + _ -> return (SBool, SBool) + + -- | A list of types that should all be different. + diffTypes :: [SimpleType] + diffTypes = [ simpleType Bool + , simpleType Int8 + , simpleType Int16 + , simpleType Int32 + , simpleType Int64 + , simpleType Word8 + , simpleType Word16 + , simpleType Word32 + , simpleType Word64 + , simpleType Float + , simpleType Double + ] -- | Test that the equality relation for simple types is reflexive. testSimpleTypesEqualityReflexive :: Property diff --git a/tests/Test/Copilot/Core/Type/Show.hs b/tests/Test/Copilot/Core/Type/Show.hs deleted file mode 100644 --- a/tests/Test/Copilot/Core/Type/Show.hs +++ /dev/null @@ -1,38 +0,0 @@ --- The following warning is disnabled in this module so that the import of --- Copilot.Core.Type.Show does not give rise to a warning. -{-# OPTIONS_GHC -fno-warn-deprecations #-} - --- | Test copilot-core:Copilot.Core.Type.Show. -module Test.Copilot.Core.Type.Show where - --- External imports -import Test.Framework (Test, testGroup) -import Test.Framework.Providers.QuickCheck2 (testProperty) -import Test.QuickCheck (Arbitrary, Property, property) -import Text.Read (readMaybe) - --- Internal imports: library modules being tested -import Copilot.Core.Type (Type (Double, Float, Int16, Int32, Int64)) -import Copilot.Core.Type.Show (ShowType (Haskell), showWithType) - --- | All unit tests for copilot-core:Copilot.Core.Type.Show. -tests :: Test.Framework.Test -tests = - testGroup "Copilot.Core.Type.Show" - [ testProperty "read . showWithType == identity (Int16)" - (testShowRead Int16) - , testProperty "read . showWithType == identity (Int32)" - (testShowRead Int32) - , testProperty "read . showWithType == identity (Int64)" - (testShowRead Int64) - , testProperty "read . showWithType == identity (Float)" - (testShowRead Float) - , testProperty "read . showWithType == identity (Double)" - (testShowRead Double) - ] - --- | Test that showing a value with 'showWithType' and reading it back results --- in the same value. -testShowRead :: (Arbitrary a, Eq a, Read a) => Type a -> a -> Property -testShowRead t v = property $ - Just v == readMaybe (showWithType Haskell t v)