copilot-language-2.2.0: A Haskell-embedded DSL for monitoring hard real-time distributed systems.

Safe HaskellTrustworthy
LanguageHaskell2010

Copilot.Language

Description

Main Copilot language export file.

Synopsis

Documentation

module Data.Int

module Data.Word

module Copilot.Core

impossible :: String -> String -> a Source

badUsage :: String -> a Source

csv :: Integer -> Spec -> IO () Source

interpret :: Integer -> Spec -> IO () Source

Much slower, but pretty-printed interpreter output.

module Copilot.Language.Operators.Boolean

module Copilot.Language.Operators.Cast

module Copilot.Language.Operators.Constant

module Copilot.Language.Operators.Eq

module Copilot.Language.Operators.Extern

module Copilot.Language.Operators.Local

module Copilot.Language.Operators.Label

module Copilot.Language.Operators.Integral

module Copilot.Language.Operators.Mux

module Copilot.Language.Operators.Ord

module Copilot.Language.Operators.Temporal

module Copilot.Language.Operators.BitWise

module Copilot.Language.Prelude

type Spec = Writer [SpecItem] () Source

data Stream :: * -> * Source

Instances

Eq (Stream a) Source

Dummy instance in order to make Stream an instance of Num.

(Typed a, Eq a, Floating a) => Floating (Stream a) Source 
(Typed a, Eq a, Fractional a) => Fractional (Stream a) Source 
(Typed a, Eq a, Num a) => Num (Stream a) Source 
Show (Stream a) Source

Dummy instance in order to make Stream an instance of Num.

observer :: Typed a => String -> Stream a -> Spec Source

trigger :: String -> Stream Bool -> [Arg] -> Spec Source

arg :: Typed a => Stream a -> Arg Source

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a) Source

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a) Source

forall :: Stream Bool -> Prop Universal Source

exists :: Stream Bool -> Prop Existential Source

prettyPrint :: Spec -> IO () Source