Conversation
| dest = C.Index (C.Ident varName) e2' | ||
| size = C.LitInt | ||
| size' = C.LitInt | ||
| (fromIntegral $ typeSize ty2) | ||
| C..* C.SizeOfType (C.TypeName (tyElemName ty2)) |
There was a problem hiding this comment.
If we make this change, we'd have to align the surrounding lines accordingly. The = in the dest definition and the two lines under size would both have to be indented by one more space.
| size arrTy'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrTy') | ||
| C..* C.SizeOfType (C.TypeName $ transType ty) |
There was a problem hiding this comment.
The * is aligned with the =. Can you align it to match?
| (i', _, _) <- get | ||
| let varName = "_v" ++ show i' |
| 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 |
| (i', _, _) <- get | ||
| let varName = "_v" ++ show i' |
| -Wall | ||
| -fno-warn-orphans | ||
|
|
There was a problem hiding this comment.
I'm confused by this. Why is it needed? Is it because it's being added to the specific modules that need it?
There was a problem hiding this comment.
the warning tuning flag is used once (Copilot/Core/Type.hs)
| import Data.Char (isLower, isUpper, toLower) | ||
| import Data.Coerce (coerce) | ||
| import Data.Int (Int16, Int32, Int64, Int8) | ||
| import qualified Data.Kind as DK |
There was a problem hiding this comment.
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 stylish-haskell for that.
| 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) |
There was a problem hiding this comment.
Can we just make it _?
| notElem t ts | ||
| forAllBlind (shuffle simpleTypes) $ \x -> case x of [] -> False; (t:ts) -> notElem t ts |
There was a problem hiding this comment.
This line goes over 80 characters. Can we wrap after -> or of?
| 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 |
There was a problem hiding this comment.
Can we align the $? Also, an alternative, shorter name could be len.
| Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..), | ||
| Trigger (..), Type (..), UExpr (..), Value (..), | ||
| arrayElems, arrayUpdate, specObservers, | ||
| arrayElems, arrayUpdate, specObservers, |
There was a problem hiding this comment.
If this is just a stylistic change that doesn't otherwise fix a warning, I'd like to keep that separate. We try to get PRs to focus on one concern only (can be over multiple files and commits, but still just focused on solving one problem).
| let Just buff = lookup id strms >>= fromDynamic in | ||
| reverse buff !! (fromIntegral i + k) | ||
| Local t1 _ name e1 e2 -> | ||
| Drop _t i id -> |
There was a problem hiding this comment.
Since the type is not captured in the Const case, we can probably just use _.
| Just buff -> reverse buff !! (fromIntegral i + k) | ||
| Nothing -> error $ "No id " ++ show id ++ " in " ++ show strms |
There was a problem hiding this comment.
Can we align the ->?
Also, is this a suitable way to show a message to a user who is not a regular Haskeller? Should the message be presented differently?
There was a problem hiding this comment.
I guess Nothing branch is unreachable code
| case lookup id strms >>= fromDynamic of | ||
| Just buff -> reverse buff !! (fromIntegral i + k) | ||
| Nothing -> error $ "No id " ++ show id ++ " in " ++ show strms | ||
| Local _t1 _ name e1 e2 -> |
There was a problem hiding this comment.
Since we don't capture the type in the Const case, we can probably just use _.
| let locs' = (name, toDyn x) : locs in | ||
| x `seq` locs' `seq` evalExpr_ k e2 locs' strms | ||
| Var t name -> fromJust $ lookup name locs >>= fromDynamic | ||
| Var _t name -> fromJust $ lookup name locs >>= fromDynamic |
There was a problem hiding this comment.
Since we don't capture the type in the Const case, we can probably just use _.
There was a problem hiding this comment.
Also, we'd want to keep the -> aligned (in this and in all cases).
| evalOp3 :: Op3 a b c d -> (a -> b -> c -> d) | ||
| evalOp3 (Mux _) = \ !v !x !y -> if v then x else y | ||
| evalOp3 (UpdateArray ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x | ||
| evalOp3 (UpdateArray _ty) = \xs n x -> arrayUpdate xs (fromIntegral n) x |
There was a problem hiding this comment.
Since we don't capture the type in the Mux case, we can probably just use _.
There was a problem hiding this comment.
In either case, we'd need to align the =.
| initStrm Stream { streamId = id | ||
| , streamBuffer = buffer | ||
| , streamExprType = t } = | ||
| } = |
There was a problem hiding this comment.
We'd have to remove the extra space in the two preceding lines, before the =, while still keeping them aligned. Also, if this fits in one line under 80 characters now, we can do that.
| import qualified Panic as Panic | ||
|
|
||
| import qualified Panic | ||
| import Prelude hiding (pred, recip, id) |
There was a problem hiding this comment.
Since the others are aligned and alphabetized, so should this (including the list of symbols imported).
| elts <- forM (CT.toValues a) $ \(CT.Value tp' (CT.Field a')) -> | ||
| translateConstExpr sym tp' a' |
| CT.Array tp' -> do | ||
| elts <- traverse (translateConstExpr sym tp') (CT.arrayElems a) |
| -> XExpr sym | ||
| -> TransM sym (XExpr sym) | ||
| translateOp1 sym origExpr op xe = case (op, xe) of | ||
| translateOp1 sym origExpr op' xe' = case (op', xe') of |
There was a problem hiding this comment.
I'd prefer to keep these as op and xe and make the ones below op' and xe'.
| -- The first argument is negative, and the second argument is a finite | ||
| -- noninteger | ||
| -- | ||
| -- * The first argument is zero, and the second argument is negative | ||
| -- The first argument is zero, and the second argument is negative | ||
| -- | ||
| -- * The arguments cause the result to overflow | ||
| -- The arguments cause the result to overflow | ||
| -- | ||
| -- * The arguments cause the result to underflow | ||
| -- The arguments cause the result to underflow |
There was a problem hiding this comment.
Do these solve warnings or does it just fix the fact that the haddock documentation would come out wrong?
There was a problem hiding this comment.
haddock of ghc 8.6.5 breaks on this
There was a problem hiding this comment.
Do the commands cabal install, cabal test or cabal haddock fail and/or give a warning during compilation?
There was a problem hiding this comment.
GHC 8.10 on the haddock generation phase breaks with:
src/Copilot/Theorem/What4/Translate.hs:739:3: error:
parse error on input ‘-- * The first argument is negative, and the second argument is a finite’
|
739 | -- * The first argument is negative, and the second argument is a finite
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
@yaitskov Thanks for the very extensive PR. As a general rule, we want PRs to focus on one concern only (e.g., fixing warnings, fixing style, adding X feature, solving X bug, etc.). While a PR can sometimes address multiple things (solving a bug may require adding a feature, or solving a warning may require some style changes), we try to limit those to the cases where it is strictly necessary. In line with this, I've marked a few changes that I believe are not really addressing a warning, so they should be part of a different PR. As you may have seen by now, it's going to take a while to review it all. Because of that, as other folks in the team start making changes towards Copilot 4.7, you may experience conflicts when trying to rebase your branch on top of their changes. I think we'd be more successful getting your many changes adopted if we split this PR into multiple PRs, one per library, one per kind of change (e.g, warnings related to unused imports, warnings related to top-level functions without signatures, etc.), or even per library and per kind of change (especially in large libraries like Please note that this is not a complaint. I'm appreciative of your PR, and I'm trying to figure out the best way to get changes adopted without taking too much time or effort on either side. |
|
Closed by mistake. |
|
Also, a heads up: for any contributions to Copilot we need contributors to sign one of these two forms (whichever applies to their situation): https://github.com/Copilot-Language/copilot-discussion/tree/master/CLAs. You'll only need to do this once. Please send that, filling in all the details it asks for and signing it, to ivan.perezdominguez@nasa.gov. Thanks! |
OOPS If formatting is that important - how about a PR with just automatic reformat and then do reformat in precommit hook or at least trigger by hand before openings a PR? HLS, besides GHC, hints lot of minor issues (though I've seen eg HLS hint doesn't like var names |
|
I extracted #694 from this PR. |
4 participants
No description provided.