Skip to content
Open
Show file tree
Hide file tree
Changes from all 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
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 arrT'@(Array ty) = C.LitInt (fromIntegral $ typeLength arrT')
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' siz'
where
dest = C.Index (C.Ident varName) e2'
size = C.LitInt
siz' = C.LitInt
(fromIntegral $ typeSize ty2)
C..* C.SizeOfType (C.TypeName (tyElemName ty2))

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
1 change: 0 additions & 1 deletion copilot-core/copilot-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ library

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

Comment on lines 41 to 42
Copy link
Member

Choose a reason for hiding this comment

The 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?

Copy link
Author

@yaitskov yaitskov Nov 18, 2025

Choose a reason for hiding this comment

The 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
Expand Down
35 changes: 20 additions & 15 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 @@ -45,21 +46,22 @@ module Copilot.Core.Type
where

-- External imports
import Data.Char (isLower, isUpper, toLower)
import Data.Coerce (coerce)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.List (intercalate)
import Data.Proxy (Proxy (..))
import Data.Type.Equality as DE
import Data.Typeable (Typeable, eqT, typeRep)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics (Datatype (..), D1, Generic (..), K1 (..), M1 (..),
U1 (..), (:*:) (..))
import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
sameSymbol, symbolVal)
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
import Data.Typeable (Typeable, eqT, typeRep)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics (D1, Datatype (..), Generic (..),
K1 (..), M1 (..), U1 (..), (:*:) (..))
import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal,
sameNat, sameSymbol, symbolVal)

-- Internal imports
import Copilot.Core.Type.Array (Array)
import Copilot.Core.Type.Array (Array)

-- | The value of that is a product or struct, defined as a constructor with
-- several fields.
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 (_: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')
7 changes: 4 additions & 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,10 @@ 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]
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 $ \lengt' ->
forAll (xsInt64 lengt') $ \ls ->
let array' :: Array n Int64
array' = array ls
in arrayElems array' == ls
where
xsInt64 length = vectorOf length arbitrary
xsInt64 lengt' = vectorOf lengt' arbitrary
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 $ \_ ->
let -- Original array
array' :: Array n Int64
array' = array ls
Expand Down
Loading