copilot-1.0.2: A stream DSL for writing embedded C monitors.




This module provides a way to check that a Copilot specification is compilable


Main error checking functions

check :: StreamableMaps Spec -> Maybe ErrorSource

Check a Copilot specification. If it is not compilable, then returns an error describing the issue. Else, returns Nothing.

data Error Source

Used for representing an error in the specification, detected by check


BadSyntax String Var

the BNF is not respected

BadDrop Int Var

A drop expression of less than 0 is used

BadPArrSpec Var Ext String

External array indexes can only take variables or constants as indexes.

BadType Var String

either a variable is not defined, or not with the good type ; there is no implicit conversion of types in Copilot.

BadTypeExt Ext Var

either an external variable is not defined, or not with the good type; there is no implicit conversion of types in Copilot

NonNegativeWeightedClosedPath [Var] Weight

The algorithm to compile Copilot specification can only work if there is no negative weighted closed path in the specification, as described in the original research paper

DependsOnClosePast [Var] Ext Weight Weight

Could be compiled, but would need bigger prophecyArrays

DependsOnFuture [Var] Ext Weight

If an output depends of a future of an input it will be hard to compile to say the least

NoInit Var

If we are sampling a function and it has an argument that is a Copilot stream, the weight of that stream must have at least one initial element.


data SpecSet Source


Varied other things