-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A stream DSL for writing embedded C monitors.
--   
--   Can you write a list in Haskell? Then you can write embedded C code
--   using Copilot. Here's a Copilot program that computes the Fibonacci
--   sequence (over Word 64s) and tests for even numbers:
--   
--   <pre>
--   fib :: Streams
--   fib = do
--    let f = varW64 "fib"
--    let t = varB "t"
--    f .= [0,1] ++ f + (drop 1 f)
--    t .= even f
--      where even :: Spec Word64 -&gt; Spec Bool
--            even w' = w' `mod` 2 == 0
--   </pre>
--   
--   Copilot contains an interpreter, a compiler, and uses a model-checker
--   to check the correctness of your program. The compiler generates
--   constant time and constant space C code via Tom Hawkin's Atom (thanks
--   Tom!). Copilot was originally developed to write embedded monitors for
--   more complex embedded systems, but it can be used to develop a variety
--   of functional-style embedded code.
@package copilot
@version 1.0


-- | Helper functions for writing free-form C code.
module Language.Copilot.AdHocC

-- | Takes a type and a list of variable names and declares them.
varDecl :: Type -> [String] -> String

-- | Takes a type and a list of array names and their sizes declares them.
arrDecl :: Type -> [(String, Int)] -> String

-- | Takes a type and a variable and initializes it. It is YOUR
--   responsibility to ensure that <tt>val</tt> is of type <tt>t</tt>.
varInit :: Show a => Type -> String -> a -> String

-- | Takes a type and an array and initializes it. It is YOUR
--   responsibility to ensure that <tt>vals</tt> is of type <tt>t</tt>.
arrayInit :: Show a => Type -> String -> [a] -> String

-- | Declare function prototypes, given a return type, a function name, and
--   a | list of argument types. Use <a>Nothing</a> for a return type of
--   <tt>void</tt>.
funcDecl :: Maybe Type -> String -> [Type] -> String

-- | Add an include of a library
includeBracket :: String -> String

-- | Add an include of a header file
includeQuote :: String -> String
printf :: String -> [String] -> String

-- | printf, with and without a newline (nl) character.
printfNewline :: String -> [String] -> String


-- | Help to display.
module Language.Copilot.Help
helpStr :: String


-- | Provides basic types and functions for other parts of <i>Copilot</i>.
--   
--   If you wish to add a new type, you need to make it an instance of
--   <tt><a>Streamable</a></tt>, to add it to
--   <tt><a>foldStreamableMaps</a></tt>, <tt><a>mapStreamableMaps</a></tt>,
--   and optionnaly to add an ext[Type], a [type] and a var[Type] functions
--   in Language.hs to make it easier to use.
module Language.Copilot.Core

-- | Atom period -- used as an option to control the duration of a Copilot
--   <a>tick</a>.
type Period = Int

-- | Names of the streams or external variables
type Var = String

-- | C file name
type Name = String

-- | Port over which to broadcast information
data Port
Port :: Int -> Port

-- | Holds external variables or external functions to call.
data Ext
ExtV :: Var -> Ext
Fun :: String -> Args -> Ext
type Exs = (Type, Ext, ExtRet)
data ExtRet
ExtRetV :: ExtRet
ExtRetA :: String -> ExtRet
type Args = [ArgConstVar]

-- | Arguments to be passed to a C function. Either a Copilot variable or a
--   constant. A little hacky that I store constants as strings so we don't
--   have to pass around types. However, these data are just used to make
--   external C calls, for which we have no type info anyway, so it's a bit
--   of a moot point.
data ArgConstVar
V :: Var -> ArgConstVar
C :: String -> ArgConstVar

-- | Specification of a stream, parameterized by the type of the values of
--   the stream. The only requirement on <tt>a</tt> is that it should be
--   <a>Streamable</a>.
data Spec a
Var :: Var -> Spec a
Const :: a -> Spec a
PVar :: Type -> Ext -> Spec a
PArr :: Type -> (Ext, Spec b) -> Spec a
F :: (b -> a) -> (E b -> E a) -> Spec b -> Spec a
F2 :: (b -> c -> a) -> (E b -> E c -> E a) -> Spec b -> Spec c -> Spec a
F3 :: (b -> c -> d -> a) -> (E b -> E c -> E d -> E a) -> Spec b -> Spec c -> Spec d -> Spec a
Append :: [a] -> Spec a -> Spec a
Drop :: Int -> Spec a -> Spec a

-- | Container for mutually recursive streams, whose specifications may be
--   parameterized by different types
type Streams = Writer LangElems ()

-- | A named stream
type Stream a = Streamable a => (Var, Spec a)

-- | An instruction to send data on a port at a given phase. data Send a =
--   Sendable a =&gt; Send (Var, Phase, Port)
data Send a
Send :: Spec a -> Port -> String -> Send a
sendVar :: Send a -> Spec a
sendPort :: Send a -> Port
sendName :: Send a -> String
data Trigger
Trigger :: Spec Bool -> String -> Args -> Trigger
trigVar :: Trigger -> Spec Bool
trigName :: Trigger -> String
trigArgs :: Trigger -> Args
type Triggers = Map String Trigger

-- | Holds all the different kinds of language elements that are pushed
--   into the Writer monad. This currently includes the actual specs,
--   <a>send</a> directives, and trigger directives. (Use the functions in
--   Language.hs to make sends and triggers.)
data LangElems
LangElems :: StreamableMaps Spec -> StreamableMaps Send -> Triggers -> LangElems
strms :: LangElems -> StreamableMaps Spec
snds :: LangElems -> StreamableMaps Send
trigs :: LangElems -> Triggers

-- | Holds the complete specification of a distributed monitor type
--   DistributedStreams = (Streams, Sends)
--   
--   A type is streamable iff a stream may emit values of that type
--   
--   There are very strong links between <tt><a>Streamable</a></tt> and
--   <tt><a>StreamableMaps</a></tt> : the types aggregated in
--   <tt><a>StreamableMaps</a></tt> are exactly the
--   <tt><a>Streamable</a></tt> types and that invariant should be kept
--   (see methods)
class (Expr a, Assign a, Show a) => Streamable a
getSubMap :: Streamable a => StreamableMaps b -> Map Var (b a)
updateSubMap :: Streamable a => (Map Var (b a) -> Map Var (b a)) -> StreamableMaps b -> StreamableMaps b
unit :: Streamable a => a
atomConstructor :: Streamable a => Var -> a -> Atom (V a)
externalAtomConstructor :: Streamable a => Var -> V a
typeId :: Streamable a => a -> String
typeIdPrec :: Streamable a => a -> String
atomType :: Streamable a => a -> Type
showAsC :: Streamable a => a -> String

-- | This is a generalization of <tt><a>Streams</a></tt> which is used for
--   storing Maps over values parameterized by different types.
--   
--   It is extensively used in the internals of Copilot, in conjunction
--   with <tt><a>foldStreamableMaps</a></tt> and
--   <tt><a>mapStreamableMaps</a></tt>
data StreamableMaps a
SM :: Map Var (a Bool) -> Map Var (a Int8) -> Map Var (a Int16) -> Map Var (a Int32) -> Map Var (a Int64) -> Map Var (a Word8) -> Map Var (a Word16) -> Map Var (a Word32) -> Map Var (a Word64) -> Map Var (a Float) -> Map Var (a Double) -> StreamableMaps a
bMap :: StreamableMaps a -> Map Var (a Bool)
i8Map :: StreamableMaps a -> Map Var (a Int8)
i16Map :: StreamableMaps a -> Map Var (a Int16)
i32Map :: StreamableMaps a -> Map Var (a Int32)
i64Map :: StreamableMaps a -> Map Var (a Int64)
w8Map :: StreamableMaps a -> Map Var (a Word8)
w16Map :: StreamableMaps a -> Map Var (a Word16)
w32Map :: StreamableMaps a -> Map Var (a Word32)
w64Map :: StreamableMaps a -> Map Var (a Word64)
fMap :: StreamableMaps a -> Map Var (a Float)
dMap :: StreamableMaps a -> Map Var (a Double)

-- | An empty streamableMaps.
emptySM :: StreamableMaps a

-- | Verifies if its argument is equal to emptySM
isEmptySM :: StreamableMaps a -> Bool

-- | Lookup into the map of the right type in
--   <tt><a>StreamableMaps</a></tt>
getMaybeElem :: Streamable a => Var -> StreamableMaps b -> Maybe (b a)

-- | Lookup into the map of the right type in
--   <tt><a>StreamableMaps</a></tt> Launch an exception if the index is not
--   in it
getElem :: Streamable a => Var -> StreamableMaps b -> b a

-- | This function is used to iterate on all the values in all the maps
--   stored by a <tt><a>StreamableMaps</a></tt>, accumulating a value over
--   time
foldStreamableMaps :: (Streamable a => Var -> c a -> b -> b) -> StreamableMaps c -> b -> b
mapStreamableMaps :: (forall a. Streamable a => Var -> s a -> s' a) -> StreamableMaps s -> StreamableMaps s'
mapStreamableMapsM :: Monad m => (Streamable a => Var -> s a -> m (s' a)) -> StreamableMaps s -> m (StreamableMaps s')

-- | Only keeps in <tt>sm</tt> the values whose key+type are in <tt>l</tt>.
--   Also returns a bool saying whether all the elements in sm were in l.
--   Works even if some elements in <tt>l</tt> are not in <tt>sm</tt>. Not
--   optimised at all.
filterStreamableMaps :: StreamableMaps c -> [(Type, Var, b)] -> (StreamableMaps c, Bool)

-- | Replace all accepted special characters by sequences of underscores.
normalizeVar :: Var -> Var

-- | Get the Copilot variables.
getVars :: StreamableMaps s -> [Var]

-- | For each typed variable, this type holds all its successive values in
--   an infinite list Beware : each element of one of those lists
--   corresponds to a full <tt>Atom</tt> period, not to a single clock
--   tick.
type Vars = StreamableMaps []
getAtomType :: Streamable a => Spec a -> Type
getSpecs :: Streams -> StreamableMaps Spec
getSends :: Streams -> StreamableMaps Send
getTriggers :: Streams -> Triggers

-- | Copilot variable reference, taking the name of the generated C file.
vPre :: Name -> String

-- | For calling a function with Atom variables.
funcShow :: Name -> String -> Args -> String

-- | Get a variable name from a spec; throw an error otherwise.
getMaybeVar :: Streamable a => Spec a -> Var

-- | If the <a>Spec</a> isn't a <a>Var</a> or <a>Const</a>, then throw an
--   error; otherwise, apply the function.
notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b
instance Eq ExtRet
instance Eq ArgConstVar
instance Show a => Show (Spec a)
instance Monoid LangElems
instance Monoid (StreamableMaps Spec)
instance Streamable Double
instance Streamable Float
instance Streamable Word64
instance Streamable Word32
instance Streamable Word16
instance Streamable Word8
instance Streamable Int64
instance Streamable Int32
instance Streamable Int16
instance Streamable Int8
instance Streamable Bool
instance Streamable a => Show (Send a)
instance Eq a => Eq (Spec a)
instance (Streamable a, NumE a, Fractional a) => Fractional (Spec a)
instance (Streamable a, NumE a) => Num (Spec a)
instance Eq Ext
instance Show Ext
instance Show Trigger
instance Show ArgConstVar


-- | This module provides a way to check that a <i>Copilot</i>
--   specification is compilable
module Language.Copilot.Analyser

-- | Check a <i>Copilot</i> specification. If it is not compilable, then
--   returns an error describing the issue. Else, returns <tt>Nothing</tt>
check :: StreamableMaps Spec -> Maybe Error

-- | Used for representing an error in the specification, detected by
--   <tt><a>check</a></tt>
data Error

-- | the BNF is not respected
BadSyntax :: String -> Var -> Error

-- | A drop expression of less than 0 is used | BadSamplingPhase Var Ext --
--   ^ if an external variable is sampled at phase -- 0 then there is no
--   time for the stream to be -- updated | BadSamplingArrPhase Var Ext --
--   ^ if an external variable is sampled at -- phase 0 then there is no
--   time for the -- stream to be updated
BadDrop :: Int -> Var -> Error

-- | External array indexes can only take variables or constants as
--   indexes.
BadPArrSpec :: Var -> Ext -> String -> Error

-- | either a variable is not defined, or not with the good type ; there is
--   no implicit conversion of types in <i>Copilot</i>
BadType :: Var -> Var -> Error

-- | either an external variable is not defined, or not with the good type;
--   there is no implicit conversion of types in <i>Copilot</i>
BadTypeExt :: Ext -> Var -> Error

-- | The algorithm to compile <i>Copilot</i> specification can only work if
--   there is no negative weighted closed path in the specification, as
--   described in the original research paper
NonNegativeWeightedClosedPath :: [Var] -> Weight -> Error

-- | Could be compiled, but would need bigger prophecyArrays
DependsOnClosePast :: [Var] -> Ext -> Weight -> Weight -> Error

-- | If an output depends of a future of an input it will be hard to
--   compile to say the least
DependsOnFuture :: [Var] -> Ext -> Weight -> Error
data SpecSet
AllSpecSet :: SpecSet
FunSpecSet :: SpecSet
DropSpecSet :: SpecSet
PArrSet :: SpecSet
getExternalVars :: StreamableMaps Spec -> [Exs]
instance Eq SpecSet
instance Show Error


-- | The Copilot interpreter.
module Language.Copilot.Interpreter

-- | The main function of this module. It takes a <i>Copilot</i>
--   specification, the values of the monitored values, and returns the
--   values of the streams.
interpretStreams :: StreamableMaps Spec -> Vars -> Vars


-- | Transform the copilot specification in an atom one, and then compile
--   that one.
module Language.Copilot.Compiler

-- | Compiles an <i>Copilot</i> specification to an <i>Atom</i> one. The
--   period is given as a Maybe : if it is Nothing, an optimal period will
--   be chosen.
copilotToAtom :: LangElems -> Maybe Period -> Name -> (Period, Atom ())
tmpSampleStr :: String
tmpArrName :: Ext -> String -> Var
tmpVarName :: Ext -> Var


-- | Defines a main() and print statements to easily execute generated
--   Copilot specs.
module Language.Copilot.AtomToC
getPrePostCode :: Name -> StreamableMaps Spec -> [Exs] -> [(Ext, Int)] -> Vars -> Period -> (String, String)


-- | Generate random specs for testing. We do not generate external array
--   indexes.
module Language.Copilot.Tests.Random
randomStreams :: RandomGen g => Operators -> Operators -> Operators -> g -> (StreamableMaps Spec, Vars)
data Operator a
Operator :: (forall g. RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec a, g)) -> Operator a
type Operators = StreamableMaps Operator
fromOp :: Operator a -> (forall g. RandomGen g => (forall a' g'. (Streamable a', Random a', RandomGen g') => g' -> SpecSet -> (Spec a', g')) -> g -> (Spec a, g))
instance Random Type
instance Random a => Random [a]
instance Random Word64
instance Random Word32
instance Random Word16
instance Random Word8
instance Random Int64
instance Random Int32
instance Random Int16
instance Random Int8


-- | Functions for sampling external variables.
module Language.Copilot.Language.Sampling
extB :: ExtCl a => a -> Spec Bool
extI8 :: ExtCl a => a -> Spec Int8
extI16 :: ExtCl a => a -> Spec Int16
extI32 :: ExtCl a => a -> Spec Int32
extI64 :: ExtCl a => a -> Spec Int64
extW8 :: ExtCl a => a -> Spec Word8
extW16 :: ExtCl a => a -> Spec Word16
extW32 :: ExtCl a => a -> Spec Word32
extW64 :: ExtCl a => a -> Spec Word64
extF :: ExtCl a => a -> Spec Float
extD :: ExtCl a => a -> Spec Double
extArrB :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Bool
extArrI8 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Int8
extArrI16 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Int16
extArrI32 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Int32
extArrI64 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Int64
extArrW8 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Word8
extArrW16 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Word16
extArrW32 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Word32
extArrW64 :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Word64
extArrF :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Float
extArrD :: (ExtCl a, Streamable b, IntegralE b) => a -> Spec b -> Spec Double
instance ExtCl Ext
instance ExtCl String

module Language.Copilot.Language.FunctionCalls
(<>) :: (ArgCl a, Streamable b) => Spec b -> a -> Args
trigger :: ArgCl a => Spec Bool -> String -> a -> Streams

-- | No C arguments
void :: Args
fun :: ArgCl a => String -> a -> Ext
instance Streamable b => ArgCl (Spec b)
instance ArgCl Args


-- | Safe casting of values.
module Language.Copilot.Language.Casting
cast :: (Castable a, Castable b, Streamable b) => Spec b -> Spec a
instance Castable Int64
instance Castable Int32
instance Castable Int16
instance Castable Int8
instance Castable Word64
instance Castable Word32
instance Castable Word16
instance Castable Word8
instance Castable Bool


-- | Describes the language <i>Copilot</i>.
--   
--   If you wish to add a new operator, the only modification needed is
--   adding it in this module. But if you want it to be used in the random
--   generated streams, add it to either <tt><tt>opsF</tt></tt>,
--   <tt><tt>opsF2</tt></tt> or <tt><tt>opsF3</tt></tt>
module Language.Copilot.Language
mod :: (Streamable a, IntegralE a) => Spec a -> Spec a -> Spec a

-- | Beware : crash without any possible recovery if a division by 0
--   happens. Same risk with mod. Use div0 and mod0 if unsure.
div :: (Streamable a, IntegralE a) => Spec a -> Spec a -> Spec a
mod0 :: (Streamable a, IntegralE a) => a -> Spec a -> Spec a -> Spec a

-- | As mod and div, except that if the division would be by 0, the first
--   argument is used as a default.
div0 :: (Streamable a, IntegralE a) => a -> Spec a -> Spec a -> Spec a
(<) :: (Streamable a, OrdE a) => Spec a -> Spec a -> Spec Bool
(<=) :: (Streamable a, OrdE a) => Spec a -> Spec a -> Spec Bool
(==) :: (Streamable a, EqE a) => Spec a -> Spec a -> Spec Bool
(/=) :: (Streamable a, EqE a) => Spec a -> Spec a -> Spec Bool
(>=) :: (Streamable a, OrdE a) => Spec a -> Spec a -> Spec Bool
(>) :: (Streamable a, OrdE a) => Spec a -> Spec a -> Spec Bool
not :: Spec Bool -> Spec Bool
(||) :: Spec Bool -> Spec Bool -> Spec Bool
(&&) :: Spec Bool -> Spec Bool -> Spec Bool
(^) :: Spec Bool -> Spec Bool -> Spec Bool
(==>) :: Spec Bool -> Spec Bool -> Spec Bool
data Bool :: *
False :: Bool
True :: Bool

-- | Basic numeric class.
--   
--   Minimal complete definition: all except <a>negate</a> or <tt>(-)</tt>
class (Eq a, Show a) => Num a
(+) :: Num a => a -> a -> a
(*) :: Num a => a -> a -> a
(-) :: Num a => a -> a -> a
negate :: Num a => a -> a
abs :: Num a => a -> a
signum :: Num a => a -> a
fromInteger :: Num a => Integer -> a

-- | Fractional numbers, supporting real division.
--   
--   Minimal complete definition: <a>fromRational</a> and (<a>recip</a> or
--   <tt>(<a>/</a>)</tt>)
class Num a => Fractional a
(/) :: Fractional a => a -> a -> a

-- | Beware : both sides are executed, even if the result of one is later
--   discarded
mux :: Streamable a => Spec Bool -> Spec a -> Spec a -> Spec a

-- | Useful for writing libraries.
var :: Streamable a => Var -> Spec a
varB :: Var -> Spec Bool
varI8 :: Var -> Spec Int8
varI16 :: Var -> Spec Int16
varI32 :: Var -> Spec Int32
varI64 :: Var -> Spec Int64
varW8 :: Var -> Spec Word8
varW16 :: Var -> Spec Word16
varW32 :: Var -> Spec Word32
varW64 :: Var -> Spec Word64
varF :: Var -> Spec Float
varD :: Var -> Spec Double

-- | Coerces a type that is <a>Streamable</a> into a Copilot constant.
const :: Streamable a => a -> Spec a
constI8 :: Int8 -> Spec Int8
constI16 :: Int16 -> Spec Int16
constI32 :: Int32 -> Spec Int32
constI64 :: Int64 -> Spec Int64
constW8 :: Word8 -> Spec Word8
constW16 :: Word16 -> Spec Word16
constW32 :: Word32 -> Spec Word32
constW64 :: Word64 -> Spec Word64
constF :: Float -> Spec Float
constD :: Double -> Spec Double
true :: Spec Bool
false :: Spec Bool

-- | Drop <tt>i</tt> elements from a stream.
drop :: Streamable a => Int -> Spec a -> Spec a

-- | Just a trivial wrapper over the <tt><a>Append</a></tt> constructor
(++) :: Streamable a => [a] -> Spec a -> Spec a

-- | Define a stream variable.
(.=) :: Streamable a => Spec a -> Spec a -> Streams

-- | Takes a function <tt>name</tt>, a port <tt>number</tt>, and a Copilot
--   variable <tt>v</tt> and constructs a call to the C function
--   <tt>name(x,y)</tt> where <tt>x</tt> is the value of the Copilot stream
--   <tt>v</tt> and <tt>y</tt> is the port number.
send :: Streamable a => String -> Port -> Spec a -> Streams
port :: Int -> Port

-- | If the <a>Spec</a> isn't a <a>Var</a> or <a>Const</a>, then throw an
--   error; otherwise, apply the function.
notConstVarErr :: Streamable a => Spec a -> (ArgConstVar -> b) -> b


-- | Sets of operators for Tests.Random.hs
module Language.Copilot.Language.RandomOps
opsF :: Operators

-- | opsF, opsF2 and opsF3 are fed to Tests.Random.randomStreams. They
--   allows the random generated streams to include lots of operators. If
--   you add a new operator to Copilot, it would be nice to add it to one
--   of those, that way it could be used in the random streams used for
--   testing. opsF holds all the operators of arity 1, opsF2 of arity 2 and
--   opsF3 of arity3 They are StreamableMaps, because operators are sorted
--   based on their return type.
opsF2 :: Operators
opsF3 :: Operators


-- | Only exports instances for Show which allows the printing of streams
module Language.Copilot.PrettyPrinter
instance Show Streams
instance (Show (a Bool), Show (a Int8), Show (a Int16), Show (a Int32), Show (a Int64), Show (a Word8), Show (a Word16), Show (a Word32), Show (a Word64), Show (a Float), Show (a Double)) => Show (StreamableMaps a)


-- | The Dispatch module : does all the IO, and offers an unified interface
--   to both the interpreter and the compiler.
--   
--   Also communicates with GCC in order to compile the C code, and then
--   transmits the results of the execution of that C code. This
--   functionnality is mostly used to check automatically the equivalence
--   between the interpreter and the compiler. The Dispatch module only
--   parses the command-line arguments before calling that module.
module Language.Copilot.Dispatch

-- | This function is the core of <i>Copilot</i> : it glues together
--   analyser, interpreter and compiler, and does all the IO. It can be
--   called either from interface (which justs decodes the command-line
--   argument) or directly from the interactive prompt in ghci.
--   <tt>streams</tt> is a specification, <tt>inputExts</tt> allows the
--   user to give at runtime values for the monitored variables. Useful for
--   testing on randomly generated values and specifications, or for the
--   interpreted version. <tt>be</tt> chooses between compilation or
--   interpretation, and if compilation is chosen (AtomToC) holds a few
--   additionnal informations. see description of <tt><a>BackEnd</a></tt>
--   <tt>iterations</tt> just gives the number of periods the specification
--   must be executed. If you would rather execute it by hand, then just
--   choose AtomToC for backEnd and 0 for iterations <tt>verbose</tt>
--   determines what is output.
dispatch :: LangElems -> Vars -> BackEnd -> Iterations -> Verbose -> IO ()
data BackEnd
Opts :: AtomToC -> BackEnd
Interpreter :: BackEnd
data AtomToC
AtomToC :: Name -> String -> Maybe Period -> Interpreted -> String -> String -> Maybe (String, String) -> [(String, Int)] -> Maybe Clock -> AtomToC

-- | Name of the C file to generate
cName :: AtomToC -> Name

-- | Options to pass to the compiler
gccOpts :: AtomToC -> String

-- | The optional period
getPeriod :: AtomToC -> Maybe Period

-- | Interpret the program or not
interpreted :: AtomToC -> Interpreted

-- | Where to put the executable
outputDir :: AtomToC -> String

-- | Which compiler to use
compiler :: AtomToC -> String

-- | Code to replace the default initialization and main
prePostCode :: AtomToC -> Maybe (String, String)
arrDecs :: AtomToC -> [(String, Int)]
clock :: AtomToC -> Maybe Clock
data Interpreted
Interpreted :: Interpreted
NotInterpreted :: Interpreted
type Iterations = Int
data Verbose
OnlyErrors :: Verbose
DefaultVerbose :: Verbose
Verbose :: Verbose
instance Eq Verbose


-- | Used by the end-user to easily give its arguments to dispatch.
module Language.Copilot.Interface
data Options
baseOpts :: Options
test :: Int -> Options -> IO ()
interpret :: Streams -> Int -> Options -> IO ()
compile :: Streams -> Name -> Options -> IO ()
verify :: FilePath -> Int -> String -> IO ()

-- | The <a>main</a> function that dispatches.
interface :: Options -> IO ()
help :: IO ()

-- | Sets the environment for simulation by giving a mapping of external
--   variables to lists of values. E.g.,
--   
--   <pre>
--   setE (emptySM {w32Map = fromList [("ext", [0,1..])]}) ...
--   </pre>
--   
--   sets the external variable names <a>ext</a> to take the natural
--   numbers, up to the limit of Word32.
setE :: Vars -> Options -> Options

-- | Sets the options for the compiler, e.g.,
--   
--   <pre>
--   setC "-O2" ...
--   </pre>
--   
--   Sets gcc options.
setC :: String -> Options -> Options
setO :: Name -> Options -> Options

-- | Manually set the period for the program. Otherwise, the minimum
--   required period is computed automatically. E.g.,
--   
--   <tt> setP 100 ... </tt> sets the period to be 100. The period must be
--   at least 1.
setP :: Period -> Options -> Options
setI :: Options -> Options

-- | Sets the code to precede and follow the copilot specification If
--   nothing, then code appropriate for communication with the interpreter
--   is generated
setPP :: (String, String) -> Options -> Options

-- | Sets the number of iterations of the program to simulation:
--   
--   <tt> setN 50 </tt> simulations the program for 50 steps.
setN :: Int -> Options -> Options

-- | Set the verbosity level.
setV :: Verbose -> Options -> Options
setR :: Int -> Options -> Options

-- | Sets the directory into which the output of compiled programs should
--   be placed. If the directory does not exist, it will be created.
setDir :: String -> Options -> Options

-- | Sets the compiler to use, given as a path to the executable. The
--   default is "gcc".
setGCC :: String -> Options -> Options

-- | Set the external arrays.
setArrs :: [(String, Int)] -> Options -> Options

-- | Sets the hardware clock. See
--   http:<i></i>github.com<i>tomahawkins</i>atom<i>blob</i>master<i>Language</i>Atom/Code.hs.
setClock :: Clock -> Options -> Options
noOpts :: Options -> Options


-- | Basic error checking for other libraries.
module Language.Copilot.Libs.ErrorChks
nOneChk :: String -> Int -> Spec a -> Spec a
nPosChk :: String -> Int -> Spec a -> Spec a
int16Chk :: String -> Int -> Spec a -> Spec a


-- | Provides past-time linear-temporal logic (ptLTL operators).
--   
--   Interface: see Examples/PTLTLExamples.hs, particularly function
--   tSinExt2 in that file. You can embed a ptLTL specification within a
--   Copilot specification using the form: <tt> var <a>ptltl</a> (operator
--   spec) </tt> where <a>var</a> is the variable you want to assign to the
--   ptLTL specification you're writing.
module Language.Copilot.Libs.PTLTL
ptltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams

-- | Once <tt>s2</tt> holds, in the following state (period), does
--   <tt>s1</tt> continuously hold?
since :: Spec Bool -> Spec Bool -> Spec Bool -> Streams

-- | Has <tt>s</tt> always held (up to and including the current state)?
alwaysBeen :: Spec Bool -> Spec Bool -> Streams

-- | Did <tt>s</tt> hold at some time in the past (including the current
--   state)?
eventuallyPrev :: Spec Bool -> Spec Bool -> Streams

-- | Did <tt>s</tt> hold in the previous period?
previous :: Spec Bool -> Spec Bool -> Streams


-- | Queries into how long until properties hold or fail. We use Int16 to
--   return the value, so your queries must not require looking more than
--   32,767 periods :) . Thus, in the following, the parameter <tt>n</tt>
--   must be <tt>0 &lt;= n &lt;= 32,767</tt>. -1 indicates the test failed.
module Language.Copilot.Libs.Indexes

-- | Returns the smallest <tt>m &lt;= n</tt> such that <tt>drop m s</tt> is
--   true, and <tt>-1</tt> if no such <tt>m</tt> exists.
soonest :: Int -> Spec Bool -> Spec Int16

-- | Returns the smallest <tt>m &lt;= n</tt> such that <tt>drop m s</tt> is
--   false, and <tt>-1</tt> if no such <tt>m</tt> exists.
soonestFail :: Int -> Spec Bool -> Spec Int16

-- | Returns the largest <tt>m &lt;= n</tt> such that <tt>drop m s</tt> is
--   true, and <tt>-1</tt> if no such <tt>m</tt> exists.
latest :: Int -> Spec Bool -> Spec Int16

-- | Returns the largest <tt>m &lt;= n</tt> such that <tt>drop m s</tt> is
--   false, and <tt>-1</tt> if no such <tt>m</tt> exists.
latestFail :: Int -> Spec Bool -> Spec Int16


-- | Bounded Linear Temporal Logic (LTL) operators. For a bound <tt>n</tt>,
--   a property <tt>p</tt> holds if it holds on the next <tt>n</tt>
--   transitions (between periods). If <tt>n == 0</tt>, then the trace
--   includes only the current period. For example, <tt> always 3 p </tt>
--   holds if <tt>p</tt> holds at least once every four periods (3
--   transitions).
--   
--   Interface: see Examples/LTLExamples.hs You can embed a LTL
--   specification within a Copilot specification using the form: <tt> var
--   <a>ltl</a> (operator spec) </tt> where <a>var</a> is the variable you
--   want to assign to the LTL specification you're writing.
--   
--   For some properties, stream dependencies may not allow their
--   specification. In particular, you cannot determine the <a>future</a>
--   value of an external variable. In general, the ptLTL library is
--   probaby more useful.
module Language.Copilot.Libs.LTL
ltl :: Spec Bool -> (Spec Bool -> Streams) -> Streams

-- | Property <tt>s</tt> holds at some period in the next <tt>n</tt>
--   periods. If <tt>n == 0</tt>, then <tt>s</tt> holds in the current
--   period. We require <tt>n &gt;= 0</tt>. E.g., if <tt>p = eventually 2
--   s</tt>, then we have the following relationship between the streams
--   generated: <tt> s =&gt; F F F T F F F T ... p =&gt; F T T T F T T T
--   ... </tt>
eventually :: Int -> Spec Bool -> Spec Bool -> Streams

-- | Property <tt>s</tt> holds at the next period. For example: <tt> 0 1 2
--   3 4 5 6 7 s =&gt; F F F T F F T F ... next s =&gt; F F T F F T F ...
--   </tt> Note: s must have sufficient history to drop a value from it.
next :: Spec Bool -> Spec Bool -> Streams

-- | Property <tt>s</tt> holds for the next <tt>n</tt> periods. We require
--   <tt>n &gt;= 0</tt>. If <tt>n == 0</tt>, then <tt>s</tt> holds in the
--   current period. E.g., if <tt>p = always 2 s</tt>, then we have the
--   following relationship between the streams generated: <tt> 0 1 2 3 4 5
--   6 7 s =&gt; T T T F T T T T ... p =&gt; T F F F T T ... </tt>
always :: Int -> Spec Bool -> Spec Bool -> Streams

-- | <tt>until n s0 s1</tt> means that <tt>eventually n s1</tt>, and up
--   until at least the period before <tt>s1</tt> holds, <tt>s0</tt>
--   continuously holds.
until :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams

-- | <tt>release n s0 s1</tt> means that either <tt>always n s1</tt>, or
--   <tt>s1</tt> holds up to and including the period at which <tt>s0</tt>
--   becomes true.
release :: Int -> Spec Bool -> Spec Bool -> Spec Bool -> Streams


-- | Basic bounded statistics. In the following, a bound <tt>n</tt> is
--   given stating the number of periods over which to compute the
--   statistic (<tt>n == 1</tt> computes it only over the current period).
module Language.Copilot.Libs.Statistics

-- | Maximum value.
max :: (Streamable a, NumE a) => Int -> Spec a -> Spec a

-- | Minimum value.
min :: (Streamable a, NumE a) => Int -> Spec a -> Spec a

-- | Summation.
sum :: (Streamable a, NumE a) => Int -> Spec a -> Spec a

-- | Mean value. <tt>n</tt> must not overflow for word size <tt>a</tt> for
--   streams over which computation is peformed.
mean :: (Streamable a, Fractional a, NumE a) => Int -> Spec a -> Spec a

module Language.Copilot.Examples.StatExamples
t0 :: Streams
tMean :: Streams

module Language.Copilot

module Language.Copilot.Examples.Examples
fib :: Streams
t1 :: Streams
t3 :: Streams
t4 :: Streams
t5 :: Streams
yy :: Streams
zz :: Streams
xx :: Streams
engine :: Streams

-- | Sending over ports.
distrib :: Streams
gcd :: Word16 -> Word16 -> Streams
gcd' :: Streams
testCoercions :: Streams
testCoercions2 :: Streams
testCoercions3 :: Streams
i8 :: Streams
trap :: Streams
testArr :: Streams
t99 :: Streams
t11 :: Streams

module Language.Copilot.Examples.LTLExamples
output :: Spec Bool
testing :: Spec Bool
tSoonest :: Int -> Streams
tLatest :: Int -> Streams
tAlways :: Int -> Int -> Streams
tNext :: Int -> Streams
tFuture :: Int -> Int -> Streams
t0 :: Spec Bool
t1 :: Spec Bool
c :: Spec Bool
tUntil :: Int -> Int -> Int -> Streams
tRelease0 :: Int -> Streams
tRelease1 :: Int -> Int -> Streams
testRules :: Streams

module Language.Copilot.Examples.PTLTLExamples
tstdatprv :: Streams
tprv :: Streams
tstdatAB :: Streams
tAB :: Streams
tstdatEP :: Streams
tEP :: Streams
q2 :: Spec Bool
z :: Spec Bool
q1 :: Spec Bool
tstdat1Sin :: Streams
tstdat2Sin :: Streams
tSince :: Streams
tSinExt :: Streams
tSinExt2 :: Streams
engine :: Streams
engineRun :: IO ()