copilot-libraries 4.7 → 4.7.1

raw patch · 4 files changed

+78/−3 lines, 4 filesdep ~copilot-languagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-language

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• copilot-libraries.cabal +5/−3
• src/Copilot/Library/Analysis.hs +23/−0
• src/Copilot/Library/StateMachines.hs +45/−0

@@ -1,3 +1,8 @@+2026-05-07+        * Version bump (4.7.1). (#730)+        * Add stream analysis module. (#726)+        * Add state machine module. (#728)+ 2026-03-07         * Version bump (4.7). (#714) 

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                copilot-libraries-version:             4.7+version:             4.7.1 synopsis:            Libraries for the Copilot language. description:   Libraries for the Copilot language.@@ -41,13 +41,15 @@                , containers       >= 0.4 && < 0.9                , mtl              >= 2.0 && < 2.4                , parsec           >= 2.0 && < 3.2-               , copilot-language >= 4.7 && < 4.8+               , copilot-language >= 4.7.1 && < 4.8    exposed-modules:-      Copilot.Library.Libraries+      Copilot.Library.Analysis+    , Copilot.Library.Libraries     , Copilot.Library.Clocks     , Copilot.Library.LTL     , Copilot.Library.PTLTL+    , Copilot.Library.StateMachines     , Copilot.Library.Statistics     , Copilot.Library.RegExp     , Copilot.Library.Utils

@@ -0,0 +1,23 @@+-- | Formally analyze streams.+module Copilot.Library.Analysis+    ( triviallyTrue+    , triviallyFalse+    )+  where++-- External imports.+import Prelude hiding (not)++-- Internal imports.+import Copilot.Language      (Stream, forAll, not)+import Copilot.Language.Spec (Prop, Universal)++-- | Property that captures whether a stream is trivially true, meaning that+-- there is no way to make it false.+triviallyTrue :: Stream Bool -> Prop Universal+triviallyTrue = forAll++-- | Property that captures whether a stream is trivially false, meaning that+-- there is no way to make it true.+triviallyFalse :: Stream Bool -> Prop Universal+triviallyFalse = triviallyTrue . not

@@ -0,0 +1,45 @@+{-# LANGUAGE ScopedTypeVariables #-}+-- | Simulate state machines using streams.+module Copilot.Library.StateMachines where++import Copilot.Language (Stream, Typed, constant, ifThenElse, (&&), (++), (==))+import Prelude          hiding ((&&), (++), (==))++-- | A definition of a state machine where some elements are defined+-- as streams.+--+-- A state machine is defined by an initial state, a final state, a no+-- transition stream (true when tere is no input coming in), a list of+-- transitions, and a bad state.+type StateMachine a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)++-- | Produce a stream that, at any given time, contains the current state of+-- the state machine.+stateMachine :: forall a . (Eq a, Typed a) => StateMachine a -> Stream a+stateMachine (initial, final, noInputData, transitions, bad) = state+  where+    state         = ifThenElses transitions+    previousState = [initial] ++ state++    ifThenElses :: [(a, Stream Bool, a)] -> Stream a+    ifThenElses [] =+      ifThenElse (previousState == constant final && noInputData)+        (constant final)+        (constant bad)++    ifThenElses ((s1, i, s2):ss) =+      ifThenElse+        (previousState == constant s1 && i)+        (constant s2)+        (ifThenElses ss)++-- | Produce a stream that, at any given time, contains the current state of+-- the state machine as the numeric representation of an enum.+stateMachineEnum :: (Eq b, Typed b, Num b, Enum a)+                 => StateMachine a+                 -> Stream b+stateMachineEnum (initial, final, noInputData, transitions, bad) =+    stateMachine (fe initial, fe final, noInputData, transitionsE, fe bad)+  where+    transitionsE = map (\(s1, t, s2) -> (fe s1, t, fe s2)) transitions+    fe           = fromIntegral . fromEnum