Currently, the program type uses a type parameter 'M for the type of messages that can be sent or received. This makes it possible for concrete applications of process to not include a “done” message. However, the rest of the mini-protocol framework requires “done” messages to be permitted. As a result, in all uses of process the type parameter 'M is instantiated with 'm or_done. It would be much more natural to include the application of or_done directly in the definition of process, but this would currently break the use of corec for programs.
That said, there is a fix for this problem, realized in the Isabelle commits e72f8009a4f0 and da437a9f2823, which should go into Isabelle2023. As soon as Isabelle2023 is released, we shall do the following:
[ ] Make the described improvement to the definition of process
[ ] Adapt the definition of the Receive syntax accordingly
[ ] Adapt all code that refers to the process type accordingly
Currently, the
programtype uses a type parameter'Mfor the type of messages that can be sent or received. This makes it possible for concrete applications ofprocessto not include a “done” message. However, the rest of the mini-protocol framework requires “done” messages to be permitted. As a result, in all uses ofprocessthe type parameter'Mis instantiated with'm or_done. It would be much more natural to include the application ofor_donedirectly in the definition ofprocess, but this would currently break the use ofcorecfor programs.That said, there is a fix for this problem, realized in the Isabelle commits e72f8009a4f0 and da437a9f2823, which should go into Isabelle2023. As soon as Isabelle2023 is released, we shall do the following:
processReceivesyntax accordinglyprocesstype accordingly