Home

the-Arioch edited this page Oct 21, 2013 · 31 revisions

Documentation for InSynth Eclipse plugin

Introduction

InSynth Eclipse plugin extends the code completion feature of Scala IDE by providing additional content assist proposals. These proposals represent the top ranking results from the InSynth tool.

InSynth tool applies theorem proving techniques to synthesize code fragments that use program declarations and imported library functions. The tool aimes to synthesize small code fragments (as opposed to entire algorithms), offer them to the developer and to save the developer's efforts for searching and typing the needed constructs and their compositions. InSynth uses information that is available at a specific program point, a desired type and all visible program declarations and imported library APIs (that could otherwise be used at that program point in the code) to search for all source code fragments that would give a result of the desired type. Afterwards it heuristically ranks them and reports only a specific number of top-ranked code snippets back to the developer.

Installation and content assist control

After installing the InSynth feature in your Eclipse a window with information about the new InSynth content assist provider and its setup should appear when you try to invoke content assist, by using Ctrl+Space in the Scala Editor.

The settings include enabling InSynth proposals in the content assist items and its position in the content assist cycle.

The settings page can be latter accessed via the Setting page (on the path Java -> Editor -> Content Assist -> Advanced).

Usage

InSynth can be invoked through the Eclipse code completion support, and it returns the specified number of code snippets that can be synthesized in the current context. Code completion is invoked by using Ctrl+Space in the Scala Editor.

If the code completion is invoked after a declared variable with a desired type InSynth will try to synthesize and return code snippets of that desired type.

The example of running InSynth can be seen below:

InSynth content assist

In the example, a Scala variable of the type StreamTokenizer has been declared and its possible initial values are being computed and suggested by InSynth.

Places for invocation

InSynth functionality can be applied when invoked at the place right after declaring a typed value, variable or a method. Examples which declare such constructs with the type of Int are

  • for declaring values
  • for declaring variables
  • for declaring methods.

Note that the cursor needs to be in the place of the construct definition when InSynth is invoked.

Limitations

InSynth cannot currently synthesize expressions that contain declarations with type parameters (e.g. def f[T](a:T):T={...}). However, the expressions may include declarations with complex types (e.g. def g(a:List[String]):Set[Int]={...}), composed of instantiated type constructors (e.g. List[String], Set[Int]). In other words, InSynth uses declarations with ground types to generate expressions.

InSynth settings

InSynth settings page can be accessed from the Scala IDE preference page category (on the path Scala -> InSynth).

"Number of snippets" option dictates how many snippets will InSynth try to synthesize. Note that InSynth will always generate number of snippets lower than or equal to this settings, since in some contexts the given number of solutions might not be feasible.

"Maximum computation time (ms)" option dictates how much time is allowed for the InSynth synthesis. InSynth will try to synthesize solutions only within the given time limit.

Note that returned number of code snippets is dictated by both of these settings and also by the current program on which source code the content assist helper is invoked.

InSynth logging

InSynth contributes to the Scala IDE plugin and also shares the same logging facilities. If any error occurs during the InSynth synthesis process the cause of error will be logged (besides the fact that there will be no returned code snippets).

Scala IDE logging configuration can be viewed and changed as described in http://scala-ide.org/docs/helium/features/logging.html. --- link broken