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