Safe Haskell	Safe
Language	Haskell2010

Copilot.Interpret.Eval

Description

A tagless interpreter for Copilot specifications.

Synopsis

Documentation

type Env nm = [(nm, Dynamic)] Source #

An environment that contains an association between (stream or extern) names and their values.

The simulation output is defined as a string. Different backends may choose to format their results differently.

An execution trace, containing the traces associated to each individual monitor trigger and observer.

Constructors

ExecTrace
Fields interpTriggers :: [(String, [Maybe [Output]])] Map from trigger names to their optional output, which is a list of strings representing their values. The output may be `Nothing` if the guard for the trigger was false. The order is important, since we compare the arg lists between the interpreter and backends. interpObservers :: [(String, [Output])] Map from observer names to their outputs.

Instances details

Show ExecTrace Source #
Instance details Defined in Copilot.Interpret.Eval Methods showsPrec :: Int -> ExecTrace -> ShowS Source # show :: ExecTrace -> String Source # showList :: [ExecTrace] -> ShowS Source #

Arguments

:: ShowType	Show booleans as `0`/`1` (C) or `True`/`False` (Haskell).
-> Int	Number of steps to evaluate.
-> Spec	Specification to evaluate.
-> ExecTrace

Evaluate a specification for a number of steps.

Target language for showing a typed value. Used to adapt the representation of booleans.

Constructors

C
Haskell