You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Being able to give names or labels to streams has the following benefits:
Traceability between the original Copilot specification and C code is improved greatly, which can be a really important point for certification purposes.
The generated C code will be easier to read, again helping with certification.
Same approach can possibly used for name arguments of triggers, making the generated header file readable for people that don't know about the Copilot specification.
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.
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:
Copilot-Language/copilot-core#18
Copilot-Language/copilot-language#9
Copilot-Language/copilot-c99#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.
The text was updated successfully, but these errors were encountered: