diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 846861da..12382d90 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -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) diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs index b9c3feb8..23b9de25 100644 --- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs +++ b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs @@ -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 ) @@ -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 @@ -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 = @@ -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 @@ -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 diff --git a/copilot-c99/src/Copilot/Compile/C99/Expr.hs b/copilot-c99/src/Copilot/Compile/C99/Expr.hs index faa522b8..1c810899 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Expr.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Expr.hs @@ -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 @@ -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. @@ -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. @@ -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 diff --git a/copilot-c99/src/Copilot/Compile/C99/Type.hs b/copilot-c99/src/Copilot/Compile/C99/Type.hs index f94dbac6..78777617 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Type.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Type.hs @@ -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 @@ -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. -- diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs index 2c98bb85..dfca1780 100644 --- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs +++ b/copilot-c99/tests/Test/Copilot/Compile/C99.hs @@ -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]) @@ -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." @@ -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." @@ -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 diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 492963d4..cf836f04 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2023-11-05 + * Compliance with style guide. (#457) + 2023-09-07 * Version bump (3.16.1). (#455) diff --git a/copilot-core/src/Copilot/Core/Type.hs b/copilot-core/src/Copilot/Core/Type.hs index 9a390806..3da6917d 100644 --- a/copilot-core/src/Copilot/Core/Type.hs +++ b/copilot-core/src/Copilot/Core/Type.hs @@ -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 @@ -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] @@ -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 ++ ">" @@ -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 diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs index 5f0995b2..2bca9bc1 100644 --- a/copilot-core/src/Copilot/Core/Type/Array.hs +++ b/copilot-core/src/Copilot/Core/Type/Array.hs @@ -13,6 +13,7 @@ module Copilot.Core.Type.Array ( Array , array + , arrayElems , arrayelems ) where @@ -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 diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs index 4a0f0f52..9a98d49c 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs @@ -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 @@ -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 diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 16411d43..b4bbd09f 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2023-11-05 + * Replace uses of deprecated functions. (#457) + 2023-09-07 * Version bump (3.16.1). (#455) diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs index 19d7e61d..a0083524 100644 --- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs +++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs @@ -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) @@ -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. diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 4bb2d40e..c982374b 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2023-11-05 + * Replace uses of deprecated functions. (#457) + 2023-09-07 * Version bump (3.16.1). (#455) diff --git a/copilot-prettyprinter/src/Copilot/PrettyPrint.hs b/copilot-prettyprinter/src/Copilot/PrettyPrint.hs index 10100a88..88734682 100644 --- a/copilot-prettyprinter/src/Copilot/PrettyPrint.hs +++ b/copilot-prettyprinter/src/Copilot/PrettyPrint.hs @@ -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. diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 867ce149..be9e693f 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -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) diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs index 12803375..f55e3884 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs @@ -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 diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 74185c53..b3764b01 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2023-11-05 + * Replace uses of deprecated functions. (#457) + 2023-11-03 * Fix typo in README. (#459) diff --git a/copilot/examples/Structs.hs b/copilot/examples/Structs.hs index f826585a..f3b83b1f 100644 --- a/copilot/examples/Structs.hs +++ b/copilot/examples/Structs.hs @@ -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) ] @@ -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) diff --git a/copilot/examples/what4/Structs.hs b/copilot/examples/what4/Structs.hs index 413bc454..ff44ec25 100644 --- a/copilot/examples/what4/Structs.hs +++ b/copilot/examples/what4/Structs.hs @@ -20,7 +20,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) ] @@ -37,7 +37,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)