Copilot-Language / copilot

A stream-based runtime-verification framework for generating hard real-time C code.
http://copilot-language.github.io
651 stars 54 forks source link

Add ability to add names / labels to streams #59

Open fdedden opened 4 years ago

fdedden commented 4 years ago

Being able to give names or labels to streams has the following benefits:

There are some existing pull requests by @avieth related to this enhancement: https://github.com/Copilot-Language/copilot-core/pull/18 https://github.com/Copilot-Language/copilot-language/pull/9 https://github.com/Copilot-Language/copilot-c99/pull/27

These are denied and closed for now, as they implement a way which we deem to specific. They might come in handy later on.

robdockins commented 2 years ago

I don't know if this is the right place to drop this idea, but I was thinking the other day that it might work out nicely to use the magic HasCallStack constraint to implement some form of traceability for stream and trigger definitions, etc. CF: https://hackage.haskell.org/package/base-4.16.0.0/docs/GHC-Stack.html#t:HasCallStack

Basically, you can add the HasCallStack constraint to any Haskell declaration, and the compiler with automatically populate it with information about call sites. That information is propagated to error calls and thrown exceptions, but can also be directly fetched using the callStack combinator. Adding HasCallStack annotations into the user-facing APIs for copilot, and then grabbing those stacks and stashing them into high-level stream definitions would allow a pretty lightweight way to maintain traceability connections to specification code.

ivanperez-keera commented 7 months ago

Tagging @RyanGlScott for awareness.