Complicated scarring following mpox infection

Since May 2022, more than 80 countries have been experiencing an outbreak of human mpox, a viral zoonotic infection caused by the mpox virus. A characteristic feature of this outbreak is the high frequency of genital and anal skin lesions. Classically, lesions heal spontaneously within a median of three weeks after the crusts have fallen off.

We describe herein four patients with complicated scarring following mpox lesions.

All four patients were men who have sex with men (MSM) and had a PCR confirmed diagnosis of mpox at Bichat-Claude Bernard hospital in Paris, France, a referral center for mpox where 624 patients have been diagnosed since may 2022.

The first pattern was hypertrophic scarring of facial lesions in two patients. Initially, the patients presented with typical mpox vesiculous lesions. Patient one was a 38-year-old HIV positive male with undetectable viral load (and CD4 T cell count of 600 cells/mm3), who presented with lesions on the cheek, the forehead, and the chin. Patient two was a 26-year-old male on HIV Pre Exposure Prophylaxis (PreP) with lesions on the chin. After one week of evolution, both patients had persistent inflammatory infiltration and meliceric crusts leading to a suspicion of Staphylococcus aureus superinfection. There was no microbiological confirmation due to restrictions for laboratory biosafety reasons in case of suspected or confirmed mpox infection [START_REF]Gestion des prélèvements biologiques d'un patient suspect ou confirmé d'infection par le Monkeypox virus (MPXV) Version[END_REF]. Only one of them was treated with antibiotic, as the second patient was not immediately referred to the consultation. Signs of superinfection regressed in both cases. After the resolution of crusting, persisted nodular erythematous lesions were observed and treated with local silicone gel (Figure 1,A).

The second pattern was a scarring folliculitis on peri-buccal lesions in two patients.

Patient 3 was a 23-year-old male, HIV negative with hypothyroidism and patient 4 was a 53-year-old-HIV positive male with undetectable viral load (CD4 T cell count of 237 cells/mm3). At diagnosis, both had signs of superinfection with meliceric crusts and major upper lip edema. Treatment with oral amoxicillin/clavulanic acid 50mg/kg daily for 1 week led to the resolution of edema in both patients. After the resolution of meliceric crusts, an erythematous patch of alopecic area persisted and was treated with corticosteroids without efficiency (Figures 1, B, andC).

The scarring mechanisms have been investigated in smallpox. According to Regan et al, five different theories can explain the scarring: the extension of suppuration into the dermis; inappropriate treatment and scratching of the lesions; secondary bacterial ecthyma; destruction of elastic fibers; or destruction of sebaceous glands [START_REF] Regan | The scarring mechanism of smallpox[END_REF][START_REF] Bras | Observations on the formation of smallpox scars[END_REF]. Histologic examination of cutaneous biopsies in mpox has demonstrated a marked inflammatory dermic infiltrate (4). Interleukin-10, an anti-inflammatory factor, has been reported to be markedly elevated among individuals suffering from mpox who have very high rash burden (>250 lesions) and it might potentiate or dampen inflammation [START_REF] Johnston | Cytokine modulation correlates with severity of monkeypox disease in humans[END_REF].

Bacterial superinfection after vesicular skin rash has been reported in multiple studies, as well as in patients with mpox infection [START_REF] Girometti | Demographic and clinical characteristics of confirmed human monkeypox virus cases in individuals attending a sexual health centre in London, UK: an observational analysis[END_REF][START_REF] Moschese | Hospitalisation for monkeypox in Milan, Italy[END_REF]. Superinfection is considered as a major risk in delaying healing process of the skin lesions and may lead to hospitalization in immunocompromised patients.

In these observations, the combination of deep dermic inflammation, local super-infection, and scratching may have led to aesthetic complications. This could emphasize the need for quick antibiotic treatment in case of superinfection and the importance of informing patients to avoid manipulations in order to reduce the risk of complicated scarring. The possibility of aesthetic sequelae should be considered in the overall burden of mpox infection. Close follow-up of those patients will help in distinguishing between complicated healing and longterm sequelae. Local treatments need further investigation.

Acknowledgments: we would like to thank the patients.

Université Paris Cité, Bichat, Assistance Publique -Hôpitaux de Paris -Claude-Bernard University Hospital, Department of dermatology, Paris, France Orcid numbers: https://orcid.org/0000-0003-0062-1184 (C. Bertin) https://orcid.org/0000-0002-1533-544X (H.Tarhini) https://orcid.org/0000-0002-2495-9406 (M. Rahi) https://orcid.org/0000-0001-7843-8895 (L.Deconinck) https://orcid.org/0000-0003-2610-7562 (S. Perrineau) https://orcid.org/0000-0002-0127-405X (M. Merlant) https://orcid.org/0000-0003-2914-959X (J. Ghosn) https://orcid.org/0000-0003-1166-1958 (N. Peiffer-Smadja)

Authors:

Chloé Bertin 1,2 , Hassan Tarhini 2 , Mayda Rahi 2 , Laurène Deconinck 2 , Ségolène Perrineau Conflicts of interest: 'none to declare'.


Correct, Fast LR(1) Unparsing

François Pottier

Inria Paris

We describe an extension of the LR(1) parser generator Menhir with new features that aim to facilitate unparsing, that is, transforming abstract syntax trees back into text. Our method supports non-LR(1) grammars decorated with precedence declarations and guarantees correct unparsing, by which we mean that parentheses or other disambiguation symbols are inserted where necessary. Furthermore, it allows the user to control other aspects of the unparsing process, such as layout. Our contributions include a novel view of unparsing as a composition of several successive transformations; the novel concept of disjunctive concrete syntax trees (DCSTs); a fast algorithm that converts DCSTs to ordinary concrete syntax trees (CSTs), thereby deciding where disambiguation symbols must be inserted; and the automated generation of safe APIs for the construction of DCSTs and deconstruction of CSTs.

In the beginning were the words, and the words were trees, and the trees were words.

Kats, Visser and Wachsmuth [START_REF] Lennart | Pure and declarative syntax definition: Paradise lost and regained[END_REF] Broadly speaking, parsing transforms text into a tree-structured representation; unparsing is the opposite transformation. Whereas parsing is a challenging problem, which has been heavily studied in the last sixty years [START_REF] Grune | Parsing techniques: a practical guide[END_REF], unparsing has received little attention, if any at all. At first, this may seem natural. Whereas parsing aims to discover tree structure, unparsing destroys this structure-what could possibly be easier?

One must recall, however, that parsing usually includes a transformation of parse trees into abstract syntax trees (ASTs). This transformation typically destroys information, such as the placement of parentheses or other syntactic delimiters. Unparsing must reconstruct this information. Thus, unparsing is not so easy after all, and it is possible to get it wrong. An incorrect unparser might insert too few parentheses and emit a sequence of tokens that does not have the intended meaning.

Parsing and unparsing in multiple steps Parsing is traditionally decomposed into multiple steps, recalled in in Figure 1: 1. A stream of characters is lexed, i.e., turned into a stream of tokens.

2. The stream of tokens is grown, i.e., turned into a concrete syntax tree (CST).

3. The concrete syntax tree is interpreted, i.e., turned into an abstract syntax tree (AST).

Step 2 alone, or the combination of steps 2 and 3, are often referred to as "parsing". We reserve "parsing" to refer to the composition of steps 1, 2, and 3. Concrete syntax trees are also known as "parse trees".

In the OCaml world, step 1 is usually performed with the help of a lexer generator, such as ocamllex. Steps 2 and 3 are performed with the help of a parser generator, such as Menhir [START_REF] Pottier | The Menhir parser generator[END_REF]. The latter two steps are usually combined: the grammar is decorated with semantic actions that indicate how to transform CSTs into ASTs, so the generated parser transforms a stream of tokens directly into an AST, without building a CST. We propose to decompose unparsing into several steps, also shown in Figure 1: 4. An AST is first described, i.e., turned into a disjunctive concrete syntax tree (DCST). This step must be programmed by the user ( §1, §2). A DCST may contain disjunction nodes. They allow the user to indicate that a subtree admits multiple descriptions, e.g., without or with surrounding parentheses. In the next step, a choice between these descriptions must be made. 5. This DCST is settled, i.e., turned into a CST c. This step is performed by an algorithm that we provide ( §3). This algorithm settles every choice: at every disjunction node, it decides which subtree must be used. This algorithm provides a correctness guarantee: it chooses a CST c such that the round-trip property grow (fringe(c)) = c holds. It fails if it is unable to satisfy this property. 6. The CST is formatted, i.e., turned into a data structure that may include layout information. The documents offered by the PPrint library [START_REF] Pottier | The PPrint pretty-printing library[END_REF] are an example of such a data structure. We provide a default implementation of this step in the form of a visitor class for CSTs ( §4). By overriding selected methods, the user can modify the default behavior and express a custom layout policy. 7. The document is rendered, i.e., turned into a string. This step is performed by the PPrint library or by whichever layout library the user chooses to rely upon. It is up to the user to ensure the correctness of the steps that she implements. The correctness of describe is expressed by the equation interpret • settle • describe(t) = t, where t is an AST. The correctness of format and render is expressed by grow • lex • render • format(c) = c, where c is a CST. Ensuring that this property holds requires some care; for instance, it may require sometimes inserting whitespace between two consecutive tokens. 5 Contribution We describe an extension of Menhir with new facilities for unparsing:

• a DCST construction API (a set of constructor functions), generated, for use in step 4;

• the settlement algorithm, written once and for all, which performs step 5;

• a CST deconstruction API (a visitor class), generated, for use in step 6.

By decomposing unparsing into several steps, we give the user the freedom to control or customize certain steps. The tasks that we leave to the user include programming step 4 and customizing step 6 insofar as desired. We do not attempt to automate these tasks. Automating step 4 would amount to automatically reversing the semantic actions. Removing the need or the ability to customize step 6 would require giving the user some other way of expressing a layout policy. We have not explored these avenues, but others have ( §5).

A correctness guarantee Because we let the user implement or customize steps 4 and 6, we cannot guarantee that these steps are correct. Thus, we cannot guarantee an end-to-end round-trip property of the form parse(unparse(t)) = t, where t is an AST. Still, we can and do guarantee a more restricted property, namely the correctness of step 5, which converts a DCST to a CST. We guarantee that this step always produces a viable CST, where a CST c is viable if the round-trip property grow (fringe(c)) = c holds.

The function fringe maps a CST to its fringe, a sequence of tokens. The partial function grow , which models a deterministic parser, transforms a sequence of tokens into a CST. Thus, the equation grow (fringe(c)) = c means that it is safe to display the CST c in the form of the sequence of tokens fringe(c): there is no danger that this sequence might be rejected or misread as a different CST.

The reverse round-trip property fringe(grow (s)) = s states that if the parser accepts the sentence s and constructs a CST c then the fringe of this CST is s. This means that grow is a correct parser. We expect this property to hold, but it is not the focus of this paper.

The reader may wonder: are there non-viable CSTs? and could one fuse steps 4 and 5 and let the user implement a direct transformation of ASTs to CSTs? Our answer is two-fold:

• If the grammar is in the class LR(1) [START_REF] Knuth | On the translation of languages from left to right[END_REF][START_REF] Grune | Parsing techniques: a practical guide[END_REF] then every concrete syntax tree is viable. In this special case, we could trust the user to implement a transformation of ASTs into CSTs, as there is no danger that the user might build a non-viable CST. • If the grammar is not in this class then the deterministic parser that is constructed by Menhir, after resolving LR(1) conflicts, is incomplete: there exist well-formed CSTs that the parser will never produce. In other words, the function grow is not surjective. As a result, there exist non-viable CSTs: if a CST c lies outside the range of grow , then grow (fringe(c)) = c cannot hold. Furthermore, it is difficult to tell which CSTs are viable and which are not viable: this requires detailed knowledge of the LR(1) automaton and of the manner in which conflicts have been resolved, perhaps under the influence of user-provided precedence declarations. Therefore, we do not trust the user to build CSTs: she might, by mistake, construct non-viable CSTs. Our approach, then, is to ask the user to build DCSTs. Thanks to disjunction nodes, a single DCST represents a family of many possible CSTs. Each member of this family may or may not be viable. It is then up to our settlement algorithm to choose a viable CST, if there exists one, among this family. The algorithm has access to a description of the LR(1) automaton and can therefore determine which CSTs are viable.

In other words, one could say that we let the user indicate where parentheses may be inserted, and we decide where to actually insert parentheses so as to ensure viability.

We do not guarantee optimality, that is, minimal use of parentheses. Instead, we offer a biased disjunction: our settlement algorithm favors the left branch. In most real-world scenarios, this lets the user achieve optimality simply by building disjunction nodes whose meaning is: "first, try displaying the subtree d without parentheses; if this is not permitted, display d surrounded with parentheses". In such a disjunction node, the subtree d is shared between the two disjuncts. Thus, although "T" stands for "tree", DCSTs are often DAGs.

If the grammar is in the class LR(1), then the user typically constructs DCSTs that do not contain any disjunction nodes ( §1). These DCSTs are also CSTs, and, because in this case every CST is viable, they are viable CSTs. Then, the settlement algorithm behaves as the identity function.

Settlement algorithms

We discuss two settlement algorithms, both of which we have implemented. One algorithm is complete: if the DCST d, viewed as a family of CSTs, contains at least one viable member, then settle(d) must succeed. This algorithm, which exploits memoization, has linear time and space complexity in the size of the DAG d, where the constant factor depends on the sizes of the alphabet and automaton. Unfortunately, in practice, it is slow. The other algorithm is simpler, much faster in practice, and has linear time complexity in the tree size of d, which we define below. However, it is incomplete: under certain conditions, it can fail even though the family d contains a viable CST.

Definitions We fix a context-free grammar [START_REF] Grune | Parsing techniques: a practical guide[END_REF]. We write a, b for terminal symbols and A for a nonterminal symbol. We write s for a sentence (a string of tokens) and α for a sentential form (a string of terminal or nonterminal symbols). We write κ for a token. We assume that there is a mapping sym of tokens to terminal symbols.

A concrete syntax tree (CST) is a tree whose nodes are terminal nodes, labeled with a token κ, or nonterminal nodes, labeled with a production A → α. A terminal node has no children. A nonterminal node has children whose number and head symbols must match α. Thus, c ::= T κ | N (A → α, ⃗ c ). The head symbol of a CST c, written head (c), is defined by the equations head (T κ) = sym(κ) and head (N (A → α, ⃗ c )) = A.

A disjunctive concrete syntax tree (DCST) may have binary disjunction nodes: thus,

d ::= T κ | N (A → α, ⃗ d ) | d ∨ d.
The two children of a disjunction node d 1 ∨ d 2 must have the same head symbol, which is considered the head symbol of the disjunction node:

head (d 1 ∨ d 2 ) = head (d 1 ) = head (d 2 ).
A DCST d represents a family of CSTs; we write c ∈ d when the CST c is a member of this family.

A DCST can be represented as a DAG in memory. We write #d for the DAG size of d, that is, for the number of vertices involved in its representation as a DAG. We write |d| for the tree size of d. This function is defined by

|T κ| = 1, |N (A → α, ⃗ d )| = 1 + Σ| ⃗ d|, and |d 1 ∨ d 2 | = max(|d 1 |, |d 2 |). Thus, |d| is the maximum size of a CST c such that c ∈ d.
1 Working with a Conflict-Free Grammar A simple grammar, expressed in Menhir's syntax, appears in Figure 3. This grammar describes arithmetic expressions that include integer literals, additions, multiplications, and parenthesized subexpressions. This grammar is stratified: three syntactic categories, also known as nonterminal symbols, are distinguished. A factor is either an integer constant or a parenthesized expression; a term is either a factor or the multiplication of a term and a factor; an expression is either a term or the addition of an expression and a term. Menhir accepts this grammar without reporting any conflict: this guarantees that this grammar is in the class LR(1), therefore is unambiguous.

To see intuitively why this grammar is unambiguous, we suggest this exercise: construct a CST whose fringe forms the token sequence INT(1); ADD; INT(2); MUL; INT(3), which corresponds to the characters 1+2 * 3. The reader will find that there exists only one such tree, namely the one shown in Figure 4a.

In the grammar of Figure 3, the productions carry semantic actions that construct ASTs. ASTs form an algebraic data type whose definition appears in Figure 2. ASTs do not keep track of parentheses: the semantic action for the production factor: LPAR; expr; RPAR (line 12) does not construct an AST node.

An unusual feature of the grammar in Figure 3 is that each production is assigned a unique name via a @name attribute. These names are used in the construction of data constructor names and method names in the generated APIs for DCSTs and CSTs. The reader may wish to peek ahead at Figures 5 and13.

The code in Figures 2 and3 is written by the programmer. Throughout the paper, hand-written code is shown on a green background, whereas code generated by Menhir appears on a yellow background. Transforming ASTs to CSTs As explained earlier, we propose to break down "unparsing" into several steps. The first two steps, namely steps 4 and 5, aim to transform an AST t into a CST c. Given an AST t, the problem is to construct a CST c that corresponds to t.

| i = INT { EConst i } [@name const] | LPAR; e = expr; RPAR { e } [@name paren] term: | f = factor { f } [@name factor] | t = term; MUL; f = factor { EBinOp (t, BMul, f) } [@name mul] expr: | t = term { t } [@
Writing interpret A for the transformation of CSTs to semantic values that is defined by the semantic actions, the problem can be stated as follows:

Given a semantic value t for a nonterminal symbol A, produce a CST c whose head symbol is A, such that interpret A (c) = t.

When the grammar is in the class LR(1), there is no danger of picking a non-viable CST c, that is, a CST whose fringe is rejected by the parser or understood by the parser as a different CST c ′ . 1 A simple and safe way of implementing the transformation of ASTs to CSTs is as a family of mutually recursive functions whose structure mirrors the structure of the grammar. For each nonterminal symbol A, one writes a function, also named A, whose specification is the one given above: this function transforms an AST t into a CST c whose head symbol is A while respecting the constraint interpret A (c) = t.

By following this pattern, for the stratified grammar of Figure 3, it is straightforward to implement a correct and optimal transformation of ASTs to CSTs. The code is shown in Figure 6. Technically, this code transforms ASTs into DCSTs that do not contain any disjunction nodes. Thus, it implements step 4 of Figure 1. Step 5 in this case is trivial-it is essentially the identity function-and is performed by Menhir's settlement algorithm ( §3).

A DCST Construction API The code in Figure 6 relies on a strongly-typed API for constructing DCSTs, offered by the module DCST, whose signature is shown in Figure 5. This module is generated by Menhir based on the grammar in Figure 3.

The module DCST offers a family of abstract types of DCSTs. For each nonterminal symbol A, there is an abstract type, also named A, of DCSTs whose head symbol is A. Furthermore, for these abstract types, the module DCST offers a family of constructor functions. For each production, there is a constructor function, whose name is determined by the production's @name attribute. This constructor function takes parameters whose number and types match the right-hand side of the production. This explains why the constructor const, which corresponds to the production factor: INT, takes one argument of type int. If a parameter corresponds to a terminal symbol that does not carry a semantic value, such as LPAR or RPAR, then this parameter is omitted. This explains why the constructor paren, which corresponds to the production factor: LPAR; expr; RPAR, takes just one argument of type expr. Furthermore and finally, for each nonterminal symbol A, there is a constructor function that constructs a disjunction node. These functions are named factor _ choice, term _ choice, expr _ choice, etc. The code in Figure 6 does not use these functions; their use is illustrated in the next section ( §2).

The module DCST allows constructing DCSTs but offers no way of deconstructing or inspecting a DCST. The only way of doing anything useful with a DCST is to convert it to a CST. This is done by the settlement algorithm ( §3).

Transforming ASTs to CSTs-More Comments Let us momentarily come back to the transformation in Figure 6. The code is straightforward. At each level A of the grammar, if the AST node at hand can be directly represented by a DCST constructor for the nonterminal symbol A, then this constructor is used; otherwise a recursive call to the next lower level is performed. A recursive call from the lowest level (factor) back to the highest level (expr) is made possible by the constructor DCST.paren (line 3), which corresponds to the production factor: LPAR; expr; RPAR.

The functions in Figure 6 always construct well-formed DCSTs. This property is enforced by the strongly-typed API of the module DCST. If the programmer mistakenly attempted to construct an ill-formed tree, this would be detected by the OCaml type-checker. For instance, attempting to call the function expr or factor in a position where one must call term would give rise to a static type error. This is a pleasant and valuable guarantee.

Working with Conflicts and Precedence Declarations

In practice, people commonly work with grammars that lie outside the class LR(1). Indeed, manually refactoring a grammar so as to fit in the class LR(1) is usually unpleasant, sometimes difficult, and can lead to a blow-up in the size of the grammar. Instead, following an approach first suggested by Aho, Johnson and Ullman [START_REF] Aho | Deterministic parsing of ambiguous grammars[END_REF] and first implemented in yacc [START_REF] Johnson | Yacc: Yet another compiler-compiler[END_REF], people often prefer to keep a non-LR(1) grammar and annotate it with precedence declarations. When building an LR(1) automaton for such a grammar, the parser generator encounters conflicts, that is, situations where several actions are possible, such as "shift", "reduce production p 1 ", and "reduce production p 2 ". The parser generator exploits precedence declarations to statically resolve conflicts: at parser construction time, in each situation where several actions are possible, at most one action is chosen. Thus, a deterministic LR(1) automaton is obtained. 2This automaton is a correct parser, but, because some legitimate actions have been removed, it is incomplete: there exist CSTs that it cannot construct. In other words, there exist non-viable CSTs. The trees shown in Figure 9 are examples: the parser will never construct them. As explained earlier, we do not trust the user to write a correct transformation of ASTs into viable CSTs. Indeed, because the user usually does not have good knowledge and understanding of the LR(1) automaton, it seems extremely difficult for her to ascertain that only viable CSTs are ever constructed. Instead, our approach is to ask the user to implement a transformation of ASTs into DCSTs and to provide an algorithm that transforms DCSTs into viable CSTs.

An Ambiguous Grammar and its Automaton This approach is illustrated by the grammar in Figure 7. This grammar does not distinguish several subcategories of expressions, such as factor, term, and expr: there is a single nonterminal symbol expr. This grammar is ambiguous. The precedence declarations on lines 7 and 8 indicate how to resolve the conflicts that appear when an LR(1) automaton for this grammar is constructed.

The LR(1) automaton that corresponds to this decorated grammar is shown in Figure 8. The vertices of this graph are the states of the automaton. Each state is identified by a number (in blue). Each state (except state 0, which is the initial state) also carries an incoming symbol (in red). This terminal or nonterminal symbol is in fact the label of every edge that enters this state. Edges labeled with a terminal symbol are shown as plain edges; edges labeled with a nonterminal symbol are dashed. Thus, starting in state 0, following the path labeled with expr; ADD; expr leads to state 8. State 8 is the only state where the automaton's behavior depends on the lookahead symbol, that is, on the first unconsumed token of the input stream. If this symbol is MUL then the automaton consumes this symbol and follows the transition from state 8 to state 5. This is known as "shifting". If this symbol is ADD, RPAR, or EOL, then the automaton does not consume this symbol, and reduces the production expr: expr; ADD; expr. 3 This means that the automaton moves back by three steps, thereby going back to state 0 or to state 1, depending on its history, which is stored in its stack. There, it follows a transition labeled with the left-hand side of this production, namely expr, thereby reaching state 10 or state 3. This is known as taking a "goto" transition.

For the purposes of this paper, it does not matter how precedence declarations are used to resolve conflicts, because our settlement algorithm ( §3) relies on a description of the deterministic LR(1) automaton and does not care how this automaton is constructed. Nevertheless, let us briefly explain the effect of the precedence declarations in Figure 7.

The declaration %left ADD suggests that "addition is left-associative". Technically, this implies that in state 8, when the lookahead symbol is ADD, reduction must be preferred over shifting. Thus, because of the precedence declaration, a transition labeled ADD out of state 8, which could have existed, is suppressed. As a result, after reading 1 + 2, if the next input symbols are + 3, then the parser constructs an AST for the subexpression 1 + 2 and considers this subexpression as the first operand of the addition _ + 3.

Similarly, the declaration %left MUL implies that in state 6, when the lookahead symbol is MUL, reduction must be preferred over shifting. This causes the removal of a transition Finally, the order in which the two %left declarations appear suggests that "MUL takes precedence over ADD". Technically, this implies that in state 8, when the lookahead symbol is MUL, shifting must be preferred over reduction, and that in state 6, when the lookahead symbol is ADD, reduction must be preferred over shifting. This causes the removal of a reduction action in state 8 and the removal of a transition labeled ADD out of state 6. Thus, for example, the text 1+2 * 3 gives rise to the concrete syntax tree depicted in Figure 4b.

Translating ASTs to DCSTs As in the previous section ( §1), for the grammar of Figure 7, Menhir generates a module DCST, whose interface is shown in Figure 10. By relying on this API, the user is expected to implement a transformation of ASTs to DCSTs. Such a transformation appears in Figure 11. The main point of interest resides in the use of possibly _ paren at line 5. Using the constructor function DCST.expr _ choice, this auxiliary function constructs a disjunction node whose children are e and DCST.paren(e). Thus, it expresses the fact that there is a choice between displaying the subtree e without parentheses and displaying it surrounded with parentheses.

This code constructs DCSTs that are analogous to the one shown in Figure 12a. There, a binary disjunction node is identified by the label expr?. This DCST is a DAG: some internal nodes are reachable via multiple paths. Because this DCST involves two disjunction nodes, it can be viewed as a compact description of a family of four different CSTs. Some members of this family are viable CSTs; some are not. For instance, the concrete syntax tree shown in Figure 12b is a viable member of this family: it is obtained by choosing the left child of the outermost disjunction node and the right child of the innermost disjunction node. On the other hand, the concrete syntax tree in Figure 9b, which is obtained by choosing the Let us say that a DCST is viable if at least one of the CSTs that it describes is viable. In our approach, it is up to the user to construct a viable DCST. The code in Figure 11 does this. Indeed, by using possibly _ paren at every AST node, this code allows parentheses to be inserted at every node, and it is intuitively clear that if parentheses are inserted everywhere then a viable CST is obtained. If for some reason the user constructs a DCST that is not viable (for example, by forgetting to use possibly _ paren at line 5) then the settlement algorithm ( §3) fails. So, such a mistake is detected; however, it is detected only at runtime.

Settling Choices

The distinction between DCSTs and CSTs, and the settlement algorithm, which offers a bridge between these concepts, are the key technical contributions of this paper.

API The API of the settlement algorithm appears in Figure 14. The type of the function Settle.main reflects the purpose of this algorithm: it transforms a DCST whose head symbol is the start symbol main into some viable CST whose head symbol is also main. If it cannot do so, it reports a failure by returning None.

The API of the module CST is shown and discussed in the next section ( §4). Let us point out that the type CST.main is abstract, so the user has no way of constructing CSTs besides invoking Settle.main. As a result, every value of type CST.main must be a viable CST.

Viability Relative to a Context Our discussion so far has relied on a simple abstract model of parsing, and our definition of viability has been based on this model. We have modeled a deterministic parser as a partial function grow: if s is a sequence of tokens then grow (s) is either undefined or a CST. Then, we have written that a CST c is viable if and only if the round-trip property grow (fringe(c)) = c holds. This models how a parser behaves both on the input that the parser has read before reaching this segment, which is summarized by the automaton's current state, and on the lookahead symbol, that is, on the first input symbol that lies beyond this segment. Therefore, when looking at a CST c that is intended to correspond to a segment of the input, it does not make sense to ask whether this CST is "viable" without any qualification. Instead, one should ask whether c is viable with respect to a certain state q and a certain lookahead symbol b. This notion can be defined as follows:

Definition 1 (Relative Viability). A CST c is viable with respect to (q, b) iff for every stack σ such that cur (σ) = q and for every nonempty sentence κ • s such that sym(κ) = b, the automaton, beginning with the stack σ and the remaining input fringe(c) • κ • s, reaches (in zero or more steps) the stack σ • (q ′ , c) and the remaining input κ • s.

In this definition, because the stack σ • (q ′ , c) must correspond to a path in the automaton's state diagram, the state q ′ must be the target of a transition labeled head (c) out of q. Therefore, for c to be viable with respect to (q, b), it is necessary that there exist a transition labeled head (c) out of q.

In short, c is viable with respect to (q, b) if and only if the automaton, beginning in state q and faced with the fringe of c followed with the lookahead symbol b, consumes precisely this fringe and constructs precisely the tree c, which it pushes onto its stack.

Our earlier notion of "viability" without qualification corresponds to viability with respect to the automaton's initial state q 0 and sentinel symbol #.

Suppose c is a nonterminal node N (A → α, ⃗ c ). If c is viable with respect to (q, b) then the following two facts must be true: (1) out of the state q, there exists a path, whose edge labels form the string α, to some state q ′ ; (2) in state q ′ , with lookahead symbol b, the automaton is willing to reduce the production A → α. When both conditions are satisfied, we say that A → α is apparently viable with respect to (q, b). This is a necessary condition for c to be viable with respect to (q, b).

Compositional Specification of a Settlement Algorithm A compositional settlement algorithm solves problems of the form (d, q, b) where d is a DCST, q is a state, and b is a terminal symbol. A solution to such a problem is a CST c such that c ∈ d and c is viable with respect to (q, b). A settlement algorithm can also return ⊥, which represents a failure. Because a solution can exist only if the state q has an outgoing transition labeled head (d), we restrict our attention to problems that satisfy this condition. A complete algorithm fails only when no solution exists; an incomplete algorithm can fail even if a solution exists.

An Eager Settlement Algorithm A linear-time, incomplete settlement algorithm settle can be described as follows. Assume the problem is (d, q, b), where q has an outgoing transition labeled head (d). Then, compute settle(d, q, b) as follows:

1. If d is a terminal node T κ, return this terminal node.

2. If d is a nonterminal node N (A → α, ⃗ d ′ ), a) Verify that A → α is apparently viable with respect to (q, b). If not, fail. b) Settle each of the subtrees ⃗ d ′ , from right to left, via recursive calls to settle, yielding a sequence of CSTs ⃗ c ′ . Then, return the nonterminal node

N (A → α, ⃗ c ′ ). 3. If d is a disjunction node d 1 ∨ d 2 , where d 1 is a nonterminal node N (A → α, ⃗ d ′ ), a) If A → α is apparently viable with respect to (q, b) then return settle(d 1 , q, b); b) otherwise return settle(d 2 , q, b).
More explanations about step 2b are needed. The check in step 2a guarantees that there exists a path out of the state q whose edge labels form the string α. This is also the string of the head symbols of the subtrees ⃗ d ′ . The source states of the edges along this path are the states that must be used in the recursive calls to settle. A key remark is that these states are known before any of the recursive calls takes place. So, there is no requirement that the recursive calls be performed from left to right. We perform them from right to left, which is crucial, because the result of settling a subtree is needed to compute the lookahead symbol that must be used while settling the next subtree towards the left. Formally, if the sequence

⃗ d ′ is decomposed as ⃗ d ′ 1 • d ′ • ⃗ d ′ 2
, and if settling ⃗ d ′ 2 has produced ⃗ c ′ 2 , then the lookahead symbol that must be passed as an argument to the next recursive call, settle(d ′ , -, -), is the first element of the nonempty sequence sym(fringe(⃗ c ′ 2 )) • b. In step 3, we assume that the left disjunct d 1 is a nonterminal node. This causes no loss of generality. Indeed, a disjunction node whose disjuncts are terminal nodes is pointless; and a disjunction node whose left-hand child is itself a disjunction can be re-associated.

This algorithm is correct: assuming that q has an outgoing transition labeled head (d), if settle(d, q, b) returns c then c ∈ d holds and c is viable with respect to (q, b).

This algorithm runs in time O(|d|), that is, in linear time in the tree size of the DCST d. In steps 3a and 3b, it is crucial that settle is recursively applied to d 1 or d 2 , but not both. Thus, even if d 1 and d 2 share a subtree, this subtree is examined only once by the algorithm. The tests in steps 2a and 3a can be carried out in constant time, provided certain tables are precomputed. In step 2b, in order to efficiently compute the lookahead symbol that must be passed to each recursive call, it is convenient to adopt the convention that settle(d, q, b) returns not only a CST c, but also the first symbol of the sequence sym(fringe(c)) • b.

This algorithm is unfortunately incomplete. The source of incompleteness lies in step 3a. The apparent viability condition in step 3a is necessary for the recursive call settle(d 1 , q, b) to succeed, but does not guarantee that this call will succeed. If this call fails, then settle(d 1 ∨ ⃗ d 2 , q, b) fails as well, even though the subproblem (d 2 , q, b) may have a solution. In other words, the algorithm is incomplete because it commits to the left-hand disjunct as soon as the apparent viability test succeeds, even though apparent viability does not imply viability. Completeness can be obtained by adding a backtracking mechanism: in step 3a, if settle(d 1 , q, b) fails, then return settle(d 2 , q, b). With this modification, the algorithm is complete, but has exponential time complexity, because d 1 and d 2 can (and usually do) share subtrees (recall Figure 12a).

A Memoizing Settlement Algorithm A complete settlement algorithm whose worstcase time complexity is polynomial can be given. This algorithm decomposes the original problem into subproblems of the form (d, q, a, b). A solution of such a subproblem is a CST c such that c ∈ d and c is viable with respect to (q, b) and the first symbol of fringe(c) • b is a. Memoization ensures that each subproblem is considered at most once. Compared with the eager algorithm, this algorithm requires a more complex internal representation of DCSTs: every DCST node must carry a unique identifier, and its "nullable" flag and "first" set must be precomputed. An apparent viability test is not needed, but can be used to speed up this algorithm.

Because this algorithm spends constant time and constant space on each subproblem, its time and space complexity is the number of subproblems that can ever be considered. Thus, in the worst case, it is O(#d.|Q|.|Σ|

2 ), where #d is the DAG size of the DCST d, |Q| is the number of states of the LR(1) automaton, and |Σ| is the number of terminal symbols. In practice, we expect that for each node d ′ in the DAG d, the number of subproblems (d ′ , q, a, b) that are ever considered is independent of the size of the alphabet and of the size of the automaton. We have experimentally confirmed this expectation: for the grammar of Figure 7, we find that in practice this number is at most 3. Therefore, the time and space complexity of this algorithm is effectively linear in #d.

Comparing Settlement Algorithms We have implemented both algorithms and performed a limited evaluation of their performance, based on the grammar of Figure 7 and on randomly-generated arithmetic expressions. As expected, both algorithms exhibit linear time complexity. The eager algorithm appears to be much faster in practice: taking into account both DCST construction time and settling time, the eager algorithm outperforms the memoizing algorithm by a factor of 15. We believe that the high cost of the memoizing algorithm is due, to a large extent, to memoization itself: even if the cost of solving subproblems is discounted, the cost of storing and fetching data in and out of a large hash table seems very high.

Choosing an Algorithm In summary, the eager algorithm is fastest, but incomplete; the memoizing algorithm is complete, but significantly slower; and the eager algorithm with backtracking is complete and usually fast, but can be exponentially slow in pathological cases. At the time of writing, Menhir offers the eager algorithm only. This could change in the future, based on user feedback.

To what extent could the incompleteness of the eager algorithm be a problem in practice? We do not know yet. For the grammar of Figure 7, it is not a problem: indeed, for this simple grammar, apparent viability implies viability. However, this implication is not obvious. Furthermore, we have constructed more complex grammars where this is not the case. More experience is required to tell whether users are likely to face difficulties caused by incompleteness.

The eager algorithm is not optimal: it does not necessarily produce the smallest viable CST c such that c ∈ d. Instead, in every disjunction node, it favors the left disjunct. The code in Figure 11 relies on this behavior: at line 2, the left disjunct proposes not to insert parentheses, while the right disjunct inserts parentheses. Thus, in this simple example, optimality is achieved anyway. Regarding the memoizing algorithm, we believe that there are two variants of it: a left-biased variant, which we have implemented, and an optimal variant, which we have not implemented, and which we imagine will be slightly more expensive.

Formatting and Rendering

Once a (viable) CST has been constructed, there remains to transform it into a printable form, such as string or a PPrint document. This corresponds to steps 6 and 7 in Figure 1.

To allow this, we could expose an API that allows deconstructing CSTs, and let the user implement this transformation entirely on her own. We could for instance present the types CST.expr and CST.main as private algebraic data types, that is, algebraic data types whose values can be inspected via match constructs, but cannot be constructed. However, this approach would have two drawbacks. First, it would leave to the user the rather dreary task of implementing step 6, whereas one might expect this task to be performed by generated code. Second, it would force us to expose a grammar-specific representation of CSTs in memory, thereby preventing us from internally using a different, grammar-independent representation, or forcing us to transform one representation into the other.

Visitors to the Rescue Our solution to these problems is to present CST.expr and CST.main as abstract types and to generate code for step 6 in such a form that the behavior of this code can be customized. Indeed, not everything about step 6 is mechanical. For one thing, we wish to let the user pick the return type of this transformation: strings, PPrint documents, or some other type of her choosing. Furthermore, should the user decide to produce PPrint documents, we wish to let her customize the layout of these documents: she must decide where and how to use the document-construction combinators offered by the PPrint library, which offer fine-grained control over indentation, line breaks, and so on. To allow customization, we generate a visitor class whose methods reduce a CST to a printable representation. For the grammar of Figure 7, this API is shown in Figure 13.

The module CST, whose code is generated by Menhir, advertises expr and main as abstract types. Then, it advertises a visitor class, reduce. This class is parameterized by a type 'r , which is the result type of every method: it is the type of the printable form to which every tree must be reduced. The user is expected to provide implementations for the three virtual methods zero, cat, and text. In short, zero is the empty printable thing; cat concatenates printable things; and text converts a string to a printable thing. Furthermore, the following methods exist:

• For each terminal symbol, there is a visitor method: these include visit _ INT, visit _ ADD, and so on. If the terminal symbol carries no semantic value and if a "token alias" (a concrete string) has been provided by the user for this symbol (Figure 7) then a default implementation of this method is generated by Menhir; this default implementation relies on the method text. Otherwise, this method is declared virtual. • For each nonterminal symbol, there is a visitor method: these are visit _ expr and visit _ main. These methods expect a CST as an argument, perform a case analysis of the root node, and apply a suitable case method to the children of the root node. • For each production, there is a visitor method: these include case _ paren, case _ const, and so on. These methods expect zero, one, or more arguments. First, each argument is reduced to a printable thing via recursive calls to suitable visit methods; then these printable things are concatenated using zero and cat.

Examples of Use Figure 15 shows how a user may rely on the class CST.reduce to convert CSTs to strings. The user defines a new class, print, which inherits reduce where the type parameter 'r is instantiated with string. Then, the user supplies trivial implementations of the methods zero, cat, and text: the empty string, string concatenation, and the identity function. Finally, the user provides implementations of the virtual methods visit _ INT and visit _ EOL. 4 Then, the method call (new print)#visit _ main converts a CST to a string. 5Figure 16 shows how a user may rely on the class CST.reduce to convert CSTs to PPrint documents. The idea is the same. This time, the type parameter 'r is instantiated with the type PPrint.document. The document construction combinators offered by PPrint are used in a few key places. For example, by overriding the method visit _ expr, the user indicates that a group combinator, which offers a choice between flat and non-flat output, should be used at every subexpression. By overriding the method case _ paren, the user customizes the manner in which parenthesized subexpressions are indented. An example of the output produced by this code appears in Figure 17.

Related Work

van den Brand and Visser [START_REF] Van Den Brand | Generation of formatters for contextfree languages[END_REF] describe a tool that generates "formatters" (that is, unparsers and pretty-printers) for ASF+SDF grammars. An ASF+SDF grammar is a context-free grammar, augmented with priority and associativity declarations. It does not have semantic actions, but a production can be marked with the attribute bracket, which means that no AST node must be produced. Thus, an unparser must decide where to insert parentheses. van den Brand and Visser spell out the round-trip property that a correct unparser must obey. They provide a brief description of a (linear-time, bottom-up) unparser of arithmetic expressions, but do not describe how they deal with the general case. They separate unparsing and layout in the same way as we do ( §3, §4).

Ramsey [START_REF] Ramsey | Unparsing expressions with prefix and postfix operators[END_REF] offers a detailed presentation of a (linear-time, bottom-up) unparser. The design and correctness proof of his algorithm are guided by thinking about the behavior of a shift-reduce parser. This is also the case in this paper: in fact, at runtime, our settlement algorithm relies directly on the parser's tables. Ramsey supports a single syntactic category of "expressions" with infix, prefix, and postfix operators whose precedence and associativity are specified by the user. We deal with the more general case of an arbitrary LR(1) automaton, yet our eager settlement algorithm is arguably simpler than Ramsey's unparser. Our eager algorithm is incomplete in general, but we believe that it is complete in the restricted setting considered by Ramsey. We sketch (and have implemented) a slower, complete algorithm.

Bouwers, Bravenboer, and Visser [START_REF] Bouwers | Grammar engineering support for precedence rule recovery and compatibility checking[END_REF] regret that the style of precedence declarations supported by most LR(1) parser generators, including yacc, bison, and Menhir, does not have a clear semantics. To clarify this semantics, and to help compare two parsers that are based on different methodologies, they propose "a core formalism for defining precedence rules", based on "tree patterns" of bounded depth. They describe a "precedence rule recovery tool", which tests whether a parser, viewed as a black box, can or cannot construct certain tree patterns. Thanks to this tool, they discover discrepancies between several parsers for C99 and PHP5. The question that their tool answers, "can this parser possibly construct a tree of this shape?", is closely related to the question that our settlement algorithm addresses. That said, we believe that the answer to such a question can depend on the current state of the LR(1) automaton: that is, it can be the case that in a certain state q the parser will construct a tree of a certain shape whereas in some other state q ′ it will refuse to construct a tree of this shape. Another source of worry is Bravenboer et al.'s remark that tree patterns of depth 1 are often sufficient, yet depths 2 and 3 are sometimes needed. Thus, it is not clear whether (or under what conditions) Bravenboer et al.'s tree pattern formalism is capable of accurately describing the behavior of an LR(1) parser. This open question could be related to the open question of clarifying under what conditions "apparent viability" ( §3) implies viability. Indeed, apparent viability is an inspection of the tree at depth 1.

Danielsson [START_REF] Anders | Correct-by-construction pretty-printing[END_REF] discusses the construction of pretty-printers in a dependently-typed programming language. He uses dependent types to express and enforce the end-to-end round-trip property parse(unparse(t)) = t. In contrast, we guarantee the more limited property grow (fringe(c)) = c, and we rely on (generated) abstract types to ensure that the user can construct only grammatically valid DCSTs and CSTs (see Figures 5 and6).

Several authors have investigated the idea of producing parsers and pretty-printers out of a single "invertible syntax description" [RO10, ANO12, MW13, ZZK + 16, ZKZ + 20]. This approach promises to reduce redundancy and guarantee that a round-trip property holds by construction. Our starting point in this paper is an existing parser generator that allows arbitrary semantic actions, so we cannot follow this approach.

Conclusion

We have described several new features offered by Menhir to support fast and correct unparsing. Menhir now generates type-safe, grammar-specific DCST construction and CST deconstruction APIs. A settlement algorithm, which transforms DCSTs into CSTs, is implemented once and for all in a library. Because it relies directly on a description of the LR(1) automaton, it supports arbitrary precedence declarations and all LR(1) construction methods. The concept of a DCST, as well as our settlement algorithms, are new.

The most unpleasant aspect of our approach is perhaps the need for the user to manually implement the translation of ASTs to (viable) DCSTs. In the future, it would be desirable to automate this transformation; this should be possible, provided the expressive power of semantic actions is restricted. Another limitation is the incompleteness of our fast settlement algorithm. Whether it is a problem in practice remains to be determined: we do not yet have practical experience with this new tool. In the future, we would like to allow decorating trees with user-specified data, such as comments or source code locations, so as to allow "high-fidelity" program transformations [START_REF] De | An algorithm for layout preservation in refactoring transformations[END_REF][START_REF] Rodin | High-fidelity metaprogramming with separator syntax trees[END_REF].

Figure 1 .

 1 Figure 1. From text to abstract syntax trees and back

  type binop = BAdd | BMul ( * Binary operators * ) type expr = ( * Expressions * ) | EConst of int | EBinOp of expr * binop * expr type main = expr

Figure 2 .

 2 Figure 2. Arithmetic expressions: the module AST

Figure 3 .Figure 4 .Figure 5 .Figure 6 .

 3456 Figure 3. Stratified grammar: the parser

Figure 7 .Figure 8 .Figure 9 .Figure 11 .

 78911 Figure 7. Non-stratified grammar: the grammar

Figure 12 .

 12 Figure 12. Non-stratified grammar: a DCST and one of the CSTs that it describes

Figure 15 .Figure 16 .Figure 17 .

 151617 Figure 15. Non-stratified grammar: translating CSTs to strings

  two

Suppose the grammar is in the class LR(1). Then, there exists a correct and complete parser, which we model as a partial function grow of sequences of tokens to CSTs. Let us prove that every CST c satisfies grow (fringe(c)) = c. Let c be a CST, and let s stand for its fringe. Then, s must be a grammatically valid sentence. Because the parser is complete, it must accept this sentence: grow (s) must be defined. Let us refer to this CST as c ′ . Because the parser is correct, we must have fringe(c ′ ) = s, that is, fringe(c ′ ) = fringe(c). Because the grammar is unambiguous, two distinct CSTs cannot have the same fringe: so, c ′ = c must hold. In other words, grow(fringe(c)) = c holds.

For example, at the time of writing, the precedence declarations found in the OCaml compiler's parser involve

distinct levels and resolve shift/reduce conflicts in 142 states (out of 2068 states).3 For readability, in Figure8, we write "reduce" but do not indicate which production must be reduced.This automaton is so simple that, in each state, at most one production can be reduced. We let the reader reconstruct which one.

Because Menhir does not allow a token alias to contain a newline character, the token alias "\n" cannot be associated with the symbol EOL.

This example happens to "just work" because two consecutive tokens can be safely concatenated: for this simple language of arithmetic expressions, in a grammatically valid sentence, there is no possibility for the concatenation of two tokens to be confused by the lexer with some other token. In a more complex scenario, greater care would be required. The type of printable things would be more elaborate than string, and the cat method would sometimes insert a space between two things.

François Pottier

module CST : sig type expr type main class virtual ['r] reduce : object ( * This class is used while formatting ( §4) * ) method virtual zero : 'r ( * Document construction methods * ) method virtual cat : 'r -> 'r -> 'r method virtual text : string -> 'r method virtual visit _ INT : int -> 'r ( * Visitor methods for terminal symbols * ) method visit _ ADD : 'r method visit _ MUL : 'r method visit _ LPAR : 'r method visit _ RPAR : 'r method virtual visit _ EOL : 'r method visit _ expr : expr -> 'r ( * Visitor methods for nonterminal symbols * ) method case _ paren : expr -> 'r method case _ const : int -> 'r method case _ add : expr -> expr -> 'r method case _ mul : expr -> expr -> 'r method visit _ main : main -> 'r method case _ eol : expr -> 'r end end when it is applied to a complete input. However, a less abstract and more compositional view is now needed: we must discuss how an LR(1) parser behaves when it is applied to an input fragment.

An LR(1) automaton maintains a stack, which records what input fragment has been consumed and reflects how this input fragment has been interpreted. A stack is a sequence of cells, where a cell is a pair of a state and a CST: σ ::= ϵ | σ • (q, c). In every cell (q, c), the head symbol of the CST c is also the incoming symbol ( §2) of the state q. We refer to it as the cell symbol of this cell. At every time, the stack σ forms a path in the automaton's state diagram. The stack σ determines the current state cur (σ) of the automaton: it is the state found in the top stack cell. If the stack is empty, it is the initial state.

An LR(1) automaton also maintains a remaining input, a nonempty sequence of tokens. A pseudo-token # is used as a terminating sentinel. If κ is the first element of the remaining input then sym(κ) is known as the lookahead symbol.

An LR(1) automaton makes progress via two kinds of actions. A shift action consumes a token κ and pushes the cell (q ′ , c) onto the stack, where q ′ is the target of a transition labeled sym(κ) out of the current state, and where c is the terminal node T κ. A reduce action for a production A → α first pops several cells off the stack, whose sequence of cell symbols is α, and whose sequence of CSTs is ⃗ c. It then pushes the cell (q ′ , c) onto the stack, where q ′ is the target of a transition labeled A out of the current state, and where c is the nonterminal node N (A → α, ⃗ c ). At every step, the choice of the next action is determined solely by the current state and by the lookahead symbol.

The behavior of an LR(1) automaton, when faced with a certain input segment, depends


Dr Chloé Bertin
email: chloe.bertin@aphp.fr

Anne-Lise Beaumont

Marie Merlant

Morgane Mailhe

Diane Le Pluart

Laurène Deconinck

Michael Thy

Marie Cortier

Mathilde Garé

Marion Dollat

Mayda Rahi

Véronique Joly

Sylvie Lariven

Christophe Rioux

Audrey Truong

Lydia Deschamps

Valentine Marie Ferré

Charlotte Charpentier

François-Xavier Lescure

Fabrice Bouscarat

Vincent Descamps

Yazdan Yazdanpanah

Nathan Peiffer-Smadja

Erythematous maculopapular rash in monkeypox virus infection: A retrospective case series of 30 patients

Keywords: Erythematous maculopapular rash in monkeypox virus infection: a retrospective case series of 30 patients Monkeypox, atypical dermatologic lesions, Exanthema, pharyngitis, maculopapular rash

come

Acknowledgments: The patients in this manuscript have given written informed consent to publication of their case details.

Data availability statement: the data that support the findings of this study are available on request from the corresponding author.

Conflict of interest: there are no conflict of interest

Funding source: none Dear editor, Monkeypox (MPX) is a zoonotic disease caused by an orthopoxvirus usually causing self-limiting outbreaks in Africa. Since May 2022, an unprecedented outbreak has spread globally [START_REF] Gessain | Monkeypox[END_REF]. The classical presentation of MPX disease associates fever, headache, myalgia, lymphadenopathy, sore throat and pleiomorphic skin lesions.

Typical skin lesions are papules, vesicles and pustules that ulcerate, become umbilicated and then crops.

However, the clinical presentation of MPX disease is sometimes aspecific and can mislead diagnosis [START_REF] Tarín-Vicente | Clinical presentation and virological assessment of confirmed human monkeypox virus cases in Spain: a prospective observational cohort study[END_REF][START_REF] Patel | Clinical features and novel presentations of human monkeypox in a central London centre during the 2022 outbreak: descriptive case series[END_REF]. We conducted a single center retrospective study in Paris, France, to analyze MPX patients presenting with an erythematous maculopapular rash. All patients gave oral consent to participate and the study was approved by a Research Ethics Committee. Between May 21st and July 28th 2022, 439 patients had a PCR-confirmed MPX infection in this center. Thirty patients (30/439, 6.8%) presented an erythematous maculopapular rash (Table 1 and Fig. 1). Patients were all men except one male to female transgender and 93% had sex with men. Among the 30 patients, 25 (83%) presented concomitant typical MPX vesiculopustular skin lesions and 15 (50%) presented concomitant pharyngitis (Fig. 1). Of note, 5 patients (17%) had no typical MPX skin lesions and presented only with an erythematous maculopapular rash and a pharyngitis. Rashes appeared in a median of 3.5 days [IQR 2 -6] after symptoms' onset. Dermatological examination revealed aspecific maculo-papular rashes, always affecting the trunk and sometimes extending to the limbs or face. Three patients were hospitalized: one for aphagious pharyngitis, one for blepharitis and one for phimosis with urinary retention. All rashes resolved in a few days without specific treatment. The prescription of an antibiotic therapy before the apparition of the rash was reported in 17 cases (59%), mostly amoxicillin (n=13) for suspected bacterial pharyngitis. In patients with antibiotics, the rash followed antibiotic use after a median of 1 day [IQR 1-2]. Among the 13 patients for whom EBV blood PCR was done, all had a replication. Of note, EBV blood PCR was performed in 7 patients of the center with MPX without a rash and found EBV replication in the 7 cases. Histopathologic findings were similar in the 6 patients who had a cutaneous biopsy to rule out a severe drug reaction. It consisted of a superficial lymphocytic infiltrate consistent with maculopapular exanthema of drug or viral origin. The immunohistochemical EBV marker (EBER) was always negative and there was no specific MPX histologic pattern to guide diagnosis. In this center, rashes frequency is estimated at 6.8% of MPX patients, which makes it less frequent than other recent reviews (8.0-13.7%) [START_REF] Patel | Clinical features and novel presentations of human monkeypox in a central London centre during the 2022 outbreak: descriptive case series[END_REF][START_REF] Girometti | Demographic and clinical characteristics of confirmed human monkeypox virus cases in individuals attending a sexual health centre in London, UK: an observational analysis[END_REF][START_REF] Mailhe | Clinical characteristics of ambulatory and hospitalised patients with monkeypox virus infection: an observational cohort study[END_REF]. Half the patients in this study had an association of rash and pharyngitis leading to antibiotics prescription to treat a suspected bacterial pharyngitis. MPX diagnosis may reduce the use of unnecessary antibiotic prescribing. MPX rashes could be related to different physiopathological mechanisms including an aspecific MPX cutaneous tropism or concomitant viral EBV replication with cutaneous manifestation [START_REF] Shiohara | A complex interaction between drug allergy and viral infection[END_REF][START_REF] Ónodi-Nagy | Amoxicillin rash in patients with infectious mononucleosis: evidence of true drug sensitization[END_REF]. Rashes onset in 59% of patients after antibiotic therapy might also suggest a drug reaction or an infectious mononucleosis-like antibiotic reaction [START_REF] Ishida | The dynamics of herpesvirus reactivations during and after severe drug eruptions: their relation to the clinical phenotype and therapeutic outcome[END_REF]. A primary EBV infection is much less probable even though clinical presentation can be misleading [START_REF] Ciccarese | Dermatological manifestations of Epstein-Barr virus systemic infection: a case report and literature review[END_REF]. An erythematous maculopapular rash was observed in 13 patients without prior antibiotic therapy making it a specific skin manifestation of MPX infection. Maculo-papular rashes are not uncommon in MPX. They are associated to pharyngitis in half of the cases and to typical skin lesions in 83% of the cases. In an epidemic context, MPX infection should thus be considered in patients with an erythematous maculopapular rash even without associated skin lesions.


Towards a linear functional translation for borrowing

Sidney Congard

. It preserves linearity and captures a new feature, namely lifetime bounds. This is a work in progress: in particular, translation rules are not set yet. We discuss perspectives for this work at the end of the paper.

Introduction

Rust is, like C++, a systems programming language. It has references called mutable and immutable borrows, giving respectively a read & write and a read-only access to their underlying value. The Rust type system comes with a borrow checker ensuring that they're safely used, notably that values can be either mutated or aliased (i.e. shared) through borrows, but not both at the same time. It eliminates a large class of errors, such as data races or use-after-free.

Recent works exploit this guarantee to give high-level semantics to Rust programs, to facilitate their formal verification. Among those works, most give a logical encoding of Rust programs such as Creusot [DJM22] (using prophecy variables), Verus [LHC + 23] (using ghost linear types) and Prusti [AMPS19] (using Rust types to apply some rules automatically). However, there is also Aeneas which instead translates Rust programs into pure functional programs, to embed them in proof assistants (initially F-Star, but now also Lean4, Coq and HOL4). Those works are complementary to RustBelt [JJKD18]: it also gives a semantic to unsafe code ignoring the borrow checker, but results in more difficult verification.

This paper builds upon the results of Aeneas, to propose a functional translation for a subset of safe Rust programs that handles lifetime bounds. Our version preserves the source program linearity, meaning that it doesn't duplicate or discard the borrowed values. For that, we present preliminary results centered around examples of translated programs:

• The second section "framework" presents the translation framework, starting with Rust borrow checker, Aeneas and then showing our translation.

• The third section "lifetime bounds" presents lifetime bounds and shows how the translation handles them. They aren't supported in Aeneas.

• The last section "work in progress and future perspectives" speaks about:

-The soundness and expressivity of the translation with respect to source programs.

-Effectful destructors and exceptions, leveraging the (for now unused) linearity from the translation.

-Two features that aren't supported in Aeneas: nested borrows and polymorphism.

Framework

For simplicity, our source language is a stripped-down version of safe Rust: in particular, we're removing all features that we'll confidently be able to incorporate later in the translation. That includes several features supported by Aeneas such as loops, inductive types, immutable borrows, pair projections, arrays, the ambient state monad and some syntactic sugar. Also, assertions are only used to access values and to illustrate the current program state: their interpretation in the functional language doesn't matter. Finally, polymorphism is restricted to types without borrows: this limitation is discussed in the last section. In the rest of this paper, "borrow" will always mean "mutable borrow". Commented "drop" instructions are inserted by the compiler: they indicate that the dropped variable becomes inaccessible, either because it's going out of scope or because of borrow checker restrictions.

Polonius [START_REF] Matsakis | An alias-based formulation of the borrow checker[END_REF], a new formulation for the borrow checker, ensures the borrow guarantees by binding each borrow to its origins with regions (also called lifetimes), i.e. sets of loans where a loan is a tag at a possible location of the borrowed value. Each region tells us that to access any loaned value in it, all borrows attached to this region must have been dropped: we can then "end" the region to retrieve the loaned values. That allows great flexibility compared to simple linear or affine types, as long as we respect this discipline of "stacked" borrows [START_REF] Jung | Stacked borrows: An aliasing model for rust[END_REF] where only the most recent borrows are available.

In the example below, after defining a, b and c, Polonius has two regions: {a}, attached to b and {*b}, attached to c. Only c does not contain any loan and is thus directly accessible.

To access b, we must drop c first and similarly, to access a we must drop b and so drop also c (as we must access a value to drop it). After running the borrow checker, we obtain the inserted drop annotations for borrows. They do nothing at run-time as they only prevent subsequent borrow uses at compile-time. In Rust function signatures, borrows must be attached to explicit regions parameters. That allows to describe the loans (i.e. possible origins) of the function output borrows in terms of the loans of the input borrows. All information about borrow dependencies is thus available in the signature, allowing the borrow checker to ignore the function implementation at its call sites. In the example below, after calling pick_first we have two regions: {v}, attached to r and {u, *r}, attached to t. // The region 'a of the output groups together loans from x and y. fn pick_first<'a, T>(x: &'a mut T, y: &'a mut T) -> &'a mut T { // drop y (goes out of scope) x } let (mut u, mut v) = (10, 20); let r = &mut v; let t = pick_first(&mut u, &mut *r); *t += 1; // drop t (ends the region {u, *r} to access r) *r += 2; // drop r (ends the region {v} to access v) assert!(u == 11 && v == 22);

To translate such a program, dependencies between overlapping borrows are reified into functions that take the values under the recent borrows and give back the values under the older borrows. Thus, dropping a borrow results in explicitly returning its updated underlying value. But, to do that, contrarily to e.g. Creusot, Aeneas doesn't get enough information from the drops inserted by the borrow checker. So, Aeneas also plays the borrow checker role, carrying additional information to know how to return the dropped values to their origin.

It first translates the Rust source program into the Low-Level Borrow Calculus (abbreviated LLBC), a new formalism equipped with a functional operational semantics that explicits the loans for each borrow at run-time. Then, following its symbolic execution which approximates at compile-time the borrow corresponding loans, we can generate the functional translation of the source program in continuation-passing style. Aeneas translates each Rust function into:

• A forward function, which translates borrows by their underlying values.

• One backward function per region, which translates it as a function taking the same arguments as the forward function plus the values of the output borrows under the region, and returning the actualized values of the input borrows under the region.

The Aeneas translation of the previous program is shown below, as a reference before exposing our translation. A backward function is called when the corresponding region is ended (and so after the borrows attached to it are all dropped), to get the actualized values of the region loans before accessing them. Below, we see that because pick_first_fwd returns x, pick_first_back returns ret (the actualized value of x) and y (which didn't change since the call to pick_first_fwd as it's loaned). Our translation comes closer to Polonius: we build linear functions (A i × ...) ⊸ (B i × ...) (i.e. functions which must be called exactly once and whose arguments cannot be duplicated or discarded) that play the role of regions enriched with information about how borrows are related to their loans, replacing backward functions. It consumes the tuple of values underlying the borrows attached to the region and returns the tuple of loaned values.

Given all the information about borrows and loans dependencies, we are now able to translate basic borrow operations:

• Creating a new borrow &mut x of type T is translated by the underlying value x and a new identity route λ(x ′ ).(x ′ ) : (T ) ⊸ (T ) which will transmit the updated value of x.

• Dropping the kth borrow drop x from the route r :

(A 0 × ...A n ) ⊸ B is translated by passing x in r with r = λ(a 0 ...a k-1 , a k+1 ...a n ).r(a 0 ...a k-1 , x, a k+1 ...a n ).
• Ending the route r : ()

⊸ (B 0 × ...B n ) loaning the values of the variables b 0 , ...b n is translated to let (b 0 , ...b n ) = r().
• Similar route manipulations are defined to permute their arguments or to compose them on a single input/output.

Each region parameter of a function is translated to a type parameter and in-&-out route arguments. Both route arguments output the type parameter, which is always instantiated with the tuple made from the types of the loaned values for the corresponding region. The input route arguments are the types of the function input borrows underlying values attached to the translated region, and similarly, the output route arguments are the types of the function output borrows underlying values attached to the region. In the translation below, the pick_first region 'a is thus translated by • The type parameter A.

• The input route a expecting the updated values under x and y.

• The output route built from a expecting the updated value under the returned borrow

x.

To call a function, we must pass it new routes that group borrows under the same regions, such as λ(u2, r2).(u2, r2) in the translation below.

The last missing ingredient is to adapt a subset of LLBC annotating Rust function signatures, variables and regions to connect borrowed values to matching route arguments. While we don't expose formal translation rules in this paper as they are still being worked out, we give our minimal borrow calculus syntax in the table below.

Sort Variable Grammar VarId v FunId f RegionId α BorrowId B i LoanId L i Value a ⋆ | (a, a ′ ) | B i a | L i Route r -→ L i ⊸ ( -→ B i | α) FunSignature s [ - → α ]( - → a , - → r ) → (a, - → r ) Environment Ω --→ f : s, - → α ⊢ ------→ v : (a | r)
Such environments annotate Rust variables and routes with a graph of borrow dependencies:

• Edges correspond to borrow and loan identifiers matching pairs B i , L i : each borrowed value is annotated with a B i and must eventually fill the corresponding hole L i . Note that this can lead to confusion as the route inputs are tagged with loans identifiers and their outputs with borrow identifiers: this is because the route acts like an indirection in which we give back borrowed values.

• Vertices correspond to either values or routes, which have more structure to retain information about compound values or regions. Star (⋆) values are values without loans or borrows.

We can then define the dependencies of a given loan identifier D(Ω, L i ) as the set of variables reachable from it, by fetching the corresponding borrow identifier:

• B i ∈ a with v : a ∈ Ω a variable annotation, in which case D(Ω, L i ) := {v}, • B i ∈ - → B with r : - → L ⊸ - → B ∈ Ω a route annotation, in which case D(Ω, L i ) := ∪{D(Ω, L j ) | L j ∈ - → L }.
Except when dropping variables, those dependencies can only grow, but we must avoid making them grow more than necessary: that would prevent us from accessing some variables without a good reason, making the borrow checker too strict. This could happen by merging too many routes while joining different environments, an operation detailed in the next section.

Finally, we can define our main borrow calculus operations on the environment:

• When accessing a variable v : L i , we fetch all the dependencies of loan identifiers in a and call their corresponding routes, removing them from the environment. The environment thus shrinks until there are no loan identifiers left in a.

• When borrowing a variable value v : a, we create a route r : L i ⊸ B j with fresh identifiers and a borrow b : B i a. The variable value is replaced by the route output corresponding loan L j .

In our translation below, we comment most lines with the borrow calculus environment.

let pick_first T A (x y: T) (a: (T * T)→A): T * (T→A) = (* α ⊢ x : B x ⋆, y : B y ⋆, a : L x × L y ⊸ α *) let a = λret. a (ret, y) in (* drop y *) (* α ⊢ x : B x ⋆, a : L x ⊸ α *) (x, a) let (u, v) = (10, 20) in (* ⊢ u : ⋆, v : ⋆ *) let (r, dr) = (v, λv2. v2) in (* ⊢ u : ⋆, v : L 1 , r : B 0 ⋆, dr : L 0 ⊸ B 1 *) let (t, dt) = pick_first u r (λ(u2, r2). (u2, r2)) in (* ⊢ u : L 2 , v : L 1 , r : B 0 L 3 , dr : L 0 ⊸ B 1 , t : B 4 ⋆, dt : L 4 ⊸ B 2 × B 3 *) let t = t + 1 in let (u, r) = dt t (* drop t *) (* ⊢ u : ⋆, v : L 1 , r : B 0 ⋆, dr : L 0 ⊸ B 1 *) let r = r + 2 in in let v = dr r in (* drop r *) (* ⊢ u : ⋆, v : ⋆ *) assert(u == 11 && v == 22)
Identity routes (that we'll now create with "id") could be inlined to get closer to Aeneas forward and backward functions: above, dr could be left implicit and function routes such as pick_first third argument could be instantiated with id. This yields an equivalent, often more concise translation. We'll keep the style presented above to recognize more easily the translated region parameters in our translations, but we could use this inlined version for any example in this article. 3 Lifetime bounds By default, regions mentioned in a function signature are disjoint. This is sometimes too restrictive, as illustrated by the second example below: there, we return either the first two or the last two borrows of a function. So, we want to explain to the borrow checker at the signature level that ret.0 (the first output) may only overlap x and y, and similarly that ret.1 may only overlap y and z. This is used in the example to avoid dropping ret.1 while accessing the value under x.

For that, we want to group ret.0, x, y under a region and ret.1, y, z under another one. However, borrows (in particular y) can only be placed in one region. So instead, we'll put it in a third region with bounds to the two other regions, meaning that both ret.0 and ret.1 may overlap y. Each lifetime bound 'a: 'b in a signature is translated as a dependency from the route 'b to the route 'a, i.e. as an argument between them. Its type is unknown from the caller's point of view and is therefore masked by an existential type.

Our translation handles the if/else construct by computing the join (a known problem in abstract interpretation) of the two branches, taking the union of their borrow dependencies: ∀L i .D(join(Ω, Ω ′ ), L i ) = D(Ω, L i ) ∪ D(Ω ′ , L i ) (the environments must have the same loan & borrow identifiers). While the obtained routes will match the function return type in this example, we cannot guarantee this in general: see the discussion in future work. To implement this, we define new operations to manipulate routes:

• Adding a dependency between two routes a ⇝ b is done by adding a unit output to a and a unit input to b, bound by a new pair of identifiers L i /B i .

• Masking a dependency between two routes is done by introducing a new existential type for their corresponding output and input.

• Composing routes along a dependency a ⇝ b, if a has a single output or b has a single input, is done by composing them as expected. The condition ensures that all loan dependencies D(L) are preserved so that this rule can be applied whenever wanted, as a normalization rule. This is not the case in general, if the single input or output condition is not verified.

Then, we can translate the if/else clauses with the following steps. They are interleaved with the environment annotations and the generated code for our example in if/else branches, where new expressions fill the previous hole ♢ to detail the expression translating three_of_two before inlining sub-expressions.

if: let ret = (x, y) in ♢ ret : (B x ⋆, B y ⋆), z : B z ⋆, a : L x ⊸ α, b : L y ⊸ β, c : L z ⊸ γ else: let ret = (y, z) in ♢ ret : (B y ′ ⋆, B z ′ ⋆), x : B x ⋆, a : L x ⊸ α, b : L y ′ ⊸ β, c : L z ′ ⊸ γ 1.
Before joining the two environments, we drop values which are not shared: in our example, z in the first branch and x in the second branch.

if: let c = c z in ♢ ret : (B x ⋆, B y ⋆), a : L x ⊸ α, b : L y ⊸ β, c : γ else: let a = a x in ♢ ret : (B y ′ ⋆, B z ′ ⋆), a : α, b : L y ′ ⊸ β, c : L z ′ ⊸ γ 2.
We insert identity routes serving as indirections for the new loans and borrows coming from each branch, to allow many-to-many dependencies between loans and borrows.

if: let (r0, r1) = (id, id) in ♢ ret : (B 0 ⋆, B 1 ⋆), a : L x ⊸ α, b : L y ⊸ β, c : γ, r0 : L 0 ⊸ B x , r1 : L 1 ⊸ B y else: let (r0, r1) = (id, id) in ♢ ret : (B 0 ⋆, B 1 ⋆), a : α, b : L y ′ ⊸ β, c : L z ′ ⊸ γ, r0 : L 0 ⊸ B y ′ , r1 : L 1 ⊸ B z ′
3. We add on those identity routes the dependencies coming from both branches. At this point, the annotations have the same shape in both branches, so we can rename matching pairs of loan/borrow identifiers to equate them (the renaming is not needed for our example).

ret : (B 0 ⋆, B 1 ⋆), a : L x ⊸ α, b : L y × L y ′ ⊸ β, c : L z ′ ⊸ γ, r0 : L 0 ⊸ B x × B y ′ , r1 : L 1 ⊸ B y × B z ′ 4.
We normalize all routes with the composition rule, which generates the same code for both branches as their environments are the same.

let r0 = (λu. let (v, w) = r0 u in (a v, w)) in let r1 = (λu. let (v, w) = r1 u in (v, c w)) in ♢ ret : (B 0 ⋆, B 1 ⋆), b : L y × L y ′ ⊸ β, r0 : L 0 ⊸ α × B y ′ , r1 : L 1 ⊸ B y × γ 5.
We mask dependencies between routes with new existential types. At this point, the routes have the same type in both branches and can be returned along each if/else result. In the example, some re-ordering of routes and their outputs is needed before returning the if/else result from the function, which is guided by its signature (and inlined in the translation for simplicity).

(ret, b, r0, r1)

4 Work in progress and future perspectives

Translation soundness and expressivity

To ensure that the translation is correct, we should aim for a theorem ensuring that the source program behaves like its translated program. For that, the source program should be interpreted with an imperative operational semantics (like the one given by RustBelt or tree borrows [START_REF] Villani | Tree borrows, a new aliasing model for rust[END_REF]), and the translated program with a standard functional semantics. If the theorem is too complicated, we can aim for an operational semantics closer to a dynamic borrow checker instead (like LLBC or stacked borrows). To see that the translation captures closely Rust programs, we may also investigate denotational completeness for some Rust function types T , i.e. that every element of type T is the denotation of a translated source program of type T . We also want to characterize the translation expressivity: as it is currently, it is determined empirically by looking at which programs the translation accepts. This is very similar to what happens with Rust borrow checker. A first step would be to study the differences between Polonius and our translation. The main difficulty seems to accommodate the lost equivalences when enriching regions/relations to routes/functions.

With regions, any two different ways to present the same dependencies between some borrows and loans are equivalent: we obtain different function signatures that can accept the same programs. In particular, we can call the first function inside the second and vice-versa. With routes, two different presentations of the same dependencies may not be equivalent, preventing the translation of the second function call in the first one or vice-versa.

So either we settle on a translation more restrictive than Polonius, which can be acceptable given that the counter-examples require complex signatures that we rarely find in Rust programs, or we try to rewrite the signatures before translating them. To make further progress, it will be necessary to understand better the structure underlying routes.

Destructors and effects

Rust sees its values as resources: they are linear values equipped with a destructor, i.e. a function that can consume them and may have an effect to clean up the program state (e.g. a dropped file handle closes its underlying file). The call to the destructor is inserted by the compiler for variables going out of scope, making the type system affine. They are also called when an exception (named "panic" in Rust) is raised.

Like Aeneas, this translation was focused on the notion of borrows. However, Rust also has effectful destructors and exceptions (named "panics") which play a major role in Rust programs:

• Some use emergent patterns, such as typestates [START_REF] Strom | Typestate: A programming language concept for enhancing software reliability[END_REF], which exploit Rust linearity and destructors to maintain guarantees about the program state. This allows to implement state machines at the type level.

• Some must be fault-tolerant, by being in a suitable state after encountering an exception. This can happen at FFI boundaries or for programs with multiple threads. This is especially important for the concurrency model of Rust which allows to share mutable data with a mutex: when an exception happens in a subroutine, it poisons the mutex to emit an error at subsequent accesses to the mutex. We thus prevent deadlocks or accesses to an invalid state. This error handling is similar to the mechanism from this paper on affine sessions [START_REF] Mostrous | Affine Sessions[END_REF], where errors do not prevent progress properties of the whole program.

Those kinds of guarantees aren't preserved in the previously mentioned works, notably Aeneas and RustBelt (where it is an explicit limitation).

Some recent works ([CFMM16]

, [START_REF] Combette | A resource modality for raii[END_REF]) study the interactions between destructors, effects, and exceptions with denotational semantics for linear logic where a suitable notion of resources can be modeled. Our long-term objective is to leverage our translation linearity to reconcile those works with our handling of borrows, to have a renewed understanding of Rust programming paradigm, and to be able to improve the verification of Rust programs.

Additional features

Other features from Rust are not present in Aeneas paper. Among those, we investigate nested borrows, i.e. borrows of another borrow, and polymorphism (which was restricted to values without borrows).

Nested borrows are treated similarly to simple borrows, except that their value is consumed by the outer borrow route, and then by the inner borrow route. They are thus carrying those two destinations around, like in the example below. With this representation of nested borrows, &'a mut T and &'a mut (&'a mut T) become equivalent: the inner borrow is dropped at the same time as the outer borrow. The example below shows how a function with nested borrows can be translated and used. The issue with polymorphism is that, when a type parameter is instantiated with a type T containing borrows, we must track the commutations and drops of values of type T . Our solution is thus to add a route consuming values of type T as if it was a borrow. That way, the caller gets back the route having consumed the dropped values, and expecting the returned values of type T .

It now remains to establish proper rules and exploit the translation linearity.

  let mut a = 1; let b = &mut a; // borrows the value a let c = &mut *b; // borrows the value previously borrowed by b // drop c (ends the region {*b} to access b) *b += 2; // drop b (ends the region {a} to access a) assert!(a == 3);

  let pick_first_fwd T (x y: T): T = x let pick_first_back T (x y ret: T): T * T = (ret, y) let (u, v) = (10, 20) in let r = v in let t = pick_first_fwd u r in let t = t + 1 in let (u, r) = pick_first_back u r t (* drop t *) let r = r + 2 in in let v = r in (* drop r *) assert(u == 11 && v == 22)

(

  * obtained by inlining a := id in the previous "pick_first" definition *) let pick_first_inl T (x y: T): T * (T→(T * T)) = let a = λret. (ret, y) in (* drop y *) (x, a)

  fn three_of_two<'a, 'c, 'b: 'a+'c, T>(i: bool, x: &'a mut T, y: &'b mut T, z: &'c mut T) -> (&'a mut T, &'c mut T) { if i { (x, y) } else { (y, z) } } let (mut u, mut v, mut w) = (10, 20, 30); let (r, s) = three_of_two(true, &mut u, &mut v, &mut w); *r += 1; *s += 2; // drop r assert!(u == 11); *s += 3; // drop s assert!(v == 25 && w == 30);

  let three_of_two T A C B (i: bool) (x y z: T) (a: T→A) (c: T→C) (b: T→B): ((T * T) * ∃R.∃S. (T→(A * R)) * (T→(C * S)) * ((R * S)→B)) = if i { ((x, y), λx2. (a x2, ()), λy2. (c z, y2), λ((), y2). b y2) } else { ((y, z), λy2. (a x, y2), λz2. (c z2, ()), λ(y2, ()). b y2) } let (u, v, w) = (10, 20, 30) in let ((r, s), dr, ds, dt) = three_of_two(true, u, v, w, id, id, id) in let r = r + 1 in let s = s + 2 in let (u, t0) = dr r in (* drop r *) assert(u == 11) in let s = s + 3 in let (w, t1) = ds s in (* drop s *) let v = dt (t0, t1) in assert(v == 25 && w == 30)

  if: let r0 = λx. (r0 x, ()) in let b = λ((), y). b y in let r1 = λy. (r1 y, ()) in let c = λ(). c in ♢ else: let r0 = λy. ((), r0 y) in let a = λ(). a in let r1 = λz. ((), r1 z) in let b = λ(y, ()). b y in ♢

  fn nested_swaps<'a, 'b, 'c, T>(x: &'a mut (&'c mut T), y: &'b mut (&'c mut T)) { swap(x, y); // Exchanges the value *x with *y. swap(*x, *y); // Exchanges the value **x with **y. } let (mut u, mut v) = (10, 20); let mut r = &mut u; let mut s = &mut v; nested_swap(&mut r, &mut s); assert!(*r == 10 && *s == 20); // drop r, s assert!(u == 20 && v == 10); let nested_swaps T A B C (x y: T) (a: T→A) (b: T→B) (c: (T*T)→C): A * B * ((T*T)→C) = let (x, y, c) = (y, x, λ(x2, y2). c (y2, x2)) in (* swap ( x, y ) *) let (x, y) = (y, x) in (* swap ( * x, * y ) *) let a = a x in (* drop x *) let b = b y in (* drop y *) (a, b, c) let (u, v) = (10, 20) in let (r, dr) = (u, id) in let (s, ds) = (v, id) in let (r, s, drs) = nested_swaps r s id id (λ(r3, s3). (dr r3, ds s3)) in assert(r == 10 && s == 20) in let (u, v) = drs (r, s) in (* drop r, s *) assert(u == 20 && v == 10)