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 an extended form of LSP as documented below.

Argot

The Argot server extends existing programming languages with 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. We refer to these new kinds collectively as "Argot." Argot is intended to provide a medium of exchange between automated program synthesis and development tools and IDEs (termed "Muses").

Argot LSP Extensions

This hub communicates with the developer and with synthesis modules or Muses using a superset of LSP, which includes the typical LSP actions along with actions for:

• Contributing synthesized code (including generated variants), tests (including unit and full-project tests), types (including unit and full-project tests), and documentation on the level of particular regions (such as an individual function), files, or the entire project.
• Querying for previously synthesized code variants, type information (including collected types, collected type refinements, inferred types, and ML-inferred type candidates), generated tests (including tests for regions, files, or the entire project), and collected or generated documentation.
• Running annotations by running tests against code, checking inferred types for soundness, and generating documentation.
• Reading input (such as new identifier names) from the user.

Interactions should work on a framework-by-framework basis. For each supported language there are many different test frameworks, 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.

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;
    }

Annotations

Argot adds two 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 buffer changes. (Annotations without regions 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.

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:

    • method: argot/didAnnotate
    • params: didAnnotateParams defined as follows:

    export interface DidAnnotateParams {
           annotations: Annotation[];
    }

• GetAnnotations request

  • Request:

    • method: argot/getAnnotations
    • params: getAnnotationsParams defined as follows:

    export interface GetAnnotationsParams {
            textDocument: TextDocumentIdentifier;
            /**
             * No range means to get the annotations for the whole file.
             */
            range?: Range;
    }

  • Response:

    • result: 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 interface, 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. The following types, then, are provided not as requirements, but as guidance for how to format data in a way other LSP clients can understand.

export interface Data {}

export interface InferredType extends Data {
        name: string;
}

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

export interface TypeCandidate {
        name: string;
        probability: number;
}

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

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

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

export interface TestCase extends Data {
        name: string;
        target: string | Location;
        testCaseKind: TestCaseKind;
        arguments: (string | number)[];
        expected: UnitTestCaseResult | BinaryTestCaseResult;
}

export interface TestSuite extends Data {
        name: string;
        cases: TestCase[];
}

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.

To ease the burden on Muse authors, we plan (eventually) to implement shims in each Mnemosyne-supported language which will handle the LSP communication. These shims will define a series of abstract functions (or methods or similar) that correspond to Mnemosyne's LSP superset, allowing Muses to overwrite them to register new actions as simple functionality. The status of our shim development is listed in the following table:

Furthermore, because Muses use 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”).

Open Questions

• How should muse initialization proceed? Should a Muse receive all of the source code, in order to determine which things it can do? (You can imagine the mypy muse determining it can't work over JavaScript, or the unittest testing library can't work over pytest definitions.)
  • In the current approach what language a muse supports is entirely out of band. For external LSP servers, there is a list of names of servers with the languages they support, and for Muses implemented in Lisp, there is a muse-lang generic function.
  • It would be useful to query a Muse for what language it supports. It may be possible to do this through LSP capabilities.
  • How should this work for mixed-code repositories?
• If multiple Muses support the same operation, how should Argot proceed? For example, for test case execution, which should be selected?

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.

Argot Language Translation Muses

Additionally, we are developing bi-directional translation between our supported base programming languages (Python, JavaScript and Common Lisp) and the DSLs often 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, Argot, providing primitives based on Lenses which may be used to easily define new bi-directional translations between DSLs and full base languages. A draft paper describing our methodology is available at argot-core-trinity/main.tex.