PROSE Framework

Standard concepts

Standard concepts are built-in PROSE operators. They have predefined semantics and, most of the time, witness functions for backpropagation. Thus, you can use standard concepts arbitrarily in your own DSLs without reimplementing them or designing your own synthesis procedures for them.

Concept rules

The grammar syntax for a simple concept rule looks as follows:

Type P := CustomOperatorName(E1, ..., Ek) = ConceptName(E1, ..., Ek);

Here ConceptName is the name of the concept (e.g. Pair), and CustomOperatorName is a DSL-specific name for this particular usage of the concept (e.g. RegexPair).
The parameter symbols E1, …, Ek are passed directly to the standard concept.

Example: in the SubstringExtraction language in our tutorial (opens in new tab), the standard concept Pair is referenced as follows:

Tuple<Regex, Regex> positionBoundaries := RegexPair(r, r) = Pair(r, r);
Regex r;

The two r parameters denote the regexes to the left and to the right of a given position boundary. They are united into a tuple with a standard concept Pair.

Lambda functions

More complex concept rules may include a lambda function on their right-hand side.
For instance, a list-processing operator Filter takes as input a predicate of type Func and a sequence of type IEnumerable, and returns the filtered subsequence of elements that satisfy the predicate.
Here is a complete example of referencing Filter in a DSL:

#reference 'file:TestLanguage.dll';
using semantics TestLanguage.Filtering;
using learners TestLanguage.Filtering.Learners;

language Filtering;

@input string[] v;
Regex r;
bool f := Match(x, r) | True();
@start string[] P := Selected(f, v) = Filter(\x: string => f, v);

Here the custom operator Selected(f, v) is implemented as a concept rule Filter.
The first parameter of Filter is a lambda \x: string => f, and the second one is v.
Notice that you can either use a formal parameter directly in a concept, or pass it down into a lambda body.

List of concepts