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.
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:
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.
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.
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”).
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:
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 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 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.
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.
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?: {
...
}
}
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:
ArgotContentParams
defined as follows:interface ArgotContentParams {
/**
* The text document to receive the content for.
*/
textDocument: TextDocumentIdentifier;
}
Response:
TextDocumentItem
Support for content requests is controlled by the argot.contentProvider
initialization option:
initializationOptions: {
argot?: {
contentProvider?: boolean,
}
}
The files request can be used by the server to list the files in the current workspace.
Request:
ArgotFilesParams
defined as follows:interface ArgotFilesParams {
/**
* The URI of a directory to search.
* Can be relative to the rootPath.
* If not given, defaults to rootPath.
*/
base?: string;
}
Response:
TextDocumentIdentifier[]
Support for files requests is controlled by the argot.filesProvider
initialization option:
initializationOptions: {
argot?: {
filesProvider?: boolean,
}
}
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,
}
}
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:
DidAnnotate notification
Notification:
argot/didAnnotate
didAnnotateParams
defined as follows:export interface DidAnnotateParams {
annotations: Annotation[];
}
GetAnnotations request
Request:
argot/getAnnotations
getAnnotationsParams
defined as follows:export interface GetAnnotationsParams {
textDocument: TextDocumentIdentifier;
/**
* No range means to get the annotations for the whole file.
*/
range?: Range;
}
Response:
Annotation[]
. Only the annotations that fall
inside the specified range are returned.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;
}
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).
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[];
}
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:
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;
}