copilot 4.1 → 4.2
raw patch · 5 files changed
+75/−74 lines, 5 filesdep ~copilot-c99dep ~copilot-coredep ~copilot-languagePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem, filepath
API changes (from Hackage documentation)
Files
- CHANGELOG +5/−0
- copilot.cabal +8/−8
- examples/Structs.hs +19/−22
- examples/StructsUpdateField.hs +24/−22
- examples/what4/Structs.hs +19/−22
CHANGELOG view
@@ -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)
copilot.cabal view
@@ -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
examples/Structs.hs view
@@ -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
examples/StructsUpdateField.hs view
@@ -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
examples/what4/Structs.hs view
@@ -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