copilot

copilot copied to clipboard

**Description** Multiple definitions in `Copilot.Core.Type.Array` are not being used by any other part of Copilot or, as far as we know, by any user of Copilot. These include the `InnerType`...

ivanperez-keera

support for nominally distinct Haskell types with identical copilot types

8

# Motivation It would be great to have domain-specific Haskell types in streams, as this can give extra type safety in the high-level model that, with correct code generation, holds...

avieth

`copilot-c99`: Add volatile qualifier to external stream variable

3

Minor enhancements to the code generation process. This adds volatile qualifiers to external stream global variables, and allows users to select an output directory for generated code.

robdockins

`copilot-theorem`: support bisimulation proofs involving C99 code

2

**Description** One of Copilot's new requirements is to produce proofs that the C code produced matches the semantics. In order to produce such proofs, we must extend `copilot-theorem​` to enable...

ivanperez-keera

`copilot-core`: externalize the interpreter in a separate library

3

**Description** Currently, the architecture of Copilot mixes backends with other libraries, which makes the result not uniform. For example, the interpreter and the Graphviz prettyprinter are part of `copilot-core`, while...

ivanperez-keera

`copilot-c99`: appending values to a stream of arrays produces incorrect C99 code

4

**Description** Appending values to a stream should delay the samples. When `(++)` is applied to a stream of arrays, the values produced by the C99 backend are incorrect. Consider the...

ivanperez-keera

Avoiding combinatorial blowup in emitted C code

4

Here's a little standalone example showing what I mean, along with a makefile that counts the size of the resulting C file in bytes. Look for the XXX in the...

simondlevy

**Description** In our effort to move Copilot to Class D, we have to comply with a style guide. In order to progressively follow those rules, we split complying with the...

ivanperez-keera

Concurrency considerations in generated code

12

The generated C code takes some care to copy the values of all the "external" streams from shared global variables to private globals before beginning the remainder of its work....

robdockins

Repeated declarations of functions in generated C code if a function is triggered twice in specification

5

If we have a Copilot specification where we have multiple conditions for triggering the same function (but perhaps we are providing different arguments), then in generated C code we would...

antanas-kalkauskas-sensmetry