diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +2024-09-07 + * Version bump (4.0). (#532) + * Add support for array updates. (#36) + 2024-07-07 * Version bump (3.20). (#522) * Remove deprecated function Copilot.Language.Spec.forall. (#518) diff --git a/copilot-language.cabal b/copilot-language.cabal --- a/copilot-language.cabal +++ b/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 3.20 +version: 4.0 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 3.20 && < 3.21 - , copilot-interpreter >= 3.20 && < 3.21 - , copilot-theorem >= 3.20 && < 3.21 + , copilot-core >= 4.0 && < 4.1 + , copilot-interpreter >= 4.0 && < 4.1 + , copilot-theorem >= 4.0 && < 4.1 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise @@ -61,6 +61,7 @@ , Copilot.Language.Operators.Ord , Copilot.Language.Operators.Temporal , Copilot.Language.Operators.Array + , Copilot.Language.Operators.Projection , Copilot.Language.Operators.Struct , Copilot.Language.Prelude , Copilot.Language.Reify diff --git a/src/Copilot/Language/Operators/Array.hs b/src/Copilot/Language/Operators/Array.hs --- a/src/Copilot/Language/Operators/Array.hs +++ b/src/Copilot/Language/Operators/Array.hs @@ -1,29 +1,89 @@ -{-# LANGUAGE Safe #-} - -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE TypeFamilies #-} +-- The following warning is disabled due to a necessary instance of Projectable +-- defined in this module. +{-# OPTIONS_GHC -fno-warn-orphans #-} -- | Combinators to deal with streams carrying arrays. module Copilot.Language.Operators.Array ( (.!!) + , (!) + , (!!) + , (=:) + , (=$) ) where -import Copilot.Core ( Typed - , Op2 (Index) - , typeOf - , Array - ) -import Copilot.Language.Stream (Stream (..)) +import Copilot.Core (Array, Op2 (Index), + Op3 (UpdateArray), Typed, typeOf) +import Copilot.Language.Operators.Projection (Projectable(..)) +import Copilot.Language.Stream (Stream (..)) -import Data.Word (Word32) -import GHC.TypeLits (KnownNat) +import Data.Word (Word32) +import GHC.TypeLits (KnownNat) +import Prelude hiding ((!!)) -- | Create a stream that carries an element of an array in another stream. -- -- This function implements a projection of the element of an array at a given -- position, over time. For example, if @s@ is a stream of type @Stream (Array +-- '5 Word8)@, then @s ! 3@ has type @Stream Word8@ and contains the 3rd +-- element (starting from zero) of the arrays in @s@ at any point in time. +(!) :: (KnownNat n, Typed t) + => Stream (Array n t) -> Stream Word32 -> Stream t +arr ! n = Op2 (Index typeOf) arr n + +-- | Create a stream that carries an element of an array in another stream. +-- +-- This function implements a projection of the element of an array at a given +-- position, over time. For example, if @s@ is a stream of type @Stream (Array -- '5 Word8)@, then @s .!! 3@ has type @Stream Word8@ and contains the 3rd -- element (starting from zero) of the arrays in @s@ at any point in time. +{-# DEPRECATED (.!!) "This function is deprecated in Copilot 4. Use (!)." #-} (.!!) :: ( KnownNat n , Typed t ) => Stream (Array n t) -> Stream Word32 -> Stream t -arr .!! n = Op2 (Index typeOf) arr n +(.!!) = (!) + +-- | Pair a stream with an element accessor, without applying it to obtain the +-- value of the element. +-- +-- This function is needed to refer to an element accessor when the goal is to +-- update the element value, not just to read it. +(!!) :: Stream (Array n t) + -> Stream Word32 + -> Projection (Array n t) (Stream Word32) t +(!!) = ProjectionA + +-- | Update a stream of arrays. + +-- This is an orphan instance; we suppress the warning that GHC would +-- normally produce with a GHC option at the top. +instance (KnownNat n, Typed t) => Projectable (Array n t) (Stream Word32) t where + + -- | A projection of an element of a stream of arrays. + data Projection (Array n t) (Stream Word32) t = + ProjectionA (Stream (Array n t)) (Stream Word32) + + -- | Create a stream where an element of an array has been updated with + -- values from another stream. + -- + -- For example, if an array has two elements of type @Int32@, and @s@ is a + -- stream of such array type (@Stream (Array 2 Int32)@), and $v0$ is a stream + -- of type @Int32@, then @s !! 0 =: v0@ has type @Stream (Array 2 Int32)@ and + -- contains arrays where the value of the first element of each array is that + -- of @v0@ at each point in time, and the value of the second element in the + -- array is the same it had in @s@. + (=:) (ProjectionA s ix) v = Op3 (UpdateArray typeOf) s ix v + + -- | Create a stream where an element of an array has been updated by + -- applying a stream function to it. + -- + -- For example, if an array has two elements of type @Int32@, and @s@ is a + -- stream of such array type (@Stream (Array 2 Int32)@), and $f$ is function + -- of type @Stream Int32 -> Stream Int32@, then @s !! 0 =$ f@ has type + -- @Stream (Array 2 Int32)@ and contains arrays where the value of the first + -- element of each array is that of @f (s ! 0)@ at each point in time, and + -- the value of the second element in the array is the same it had in @s@. + (=$) (ProjectionA s ix) op = Op3 (UpdateArray typeOf) s ix (op (s ! ix)) diff --git a/src/Copilot/Language/Operators/Projection.hs b/src/Copilot/Language/Operators/Projection.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Language/Operators/Projection.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilies #-} +-- | Interface to access portions of a larger data structure. +-- +-- Default operations to access elements from structs and arrays (e.g., a field +-- of a struct, an element of an array) allow obtaining the values of those +-- elements, but not modifying. +-- +-- This module defines a common interface to manipulate portions of a larger +-- data structure. We define the interface in a generic way, using a type +-- class with two operations: one to set the value of the sub-element, and +-- one to update the value of such element applying a stream function. +module Copilot.Language.Operators.Projection + ( Projectable (..) ) + where + +import Copilot.Language.Stream (Stream) + +infixl 8 =: +infixl 8 =$ + +-- | Common interface to manipulate portions of a larger data structure. +-- +-- A projectable d s t means that it is possible to manipulate a sub-element s +-- of type t carried in a stream of type d.. +class Projectable d s t | d s -> t where + + -- | Unapplied projection or element access on a type. + data Projection d s t + + -- | Modify the value of a sub-element of a type in a stream of elements + -- of that type. + (=:) :: Projection d s t -> Stream t -> Stream d + + -- | Update the value of a sub-element of a type in a stream of elements of + -- that type, by applying a function on streams. + (=$) :: Projection d s t -> (Stream t -> Stream t) -> Stream d diff --git a/src/Copilot/Language/Operators/Struct.hs b/src/Copilot/Language/Operators/Struct.hs --- a/src/Copilot/Language/Operators/Struct.hs +++ b/src/Copilot/Language/Operators/Struct.hs @@ -1,4 +1,10 @@ -{-# LANGUAGE Safe #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE TypeFamilies #-} +-- The following warning is disabled due to a necessary instance of Projectable +-- defined in this module. +{-# OPTIONS_GHC -fno-warn-orphans #-} -- | Combinators to deal with streams carrying structs. -- @@ -25,18 +31,17 @@ -- expr = s ## x =$ (+1) -- @ module Copilot.Language.Operators.Struct - ( (#) - , Projection + ( Projectable(..) + , (#) , (##) - , (=:) - , (=$) ) where import Copilot.Core.Type import Copilot.Core.Operators -import Copilot.Language.Stream (Stream (..)) +import Copilot.Language.Operators.Projection +import Copilot.Language.Stream (Stream (..)) -import GHC.TypeLits (KnownSymbol) +import GHC.TypeLits (KnownSymbol) -- | Create a stream that carries a field of a struct in another stream. -- @@ -49,42 +54,44 @@ => 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 + => Stream s -> (s -> Field f t) -> Projection s (s -> Field f t) t +(##) = ProjectionS --- | 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 +-- | Update a stream of structs. --- | 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)) +-- This is an orphan instance; we suppress the warning that GHC would +-- normally produce with a GHC option at the top. +instance (KnownSymbol f, Typed s, Typed t, Struct s) + => Projectable s (s -> Field f t) t + where + + -- | A projection of a field of a stream of structs. + data Projection s (s -> Field f t) t = ProjectionS (Stream s) (s -> Field f t) + + -- | 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. + (=:) (ProjectionS 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. + (=$) (ProjectionS s f) op = Op2 (UpdateField typeOf typeOf f) s (op (s # f))