Mnemo

Architecture

Argot Server

Mnemosyne follows a simple hub-and-spokes architecture. The central hub is an LSP server (called the "Argot Server") which integrates a number of synthesis modules (called "Muses") and the developer's IDE.

The muses communicate using Argot, an extension to LSP, the Language Server Protocol (including extensions from BSP, the Build Server Protocol). Argot is documented below.

Mnemosyne Architecture

Muses

See Muses for a list of the specific synthesis techniques currently integrated into Mnemosyne.

From Argot Server’s perspective, each Muse is an LSP server in its own right, which uses LSP's existing capability discovery interface to indicate the operations it supports. This provides uniformity for Argot Server at the hub of Mnemosyne’s design. This allows a Muse to, say, offer capabilities for type extraction, or test runs, individually. Whenever possible, these endpoints should adopt existing LSP definitions (e.g., Locations).

Using base LSP along with these extensions, LSP provides sufficient primitives to cover all communication needs between Argot Server and the Muses, including:

  1. Passing user actions through to the Muse, and reporting the resultant edits / information / status.
  2. Reporting partial snippets of code to a Muse for focused operation.
  3. Allowing Muses to invoke each other through these registered capabilities (e.g., asking for type information for a region of code). In some cases, such as asking for additional code for context, Argot Server may handle the request itself. Critically, all of these requests use the same LSP interface as the IDE. This design results in the user's IDE being effectively an equal peer to the many synthesis engines—a symmetry which is both conceptually and architecturally appealing.

Unified Results

Argot Server is more than a router: it also understands how to combine results from multiple Muses. This allows preexisting LSP servers to be used as Muses, guaranteeing a baseline experience for supported languages that other Muses may augment. This allows developers to migrate from an existing language server to Argot as a purely additive experience: everything they are already used to, plus what Mnemosyne can do.

Developing Muses

For technical information on how to write a new Muse and integrate it with Mnemosyne's argot-server see argot-server/CONTRIBUTING.md#how-to-write-a-muse.

Muses as Reusable Components

Because Muses use Argot LSP as their uniform interface, it is possible to define Muses compositionally, as pipelines of simpler Muses working in stages. Muses may be instantiated from other full-fledged Muses, or from simple Muses purpose-built for composition (which may be referred to as “middleware”).

View Muses

Views are responsible for non-synthesis management of software information, including collecting and writing code, types, tests, and prose from and to the software project. They provide baseline capabilities for the LSP superset for use by the IDE and downstream Muses. For example, a test View will register with Argot Server and provide endpoints to look up the available test cases and write new ones. When a downstream Muse generates new test cases, it may use this View Muse's registered test writing capabilities to add them to the project in a general way. In this way multiple downstream Muses can leverage the test wrangling functionality provided by a View Muse. This approach has three main advantages:

  1. Synthesis Muses do not need to reimplement reading/writing operations.
  2. The synthesis Muses (e.g., test or type generators) are not tied to the chosen testing framework; only the View Muse is. This allows the synthesis effort to work independent of the testing framework chosen for the project, relying on the View to handle encoding the results.
  3. New language frameworks (e.g., alternative typecheckers) can be easily added as secondary View Muses and used interchangeably.

Language Translation

Additionally, we are developing bi-directional translation between our supported base programming languages and the DSLs used by program synthesis tools. These translation defining facilities will allow Muses to operate over simplified DSLs tailored to their synthesis technique and target domain, while ensuring that the synthesis results may be inserted into real-world programs written in the full base programming languages.

We are building a library, Fresnel, providing primitives based on Lenses which may be used to easily define new bi-directional translations between DSLs and full base languages.

Argot

Argot LSP supports explicitly represented (i) existential quantifiers such as examples and tests, (ii) universal quantifiers such as contracts and types, and (iii) natural language documentation and prose. These new kinds accompany subtrees of a software program.

Argot provides a medium of exchange between tools for program synthesis and analysis (termed "Muses") and the developer’s IDE.

Argot

Argot includes the typical LSP actions along with actions for:

Interactions should work on a framework-by-framework basis. For each supported language there are many different test frameworks, different type inference frameworks (e.g. Mypy vs. Reticulated for Python, or TypeScript vs. Flow for JavaScript), and different documentation generators, with their different input conventions (see this long list of Python documentation tools). Typically there will be one Muse per framework, responsible for watching for opportunities to contribute or to act on the contributions of other muses.

Remote files

Argot is designed to run locally or remotely. Running remotely allows for muses with specific hardware requirements (e.g. GPU availability for muses that make use of Tensorflow).

The problem is that a remote Argot Server instance has no access to the local filesystem. To work around this, Argot incorporates prior work in extending LSP with the minimal endpoints necessary for the server to be able to list and retrieve local files.

Client extensions

While Mnemosyne can be used over plain LSP, Argot defines extensions which, when implemented by the client, extend the range of what muses can do. We already implement extensions for a number of editors that provide support for these extensions.

Client support for Argot extensions is opt-in. Clients must signal their support when connecting, in the argot key of the initializationOptions (not capabilities!) of the initialize request.

initializationOptions: {
argot?: {
...
}
}
Content Request

The content request can be used by the server to request the content of a particular file from the client. (Note that requests for binary files will be rejected.)

Request:

interface ArgotContentParams {
/**
* The text document to receive the content for.
*/

textDocument: TextDocumentIdentifier;
}

Response:

Support for content requests is controlled by the argot.contentProvider initialization option:

initializationOptions: {
argot?: {
contentProvider?: boolean,
}
}
Files Request

The files request can be used by the server to list the files in the current workspace.

Request:

interface ArgotFilesParams {
/**
* The URI of a directory to search.
* Can be relative to the rootPath.
* If not given, defaults to rootPath.
*/

base?: string;
}

Response:

Support for files requests is controlled by the argot.filesProvider initialization option:

initializationOptions: {
argot?: {
filesProvider?: boolean,
}
}

Reading user input

Argot adds a new interface (ArgotShowPromptParams) and a new endpoint (argot/window/showPrompt) for reading input from the user.

argot/window/showPrompt is exactly the same as window/showMessageRequest, except that instead of the user being restricted to picking from a fixed set of inputs, the user is also allowed to simply enter a string.

export interface ArgotShowPromptParams extends ShowMessageRequestParams {
/**
* A default value for the user to edit.
*/

defaultValue?: string;
/**
* Whether a multi-line input widget is preferred.
*/

multiLine?: boolean;
}

Support for reading input is controlled by the argot.inputBoxProvider initialization option:

initializationOptions: {
argot?: {
inputBoxProvider?: boolean,
}
}

Annotations

Argot adds new concepts to LSP: Annotations and Contributions. Annotations are attached to regions in files (or entire files), and each Annotation has a list of Contributions.

Annotations are created with LSP ranges, but their start and end points are updated as the file changes. (Annotations without regions always apply to the whole file.)

Contributions are tagged with a kind (code, type, test, or prose) and the name of the muse that contributed them. A Contribution has a data slot that contains a table of properties.

(Optionally a Contribution can also have a key, allowing the same muse to make multiple Contributions, with different keys, to the same Annotation.)

Annotations are created by muses, but they have no provenance. They belong to the document. Contributions, on the other hand, always belong to the muse that contributed them. Two muses can make separate Contributions to the same Annotation, but their Contributions always remain distinct.

At a very high level this approach could be thought of as being analogous to a "tuple space," where the tuples are addressed by (file, range, kind, muse, key)—bearing in mind that the range is updated as the file is edited. Muses are able to contribute what they know when they know it, and can both look up what has already been contributed and be notified as other muses contribute.

Currently this involves a minimal extension to LSP: a GetAnnotations request, to get the Annotations for a file or a region in a file, and a didAnnotate notification, to add new annotations.

As a file changes, Annotations move around. If an Annotation applies to a region in a file that has been deleted, that Annotation is also deleted. The GetAnnotations request only returns Annotations that fall entirely within the requested range, not Annotations that only overlap it at one end.

There are two new endpoints:

Annotation and Contribution are defined as follows:

export namespace ArgotKind {
export const Code = 'code';
export const Types = 'types';
export const Tests = 'tests';
export const Prose = 'prose';
}

export interface Annotation {
/**
* The file to annotate.
*/

textDocument: TextDocumentIdentifier;
/**
* The range the annotation applies to.
* An annotation without a range applies to the whole file.
*/

range?: Range;
contributions: Contribution[];
}

export interface Contribution {
/**
* The muse responsible for this contribution.
*/

source: string;
/**
* An optional sub-key for the contribution.
* Within an Annotation, Contributions are addressed by source and key.
* If there is no key, there can only be one Contribution from a given
* muse per Annotation.
*/

key?: number | string;
kind: ArgotKind;
/**
* A dictionary of properties.
*/

data: any;
}

Data for Contributions

While LSP does define interfaces with member types that are disjunctions of interfaces, this is a feature that is not widely supported by LSP clients. Accordingly the data member of a Contribution is only defined as a dictionary.

All data contributions implement the Data interface.

export interface Data {
interface?: string;
}

Optionally, the Data interface allows for specifying the intended interface in the interface key. E.g. if a client receives the following JSON:


{
"name": "int",
"interface": "InferredType"
}

They should treat it as an instance of InferredType (see below).

Types as Data

Inferred types are represented as lists of candidates, with associated probabilities.

export interface InferredType extends Data {
name: string;
}

export interface TypeCandidates extends Data {
candidates: TypeCandidate[];
}

export interface TypeCandidate extends Data {
typeName: string;
probability: number;
}

export interface FunctionReturnType extends Data {
/**
* The name of the function.
*/

functionName: string;
/**
* The type the function returns.
*/

returns: string;
}

export interface FunctionReturnTypeCandidate extends FunctionReturnType {
probability: number;
}

export interface FunctionReturnTypeCandidates extends Data {
candidates: FunctionReturnTypeCandidate[];
}
Tests as Data

Argot LSP must represent tests from both the perspective of a test runner and the perspective of a test harness.

A test runner is interested in the actual and expected output of a test, so it can compare them. We call this output, whether actual or expected, a result.

export interface TestCaseResult extends Data {
path?: string[];
}

export interface UnitTestCaseResult extends TestCaseResult {
expected: string | number | boolean;
}

export interface BinaryTestCaseResult extends TestCaseResult {
stdout?: string;
stderr?: string;
/**
* A non-negative integer representing an exit code.
*/

exitCode: number;
}

A test harness, on the other hand, is interested in whether the test passed or failed. We call whether this information about whether the test passed or failed (or was skipped) the test’s status.

export namespace TestStatusKind {
export const Skipped = 0;
export const Passed = 1;
export const Failed = 2;
export const Errored = 3;
export const Unknown = 7;
}

export interface TestStatus {
testStatusKind: TestStatusKind;
path: string[];
/**
* How long the test took to run.
*/

time?: number;
message?: string;
trace?: string;
}

We address tests by their path, a list of strings, where the last element is the name of the test and the preceding elements are the names of any enclosing suites (including suites nested inside each other).

export namespace TestCaseKind {
export const UnitTest = 1;
export const BinaryTest = 2;
}

export interface Testable extends Data {
path: string[];
disabled?: boolean;
}

export interface TestCase extends Testable {
target: string | Location;
testCaseKind?: TestCaseKind;
conditions: TestCondition[];
arguments?: (string | number)[];
expected?: UnitTestCaseResult | BinaryTestCaseResult;
}

export interface TestSuite extends Testable {
cases: TestCase[];
verificationResults?: TestCaseResult[];
environment?: any;
nestable?: boolean;
}

Besides test cases and test suites Argot also represents test conditions – the individual assertions inside the test. (We call these conditions per ISTQB, and to avoid confusion with the way different test frameworks use the term “assertion”.)

export namespace TestConditionKind {
export const Fatal = 0;
export const Nonfatal = 1;
}

export interface TestCondition extends Testable {
testConditionKind: TestConditionKind;
target: string | Location;
}

Test examples are similar to, but disjoint from, conditions. A test example is a condition with a particular three-place form:

  1. A comparator.
  2. A literal argument on the right-hand side
  3. A call to a function on the left-hand side, with the call having only literals for arguments.

This is a form particularly amenable to synthesis. Examples are disjoint from conditions because they may or may not derive from any particular location. An example starts as a condition, but the correspondence is not exact – it might swap the sides of the conditions, inline bound literals from the condition’s environment, or even split a single condition into multiple examples.

export interface Example extends Testable {
target?: string | Location;
/**
* How the expected output should be compared to the actual output.
*/

comparator?: string;
callee: string;
/**
* The literal arguments to the callee.
*/

arguments: any[];
/**
* What the callee is expected to return.
*/

output: any;
}