|
|
---
|
|
|
author: Laurent Prosperi
|
|
|
date: 09/02/2022
|
|
|
geometry: margin=1in
|
|
|
title: Event Auto-Boxing
|
|
|
header-includes:
|
|
|
- \hypersetup{colorlinks=true}
|
|
|
# - \usepackage{minted}
|
|
|
# - \def\mylexer{../Lg4DC.documents/shared/speclexer.py:SpecLexer -x}
|
|
|
#pandoc-minted:
|
|
|
# #language: \mylexer
|
|
|
# language: C
|
|
|
---
|
|
|
|
|
|
## How to
|
|
|
|
|
|
### Rewriting types
|
|
|
|
|
|
All session type st such that
|
|
|
!tmsg or ?tmsg such that tmsg
|
|
|
is not an event
|
|
|
|
|
|
### Rewriting expression
|
|
|
|
|
|
#### At message sending
|
|
|
|
|
|
* fire(s, msg)
|
|
|
``fire(s, autobox(msg))``
|
|
|
|
|
|
#### At message reception
|
|
|
|
|
|
* receive(s) **Not yet implemented**
|
|
|
``
|
|
|
(autounbox(receive(s))
|
|
|
``
|
|
|
* inport ... on ... expecting st = callback
|
|
|
``
|
|
|
inport .... = lambda x:box_msg lambda s:st - callback(autounbox(x), s)
|
|
|
``
|
|
|
|
|
|
N.B select/select_branch/branch are concerned since blabel is a builtin event |