copilot-core 4.1 → 4.2

raw patch · 6 files changed

+468/−45 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG +6/−0
• copilot-core.cabal +1/−1
• src/Copilot/Core/Expr.hs +1/−0
• src/Copilot/Core/Type.hs +195/−15
• tests/Test/Copilot/Core/Type.hs +138/−26
• tests/Test/Copilot/Core/Type/Array.hs +127/−3

@@ -1,3 +1,9 @@+2025-01-07+        * Version bump (4.2). (#577)+        * Deprecate fields of Copilot.Core.Expr.UExpr. (#565)+        * Increase test coverage. (#555)+        * Define generic implementations of Struct and Typed methods. (#564)+ 2024-11-07         * Version bump (4.1). (#561)         * Add Haddocks for updateField. (#525)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             4.1+version:             4.2 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.

@@ -71,3 +71,4 @@   { uExprType :: Type a   , uExprExpr :: Expr a   }+{-# DEPRECATED uExprType, uExprExpr "These fields are deprecated in Copilot 4.2. Use pattern matching instead." #-}

@@ -4,8 +4,9 @@ {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE GADTs                     #-} {-# LANGUAGE KindSignatures            #-}-{-# LANGUAGE Safe                      #-} {-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE Trustworthy               #-}+{-# LANGUAGE TypeApplications          #-} {-# LANGUAGE TypeOperators             #-} {-# LANGUAGE UndecidableInstances      #-} -- |@@ -20,6 +21,7 @@ module Copilot.Core.Type     ( Type (..)     , Typed (..)+    , typeOfDefault     , UType (..)     , SimpleType (..) @@ -28,25 +30,32 @@      , Value (..)     , toValues+    , toValuesDefault     , Field (..)     , typeName+    , typeNameDefault      , Struct     , fieldName     , accessorName     , updateField+    , updateFieldDefault     )   where  -- External imports+import Data.Char          (isLower, isUpper, toLower)+import Data.Coerce        (coerce) import Data.Int           (Int16, Int32, Int64, Int8) import Data.List          (intercalate) import Data.Proxy         (Proxy (..)) import Data.Type.Equality as DE import Data.Typeable      (Typeable, eqT, typeRep) import Data.Word          (Word16, Word32, Word64, Word8)+import GHC.Generics       (Datatype (..), D1, Generic (..), K1 (..), M1 (..),+                           U1 (..), (:*:) (..)) import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, sameNat,-                           symbolVal)+                           sameSymbol, symbolVal)  -- Internal imports import Copilot.Core.Type.Array (Array)@@ -61,24 +70,35 @@   toValues :: a -> [Value a]    -- | Update the value of a struct field. This is only used by the Copilot-  -- interpreter, so if you do not plan to use the interpreter, it is safe to-  -- omit an implementation of this method.+  -- interpreter.   ---  -- In order to implement 'updateField', you should do the following for each-  -- 'Field' in a struct:+  -- If you do not plan to use the interpreter, you can omit an implementation+  -- of this method. If you do so, it is recommended that you derive a 'Generic'+  -- instance for the struct data type. This is because in a future release, the+  -- default implementation of 'updateField' (which will be picked if there is+  -- not a manually written implementation) will be changed to require a+  -- 'Generic' instance.   ---  -- 1. Check that the name of the 'Field' matches the name of the supplied-  --    'Value' (using 'GHC.TypeLits.sameSymbol').+  -- In order to implement 'updateField', pick one of the following approaches:   ---  -- 2. Check that the type of the 'Field' matches the 'Type' of the supplied-  --    'Value' (using 'DE.testEquality').+  -- * Derive a 'Generic' instance for the struct data type and then define+  --   @'updateField' = 'updateFieldDefault'@ in the 'Struct' instance.   ---  -- 3. If both (1) and (2) succeed, update the corresponding struct field using-  --    a record update.+  -- * Manually implement 'updateField' by doing the following for each 'Field'+  --   in a struct:   ---  -- For a complete end-to-end example that demonstrates how to implement-  -- 'updateField' and use it in the Copilot interpreter, see the-  -- @examples/StructsUpdateField.hs@ example in the @copilot@ library.+  --   1. Check that the name of the 'Field' matches the name of the supplied+  --      'Value' (using 'GHC.TypeLits.sameSymbol').+  --+  --   2. Check that the type of the 'Field' matches the 'Type' of the supplied+  --      'Value' (using 'DE.testEquality').+  --+  --   3. If both (1) and (2) succeed, update the corresponding struct field+  --      using a record update.+  --+  --   For a complete end-to-end example that demonstrates how to manually+  --   implement 'updateField' and use it in the Copilot interpreter, see the+  --   @examples/StructsUpdateField.hs@ example in the @copilot@ library.   updateField :: a -> Value t -> a   updateField = error $ unlines     [ "Field updates not supported for this type."@@ -272,3 +292,163 @@  instance Eq UType where   UType ty1 == UType ty2 = typeRep ty1 == typeRep ty2++-- * GHC.Generics-based defaults++-- | A default implementation of 'typeName' that leverages 'Generic'. In order+-- to use this, make sure you derive a 'Generic' instance for your data type and+-- then define @'typeName' = 'typeNameDefault'@ in its 'Struct' instance.+--+-- This generates a struct name that consists of the name of the original+-- Haskell data type, but converted to snake_case.+typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String+typeNameDefault = convert . gTypeName . from+  where+    convert :: String -> String+    convert = convert' True True++    convert' :: Bool   -- ^ Is this the first letter+             -> Bool   -- ^ Was the previous letter capital+             -> String -- ^ Remainder of the string+             -> String+    convert' _ _ []    = []+    convert' _ v [x]+      | v && isUpper x = toLower x : []+      | isUpper x      = '_' : toLower x : []+      | otherwise      = x : []+    convert' b v (x1:x2:xs)+      | not b && isUpper x1 && (isLower x2 || not v)+      = '_' : toLower x1 : convert' False (isUpper x1) (x2:xs)+      | otherwise+      = toLower x1 : convert' False (isUpper x1) (x2:xs)++-- | A default implementation of 'toValues' that leverages 'Generic'. In order+-- to use this, make sure you derive a 'Generic' instance for your data type and+-- then define @'toValues' = 'toValuesDefault'@ in its 'Struct' instance.+toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a]+toValuesDefault x = coerce $ gToValues $ from x++-- | A default implementation of 'updateField' that leverages 'Generic'. In+-- order to use this, make sure you derive a 'Generic' instance for your data+-- type and then define @'updateField' = 'updateFieldDefault'@ in its 'Struct'+-- instance.+updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a+updateFieldDefault a v@(Value _ field)+    | updated   = to a'+    | otherwise = error $ "Unexpected field: " ++ show field+  where+    (a', updated) = gUpdateField (from a) v++-- | A default implementation of 'typeOf' that leverages 'Generic'. In order to+-- use this, make sure you derive a 'Generic' instance for your data type and+-- then define @'typeOf' = 'typeOfDefault'@ in its 'Typed' instance.+typeOfDefault ::+  forall a. (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a+typeOfDefault = Struct $ to $ gStructPlaceholder @(Rep a) @()++-- ** Generic-based classes (not exported)++-- | Capture the name of a Haskell data type from its 'Generic' metadata.+class GDatatype f where+  -- | Returns the name of a Haskell data type. (Note that this differs from+  -- 'typeName', which is expected to return the name of the struct in the+  -- /target/ language).+  gTypeName :: f p -> String++-- | The only 'GDatatype' instance we need is for 'D1', which describes+-- 'Datatype' metadata (@d@). We ignore all other metadata (@_f@).+instance Datatype d => GDatatype (D1 d _f) where+  gTypeName = datatypeName++-- | Perform struct-related operations on 'Generic' representation types.+class GStruct f where+  -- | Transforms all the struct representation's fields into a list of values.+  gToValues :: f p -> [Value (f p)]++  -- | Update the value of a struct representation's field. This returns two+  -- things:+  --+  -- 1. @f p@: The struct representation, but with the field updated.+  --+  -- 2. 'Bool': This is 'True' if the field was successfully updated and 'False'+  --    otherwise. If this returns 'False', it is the responsibility of the+  --    caller to raise an error.+  gUpdateField :: f p -> Value t -> (f p, Bool)++-- | 'U1' represents a data constructor with no fields. As such, 'gToValues'+-- returns an empty list of 'Value's, and 'gUpdateField' does not update+-- anything.+instance GStruct U1 where+  gToValues U1 = []+  gUpdateField u _ = (u, False)++-- | 'M1' is only used to store metadata, which the 'GStruct' class does not+-- make use of. As such, this instance discards the metadata and recurses.+instance GStruct f => GStruct (M1 _i _c f) where+  gToValues (M1 x) = coerce (gToValues x)+  gUpdateField (M1 x) v = (M1 x', updated)+    where+      (x', updated) = gUpdateField x v++-- | @(':*:')@ represents a data constructor with multiple fields.+instance (GStruct f, GStruct g) => GStruct (f :*: g) where+  -- Recursively compute two lists of Values and append them.+  gToValues (f :*: g) = coerce (gToValues f) ++ coerce (gToValues g)+  -- Recursively attempt to update the field in both branches and combine the+  -- updated branches. We will have successfully updated the field if either+  -- branch was successfully updated.+  gUpdateField (f :*: g) v = (f' :*: g', updatedF || updatedG)+    where+      (f', updatedF) = gUpdateField f v+      (g', updatedG) = gUpdateField g v++-- | 'K1' represents a single field in a data constructor. This is the base+-- case.+instance (KnownSymbol name, Typed ty, c ~ Field name ty) =>+    GStruct (K1 _i c) where+  -- Now that we have the field, return it in a singleton list.+  gToValues (K1 field) = [Value typeOf field]+  -- In order to update the field, we check that the field names and types+  -- match. If they do, return the updated field and declare the update as+  -- successful. Otherwise, return the old field and declare the update as+  -- unsuccessful.+  gUpdateField (K1 oldField) (Value newTy (newField :: Field newName newTy)) =+    case (sameSymbol pName pNewName, testEquality ty newTy) of+      (Just Refl, Just Refl) -> (K1 newField, True)+      _                      -> (K1 oldField, False)+    where+      pName    = Proxy @name+      pNewName = Proxy @newName+      ty       = typeOf @ty++-- | Compute a 'Generic' placeholder value to use for a struct type.+class GTypedStruct f where+  -- | A placeholder value to supply to use in a generic implementation of+  -- 'typeOf' for a struct type.+  gStructPlaceholder :: f p++-- | 'U1' represents a data constructor with no fields. As such,+-- 'gStructPlaceholder' simply returns the data constructor with no other+-- information.+instance GTypedStruct U1 where+  gStructPlaceholder = U1++-- | 'M1' is only used to store metadata, which the 'GTypedStruct' class does+-- not make use of. As such, this instance recursively computes a placeholder+-- value without inspecting the metadata.+instance GTypedStruct f => GTypedStruct (M1 _i _c f) where+  gStructPlaceholder = M1 gStructPlaceholder++-- | @(':*:')@ represents a data constructor with multiple fields. As such,+-- 'gStructPlaceholder' recursively computes placeholders for each field and+-- combines them into the overall data constructor.+instance (GTypedStruct f, GTypedStruct g) => GTypedStruct (f :*: g) where+  gStructPlaceholder = gStructPlaceholder :*: gStructPlaceholder++-- | 'K1' represents a single field in a data constructor. This is the base+-- case. This instance computes a placeholder value that works for any field of+-- any type.+instance (c ~ Field name ty) => GTypedStruct (K1 _i c) where+  -- We use 'undefined' as the actual value for the 'Field' because Copilot+  -- never inspects the value.+  gStructPlaceholder = K1 $ Field undefined

@@ -1,12 +1,19 @@-{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-} -- | Test copilot-core:Copilot.Core.Type. module Test.Copilot.Core.Type where  -- External imports import Data.Int                             (Int16, Int32, Int64, Int8) import Data.Maybe                           (isJust)-import Data.Type.Equality                   (testEquality)+import Data.Proxy                           (Proxy (..))+import Data.Type.Equality                   (TestEquality (..), testEquality,+                                             (:~:) (..)) import Data.Word                            (Word16, Word32, Word64, Word8)+import GHC.TypeLits                         (sameSymbol)+import Prelude                              as P import Test.Framework                       (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.QuickCheck                      (Gen, Property, arbitrary, elements,@@ -50,6 +57,8 @@         testUTypesInequality     , testProperty "inequality of utype via typeOf"         testUTypesTypeOfInequality+    , testProperty "inequality of different types"+        testTypesInequality     , testProperty "fieldName matches field name (positive)"         testFieldNameOk     , testProperty "fieldName matches field name (negative)"@@ -58,6 +67,10 @@         testShowField     , testProperty "Show struct"         testShowStruct+    , testProperty "Update struct"+        testUpdateStruct+    , testProperty "Update struct"+        testUpdateStructFail     , testProperty "accessorName matches field name (positive)"         testAccessorNameOk     , testProperty "accessorName matches field name (negative)"@@ -96,7 +109,7 @@                 , simpleType Float                 , simpleType Double                 , simpleType (Array Int8 :: Type (Array 3 Int8))-                , simpleType (Struct (S (Field 0)))+                , simpleType (Struct (S (Field 0) (Field 0)))                 ]  -- | Test that the equality relation for simple types is reflexive.@@ -177,12 +190,12 @@ -- | Test that equality is symmetric for UTypes via testEquality. testUTypesEqualitySymmetric :: Property testUTypesEqualitySymmetric =-  forAllBlind (elements utypes) $ \(UType t1) -> isJust (testEquality t1 t1)+  forAllBlind (elements utypes) $ \(UType t1) -> testEquality t1 t1 == Just Refl  -- | Test that testEquality implies equality for UTypes. testUTypesEq :: Property testUTypesEq =-  forAllBlind (elements utypes) $ \t@(UType t1) -> isJust (testEquality t1 t1) ==> t == t+  forAllBlind (elements utypes) $ \t@(UType t1) -> (testEquality t1 t1 == Just Refl) ==> t == t  -- | Test that any two different UTypes are not equal. --@@ -199,6 +212,21 @@         (t1:t2:_) -> return (t1, t2)         _         -> return (UType Bool, UType Bool) +-- | Test that any two different Types are not equal.+--+-- This function pre-selects two Types from a list of different UTypes, which+-- guarantees that they will be different.+testTypesInequality :: Property+testTypesInequality = forAllBlind twoDiffTypes $ \(UType t1, UType t2) ->+    testEquality t1 t2 == Nothing+  where+    twoDiffTypes :: Gen (UType, UType)+    twoDiffTypes = do+      shuffled <- shuffle utypes+      case shuffled of+        (t1:t2:_) -> return (t1, t2)+        _         -> return (UType Bool, UType Bool)+ -- | Different UTypes. utypes :: [UType] utypes =@@ -213,19 +241,43 @@     , UType Word64     , UType Float     , UType Double-    , UType a-    , UType b+    , UType a1+    , UType a2+    , UType a3+    , UType a4+    , UType b1+    , UType b2+    , UType b3+    , UType b4     , UType c     ]   where-    a :: Type (Array 3 Int8)-    a = Array Int8+    a1 :: Type (Array 3 Int8)+    a1 = Array Int8 -    b :: Type (Array 4 Int8)-    b = Array Int8+    a2 :: Type (Array 4 Int8)+    a2 = Array Int8 +    a3 :: Type (Array 5 Int8)+    a3 = Array Int8++    a4 :: Type (Array 6 Int8)+    a4 = Array Int8++    b1 :: Type (Array 3 Int16)+    b1 = Array Int16++    b2 :: Type (Array 4 Int16)+    b2 = Array Int16++    b3 :: Type (Array 5 Int16)+    b3 = Array Int16++    b4 :: Type (Array 6 Int16)+    b4 = Array Int16+     c :: Type S-    c = Struct (S (Field 0))+    c = Struct (S (Field 0) (Field 0))  -- | Test that any two different UTypes are not equal. --@@ -259,47 +311,86 @@     , UType (typeOf :: Type Float)     , UType (typeOf :: Type Double)     , UType (typeOf :: Type (Array 3 Int8))+    , UType (typeOf :: Type (Array 3 Int16))+    , UType (typeOf :: Type (Array 3 Int32))+    , UType (typeOf :: Type (Array 3 Int64))+    , UType (typeOf :: Type (Array 3 Word8))+    , UType (typeOf :: Type (Array 3 Word16))+    , UType (typeOf :: Type (Array 3 Word32))+    , UType (typeOf :: Type (Array 3 Word64))+    , UType (typeOf :: Type (Array 3 Double))+    , UType (typeOf :: Type (Array 3 Float))     , UType (typeOf :: Type S)     ]  -- | Test the fieldName function (should succeed). testFieldNameOk :: Property-testFieldNameOk = forAll arbitrary $ \k ->-    fieldName (s1 (S (Field k))) == s1FieldName+testFieldNameOk = forAll arbitrary $ \k1 ->+                  forAll arbitrary $ \k2 ->+    fieldName (s1 (S (Field k1) (Field k2))) == s1FieldName   where-    s1FieldName = "field"+    s1FieldName = "field1"  -- | Test the fieldName function (should fail). testFieldNameFail :: Property testFieldNameFail = expectFailure $ property $     fieldName (s1 sampleS) == s1FieldName   where-    sampleS     = S (Field 0)+    sampleS     = S (Field 0) (Field 0)     s1FieldName = "Field"  -- | Test showing a field of a struct. testShowField :: Property testShowField = forAll arbitrary $ \k ->-  show (s1 (S (Field k))) == ("field:" ++ show k)+  show (s1 (S (Field k) (Field 0))) == ("field1:" ++ show k)  -- | Test showing a struct. testShowStruct :: Property-testShowStruct = forAll arbitrary $ \k ->-  show (S (Field k)) == "<field:" ++ show k ++ ">"+testShowStruct = forAll arbitrary $ \k1 ->+                 forAll arbitrary $ \k2 ->+  show (S (Field k1) (Field k2)) == "<field1:" ++ show k1 ++ ",field2:" ++ show k2 ++ ">" +-- | Test showing a struct.+testUpdateStruct :: Property+testUpdateStruct =+   forAll arbitrary $ \k1 ->+   forAll arbitrary $ \k2 ->+     let f :: Field "field1" Int8+         f = Field k2+         v :: Value Int8+         v = Value Int8 f+     in unField (s1 (updateField (S (Field k1) (Field 0)) v)) == k2++ where+   unField (Field x) = x++-- | Test showing a struct.+testUpdateStructFail :: Property+testUpdateStructFail = expectFailure $+   forAll arbitrary $ \k1 ->+   forAll arbitrary $ \k3 ->+     let f :: Field "field" Int8+         f = Field k3+         v :: Value Int8+         v = Value Int8 f+     in unField (s3 (updateField (S3 (Field k1)) v)) == k3++ where+   unField (Field x) = x+ -- | Test the accessorName of a field of a struct (should succeed). testAccessorNameOk :: Property testAccessorNameOk = property $     accessorName s1 == s1FieldName   where-    s1FieldName = "field"+    s1FieldName = "field1"  -- | Test the accessorName of a field of a struct (should fail). testAccessorNameFail :: Property testAccessorNameFail = expectFailure $ property $     accessorName s1 == s1FieldName   where-    s1FieldName = "Field"+    s1FieldName = "Field1"  -- | Test the typeName of a struct (should succeed). testTypeNameOk :: Property@@ -309,7 +400,7 @@   where      sampleS :: S-    sampleS = S (Field 0)+    sampleS = S (Field 0) (Field 0)      s1TypeName :: String     s1TypeName = "S"@@ -322,18 +413,39 @@   where      sampleS :: S-    sampleS = S (Field 0)+    sampleS = S (Field 0) (Field 0)      s1TypeName :: String     s1TypeName = "s"  -- | Auxiliary struct defined for testing purposes.-data S = S { s1 :: Field "field" Int8 }+data S = S { s1 :: Field "field1" Int8, s2 :: Field "field2" Word8 }  instance Struct S where   typeName _ = "S" -  toValues s = [ Value Int8 (s1 s) ]+  toValues s = [ Value Int8 (s1 s), Value Word8 (s2 s) ] +  updateField s (Value fieldTy (field :: Field fieldName a))+    | Just Refl <- sameSymbol (Proxy @"field1") (Proxy @fieldName)+    , Just Refl <- testEquality Int8 fieldTy+    = s { s1 = field }+    | Just Refl <- sameSymbol (Proxy @"field2") (Proxy @fieldName)+    , Just Refl <- testEquality Word8 fieldTy+    = s { s2 = field }+    | otherwise+    = error $ "Unexpected field: " P.++ show field+ instance Typed S where-  typeOf = Struct (S (Field 0))+  typeOf = Struct (S (Field 0) (Field 0))++-- | Auxiliary struct defined for testing purposes.+data S3 = S3 { s3 :: Field "field" Int8 }++instance Struct S3 where+  typeName _ = "S3"++  toValues s = [ Value Int8 (s3 s) ]++instance Typed S3 where+  typeOf = Struct (S3 (Field 0))

@@ -10,11 +10,12 @@ import Test.Framework                       (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.QuickCheck                      (Gen, Property, arbitrary,-                                             expectFailure, forAll, property,-                                             vector, vectorOf)+                                             chooseInt, expectFailure, forAll,+                                             getNegative, getNonNegative, oneof,+                                             property, vector, vectorOf)  -- Internal imports: library modules being tested-import Copilot.Core.Type.Array (Array, array, arrayElems)+import Copilot.Core.Type.Array (Array, array, arrayElems, arrayUpdate)  -- | All unit tests for copilot-core:Copilot.Core.Array. tests :: Test.Framework.Test@@ -30,6 +31,14 @@         testArrayElemsFail     , testProperty "Show for arrays"         testShowArray+    , testProperty "arrayElems (arrayUpdate x i v) !! i == v"+        (testArrayUpdateElem (Proxy :: Proxy 5))+    , testProperty "arrayUpdate x i ((arrayElems x) !! i) == x"+        (testArrayUpdateElems (Proxy :: Proxy 5))+    , testProperty "arrayUpdate fails if out of range of array"+        (testArrayUpdateWrong (Proxy :: Proxy 5))+    , testProperty "array fails length is wrong"+        (testArrayMakeWrongLength (Proxy :: Proxy 5))     ]  -- * Individual tests@@ -60,3 +69,118 @@ testShowArray :: Property testShowArray = forAll (vector 3) $ \l -> property $   show (array l :: Array 3 Int64) == show (l :: [Int64])++-- | Test that updating an array updates the element appropriately (if we+-- project that element we get the value we put in).+testArrayUpdateElem :: forall n . KnownNat n => Proxy n -> Property+testArrayUpdateElem len =+    forAll xsInt64  $ \ls ->+    forAll position $ \p ->+    forAll xInt64   $ \v ->+      let -- Original array+          array' :: Array n Int64+          array' = array ls++          -- Updated array+          array'' :: Array n Int64+          array'' = arrayUpdate array' p v++      in arrayElems array'' !! p == v++  where++    -- Generator for lists of Int64 of known length.+    xsInt64 :: Gen [Int64]+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary++    -- Generator for element of type Int64.+    xInt64 :: Gen Int64+    xInt64 = arbitrary++    -- Generator for positions within the list.+    position :: Gen Int+    position = chooseInt (0, fromIntegral (natVal len) - 1)++-- | Test that updating an array updates the element appropriately (if we+-- project that element we get the value we put in).+testArrayUpdateWrong :: forall n . KnownNat n => Proxy n -> Property+testArrayUpdateWrong len =+    expectFailure   $+    forAll xsInt64  $ \ls ->+    forAll position $ \p ->+    forAll xInt64   $ \v ->+      let -- Original array+          array' :: Array n Int64+          array' = array ls++          -- Updated array+          array'' :: Array n Int64+          array'' = arrayUpdate array' (p + 10) v++      in arrayElems array'' !! p == v++  where++    -- Generator for lists of Int64 of known length.+    xsInt64 :: Gen [Int64]+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary++    -- Generator for element of type Int64.+    xInt64 :: Gen Int64+    xInt64 = arbitrary++    -- Generator for positions within the list.+    position :: Gen Int+    position = oneof+      [ (fromIntegral (natVal len) +) . getNonNegative <$> arbitrary+      , getNegative <$> arbitrary+      ]++-- | Test that making an array of a specific length fails if the list of+-- elements supplied doesn't have the same length.+testArrayMakeWrongLength :: forall n . KnownNat n => Proxy n -> Property+testArrayMakeWrongLength len =+    expectFailure           $+    forAll wrongLength      $ \length ->+    forAll (xsInt64 length) $ \ls ->+      let array' :: Array n Int64+          array' = array ls+      in arrayElems array' == ls+  where+    xsInt64 length = vectorOf length arbitrary+    expectedLength = fromIntegral (natVal len)+    wrongLength    = (expectedLength +) . getNonNegative <$> arbitrary++-- | Test that updating an array updates the element appropriately (if we+-- project that element we get the value we put in).+testArrayUpdateElems :: forall n . KnownNat n => Proxy n -> Property+testArrayUpdateElems len =+    forAll xsInt64  $ \ls ->+    forAll position $ \p ->+    forAll xInt64   $ \v ->+      let -- Original array+          array' :: Array n Int64+          array' = array ls++          -- Updated array+          e :: Int64+          e = arrayElems array' !! p++          array'' :: Array n Int64+          array'' = arrayUpdate array' p e++      in arrayElems array'' == ls++  where++    -- Generator for lists of Int64 of known length.+    xsInt64 :: Gen [Int64]+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary++    -- Generator for element of type Int64.+    xInt64 :: Gen Int64+    xInt64 = arbitrary++    -- Generator for positions within the list.+    position :: Gen Int+    position = chooseInt (0, fromIntegral (natVal len) - 1)