copilot-interpreter-4.8: Interpreter for Copilot.

Safe Haskell | Safe
Language | Haskell2010

Copilot.Interpret.Eval

Description

A tagless interpreter for Copilot specifications.

Synopsis

- type Env nm = [(nm, Dynamic)]
- type Output = String
- data ExecTrace = ExecTrace {
  - interpTriggers :: [(String, [Maybe [Output]])]
  - interpObservers :: [(String, [Output])]
  }
- eval :: ShowType -> Int -> Spec -> ExecTrace
- data ShowType
  - = C
  - | Haskell

# Documentation

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

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

type Output = String Source #

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

data ExecTrace Source #

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

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 #

eval 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.

data ShowType Source #

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

Constructors

C |
Haskell |