-- 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 3.2
-- | This library generates new clocks based on a base period and phase.
--
-- Example Usage
--
-- Also see Examples/ClockExamples.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
-- | Once s2 holds, in the following state (period), does
-- s1 continuously hold?
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 examples, see Examples/RegExpExamples.hs in the
-- Copilot repository.
module Copilot.Library.RegExp
copilotRegexp :: (Typed t, SymbolParser t, Eq t) => Stream t -> SourceName -> Stream Bool -> Stream Bool
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
take :: (Integral a, Typed b) => a -> Stream b -> [Stream b]
tails :: Typed a => Stream a -> [Stream a]
cycle :: Typed a => [a] -> Stream a
nfoldl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> Stream a
nfoldl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
nfoldr :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> Stream b
nfoldr1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
nscanl :: (Typed a, Typed b) => Int -> (Stream a -> Stream b -> Stream a) -> Stream a -> Stream b -> [Stream a]
nscanr :: Typed a => Int -> (Stream a -> Stream b -> Stream b) -> Stream b -> Stream a -> [Stream b]
nscanl1 :: Typed a => Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> [Stream a]
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.
(!!) :: (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
module Copilot.Library.MTL
eventually :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
eventuallyPrev :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
always :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
alwaysBeen :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool
until :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
release :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
since :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
trigger :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingUntil :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingRelease :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
matchingSince :: (Typed a, Integral a) => a -> a -> Stream a -> a -> Stream Bool -> Stream Bool -> Stream Bool
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. 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 ...
--
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 ...
--
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.
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.
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 in
-- copilot-discussion explains 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/VotingExamples.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
module Copilot.Library.Libraries