-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Libraries for the Copilot language.
--
-- Libraries for the Copilot language.
--
-- Copilot is a stream (i.e., infinite lists) domain-specific language
-- (DSL) in Haskell that compiles into embedded C. Copilot contains an
-- interpreter, multiple back-end compilers, and other verification
-- tools.
--
-- A tutorial, examples, and other information are available at
-- https://copilot-language.github.io.
@package copilot-libraries
@version 4.2
-- | This library generates new clocks based on a base period and phase.
--
-- Example Usage
--
-- Also see examples/Clock.hs in the Copilot repository.
--
--
-- clk ( period 3 ) ( phase 1 )
--
--
-- is equivalent to a stream of values like:
--
--
-- cycle [False, True, False]
--
--
-- that generates a stream of values
--
--
-- False True False False True False False True False ...
-- 0 1 2 3 4 5 6 7 8
--
--
-- That is true every 3 ticks (the period) starting on the 1st tick (the
-- phase).
module Copilot.Library.Clocks
-- | Generate a clock that counts every n ticks, starting at tick
-- m, by using an array of size n.
clk :: Integral a => Period a -> Phase a -> Stream Bool
-- | This follows the same convention as clk, but uses a counter
-- variable of integral type a rather than an array.
clk1 :: (Integral a, Typed a) => Period a -> Phase a -> Stream Bool
-- | Constructor for a Period. Note that period must be greater than
-- 0.
period :: Integral a => a -> Period a
-- | Constructor for a Phase. Note that phase must be greater than
-- or equal to 0, and must be less than the period.
phase :: Integral a => a -> Phase a
-- | Provides past-time linear-temporal logic (ptLTL operators).
--
-- Interface: See Examples/PTLTLExamples.hs in the
-- Copilot repository.
--
-- You can embed a ptLTL specification within a Copilot specification
-- using the form:
--
--
-- operator stream
--
module Copilot.Library.PTLTL
-- | Is there a time when s2 holds and after which s1
-- continuously holds?
since :: Stream Bool -> Stream Bool -> Stream Bool
-- | Has s always held (up to and including the current state)?
alwaysBeen :: Stream Bool -> Stream Bool
-- | Did s hold at some time in the past (including the current
-- state)?
eventuallyPrev :: Stream Bool -> Stream Bool
-- | Did s hold in the previous period?
previous :: Stream Bool -> Stream Bool
-- | A regular expression library.
--
-- For an example, see
-- https://github.com/Copilot-Language/examplesForACSL/blob/master/example15/main.hs
module Copilot.Library.RegExp
-- | Regular expression matching over an arbitrary stream
copilotRegexp :: (Typed t, SymbolParser t, Eq t) => Stream t -> SourceName -> Stream Bool -> Stream Bool
-- | Regular expression matching over a collection of boolean streams.
--
-- Regular expressions can contain symbols, which are expanded to match
-- specific streams.
--
-- For example, the regular expression:
--
--
-- "<s0>(<s1>)+"
--
--
-- would match if you provide a map (association list) that assigns, to
-- the symbol "s0", a stream that is true at the first sample,
-- and to "s1", a stream that is true at every sample after the
-- first sample.
copilotRegexpB :: SourceName -> [(StreamName, Stream Bool)] -> Stream Bool -> Stream Bool
instance GHC.Show.Show t => GHC.Show.Show (Copilot.Library.RegExp.Sym t)
instance GHC.Classes.Ord t => GHC.Classes.Ord (Copilot.Library.RegExp.Sym t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Copilot.Library.RegExp.Sym t)
instance GHC.Show.Show t => GHC.Show.Show (Copilot.Library.RegExp.NumSym t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Copilot.Library.RegExp.NumSym t)
instance GHC.Show.Show t => GHC.Show.Show (Copilot.Library.RegExp.RegExp t)
instance GHC.Classes.Eq Copilot.Library.RegExp.P
instance Copilot.Library.RegExp.SymbolParser Copilot.Library.RegExp.P
instance Copilot.Library.RegExp.SymbolParser GHC.Types.Bool
instance Copilot.Library.RegExp.SymbolParser GHC.Word.Word8
instance Copilot.Library.RegExp.SymbolParser GHC.Word.Word16
instance Copilot.Library.RegExp.SymbolParser GHC.Word.Word32
instance Copilot.Library.RegExp.SymbolParser GHC.Word.Word64
instance Copilot.Library.RegExp.SymbolParser GHC.Int.Int8
instance Copilot.Library.RegExp.SymbolParser GHC.Int.Int16
instance Copilot.Library.RegExp.SymbolParser GHC.Int.Int32
instance Copilot.Library.RegExp.SymbolParser GHC.Int.Int64
-- | This is a stream for a stack machine.
--
-- The stack is created from a specified depth, a specified start value,
-- and three input streams:
--
--
-- - a pop signal which pops off the stack when true,
-- - a push signal which pushes the value from the push stream onto the
-- stack when true,
-- - a push stream. The resultant stream is the top value of the
-- stack.
--
--
-- In stack the push signal takes priority over the pop signal in
-- the event that both are true in the same tick. This priority is
-- reversed in stack'.
--
-- Here is an example sequence with one stack of each type, both depth 3
-- and starting value 0:
--
--
-- popSignal: pushSignal: pushValue: stack: stack':
-- false true 100 0 0
-- false true 101 100 100
-- true true 102 101 101
-- true false 103 100 102
-- true false 104 0 101
-- true false 105 0 100
-- true false 106 0 0
--
--
-- Note the difference at the 4th tick after popSignal and
-- pushSignal were both true. Note also that one cannot pop the
-- start value off the stack - that is, the stack is never empty.
module Copilot.Library.Stacks
-- | Stack stream in which the pop signal has precedence over the push
-- signal in case both are true in the same tick
stack :: (Integral a, Typed b) => a -> b -> Stream Bool -> Stream Bool -> Stream b -> Stream b
-- | Stack stream in which the push signal has precedence over the pop
-- signal in case both are true in the same tick
stack' :: (Integral a, Typed b) => a -> b -> Stream Bool -> Stream Bool -> Stream b -> Stream b
-- | Utility bounded-list functions (e.g., folds, scans, etc.)
module Copilot.Library.Utils
-- | Given a stream and a number, produce a finite list of streams dropping
-- an increasing number of elements of the given stream, up to that
-- number. For example, for a given stream s, the expression
-- take 2 s is equal to [ drop 0 s, drop 1 s].
take :: (Integral a, Typed b) => a -> Stream b -> [Stream b]
-- | Given a stream, produce an infinite list of streams dropping an
-- increasing number of elements of the given stream. For example, for a
-- given stream s, the expression tails s is equal to
-- [ drop 0 s, drop 1 s, drop 2 s, ...].
tails :: Typed a => Stream a -> [Stream a]
-- | Cycle a list to form an infinite stream.
cycle :: Typed a => [a] -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
nfoldl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldl in that it does not require
-- an initial accumulator and it assumes the argument number n
-- is positive.
nfoldl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
nfoldr :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> Stream b
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldr in that it does not require
-- an initial accumulator and it assumes the argument number n
-- is positive.
nfoldr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldl in that it returns the
-- intermediate results as well.
nscanl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> [Stream a]
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldr in that it returns the
-- intermediate results as well.
nscanr :: Typed a => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> [Stream b]
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function assumes the number of elements to scan is positive, and
-- it also returns the intermediate results.
nscanl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a]
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function assumes the number of elements to scan is positive, and
-- it also returns the intermediate results.
nscanr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a]
-- | Case-like function: The index of the first predicate that is true in
-- the predicate list selects the stream result. If no predicate is true,
-- the last element is chosen (default element)
case' :: Typed a => [Stream Bool] -> [Stream a] -> Stream a
-- | Index.
--
-- WARNING: Very expensive! Consider using this only for very short
-- lists.
-- | Deprecated: This function is deprecated in Copilot 4. Use
-- (!!!).
(!!) :: (Typed a, Eq b, Num b, Typed b) => [Stream a] -> Stream b -> Stream a
-- | Index.
--
-- WARNING: Very expensive! Consider using this only for very short
-- lists.
(!!!) :: (Typed a, Eq b, Num b, Typed b) => [Stream a] -> Stream b -> Stream a
-- | Basic bounded statistics. In the following, a bound n is
-- given stating the number of periods over which to compute the
-- statistic (n == 1 computes it only over the current period).
module Copilot.Library.Statistics
-- | Maximum value.
max :: (Typed a, Ord a) => Int -> Stream a -> Stream a
-- | Minimum value.
min :: (Typed a, Ord a) => Int -> Stream a -> Stream a
-- | Summation.
sum :: (Typed a, Num a, Eq a) => Int -> Stream a -> Stream a
-- | Mean value. n must not overflow for word size a for
-- streams over which computation is peformed.
mean :: (Typed a, Eq a, Fractional a) => Int -> Stream a -> Stream a
-- | Mean value over the current set of streams passed in.
meanNow :: (Typed a, Integral a) => [Stream a] -> Stream a
-- | Metric Temporal Logic (MTL) over a discrete time domain consisting of
-- sampled time values.
--
-- The operators in this module receive two additional arguments: a clock
-- stream clk, indicating the current time, and a distance
-- between samples dist. For the purposes of explaining the MTL
-- aspects, we ignore those arguments. If you are using streams for which
-- you can treat time as a discrete increasing number, you can safely
-- assume that the clock is a counter (i.e., [0, 1, 2,...],
-- which can be defined by the stream counter = [0] ++ counter)
-- and the distance between samples is 1.
module Copilot.Library.MTL
-- | Eventually true in the future, within the time bounds specified.
--
-- eventually l u clk dist s is true at time t if and
-- only if s is true at some time t', where (t + l)
-- <= t' <= (t + u).
eventually :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-- | True at some point in the past within the time bounds specified.
--
-- eventuallyPrev l u clk dist s is true at time t if
-- and only if s is true at some time t', where (t
-- - u) <= t' <= (t - l).
eventuallyPrev :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-- | Always true in the future, within the time bounds specified.
--
-- always l u clk dist s is true at time t iff
-- s is true at all times t' where (t + l) <= t'
-- <= (t + u).
always :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-- | Always true in the past, within the time bounds specified.
--
-- alwaysBeen l u clk dist s is true at time t iff
-- s is true at all times t' where (t - u) <= t'
-- <= (t - l).
alwaysBeen :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
-- | True until another stream is true, within the time bounds specified.
--
-- until l u clk dist s0 s1 is true at time t iff there
-- exists a d, with l <= d <= u, such that
-- s1 is true at time (t + d), and for all times
-- t' with t <= t' < t + d, s0 is true
-- at those times.
until :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | True if a stream is true until another one releases it.
--
-- release l u clk dist s0 s1 is true at time t iff for
-- all d with l <= d <= u where there is a sample
-- at time (t + d), s1 is true at time (t +
-- d), or s0 has a true sample at some time t'
-- with t <= t' < t + d.
release :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | True since another stream became true, within the time bounds
-- specified.
--
-- since l u clk dist s0 s1 is true at time t iff there
-- exists a d, with l <= d <= u, such that
-- s1 is true at time (t - d), and for all times
-- t' with t - d < t' <= t, s0 is true
-- at those times.
since :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | True if a stream is true until another one releases it.
--
-- Trigger: True at time t iff for all d with l
-- <= d <= u where there is a sample at time (t - d),
-- s1 is true at time (t - d), or s0 has a
-- true sample at some time t' with t - d < t' <=
-- t.
trigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | Matching Until: Same semantics as until, except with both
-- s1 and s0 needing to hold at time (t + d)
-- instead of just s1.
matchingUntil :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | Matching Release: Same semantics as release, except with
-- s1 or s0 needing to hold at time (t + d)
-- instead of just s1.
matchingRelease :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | Matching Since: Same semantics as since, except with both
-- s1 and s0 needing to hold at time (t - d)
-- instead of just s1.
matchingSince :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | Matching Trigger: Same semantics as trigger, except with
-- s1 or s0 needing to hold at time (t - d)
-- instead of just s1.
matchingTrigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
-- | Bounded Linear Temporal Logic (LTL) operators. For a bound n,
-- a property p holds if it holds on the next n
-- transitions (between periods). If n == 0, then the trace
-- includes only the current period. For example,
--
--
-- eventually 3 p
--
--
-- holds if p holds at least once every four periods (3
-- transitions).
--
-- Interface: See Examples/LTLExamples.hs in the
-- Copilot repository.
--
-- You can embed an LTL specification within a Copilot specification
-- using the form:
--
--
-- operator spec
--
--
-- For some properties, stream dependencies may not allow their
-- specification. In particular, you cannot determine the "future" value
-- of an external variable.
--
-- Formulas defined with this module require that predicates have enough
-- history, which is only true if they have an append directly in front
-- of them. This results in a limited ability to nest applications of
-- temporal operators, since simple application of pointwise combinators
-- (e.g., always n1 (p ==> eventually n2 p2)) will hinder
-- Copilot's ability to determine that there is enough of a buffer to
-- carry out the necessary drops to look into the future.
--
-- In general, the Copilot.Library.PTLTL library is probably more
-- useful.
module Copilot.Library.LTL
-- | Property s holds at the next period. For example:
--
--
-- 0 1 2 3 4 5 6 7
-- s => F F F T F F T F ...
-- next s => F F T F F T F ...
--
--
-- Note: s must have sufficient history to drop a value
-- from it.
next :: Stream Bool -> Stream Bool
-- | Property s holds at some period in the next n
-- periods. If n == 0, then s holds in the current
-- period. We require n >= 0. E.g., if p = eventually 2
-- s, then we have the following relationship between the streams
-- generated:
--
--
-- s => F F F T F F F T ...
-- p => F T T T F T T T ...
--
--
-- Note: s must have sufficient history to drop
-- n values from it.
eventually :: Integral a => a -> Stream Bool -> Stream Bool
-- | Property s holds for the next n periods. We require
-- n >= 0. If n == 0, then s holds in the
-- current period, e.g., if p = always 2 s, then we have the
-- following relationship between the streams generated:
--
--
-- 0 1 2 3 4 5 6 7
-- s => T T T F T T T T ...
-- p => T F F F T T ...
--
--
-- Note: s must have sufficient history to drop
-- n values from it.
always :: Integral a => a -> Stream Bool -> Stream Bool
-- | until n s0 s1 means that eventually n s1, and up
-- until at least the period before s1 holds, s0
-- continuously holds.
--
-- Note: Both argument streams must have sufficient history to
-- drop n values from them.
until :: Integral a => a -> Stream Bool -> Stream Bool -> Stream Bool
-- | release n s0 s1 means that either always n s1, or
-- s1 holds up to and including the period at which s0
-- becomes true.
--
-- Note: Both argument streams must have sufficient history to
-- drop n values from them.
release :: Integral a => a -> Stream Bool -> Stream Bool -> Stream Bool
-- | This is an implementation of the Boyer-Moore Majority Vote Algorithm
-- for Copilot, which solves the majority vote problem in linear time and
-- constant memory in two passes. majority implements the first
-- pass, and aMajority the second pass. For details of the
-- Boyer-Moore Majority Vote Algorithm see the following papers:
--
--
--
-- In addition, An Introduction to Copilot and
-- copilot-discussion explain a form of this code in section 4.
--
-- For instance, with four streams passed to majority, and the
-- candidate stream then passed to aMajority:
--
--
-- vote1: vote2: vote3: vote4: majority: aMajority:
-- 0 0 0 0 0 true
-- 1 0 0 0 0 true
-- 1 1 0 0 1 false
-- 1 1 1 0 1 true
-- 1 1 1 1 1 true
--
--
-- For other examples, see examples/Voting.hs in the Copilot
-- repository.
module Copilot.Library.Voting
-- | Majority vote first pass: choosing a candidate.
majority :: (Eq a, Typed a) => [Stream a] -> Stream a
-- | Majority vote second pass: checking that a candidate indeed has more
-- than half the votes.
aMajority :: (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool
-- | This is a convenience module that re-exports a useful subset of
-- modules from copilot-library. Not all modules are exported
-- due to name clashes (e.g., in temporal logics implementations).
module Copilot.Library.Libraries
-- | Given a stream and a number, produce a finite list of streams dropping
-- an increasing number of elements of the given stream, up to that
-- number. For example, for a given stream s, the expression
-- take 2 s is equal to [ drop 0 s, drop 1 s].
take :: (Integral a, Typed b) => a -> Stream b -> [Stream b]
-- | Cycle a list to form an infinite stream.
cycle :: Typed a => [a] -> Stream a
-- | Given a stream, produce an infinite list of streams dropping an
-- increasing number of elements of the given stream. For example, for a
-- given stream s, the expression tails s is equal to
-- [ drop 0 s, drop 1 s, drop 2 s, ...].
tails :: Typed a => Stream a -> [Stream a]
-- | Index.
--
-- WARNING: Very expensive! Consider using this only for very short
-- lists.
(!!!) :: (Typed a, Eq b, Num b, Typed b) => [Stream a] -> Stream b -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
nfoldl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldl in that it does not require
-- an initial accumulator and it assumes the argument number n
-- is positive.
nfoldl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
nfoldr :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> Stream b
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldr in that it does not require
-- an initial accumulator and it assumes the argument number n
-- is positive.
nfoldr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldl in that it returns the
-- intermediate results as well.
nscanl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> [Stream a]
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function differs from nfoldr in that it returns the
-- intermediate results as well.
nscanr :: Typed a => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> [Stream b]
-- | Given a number, a function on streams, and two streams, fold from the
-- left the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function assumes the number of elements to scan is positive, and
-- it also returns the intermediate results.
nscanl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a]
-- | Given a number, a function on streams, and two streams, fold from the
-- right the function over the finite list of tails of the second stream
-- (up to the given number).
--
-- This function assumes the number of elements to scan is positive, and
-- it also returns the intermediate results.
nscanr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a]
-- | Case-like function: The index of the first predicate that is true in
-- the predicate list selects the stream result. If no predicate is true,
-- the last element is chosen (default element)
case' :: Typed a => [Stream Bool] -> [Stream a] -> Stream a