diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ +2025-01-07 + * Version bump (4.2). (#577) + * Bump upper version constraint on filepath. (#570) + * Update struct examples to use generic method implementations. (#564) + 2024-11-07 * Version bump (4.1). (#561) * Update contribution guidelines. (#476) diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.1 +version: 4.2 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -50,14 +50,14 @@ base >= 4.9 && < 5 , optparse-applicative >= 0.14 && < 0.19 , directory >= 1.3 && < 1.4 - , filepath >= 1.4 && < 1.5 + , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.1 && < 4.2 - , copilot-theorem >= 4.1 && < 4.2 - , copilot-language >= 4.1 && < 4.2 - , copilot-libraries >= 4.1 && < 4.2 - , copilot-c99 >= 4.1 && < 4.2 - , copilot-prettyprinter >= 4.1 && < 4.2 + , copilot-core >= 4.2 && < 4.3 + , copilot-theorem >= 4.2 && < 4.3 + , copilot-language >= 4.2 && < 4.3 + , copilot-libraries >= 4.2 && < 4.3 + , copilot-c99 >= 4.2 && < 4.3 + , copilot-prettyprinter >= 4.2 && < 4.3 exposed-modules: Language.Copilot, Language.Copilot.Main diff --git a/examples/Structs.hs b/examples/Structs.hs --- a/examples/Structs.hs +++ b/examples/Structs.hs @@ -1,28 +1,29 @@ -- | An example showing how specifications involving structs (in particular, -- nested structs) are compiled to C using copilot-c99. -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} module Main where import qualified Prelude as P import Control.Monad (void, forM_) +import GHC.Generics (Generic) import Language.Copilot import Copilot.Compile.C99 -- | Definition for `Volts`. data Volts = Volts - { numVolts :: Field "numVolts" Word16 - , flag :: Field "flag" Bool - } + { numVolts :: Field "numVolts" Word16 + , flag :: Field "flag" Bool + } + deriving Generic -- | `Struct` instance for `Volts`. instance Struct Volts where - typeName _ = "volts" - toValues volts = [ Value Word16 (numVolts volts) - , Value Bool (flag volts) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- Note that we do not implement `updateField` here. `updateField` is only -- needed to make updates to structs work in the Copilot interpreter, and we -- do not use the interpreter in this example. (See @@ -31,29 +32,25 @@ -- | `Volts` instance for `Typed`. instance Typed Volts where - typeOf = Struct (Volts (Field 0) (Field False)) + typeOf = typeOfDefault data Battery = Battery - { temp :: Field "temp" Word16 - , volts :: Field "volts" (Array 10 Volts) - , other :: Field "other" (Array 10 (Array 5 Word32)) - } + { temp :: Field "temp" Word16 + , volts :: Field "volts" (Array 10 Volts) + , other :: Field "other" (Array 10 (Array 5 Word32)) + } + deriving Generic -- | `Battery` instance for `Struct`. instance Struct Battery where - typeName _ = "battery" - toValues battery = [ Value typeOf (temp battery) - , Value typeOf (volts battery) - , Value typeOf (other battery) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- Note that we do not implement `updateField` here for the same reasons as in -- the `Struct Volts` instance above. --- | `Battery` instance for `Typed`. Note that `undefined` is used as an --- argument to `Field`. This argument is never used, so `undefined` will never --- throw an error. +-- | `Battery` instance for `Typed`. instance Typed Battery where - typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined)) + typeOf = typeOfDefault spec :: Spec spec = do diff --git a/examples/StructsUpdateField.hs b/examples/StructsUpdateField.hs --- a/examples/StructsUpdateField.hs +++ b/examples/StructsUpdateField.hs @@ -3,6 +3,7 @@ -- copilot-c99. {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -13,6 +14,7 @@ import Control.Monad (void, forM_) import Data.Proxy (Proxy(..)) import Data.Type.Equality (TestEquality(..), (:~:)(..)) +import GHC.Generics (Generic) import GHC.TypeLits (sameSymbol) import Language.Copilot @@ -20,20 +22,22 @@ -- | Definition for `Volts`. data Volts = Volts - { numVolts :: Field "numVolts" Word16 - , flag :: Field "flag" Bool - } + { numVolts :: Field "numVolts" Word16 + , flag :: Field "flag" Bool + } + deriving Generic -- | `Struct` instance for `Volts`. instance Struct Volts where - typeName _ = "volts" - toValues volts = [ Value Word16 (numVolts volts) - , Value Bool (flag volts) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- In order to run struct updates (as used in the "equalityStructUpdate" -- trigger below) in the Copilot interpreter, we must implement the -- `updateField` method. To do so, we must check to see if the supplied -- `Value` has a `Field` with the same name and type as a field in `Volts`. + -- (Alternatively, we could define this as @updateField = updateFieldDefault@, + -- but we demonstrate how to manually implement it below for educational + -- purposes.) updateField volts (Value fieldTy (field :: Field fieldName a)) -- For each field in `Volts`, we must: -- @@ -67,23 +71,23 @@ -- | `Volts` instance for `Typed`. instance Typed Volts where - typeOf = Struct (Volts (Field 0) (Field False)) + typeOf = typeOfDefault data Battery = Battery - { temp :: Field "temp" Word16 - , volts :: Field "volts" (Array 10 Volts) - , other :: Field "other" (Array 10 (Array 5 Word32)) - } + { temp :: Field "temp" Word16 + , volts :: Field "volts" (Array 10 Volts) + , other :: Field "other" (Array 10 (Array 5 Word32)) + } + deriving Generic -- | `Battery` instance for `Struct`. instance Struct Battery where - typeName _ = "battery" - toValues battery = [ Value typeOf (temp battery) - , Value typeOf (volts battery) - , Value typeOf (other battery) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- We implement `updateField` similarly to how we implement it in the - -- `Struct Volts` instance above. + -- `Struct Volts` instance above. (Alternatively, we could define this as + -- @updateField = updateFieldDefault@, but we demonstrate how to manually + -- implement it below for educational purposes.) updateField battery (Value fieldTy (field :: Field fieldName a)) | Just Refl <- sameSymbol (Proxy @fieldName) (Proxy @"temp") , Just Refl <- testEquality fieldTy Word16 @@ -103,11 +107,9 @@ | otherwise = error $ "Unexpected field: " P.++ show field --- | `Battery` instance for `Typed`. Note that `undefined` is used as an --- argument to `Field`. This argument is never used, so `undefined` will never --- throw an error. +-- | `Battery` instance for `Typed`. instance Typed Battery where - typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined)) + typeOf = typeOfDefault spec :: Spec spec = do diff --git a/examples/what4/Structs.hs b/examples/what4/Structs.hs --- a/examples/what4/Structs.hs +++ b/examples/what4/Structs.hs @@ -2,28 +2,29 @@ -- structs and arrays. Particular focus is on nested structs. -- For general usage of structs, refer to the general structs example. -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} module Main where import qualified Prelude as P import Control.Monad (void, forM_) +import GHC.Generics (Generic) import Language.Copilot import Copilot.Theorem.What4 -- | Definition for `Volts`. data Volts = Volts - { numVolts :: Field "numVolts" Word16 - , flag :: Field "flag" Bool - } + { numVolts :: Field "numVolts" Word16 + , flag :: Field "flag" Bool + } + deriving Generic -- | `Struct` instance for `Volts`. instance Struct Volts where - typeName _ = "volts" - toValues volts = [ Value Word16 (numVolts volts) - , Value Bool (flag volts) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- Note that we do not implement `updateField` here. `updateField` is only -- needed to make updates to structs work in the Copilot interpreter, and we -- do not use the interpreter in this example. (See @@ -32,29 +33,25 @@ -- | `Volts` instance for `Typed`. instance Typed Volts where - typeOf = Struct (Volts (Field 0) (Field False)) + typeOf = typeOfDefault data Battery = Battery - { temp :: Field "temp" Word16 - , volts :: Field "volts" (Array 10 Volts) - , other :: Field "other" (Array 10 (Array 5 Word32)) - } + { temp :: Field "temp" Word16 + , volts :: Field "volts" (Array 10 Volts) + , other :: Field "other" (Array 10 (Array 5 Word32)) + } + deriving Generic -- | `Battery` instance for `Struct`. instance Struct Battery where - typeName _ = "battery" - toValues battery = [ Value typeOf (temp battery) - , Value typeOf (volts battery) - , Value typeOf (other battery) - ] + typeName = typeNameDefault + toValues = toValuesDefault -- Note that we do not implement `updateField` here for the same reasons as in -- the `Struct Volts` instance above. --- | `Battery` instance for `Typed`. Note that `undefined` is used as an --- argument to `Field`. This argument is never used, so `undefined` will never --- throw an error. +-- | `Battery` instance for `Typed`. instance Typed Battery where - typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined)) + typeOf = typeOfDefault spec :: Spec spec = do