copilot-core 4.2 → 4.3

raw patch · 4 files changed

+30/−3 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG +6/−0
• copilot-core.cabal +1/−1
• src/Copilot/Core/Spec.hs +21/−2
• src/Copilot/Core/Type.hs +2/−0

@@ -1,3 +1,9 @@+2025-03-07+        * Version bump (4.3). (#604)+        * Fix typo in documentation. (#587)+        * Add a Show instance for Type. (#589)+        * Add a Prop type to capture how a property is quantified. (#254)+ 2025-01-07         * Version bump (4.2). (#577)         * Deprecate fields of Copilot.Core.Expr.UExpr. (#565)

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-core-version:             4.2+version:             4.3 synopsis:            An intermediate representation for Copilot. description:   Intermediate representation for Copilot.

@@ -13,13 +13,15 @@ -- -- In order to be executed, high-level Copilot Language Spec must be turned -- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core--- representations for Specs and the main types of element in a spec..+-- representations for Specs and the main types of element in a spec. module Copilot.Core.Spec     ( Stream (..)     , Observer (..)     , Trigger (..)     , Spec (..)     , Property (..)+    , Prop (..)+    , extractProp     )   where @@ -62,8 +64,25 @@ -- universally quantified over time. data Property = Property   { propertyName :: Name-  , propertyExpr :: Expr Bool+  , propertyProp :: Prop   }++-- | A proposition, representing a boolean stream that is existentially or+-- universally quantified over time.+data Prop+  = Forall (Expr Bool)+  | Exists (Expr Bool)++-- | Extract the underlying stream from a quantified proposition.+--+-- Think carefully before using this function, as this function will remove the+-- quantifier from a proposition. Universally quantified streams usually require+-- separate treatment from existentially quantified ones, so carelessly using+-- this function to remove quantifiers can result in hard-to-spot soundness+-- bugs.+extractProp :: Prop -> Expr Bool+extractProp (Forall e) = e+extractProp (Exists e) = e  -- | A Copilot specification is a list of streams, together with monitors on -- these streams implemented as observers, triggers or properties.

@@ -5,6 +5,7 @@ {-# LANGUAGE GADTs                     #-} {-# LANGUAGE KindSignatures            #-} {-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE StandaloneDeriving        #-} {-# LANGUAGE Trustworthy               #-} {-# LANGUAGE TypeApplications          #-} {-# LANGUAGE TypeOperators             #-}@@ -154,6 +155,7 @@                          , Typed t                          ) => Type t -> Type (Array n t)   Struct :: (Typed a, Struct a) => a -> Type a+deriving instance Show (Type a)  -- | Return the length of an array from its type typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int