copilot-language 3.20 → 4.0

raw patch · 5 files changed

+164/−54 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 +4/−0
• copilot-language.cabal +5/−4
• src/Copilot/Language/Operators/Array.hs +72/−12
• src/Copilot/Language/Operators/Projection.hs +38/−0
• src/Copilot/Language/Operators/Struct.hs +45/−38

@@ -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)

@@ -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

@@ -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))

@@ -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

@@ -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))