Term Search in Rust
Tavo Annus
Tallinn University of Technology
Abstract:
The Rust programming language offers a rich type system,
including sum- and product types. Developer experience is
often similar to that of a high-level functional programming
language. Yet, it lacks a tool for interactively synthesizing
programs based on types; a feature of many functional lan-
guages.
We devise a general term search algorithm, and integrate it
with rust-analyzer, Rust’s official language server, making
it usable from any client supporting standard LSP features. It
suggests expressions for unfinished parts of a Rust program
(as long as their type is known), or offers terms of matching
type while typing via autocompletion. We develop the algo-
rithm in three iterations. The first iteration is a backward
search, inspired by Agsy, a similar tool for Agda proof as-
sistant. The second iteration reverses the search direction,
simplifying the caching of intermediate results. In the final
iteration, we implement a tactic-based bidirectional search.
This algorithm can synthesize terms in many more situations
than the previous iterations, without a significant decrease
in performance.
To evaluate the performance of our algorithm, we run it
on 155 popular open-source Rust libraries. We delete parts
of their source code, creating holes, and let the algorithm
re-synthesize the missing code. We measure how many holes
the algorithm can fill and how often it suggests the original
code.
We have upstreamed our code, and term search is available
as part of the official rust-analyzer distribution starting
from v0.3.1850