copilot-language 3.19.1 → 3.20

raw patch · 5 files changed

+85/−18 lines, 5 filesdep ~copilot-coredep ~copilot-interpreterdep ~copilot-theoremPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core, copilot-interpreter, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot-language.cabal +9/−9
• src/Copilot/Language.hs +1/−1
• src/Copilot/Language/Operators/Struct.hs +69/−2
• src/Copilot/Language/Spec.hs +1/−6

@@ -1,3 +1,8 @@+2024-07-07+        * Version bump (3.20). (#522)+        * Remove deprecated function Copilot.Language.Spec.forall. (#518)+        * Add support for struct field updates. (#520)+ 2024-05-07         * Version bump (3.19.1). (#512) 

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-language-version:             3.19.1+version:             3.20 synopsis:            A Haskell-embedded DSL for monitoring hard real-time                      distributed systems. description:@@ -35,16 +35,16 @@ library   default-language: Haskell2010   hs-source-dirs: src-  build-depends: base                  >= 4.9    && < 5+  build-depends: base                  >= 4.9  && < 5 -               , array                 >= 0.5    && < 0.6-               , containers            >= 0.4    && < 0.7-               , data-reify            >= 0.6    && < 0.7-               , mtl                   >= 2.0    && < 3+               , array                 >= 0.5  && < 0.6+               , containers            >= 0.4  && < 0.7+               , data-reify            >= 0.6  && < 0.7+               , mtl                   >= 2.0  && < 3 -               , copilot-core          >= 3.19.1 && < 3.20-               , copilot-interpreter   >= 3.19.1 && < 3.20-               , copilot-theorem       >= 3.19.1 && < 3.20+               , copilot-core          >= 3.20 && < 3.21+               , copilot-interpreter   >= 3.20 && < 3.21+               , copilot-theorem       >= 3.20 && < 3.21    exposed-modules: Copilot.Language                  , Copilot.Language.Operators.BitWise

@@ -38,7 +38,7 @@   , prop   , theorem   , forAll-  , forall, exists+  , exists   ) where  import Data.Int hiding (Int)

@@ -1,8 +1,35 @@ {-# LANGUAGE Safe #-}  -- | Combinators to deal with streams carrying structs.+--+-- We support two kinds of operations on structs: reading the fields of structs+-- and modifying the fields of structs.+--+-- To obtain the values of field @x@ of a struct @s@, you can just write:+--+-- @+-- expr = s # x+-- @+--+-- If you want to update it, use instead a double hash to refer to the field.+-- You can either update the field:+--+-- @+-- expr = s ## x =: 75+-- @+--+-- To update it by applying a function to it, for example, the function that+-- updates a stream by one unit, just do:+--+-- @+-- expr = s ## x =$ (+1)+-- @ module Copilot.Language.Operators.Struct   ( (#)+  , Projection+  , (##)+  , (=:)+  , (=$)   ) where  import Copilot.Core.Type@@ -18,6 +45,46 @@ -- of type @Word8@, and @s@ is a stream of type @Stream T@, then @s # t2@ has -- type @Stream Word8@ and contains the values of the @t2@ field of the structs -- in @s@ at any point in time.-(#) :: (KnownSymbol s, Typed t, Typed a, Struct a)-      => Stream a -> (a -> Field s t) -> Stream t+(#) :: (KnownSymbol f, Typed t, Typed s, Struct s)+      => Stream s -> (s -> Field f t) -> Stream t (#) s f = Op1 (GetField typeOf typeOf f) s++-- | Type represented an unapplied struct field accessor and a stream carrying+-- structs.+data Projection s f t = Projection (Stream s) (s -> Field f t)++-- | Pair a stream with a field accessor, without applying it to obtain the+-- value of the field.+--+-- This function is needed to refer to a field accessor when the goal is to+-- update the field value, not just to read it.+(##) :: (KnownSymbol f, Typed t, Typed s, Struct s)+     => Stream s -> (s -> Field f t) -> Projection s f t+(##) = Projection++-- | Create a stream where the field of a struct has been updated with values+-- from another stream.+--+-- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@+-- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and $sT1$+-- is a stream of type @Int32@ then @s ## t2 =: sT1@ has type @Stream T@ and+-- contains structs where the value of @t1@ is that of @sT1@ and the value of+-- @t2@ is the value that the same field had in @s@, at any point in time.+infixl 8 =:+(=:) :: (KnownSymbol f, Typed t, Typed s, Struct s)+     => Projection s f t -> Stream t -> Stream s+(=:) (Projection s f) v = Op2 (UpdateField typeOf typeOf f) s v++-- | Create a stream where the field of a struct has been updated by applying a+-- function to it.+--+-- For example, if a struct of type @T@ has two fields, @t1@ of type @Int32@+-- and @t2@ of type @Word8@, and @s@ is a stream of type @Stream T@, and $f$ is+-- a function from @Stream Int32 -> Stream Int32@ then @s ## t2 =$ f@ has type+-- @Stream T@ and contains structs where the value of @t1@ is that of @f@+-- applied to the original value of @t1@ in @s@, and the value of @t2@ is the+-- value that the same field had in @s@, at any point in time.+infixl 8 =$+(=$) :: (KnownSymbol f, Typed t, Typed s, Struct s)+     => Projection s f t -> (Stream t -> Stream t) -> Stream s+(=$) (Projection s f) op = s ## f =: (op (s # f))

@@ -28,7 +28,7 @@   , prop, properties   , theorem, theorems   , forAll-  , forall, exists+  , exists   , extractProp   , Universal, Existential   ) where@@ -164,11 +164,6 @@ -- | Universal quantification of boolean streams over time. forAll :: Stream Bool -> Prop Universal forAll = Forall--{-# DEPRECATED forall "Use forAll instead." #-}--- | Universal quantification of boolean streams over time.-forall :: Stream Bool -> Prop Universal-forall = forAll  -- | Existential quantification of boolean streams over time. exists :: Stream Bool -> Prop Existential