Skip to content
Open
Show file tree
Hide file tree
Changes from 7 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion copilot-bluespec/copilot-bluespec.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ library
default-language : Haskell2010
hs-source-dirs : src

ghc-options : -Wall
ghc-options : -Wall -Werror
build-depends : base >= 4.9 && < 5
, directory >= 1.3 && < 1.4
, filepath >= 1.4 && < 1.6
Expand Down Expand Up @@ -98,3 +98,4 @@ test-suite tests

ghc-options:
-Wall
-Werror
3 changes: 2 additions & 1 deletion copilot-c99/copilot-c99.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ library
default-language : Haskell2010
hs-source-dirs : src

ghc-options : -Wall
ghc-options : -Wall -Werror
build-depends : base >= 4.9 && < 5
, directory >= 1.3 && < 1.4
, filepath >= 1.4 && < 1.6
Expand Down Expand Up @@ -95,3 +95,4 @@ test-suite unit-tests

ghc-options:
-Wall
-Werror
2 changes: 2 additions & 0 deletions copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -75,12 +75,14 @@ mkStructDecln (Struct x) = C.TypeDecln struct

mkField :: Value a -> C.FieldDecln
mkField (Value ty field) = C.FieldDecln (transType ty) (fieldName field)
mkStructDecln _ = error "Unhandled case"

-- | Write a forward struct declaration.
mkStructForwDecln :: Struct a => Type a -> C.Decln
mkStructForwDecln (Struct x) = C.TypeDecln struct
where
struct = C.TypeSpec $ C.Struct (typeName x)
mkStructForwDecln _ = error "Unhandled case"

-- * Ring buffers

Expand Down
18 changes: 10 additions & 8 deletions copilot-c99/src/Copilot/Compile/C99/Expr.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

modify (\(i, x, y) -> (i + 1, x, y))

-- Add new var decl
Expand Down Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The 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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

modify (\(i, x, y) -> (i + 1, x, y))

-- Add new var decl
Expand All @@ -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)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The * is aligned with the =. Can you align it to match?

Copy link
Author

Choose a reason for hiding this comment

The 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
Copy link
Member

Choose a reason for hiding this comment

The 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 = in the dest definition and the two lines under size would both have to be indented by one more space.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.


Expand Down Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion copilot-c99/src/Copilot/Compile/C99/Representation.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,6 @@ data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger

-- | Given a list of triggers, make their names unique.
mkUniqueTriggers :: [Trigger] -> [UniqueTrigger]
mkUniqueTriggers ts = zipWith mkUnique ts [0..]
mkUniqueTriggers ts = zipWith mkUnique ts [0 :: Integer ..]
where
mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t
24 changes: 11 additions & 13 deletions copilot-c99/tests/Test/Copilot/Compile/C99.hs
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,6 @@ import Test.QuickCheck.Gen (chooseAny, chooseBoundedIntegral)

-- External imports: Copilot
import Copilot.Core hiding (Property)
import Copilot.Core.Type.Array (array)

-- External imports: Modules being tested
import Copilot.Compile.C99 (cSettingsOutputDirectory, compile, compileWith,
mkDefaultCSettings)
Expand Down Expand Up @@ -434,15 +432,15 @@ funCompose2 (f1, g1) (f2, g2) (f3, g3) =

-- | Test case specification for specs with one input variable and one output.
data TestCase1 a b = TestCase1
{ wrapTC1Expr :: Spec
Spec
-- ^ Specification containing a trigger an extern of type 'a' and a trigger
-- with an argument of type 'b'.

, wrapTC1Fun :: [a] -> [b]
([a] -> [b])
-- ^ Function expected to function in the same way as the Spec being
-- tested.

, wrapTC1CopInp :: (String -> String, String, String, Gen a)
(String -> String, String, String, Gen a)
-- ^ Input specification.
--
-- - The first element is a function that prints the variable declaration
Expand All @@ -456,26 +454,26 @@ data TestCase1 a b = TestCase1
-- - The latter contains a randomized generator for values of the given
-- type.

, wrapTC1CopOut :: (String, String)
(String, String)
-- ^ Output specification.
--
-- The first element of the tuple contains the type of the output in C.
--
-- The second element of the tuple is the formatting string when printing
-- values of the given kind.
}


-- | Test case specification for specs with two input variables and one output.
data TestCase2 a b c = TestCase2
{ wrapTC2Expr :: Spec
Spec
-- ^ Specification containing a trigger an extern of type 'a' and a trigger
-- with an argument of type 'b'.

, wrapTC2Fun :: [a] -> [b] -> [c]
([a] -> [b] -> [c])
-- ^ Function expected to function in the same way as the Spec being
-- tested.

, wrapTC2CopInp1 :: (String -> String, String, String, Gen a)
(String -> String, String, String, Gen a)
-- ^ Input specification for the first input.
--
-- - The first element is a function that prints the variable declaration
Expand All @@ -489,7 +487,7 @@ data TestCase2 a b c = TestCase2
-- - The latter contains a randomized generator for values of the given
-- type.

, wrapTC2CopInp2 :: (String -> String, String, String, Gen b)
(String -> String, String, String, Gen b)
-- ^ Input specification for the second input.
--
-- - The first element is a function that prints the variable declaration
Expand All @@ -503,14 +501,14 @@ data TestCase2 a b c = TestCase2
-- - The latter contains a randomized generator for values of the given
-- type.

, wrapTC2CopOut :: (String, String)
(String, String)
-- ^ Output specification.
--
-- The first element of the tuple contains the type of the output in C.
--
-- The second element of the tuple is the formatting string when printing
-- values of the given kind.
}


-- | Generate test cases for expressions that behave like unary functions.
mkTestCase1 :: (Typed a, Typed b)
Expand Down
3 changes: 2 additions & 1 deletion copilot-core/copilot-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ library

ghc-options:
-Wall
-fno-warn-orphans
-Werror

build-depends:
base >= 4.9 && < 5
Expand Down Expand Up @@ -83,3 +83,4 @@ test-suite unit-tests

ghc-options:
-Wall
-Werror
9 changes: 7 additions & 2 deletions copilot-core/src/Copilot/Core/Type.hs
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 #-}
Expand Down Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The 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 stylish-haskell for that.

Copy link
Author

Choose a reason for hiding this comment

The 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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions copilot-core/src/Copilot/Core/Type/Array.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Member

@ivanperez-keera ivanperez-keera Nov 18, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we just make it _?

Copy link
Author

Choose a reason for hiding this comment

The 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')
4 changes: 1 addition & 3 deletions copilot-core/tests/Test/Copilot/Core/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
(:~:) (..))
Expand Down Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line goes over 80 characters. Can we wrap after -> or of?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.


-- | Simple types tested.
simpleTypes :: [SimpleType]
Expand Down
8 changes: 4 additions & 4 deletions copilot-core/tests/Test/Copilot/Core/Type/Array.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we align the $? Also, an alternative, shorter name could be len.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

expectedLength = fromIntegral (natVal len)
wrongLength = (expectedLength +) . getNonNegative <$> arbitrary

Expand All @@ -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
Expand Down
2 changes: 2 additions & 0 deletions copilot-interpreter/copilot-interpreter.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ library

ghc-options:
-Wall
-Werror

build-depends:
base >= 4.9 && < 5,
Expand Down Expand Up @@ -86,3 +87,4 @@ test-suite unit-tests

ghc-options:
-Wall
-Werror
Loading