Language.Copilot

Copilot is a stream-based runtime verification framework. Programs can be interpreted for testing, or translated into C99 code to be incorporated in a project, or as a standalone application. The C99 backend output is constant in memory and time, making it suitable for systems with hard realtime requirements.

This module is the main entry point for the Copilot language. The expectation is that most Copilot users will only need to import this module, together with one of the backend modules (at present, only C99 from the copilot-c99 library is available).

Documentation

module Copilot.Language

module Copilot.Language.Prelude

module Copilot.Language.Reify

module Copilot.Library.Libraries

copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()

Create a main to either compile or interpret a copilot specification.

This function must be provided an auxiliary function capable of compiling Copilot Core specifications for some target.

The command line program supports four main commands:

• --output/-o: use the given compiler to produce C code.
• --justrun/-c: execute a dry-run, which parses and converts the specification to core but does not produce any output.
• --print/-p: pretty print the specification.
• --interpret/-i NUM: interpret the specification for a given number of steps.

defaultMain :: Compiler -> Spec -> IO ()

Create a main function with a default interpreter and pretty printer.

This function must be provided an auxiliary function capable of compiling Copilot Core specifications for some target.

This function relies on copilotMain, please refer to that function for the command line options.