Skip to content

Commit

Permalink
Merge branch 'develop-core-lowerCamelCase'. Close #457.
Browse files Browse the repository at this point in the history
**Description**

To comply with our NASA Class D requirements, our code must abide by a style
guide.

This is the third issue pertaining to style changes for conformance with Class
D within `copilot-core`. We focus only on `copilot-core` to limit the size of
the issue.

**Type**

- Management: conformance with new requirement.

**Additional context**

- See issues 332 and 316 for other style changes addressed in `copilot-core`.

**Requester**

- Ivan Perez

**Method to check presence of bug**

The following Dockerfile checks that each of the functions in question have
been deprecated, in which case it prints the message Success:

```
FROM ubuntu:trusty

RUN apt-get update

RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update

RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
RUN apt-get install --yes libz-dev

ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN cabal v1-install alex happy
RUN apt-get install --yes git

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
  && cabal v1-install copilot/copilot-core/ \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "import Copilot.Core.Type(typename,Struct); t :: Struct a => a -> String ; t = typename; main :: IO (); main = return ()" \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "{-# LANGUAGE DataKinds #-}; import Copilot.Core.Type(tylength, Type); import Copilot.Core.Type.Array(Array); t :: Type (Array 3 Bool) -> Int ; t = tylength; main :: IO (); main = return ()" \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "{-# LANGUAGE DataKinds #-}; import Copilot.Core.Type(tysize, Type); import Copilot.Core.Type.Array(Array); t :: Type (Array 3 Bool) -> Int ; t = tysize; main :: IO (); main = return ()" \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "import GHC.TypeLits(KnownSymbol); import Copilot.Core.Type(fieldname, Field); t :: KnownSymbol s0 => Field s0 t0 -> String; t = fieldname; main :: IO (); main = return ()" \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "import GHC.TypeLits(KnownSymbol); import Copilot.Core.Type(Field, Struct, accessorname); t :: (Struct a0, KnownSymbol s0) => (a0 -> Copilot.Core.Type.Field s0 t0) -> String; t = accessorname; main :: IO (); main = return ()" \
  && ! cabal v1-exec -- runhaskell -Wall -Werror=deprecations <<< "import Copilot.Core.Type.Array(arrayelems); t = arrayelems; main :: IO (); main = return ()" \
  && echo "Success"
```

Command (substitute variables based on new path after merge):
```sh
$ docker run -e "REPO=https://github.com/copilot-language/copilot" -e "NAME=copilot" -e "COMMIT=<commit_hash>" copilot-verify-457
```

**Expected result**

All Copilot Core code conforms to the following rules:

- Variable and function names should be lowerCamelCase.

Running the docker file above prints the message Success, indicating that, for
all functions identified as non-conforming with the style guide, importing them
(and using them) results in an error.

**Solution implemented**

Deprecate `Copilot.Core.Type.typename`, `Copilot.Core.Type.tylength`,
`Copilot.Core.Type.tysize`, `Copilot.Core.Type.fieldname`,
`Copilot.Core.Type.accessorname`, `Copilot.Core.Type.Array.arrayelems`, and
define corresponding functions with lowerCamelCase names.

Update all uses across all of copilot to match the new function names.

**Further notes**

These changes are public facing, they affect functions that are part of the
API. We follow the deprecation policy for them.

In the docker file, we have to use the functions or GHC will not actually
report an error. In some cases, using them, even if just to define a synonym
for them (one of the simplest ways to use them), requires substantial
boilerplate (signatures, additional imports, extensions, etc).
  • Loading branch information
ivanperez-keera committed Nov 6, 2023
2 parents 526cb74 + 73aee20 commit e0a86dd
Show file tree
Hide file tree
Showing 18 changed files with 94 additions and 37 deletions.
3 changes: 3 additions & 0 deletions copilot-c99/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-05
* Replace uses of deprecated functions. (#457)

2023-09-07
* Version bump (3.16.1). (#455)
* Clean code. (#453)
Expand Down
14 changes: 7 additions & 7 deletions copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ import qualified Language.C99.Simple as C

-- Internal imports: Copilot
import Copilot.Core ( Expr (..), Id, Stream (..), Struct (..), Trigger (..),
Type (..), UExpr (..), Value (..), fieldname, tysize )
Type (..), UExpr (..), Value (..), fieldName, typeSize )

-- Internal imports
import Copilot.Compile.C99.Error ( impossible )
Expand Down Expand Up @@ -67,17 +67,17 @@ mkExtCpyDecln (External _name cpyName ty) = decln
mkStructDecln :: Struct a => Type a -> C.Decln
mkStructDecln (Struct x) = C.TypeDecln struct
where
struct = C.TypeSpec $ C.StructDecln (Just $ typename x) fields
struct = C.TypeSpec $ C.StructDecln (Just $ typeName x) fields
fields = NonEmpty.fromList $ map mkField (toValues x)

mkField :: Value a -> C.FieldDecln
mkField (Value ty field) = C.FieldDecln (transType ty) (fieldname field)
mkField (Value ty field) = C.FieldDecln (transType ty) (fieldName field)

-- | 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)
struct = C.TypeSpec $ C.Struct (typeName x)

-- * Ring buffers

Expand Down Expand Up @@ -134,7 +134,7 @@ mkGenFunArray name nameArg expr ty@(Array _) =

-- Copy expression to output argument
stmts = [ C.Expr $ memcpy (C.Ident nameArg) cExpr size ]
size = C.LitInt (fromIntegral $ tysize ty)
size = C.LitInt (fromIntegral $ typeSize ty)
C..* C.SizeOfType (C.TypeName $ tyElemName ty)

mkGenFunArray _name _nameArg _expr _ty =
Expand Down Expand Up @@ -180,7 +180,7 @@ mkStep cSettings streams triggers exts =
where
dest = C.Index buffVar indexVar
size = C.LitInt
(fromIntegral $ tysize ty)
(fromIntegral $ typeSize ty)
C..* C.SizeOfType (C.TypeName (tyElemName ty))
_ -> C.Expr $
C.Index buffVar indexVar C..= C.Ident tmpVar
Expand All @@ -203,7 +203,7 @@ mkStep cSettings streams triggers exts =
where
exVar = C.Ident cpyName
locVar = C.Ident name
size = C.LitInt (fromIntegral $ tysize ty)
size = C.LitInt (fromIntegral $ typeSize ty)
C..* C.SizeOfType (C.TypeName (tyElemName ty))

_ -> C.Ident cpyName C..= C.Ident name
Expand Down
8 changes: 4 additions & 4 deletions copilot-c99/src/Copilot/Compile/C99/Expr.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ import qualified Language.C99.Simple as C

-- Internal imports: Copilot
import Copilot.Core ( Expr (..), Field (..), Op1 (..), Op2 (..), Op3 (..),
Type (..), Value (..), accessorname, arrayelems,
Type (..), Value (..), accessorName, arrayElems,
toValues )

-- Internal imports
Expand Down Expand Up @@ -96,7 +96,7 @@ transOp1 op e =
Floor ty -> funCall (specializeMathFunName ty "floor") [e]
BwNot _ -> (C..~) e
Cast _ ty -> C.Cast (transTypeName ty) e
GetField (Struct _) _ f -> C.Dot e (accessorname f)
GetField (Struct _) _ f -> C.Dot e (accessorName f)

-- | Translates a Copilot binary operator and its arguments into a C99
-- expression.
Expand Down Expand Up @@ -239,7 +239,7 @@ constTy ty = case ty of
Float -> explicitTy ty . C.LitFloat
Double -> explicitTy ty . C.LitDouble
Struct _ -> C.InitVal (transTypeName ty) . constStruct . toValues
Array ty' -> C.InitVal (transTypeName ty) . constArray ty' . arrayelems
Array ty' -> C.InitVal (transTypeName ty) . constArray ty' . arrayElems

-- | Transform a Copilot Core literal, based on its value and type, into a C99
-- initializer.
Expand All @@ -265,7 +265,7 @@ constInit ty val = case ty of
-- whole expression as an array of two int32_t's (as opposed to a nested
-- array). This can either lead to compile-time errors (if you're lucky) or
-- incorrect runtime semantics (if you're unlucky).
Array ty' -> C.InitList $ constArray ty' $ arrayelems val
Array ty' -> C.InitList $ constArray ty' $ arrayElems val

-- We use InitArray to initialize a struct because the syntax used for
-- initializing arrays and structs is compatible. For instance, {1, 2} works
Expand Down
6 changes: 3 additions & 3 deletions copilot-c99/src/Copilot/Compile/C99/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ module Copilot.Compile.C99.Type
import qualified Language.C99.Simple as C

-- Internal imports: Copilot
import Copilot.Core ( Type (..), tylength, typename )
import Copilot.Core ( Type (..), typeLength, typeName )

-- | Translate a Copilot type to a C99 type.
transType :: Type a -> C.Type
Expand All @@ -30,8 +30,8 @@ transType ty = case ty of
Double -> C.TypeSpec C.Double
Array ty' -> C.Array (transType ty') len
where
len = Just $ C.LitInt $ fromIntegral $ tylength ty
Struct s -> C.TypeSpec $ C.Struct (typename s)
len = Just $ C.LitInt $ fromIntegral $ typeLength ty
Struct s -> C.TypeSpec $ C.Struct (typeName s)

-- | Translate a Copilot type to a valid (local) variable declaration C99 type.
--
Expand Down
8 changes: 4 additions & 4 deletions copilot-c99/tests/Test/Copilot/Compile/C99.hs
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ arbitraryArrayIx :: forall t n . (Typed t, KnownNat n, Num t)
, [Array n t] -> [Word32] -> [t]
)
arbitraryArrayIx = return
(Op2 (Index typeOf), zipWith (\x y -> arrayelems x !! fromIntegral y))
(Op2 (Index typeOf), zipWith (\x y -> arrayElems x !! fromIntegral y))

-- | Generator of functions on Floating point numbers.
arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t])
Expand Down Expand Up @@ -860,7 +860,7 @@ varDeclC Word64 v = "uint64_t " ++ v
varDeclC Float v = "float " ++ v
varDeclC Double v = "double " ++ v
varDeclC t@(Array tE) v =
typeC tE ++ " " ++ v ++ "[" ++ show (tylength t) ++ "]"
typeC tE ++ " " ++ v ++ "[" ++ show (typeLength t) ++ "]"
varDeclC _ _ = error
"copilot-c99 (test): Input variables of type struct are not yet supported."

Expand All @@ -877,7 +877,7 @@ sizeC Word32 = "sizeof(uint32_t)"
sizeC Word64 = "sizeof(uint64_t)"
sizeC Float = "sizeof(float)"
sizeC Double = "sizeof(double)"
sizeC t@(Array tE) = show (tylength t) ++ "* sizeof(" ++ typeC tE ++ ")"
sizeC t@(Array tE) = show (typeLength t) ++ "* sizeof(" ++ typeC tE ++ ")"
sizeC _ = error
"copilot-c99 (test): Input variables of type struct are not yet supported."

Expand Down Expand Up @@ -920,7 +920,7 @@ instance CShow Bool where
cshow False = "false"

instance CShow t => CShow (Array n t) where
cshow a = intercalate "," $ map cshow $ arrayelems a
cshow a = intercalate "," $ map cshow $ arrayElems a

-- | Read a value of a given type in C.
class ReadableFromC a where
Expand Down
3 changes: 3 additions & 0 deletions copilot-core/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-05
* Compliance with style guide. (#457)

2023-09-07
* Version bump (3.16.1). (#455)

Expand Down
47 changes: 41 additions & 6 deletions copilot-core/src/Copilot/Core/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,16 +23,21 @@ module Copilot.Core.Type
, UType (..)
, SimpleType (..)

, typeSize
, tysize
, typeLength
, tylength

, Value (..)
, toValues
, Field (..)
, typeName
, typename

, Struct
, fieldName
, fieldname
, accessorName
, accessorname
)
where
Expand All @@ -50,11 +55,19 @@ import GHC.TypeLits (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
-- Internal imports
import Copilot.Core.Type.Array (Array)

{-# DEPRECATED typename "Use typeName instead." #-}

-- | The value of that is a product or struct, defined as a constructor with
-- several fields.
class Struct a where
-- | Returns the name of struct in the target language.
typeName :: a -> String
typeName = typename

-- | Returns the name of struct in the target language.
typename :: a -> String
typename = typeName

-- | Transforms all the struct's fields into a list of values.
toValues :: a -> [Value a]

Expand All @@ -66,18 +79,30 @@ data Value a =
-- level.
data Field (s :: Symbol) t = Field t

-- | Extract the name of a field.
fieldName :: forall s t . KnownSymbol s => Field s t -> String
fieldName _ = symbolVal (Proxy :: Proxy s)

{-# DEPRECATED fieldname "Use fieldName instead." #-}
-- | Extract the name of a field.
fieldname :: forall s t . KnownSymbol s => Field s t -> String
fieldname _ = symbolVal (Proxy :: Proxy s)
fieldname = fieldName

-- | Extract the name of an accessor (a function that returns a field of a
-- struct).
accessorName :: forall a s t . (Struct a, KnownSymbol s)
=> (a -> Field s t) -> String
accessorName _ = symbolVal (Proxy :: Proxy s)

{-# DEPRECATED accessorname "Use accessorName instead." #-}
-- | Extract the name of an accessor (a function that returns a field of a
-- struct).
accessorname :: forall a s t . (Struct a, KnownSymbol s)
=> (a -> Field s t) -> String
accessorname _ = symbolVal (Proxy :: Proxy s)
accessorname = accessorName

instance (KnownSymbol s, Show t) => Show (Field s t) where
show f@(Field v) = fieldname f ++ ":" ++ show v
show f@(Field v) = fieldName f ++ ":" ++ show v

instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
show t = "<" ++ fields ++ ">"
Expand Down Expand Up @@ -108,14 +133,24 @@ data Type :: * -> * where
) => Type t -> Type (Array n t)
Struct :: (Typed a, Struct a) => a -> Type a

-- | Return the length of an array from its type
typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int
typeLength _ = fromIntegral $ natVal (Proxy :: Proxy n)

{-# DEPRECATED tylength "Use typeLength instead." #-}
-- | Return the length of an array from its type
tylength :: forall n t . KnownNat n => Type (Array n t) -> Int
tylength _ = fromIntegral $ natVal (Proxy :: Proxy n)
tylength = typeLength

-- | Return the total (nested) size of an array from its type
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

{-# DEPRECATED tysize "Use typeSize instead." #-}
-- | Return the total (nested) size of an array from its type
tysize :: forall n t . KnownNat n => Type (Array n t) -> Int
tysize ty@(Array ty'@(Array _)) = tylength ty * tysize ty'
tysize ty@(Array _ ) = tylength ty
tysize = typeSize

instance TestEquality Type where
testEquality Bool Bool = Just DE.Refl
Expand Down
8 changes: 7 additions & 1 deletion copilot-core/src/Copilot/Core/Type/Array.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
module Copilot.Core.Type.Array
( Array
, array
, arrayElems
, arrayelems
)
where
Expand All @@ -39,6 +40,11 @@ array xs | datalen == typelen = Array xs
errmsg = "Length of data (" ++ show datalen ++
") does not match length of type (" ++ show typelen ++ ")."

-- | Return the elements of an array.
arrayElems :: Array n a -> [a]
arrayElems (Array xs) = xs

{-# DEPRECATED arrayelems "Use ArrayElems instead." #-}
-- | Return the elemts of an array.
arrayelems :: Array n a -> [a]
arrayelems (Array xs) = xs
arrayelems = arrayElems
6 changes: 3 additions & 3 deletions copilot-core/tests/Test/Copilot/Core/Type/Array.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import Test.QuickCheck (Gen, Property, arbitrary, forAll,
vectorOf)

-- Internal imports: library modules being tested
import Copilot.Core.Type.Array (Array, array, arrayelems)
import Copilot.Core.Type.Array (Array, array, arrayElems)

-- | All unit tests for copilot-core:Copilot.Core.Array.
tests :: Test.Framework.Test
Expand All @@ -30,13 +30,13 @@ tests =
-- * Individual tests

-- | Test that building an array from a list and extracting the elements with
-- the function 'arrayelems' will result in the same list.
-- the function 'arrayElems' will result in the same list.
testArrayElemsLeft :: forall n . KnownNat n => Proxy n -> Property
testArrayElemsLeft len =
forAll xsInt64 $ \ls ->
let array' :: Array n Int64
array' = array ls
in arrayelems array' == ls
in arrayElems array' == ls

where

Expand Down
3 changes: 3 additions & 0 deletions copilot-interpreter/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-05
* Replace uses of deprecated functions. (#457)

2023-09-07
* Version bump (3.16.1). (#455)

Expand Down
4 changes: 2 additions & 2 deletions copilot-interpreter/src/Copilot/Interpret/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ module Copilot.Interpret.Eval

import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..),
Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),
Trigger (..), Type (..), UExpr (..), arrayelems,
Trigger (..), Type (..), UExpr (..), arrayElems,
specObservers, specStreams, specTriggers)
import Copilot.Interpret.Error (badUsage)

Expand Down Expand Up @@ -242,7 +242,7 @@ evalOp2 op = case op of
BwXor _ -> (xor)
BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )
BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )
Index _ -> \xs n -> (arrayelems xs) !! (fromIntegral n)
Index _ -> \xs n -> (arrayElems xs) !! (fromIntegral n)

-- | Apply a function to two numbers, so long as the second one is
-- not zero.
Expand Down
3 changes: 3 additions & 0 deletions copilot-prettyprinter/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-05
* Replace uses of deprecated functions. (#457)

2023-09-07
* Version bump (3.16.1). (#455)

Expand Down
2 changes: 1 addition & 1 deletion copilot-prettyprinter/src/Copilot/PrettyPrint.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ ppOp1 op = case op of
Floor _ -> ppPrefix "floor"
BwNot _ -> ppPrefix "~"
Cast _ _ -> ppPrefix "(cast)"
GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f)
GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorName f)
GetField _ _ _ -> impossible "ppOp1" "Copilot.PrettyPrint"

-- | Pretty-print a binary operation.
Expand Down
3 changes: 2 additions & 1 deletion copilot-theorem/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
2023-11-03
2023-11-05
* Relax version constraint on what4. (#461)
* Replace uses of deprecated functions. (#457)

2023-09-07
* Version bump (3.16.1). (#455)
Expand Down
2 changes: 1 addition & 1 deletion copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,7 @@ translateConstExpr sym tp a = case tp of
CT.Float -> XFloat <$> WFP.iFloatLitSingle sym a
CT.Double -> XDouble <$> WFP.iFloatLitDouble sym a
CT.Array tp -> do
elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a)
elts <- traverse (translateConstExpr sym tp) (CT.arrayElems a)
Some n <- return $ mkNatRepr (genericLength elts)
case isZeroOrGT1 n of
Left Refl -> return XEmptyArray
Expand Down
3 changes: 3 additions & 0 deletions copilot/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-05
* Replace uses of deprecated functions. (#457)

2023-11-03
* Fix typo in README. (#459)

Expand Down
4 changes: 2 additions & 2 deletions copilot/examples/Structs.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ data Volts = Volts

-- | `Struct` instance for `Volts`.
instance Struct Volts where
typename _ = "volts"
typeName _ = "volts"
toValues volts = [ Value Word16 (numVolts volts)
, Value Bool (flag volts)
]
Expand All @@ -36,7 +36,7 @@ data Battery = Battery

-- | `Battery` instance for `Struct`.
instance Struct Battery where
typename _ = "battery"
typeName _ = "battery"
toValues battery = [ Value typeOf (temp battery)
, Value typeOf (volts battery)
, Value typeOf (other battery)
Expand Down
Loading

0 comments on commit e0a86dd

Please sign in to comment.