-
Notifications
You must be signed in to change notification settings - Fork 73
WIP: fix warnings #688
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
WIP: fix warnings #688
Changes from 2 commits
21333a5
269b649
268b6eb
d952fed
303ca49
71fcfa8
d7f0179
895828e
fc5db37
8a8a0b1
4c1e5b5
0308c1d
664260a
a52c577
89863b9
e1d0d55
496382d
898b27a
ec6960a
e2e92e5
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,4 @@ | ||
| {-# OPTIONS_GHC -fno-warn-orphans #-} | ||
| {-# LANGUAGE DataKinds #-} | ||
| {-# LANGUAGE ExistentialQuantification #-} | ||
| {-# LANGUAGE FlexibleContexts #-} | ||
|
|
@@ -48,6 +49,7 @@ module Copilot.Core.Type | |
| import Data.Char (isLower, isUpper, toLower) | ||
| import Data.Coerce (coerce) | ||
| import Data.Int (Int16, Int32, Int64, Int8) | ||
| import qualified Data.Kind as DK | ||
|
||
| import Data.List (intercalate) | ||
| import Data.Proxy (Proxy (..)) | ||
| import Data.Type.Equality as DE | ||
|
|
@@ -139,7 +141,7 @@ instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where | |
| -- Note that both arrays and structs use dependently typed features. In the | ||
| -- former, the length of the array is part of the type. In the latter, the | ||
| -- names of the fields are part of the type. | ||
| data Type :: * -> * where | ||
| data Type :: DK.Type -> DK.Type where | ||
| Bool :: Type Bool | ||
| Int8 :: Type Int8 | ||
| Int16 :: Type Int16 | ||
|
|
@@ -165,6 +167,7 @@ typeLength _ = fromIntegral $ natVal (Proxy :: Proxy n) | |
| typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int | ||
| typeSize ty@(Array ty'@(Array _)) = typeLength ty * typeSize ty' | ||
| typeSize ty@(Array _ ) = typeLength ty | ||
| typeSize ty = error $ "There is a bug in the type checker " ++ show ty | ||
|
|
||
| instance TestEquality Type where | ||
| testEquality Bool Bool = Just DE.Refl | ||
|
|
@@ -286,7 +289,9 @@ instance Typed Double where | |
|
|
||
| instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where | ||
| typeOf = Array typeOf | ||
| simpleType (Array t) = SArray t | ||
| simpleType = \case | ||
| Array t -> SArray t | ||
| o -> error $ "There is a bug in the type checker " ++ show o | ||
|
|
||
| -- | A untyped type (no phantom type). | ||
| data UType = forall a . Typeable a => UType (Type a) | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -53,12 +53,12 @@ arrayUpdate (Array []) _ _ = error errMsg | |
| where | ||
| errMsg = "copilot-core: arrayUpdate: Attempt to update empty array" | ||
|
|
||
| arrayUpdate (Array (x:xs)) 0 y = Array (y:xs) | ||
| arrayUpdate (Array (_x:xs)) 0 y = Array (y:xs) | ||
|
||
|
|
||
| arrayUpdate (Array (x:xs)) n y = | ||
| arrayAppend x (arrayUpdate (Array xs) (n - 1) y) | ||
| where | ||
| -- | Append to an array while preserving length information at the type | ||
| -- level. | ||
| arrayAppend :: a -> Array (n - 1) a -> Array n a | ||
| arrayAppend x (Array xs) = Array (x:xs) | ||
| arrayAppend x' (Array xs') = Array (x':xs') | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -141,13 +141,13 @@ testArrayUpdateWrong len = | |
| testArrayMakeWrongLength :: forall n . KnownNat n => Proxy n -> Property | ||
| testArrayMakeWrongLength len = | ||
| expectFailure $ | ||
| forAll wrongLength $ \length -> | ||
| forAll (xsInt64 length) $ \ls -> | ||
| 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 | ||
| xsInt64 length' = vectorOf length' arbitrary | ||
|
||
| expectedLength = fromIntegral (natVal len) | ||
| wrongLength = (expectedLength +) . getNonNegative <$> arbitrary | ||
|
|
||
|
|
@@ -157,7 +157,7 @@ testArrayUpdateElems :: forall n . KnownNat n => Proxy n -> Property | |
| testArrayUpdateElems len = | ||
| forAll xsInt64 $ \ls -> | ||
| forAll position $ \p -> | ||
| forAll xInt64 $ \v -> | ||
| forAll xInt64 $ \_v -> | ||
| let -- Original array | ||
| array' :: Array n Int64 | ||
| array' = array ls | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.