copilot-core 3.12 → 3.13

raw patch · 16 files changed

+153/−1078 lines, 16 filesdep −dlistPVP ok

version bump matches the API change (PVP)

Dependencies removed: dlist

API changes (from Hackage documentation)

Files

• CHANGELOG +10/−0
• copilot-core.cabal +3/−9
• src/Copilot/Core.hs +0/−7
• src/Copilot/Core/External.hs +0/−78
• src/Copilot/Core/Interpret.hs +1/−1
• src/Copilot/Core/Interpret/Eval.hs +7/−8
• src/Copilot/Core/PrettyDot.hs +1/−1
• src/Copilot/Core/PrettyPrint.hs +1/−1
• src/Copilot/Core/Type.hs +20/−3
• src/Copilot/Core/Type/Show.hs +74/−8
• src/Copilot/Core/Type/ShowInternal.hs +0/−77
• tests/Main.hs +1/−7
• tests/Test/Copilot/Core/External.hs +0/−47
• tests/Test/Copilot/Core/Interpret/Eval.hs +0/−789
• tests/Test/Copilot/Core/Type.hs +35/−4
• tests/Test/Copilot/Core/Type/Show.hs +0/−38

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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   ]

@@ -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

@@ -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

@@ -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

@@ -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)