PEPM 2020- Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Full Citation in the ACM Digital Library

SESSION: Research Papers

Module generation without regret

Modules are an indispensable mechanism for providing abstraction to programming languages. To reduce the abstraction overhead in the usage of modules, Watanabe et al. proposed a language for generating and manipulating code of modules, and implemented it via a translation to plain MetaOCaml. Unfortunately, their solution has a serious problem of code explosion if functors are repeatedly applied to modules. Another problem in their solution is that it does not allow nested modules.

This paper proposes a refined translation for a two-stage typed language with module generation where nested modules are allowed. Our translation does not suffer from the code-duplication problem. The key idea is to use the genlet operator in latest MetaOCaml, which performs let insertion at the code-generation time to allow sharing of code fragments. To our knowledge, our work is the first to apply genlet to code generation for modules. We conduct an experiment using a microbenchmark, and the result shows that our method is effective to reduce the size of generated code that would have been exponentially large.

Symbolic bisimulation for open and parameterized systems

Open Automata (OA) are symbolic and parameterized models for open concurrent systems. Here open means partially specified systems, that can be instantiated or assembled to build bigger systems. An important property for such systems is ”compositionality”, meaning that logical properties, and equivalences, can be checked locally, and will be preserved by composition. In previous work, a notion of equivalence named FH-Bisimulation was defined for open-automata, and proved to be a congruence for their composition. But this equivalence was defined for a variant of open-automata that are intrinsically infinite, making it unsuitable for algorithmic treatment.

We define a new form of equivalence named StrFH-Bisimulation, working on finite encodings of OAs. We prove that StrFH-Bisimulation is consistent and complete with respect to the FH-Bisimulation.

Then we propose two algorithms to check StrFH-Bisimulation: the first one requires a (user-defined) relation between the states of two finite OAs, and checks whether it is a StrFH-Bisimulation. The second one takes two finite OAs as input, and builds a ”weakest StrFH-bisimulation” such that their initial states are bisimilar. We prove that this algorithm terminates when the data domains are finite. Both algorithms use an SMT-solver as a basis to solve the proof obligations.

High-fidelity metaprogramming with separator syntax trees

Many metaprogramming tasks, such as refactorings, automated bug fixing, or large-scale software renovation, require high-fidelity source code transformations -- transformations which preserve comments and layout as much as possible. Abstract syntax trees (ASTs) typically abstract from such details, and hence would require pretty printing, destroying the original program layout. Concrete syntax trees (CSTs) preserve all layout information, but transformation systems or parsers that support CSTs are rare and can be cumbersome to use.

In this paper we present separator syntax trees (SSTs), a lightweight syntax tree format, that sits between AST and CSTs, in terms of the amount of information they preserve. SSTs extend ASTs by recording textual layout information separating AST nodes. This information can be used to reconstruct the textual code after parsing, but can largely be ignored when implementing high-fidelity transformations.

We have implemented SSTs in Rascal, and show how it enables the concise definition of high-fidelity source code transformations using a simple refactoring for C++.

SESSION: Short Papers

An approach to generate text-based IDEs for syntax completion based on syntax specification

The integrated development environments provide several types of functionalities. Herein, we intend to generate a syntax completion functionality from the grammar of the target language as long as the sentences of the language can be analyzed via LR parsing. We specify the syntax candidates to be completed based on the sentential forms and reductions in LR parsing. Furthermore, we implement a prototype system for computing the syntax candidates to be completed at the cursor position in the source code written in a small subset of Standard ML; the system only uses the program text up to the cursor position to ensure simplicity.

GOOL: a generic object-oriented language

We present GOOL, a Generic Object-Oriented Language. GOOL shows that with the right abstractions, a language can capture the essence of object-oriented programs. GOOL generates human-readable, documented and idiomatic code in Python, Java, C#, and C++. In it, we can express common programming idioms and patterns.