-
Notifications
You must be signed in to change notification settings - Fork 75
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 7 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 |
|---|---|---|
|
|
@@ -61,8 +61,8 @@ transExpr (Op2 (UpdateField ty1@(Struct _) ty2 f) e1 e2) = do | |
| e2' <- transExpr e2 | ||
|
|
||
| -- Variable to hold the updated struct | ||
| (i, _, _) <- get | ||
| let varName = "_v" ++ show i | ||
| (i', _, _) <- get | ||
| let varName = "_v" ++ show i' | ||
|
Comment on lines
+64
to
+65
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 👍 |
||
| modify (\(i, x, y) -> (i + 1, x, y)) | ||
|
|
||
| -- Add new var decl | ||
|
|
@@ -101,14 +101,14 @@ transExpr (Op2 op e1 e2) = do | |
| e2' <- transExpr e2 | ||
| return $ transOp2 op e1' e2' | ||
|
|
||
| transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do | ||
| transExpr (Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 👍 |
||
| e1' <- transExpr e1 | ||
| e2' <- transExpr e2 | ||
| e3' <- transExpr e3 | ||
|
|
||
| -- Variable to hold the updated array | ||
| (i, _, _) <- get | ||
| let varName = "_v" ++ show i | ||
| (i', _, _) <- get | ||
| let varName = "_v" ++ show i' | ||
|
Comment on lines
+110
to
+111
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 👍 |
||
| modify (\(i, x, y) -> (i + 1, x, y)) | ||
|
|
||
| -- Add new var decl | ||
|
|
@@ -117,18 +117,19 @@ transExpr e@(Op3 (UpdateArray arrTy@(Array ty2)) e1 e2 e3) = do | |
| modify (\(i, x, y) -> (i, x ++ [initDecl], y)) | ||
|
|
||
| let size :: Type (Array n t) -> C.Expr | ||
| size arrTy@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy) | ||
| size arrTy'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy') | ||
| C..* C.SizeOfType (C.TypeName $ transType ty) | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
| size _ = error "Unhandled case" | ||
|
|
||
| -- Initialize the var to the same value as the original array | ||
| let initStmt = C.Expr $ memcpy (C.Ident varName) e1' (size arrTy) | ||
|
|
||
| -- Update element of array | ||
| let updateStmt = case ty2 of | ||
| Array _ -> C.Expr $ memcpy dest e3' size | ||
| Array _ -> C.Expr $ memcpy dest e3' size' | ||
| where | ||
| dest = C.Index (C.Ident varName) e2' | ||
| size = C.LitInt | ||
| size' = C.LitInt | ||
| (fromIntegral $ typeSize ty2) | ||
| C..* C.SizeOfType (C.TypeName (tyElemName ty2)) | ||
|
Comment on lines
131
to
134
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If we make this change, we'd have to align the surrounding lines accordingly. The
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
|
|
||
|
|
@@ -183,6 +184,7 @@ transOp1 op e = | |
| BwNot _ -> (C..~) e | ||
| Cast _ ty -> C.Cast (transTypeName ty) e | ||
| GetField (Struct _) _ f -> C.Dot e (accessorName f) | ||
| _ -> error "Unhandled case" | ||
|
|
||
| -- | Translates a Copilot binary operator and its arguments into a C99 | ||
| -- expression. | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -39,7 +39,7 @@ library | |
|
|
||
| ghc-options: | ||
| -Wall | ||
| -fno-warn-orphans | ||
| -Werror | ||
|
|
||
|
Comment on lines
41
to
42
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm confused by this. Why is it needed? Is it because it's being added to the specific modules that need it?
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. the warning tuning flag is used once (Copilot/Core/Type.hs) |
||
| build-depends: | ||
| base >= 4.9 && < 5 | ||
|
|
@@ -83,3 +83,4 @@ test-suite unit-tests | |
|
|
||
| ghc-options: | ||
| -Wall | ||
| -Werror | ||
| 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 | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If we make this change, we have to align the surrounding imports (the module names need to be aligned, and the symbols imported need to be aligned. I normally use
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
| 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 t = case t of | ||
| 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) | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can we just make it
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
|
|
||
| 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 |
|---|---|---|
|
|
@@ -7,7 +7,6 @@ module Test.Copilot.Core.Type where | |
|
|
||
| -- External imports | ||
| import Data.Int (Int16, Int32, Int64, Int8) | ||
| import Data.Maybe (isJust) | ||
| import Data.Proxy (Proxy (..)) | ||
| import Data.Type.Equality (TestEquality (..), testEquality, | ||
| (:~:) (..)) | ||
|
|
@@ -136,8 +135,7 @@ testSimpleTypesEqualityTransitive = | |
| -- | Test that each type is only equal to itself. | ||
| testSimpleTypesEqualityUniqueness :: Property | ||
| testSimpleTypesEqualityUniqueness = | ||
| forAllBlind (shuffle simpleTypes) $ \(t:ts) -> | ||
| notElem t ts | ||
| forAllBlind (shuffle simpleTypes) $ \x -> case x of [] -> False; (t:ts) -> notElem t ts | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This line goes over 80 characters. Can we wrap after
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
|
|
||
| -- | Simple types tested. | ||
| simpleTypes :: [SimpleType] | ||
|
|
||
| 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 | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can we align the
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. |
||
| 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.