|
| Language.Copilot.Dispatch |
|
|
| Description |
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.
|
|
| Synopsis |
|
|
|
| Documentation |
|
| dispatch :: StreamableMaps Spec -> Sends -> Vars -> BackEnd -> Iterations -> Verbose -> IO () |
| This function is the core of Copilot :
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.
streams is a specification,
inputExts 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.
be chooses between compilation or interpretation,
and if compilation is chosen (AtomToC) holds a few additionnal informations.
see description of BackEnd
iterations 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
verbose determines what is output.
|
|
| data BackEnd |
|
|
| data AtomToC |
| Constructors | | AtomToC | | | cName :: Name | Name of the C file to generate
| | gccOpts :: String | Options to pass to the compiler
| | getPeriod :: Maybe Period | The optional period
| | interpreted :: Interpreted | Interpret the program or not
| | outputDir :: String | Where to put the executable
| | compiler :: String | Which compiler to use
| | prePostCode :: Maybe (String, String) | Code to replace the default initialization and main
| | triggers :: Maybe [(Var, String)] | A list of Copilot variable C
function name pairs. The C
funciton is called if the
Copilot stream becomes True.
The Stream must be of Booleans
and the C function must be of
type void foo(void).
|
|
|
|
|
| data Interpreted |
| Constructors | | Interpreted | | | NotInterpreted | |
|
|
|
| type Iterations = Int |
|
| data Verbose |
| Constructors | | OnlyErrors | | | DefaultVerbose | | | Verbose | |
|  Instances | |
|
|
| Produced by Haddock version 2.6.1 |
