The merge point premise is superseded by the case pattern match. The deprecated merge point premise should be cleaned up from the source code.

Can we please desugar overloaded arrows to give them different names, so that they become distinguishable without doing sort inference?

What does the interpreter actually do - does it lug overloaded arrows into the same class and disregard the fact that it is defined on several different sorts, or does it actually dispatch based on sorts?

Somewhat related to: #34

Presently, when an interpreter crashes (due to a program error or due to a specification error) the error messages are cryptic since they expose the stack and variables of the specification interpreter. This makes crash analysis quite cumbersome.

This should be improved. This involves the following:

• Analysis should check that -init-> arrow passes all required semantic components
• Interpreter should catch and halt on null values.
• Interpreter should carry meaningful SourceSection entities to relate to the specification
• Interpreter should use Truffle's mechanism for flagging interpreter nodes to automatically obtain a specification stack trace on failure
• Dynamically catch errors caused by undefined constructors (in pattern matches & term builds)

Generate hashCode() functions for language terms. This is essential for performance of environments and heaps.

Currently it is supported in backend to use a pattern match to test equality to a literal. The premises do not work:

foo => true;
bar => 55;
baz => "hello";

One has to use a term equality premise instead:

foo == true;
bar == 55;
baz == "hello";

And this is not uniform with testing for empty list literal which is permitted:

bazz => [];

Task is to implement pattern matching for literal terms as well. This is also required for nested pattern matches in positions which cannot (easily) be factorized. What are the semantics of the remaining term equality premise?

#26 depends on this.

Sort reductions of the form:

rules
  e : Expr --> v.

Are not working in the DynSem interpreter. The dispatch semantics should be:

Dispatching relation r on term t looks for a rule matching on constructorof(t)/arityof(t) and dispatches to that rule if it exists. Otherwise if a sort rule matching on sortof(t) exists it dispatches to that, or halt otherwise.

If multiple reduction relations are applicable at a location where an implicit reduction is expected the analysis simply picks one instead of reporting an error.

If multiple implicit reductions are possible at a position an error should be reported. Type analysis should be allowed to continue though.

It is useful to be able to visualize terms (for example as text to see the output of an evaluation). The compiler needs to generate toStrategoTerm and toString methods for terms. The latter methods should forward to the toString methods in the StrategoTerms library.

It appears that DynSem doesn't expect project names to contain hyphens, as they appear in the names of the generated Java packages, e.g., package org.metaborg.simpl-funcons.interpreter.generated

A deeper pattern match in the source of a rule:

Plus(Plus(Plus(a, b), c), d) --> NumV(42)
where
  a --> _.

Becomes incorrectly simplified to:

Plus(Plus(_, _), _) --> NumV(42)
where
  a --> _.

Where the variables are no longer bound, the pattern match is eliminated and variable a remains free.

Can we explicate meta-functions as named arrows instead of overloaded
default arrows?

Consider:

  constructors
    concat: String * String --> String

  rules
    concat(s1, s2) --> prim_concat(s1, s2)

Using the current scheme, this meta-function is explicated as an
overloaded default arrow:

  sorts
    concat__Arrow

  constructors
    concat : String * String -> concat__Arrow {meta-function}

  arrows
    concat__Arrow -default-> String

  rules
    concat__Arrow(s1, s2) -default-> prim_concat(s1, s2)

Could we model meta-functions as a named arrow instead?:

  arrows
    String * String -concat-> String

  rules
    (s1, s2) -concat-> prim_concat(s1, s2)

And simply treat:

  concat(s1, s2) --> s

as syntactic sugar for?:

  (s1, s2) -concat-> s

This strikes me as cleaner, and will improve the quality of generated
Coq code, since we can map meta-functions onto built-in Coq relations (or functions)
more easily, without having to un-overload arrows and avoid the (I
think) artificial sort concat__Arrow.

The declaration of isSafeComponentsEnabled() in a generated interpreter is flagged as an error in Eclipse, indicating that it "must override or implement a supertype".

When running a program using the generated interpreter, Eclipse warns about the error, but allows the run to proceed.

I'm using 2.0.0.20160620-165733-master. I didn't see any errors when using a nightly from about a week ago.

Add the capability to automatically generate the initial interpreter project for a language using information from the configuration file (dynsem.properties).

The barebones minimal project should contain all the right dependencies in all the right places. If possible it should also configure the annotation processor for the project. The project will be manually imported by the user into the workspace.

It may be necessary to extend dynsem.properties configuration file with extra fields.

The DynSem getting started guide should be updated accordingly.

The following program seems to crash something in the analysis pipeline:

module test/coq-semantics/features/import1

imports importx

Crashes when trying any transformation menu-item in Spoofax > Semantics

Removing the import fixes the error. Any idea why?

Error:

org.metaborg.core.transform.TransformException: Invoking Stratego strategy module-to-core-editor failed at term
    ( Module("test/coq-semantics/features/import1", [Imports([Import("importx")])])
, []
, Module("test/coq-semantics/features/import1", [Imports([Import("importx")])])
, "test/coq-semantics/features/import1.ds"
, "eclipse:///dynsem"
)
Stratego trace:
    module_to_core_editor_0_0
    module_to_core_editor_0_0
    report_with_failure_0_1
    report_failure_0_2
    SRTS_EXT_fatal_err_0_2

    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:136) ~[org.metaborg.spoofax.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:63) ~[org.metaborg.spoofax.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:1) ~[org.metaborg.spoofax.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.core.transform.TransformService.transform(TransformService.java:51) ~[org.metaborg.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.transform(TransformJob.java:141) [org.metaborg.spoofax.eclipse_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.transformAll(TransformJob.java:108) [org.metaborg.spoofax.eclipse_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.eclipse.transform.TransformJob.run(TransformJob.java:70) [org.metaborg.spoofax.eclipse_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54) [org.eclipse.core.jobs_3.6.1.v20141014-1248.jar:na]
Caused by: org.spoofax.interpreter.core.InterpreterErrorExit: Internal error: with clause failed unexpectedly in 'module-to-core-editor'
    (Module("test/coq-semantics/features/import1",[Imports([Import("importx")])]),[],Module("test/coq-semantics/features/import1",[Imports([Import("importx")])]),"test/coq-semantics/features/import1.ds","eclipse:///dynsem")
    at org.strategoxt.lang.InteropSDefT.evaluate(InteropSDefT.java:194) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.strategoxt.lang.InteropSDefT.evaluate(InteropSDefT.java:183) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.strategoxt.lang.InteropSDefT$StrategyBody.evaluate(InteropSDefT.java:245) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.spoofax.interpreter.core.Interpreter.evaluate(Interpreter.java:109) ~[org.spoofax.interpreter.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.spoofax.interpreter.core.Interpreter.invoke(Interpreter.java:82) ~[org.spoofax.interpreter.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.strategoxt.HybridInterpreter.invoke(HybridInterpreter.java:442) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.metaborg.spoofax.core.stratego.StrategoCommon.invoke(StrategoCommon.java:78) ~[org.metaborg.spoofax.core_2.0.0.20160527-092423-DETACHED.jar:na]
    at org.metaborg.spoofax.core.transform.StrategoTransformer.transform(StrategoTransformer.java:134) ~[org.metaborg.spoofax.core_2.0.0.20160527-092423-DETACHED.jar:na]
    ... 7 common frames omitted
Caused by: org.strategoxt.lang.StrategoErrorExit: Internal error: with clause failed unexpectedly in 'module-to-core-editor'
    at org.strategoxt.lang.SRTS_EXT_fatal_err_0_3.invoke(SRTS_EXT_fatal_err_0_3.java:28) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.strategoxt.lang.compat.override.java_integration.SRTS_EXT_fatal_err_0_2.invoke(SRTS_EXT_fatal_err_0_2.java:33) ~[strategoxt-min-jar-2.0.0-SNAPSHOT.jar:na]
    at org.strategoxt.lang.compat.override.java_integration.report_failure_0_2_override.invoke(report_failure_0_2_override.java:27) ~[strategoxt-min-jar-2.0.0-SNAPSHOT.jar:na]
    at org.strategoxt.stratego_lib.report_with_failure_0_1.invoke(report_with_failure_0_1.java:32) ~[strategoxt-min-jar-2.0.0-SNAPSHOT.jar:na]
    at trans.module_to_core_editor_0_0.invoke(module_to_core_editor_0_0.java:69) ~[na:na]
    at org.strategoxt.lang.Strategy.invokeDynamic(Strategy.java:30) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    at org.strategoxt.lang.InteropSDefT.evaluate(InteropSDefT.java:192) ~[org.strategoxt.strj_2.0.0.20160527-092423-DETACHED/:na]
    ... 14 common frames omitted

The DynSem compiler uses Stratego dynamic rules in the backend to keep track of things such as compiler settings. It currently uses one rule per setting. Dynamic rules appear to severely impact compilation time of Stratego due to the number of classes generated for each of the rules.

Perhaps we can reduce the compilation time by using less dynamic rules in the backend.

There is currently NO documentation for DynSem. Something, even if it's just a 1-page tutorial for getting started need to happen.

Analysis incorrectly reports duplicate variable errors on variables that are bound in distinct branches of the case pattern match premise.

Escape hyphens in all generated identifiers. Related to #68.

We're currently using Truffle version 0.11, we should update to 0.15.

It would be nice to have built-in support for tuples/pairs on a par with lists/maps. For example, the following is currently not valid:

sorts P Q R S
arrows
  (P * Q) --> (R * S)

Currently every source-to-source transformation starts with a type analysis phase, even if a type analysis phase was performed by the previous transformation. This is detrimental for performance. Where possible the analysis results should be reused. This requires that source-to-source transformations update the analysis results (definitions, uses) as they progress.

Generate a language-specific library of terms which contains List implementations that are specialized to the types of terms they contain.

The MatchPattern currently returns a boolean flag to indicate whether matching has succeeded or failed. This is detrimental to quick unrolling of the stack in the case of match failure. A better mechanism is to signal match failure using a ControlFlowException.

Variables introduced for lifted pattern matches are quite uninformative (of the form lifted_1234). This could be improved by basing the name on the sort of the introduced variable.

Probably the simplest implementation is to mark lifted variables during lifting and then in a post-pass, once type information is available, to rename them to something that makes sense.

When generating the interpreter for the language project simpl, I get the following error message.

'Transform resources' has encountered a problem.
Transformation failed for eclipse:///simpl/trans/simpl.ds

Note: The triple slashes look odd to me.

The console output can be found here: https://gist.github.com/aaronang/9272577537e857c204f7807e559a8807.

The full path from the simpl language project is: /home/aaronang/Code/simpl/simpl, and for the interpreter project: /home/aaronang/Code/simpl/simpl.interpreter.

The analysis mangles variable names to make them compilation-unit unique but this makes recognizing variables harder. Initial and renamed variable names should be related and the original name should be restored after the analysis if the variable still exists.

A nested pattern match which leave early variables bound. Example premise:

Plus(Lit(1), Minus(Lit(2), Lit(3)) => Plus(e1, Plus(_, _))

The variable e1 will be bound although the pattern match fails. This is not an issue in normal match premises but is a problem in the merge point premise and the future case pattern match premise (#26).

The rule design dispatch in the current implementation is limited to reductions on lists and constructors. It is not adaptable to support reductions on sorts, primitives, native data types or maps.

Other design issues in the current mechanism restrict the possibility of inlining only one/some of the alternatives of an overloaded rule.

A DynSem interpreter for a language A should be invokable from the editor for Language A.

Currently an interpreter can only be invoked as a Java application and there is no integration with the language editor whatsoever.

The current approach to specifying semantics of exceptions in DynSem requires encoding exceptions as part of the values. A better mechanism is definitely needed.

The transformation menu contains a lot of entries that no longer work or they do not work standalone. These should be fixed/removed.

In the generated interpreter entry point (LANGLanguage.java) it should be somehow possible to override the paths to the specifications (in case they are not local).

Sometimes it's desirable to evaluate and AST rather than a program which needs to first be parsed. The generated language interpreter entry point should have a method that takes an AST instead of a Source.

Add a case pattern match premise:

case bv of {
  BoolV(true) =>
    s1 --> u
  BoolV(false) =>
    s1 --> u
  otherwise =>
    s1 --> u
}

Any serious programming language has arrays but there is currently no (efficient) way to specify semantics of languages with arrays in DynSem. This problem should be resolved by adding arrays as built-in types in DynSem.

Try to produce a stack trace of reduction rules when the interpreter crashes. This should make debugging bad semantics way easier.

Derived interpreters use the PersistentMap implementation from Clojure indiscriminately. This leads to clear overhead in execution performance and memory consumption. This should be improved:

• Explore using the Rascal Capsule collections (https://github.com/usethesource/capsule)
• Keep the maps transient and only freeze them when we need to capture them (e.g. closures)
• Explore switching map implementations (at runtime) based on specification behavior
• Unlock usage of the host language (Java) GC for specifications that do not capture maps (e.g. snapshots)

Implement backend support for as-match pattern:

Foo(cs@[])
...
case es@[_|_] => ...

Almost every specification will perform operations such as integer arithmetics and boolean operations. A library of operators and built-in interpreter support should be added so that operations can simply be reused instead of being redefined in every language specification.

Post-analysis arrow declarations should be annotated with the semantic components that are associated with an arrow.

The entry point for the language must be refactored to allow better (re)usability of the components.

The syntax of the map type, currently Map<T1,T2> is not in line with that of list types, currently List(T). Update the syntax for map type to be Map(T1, T2) and deprecate the old syntax

The variable pretty-fication transformation erroneously renames variables for implicitly propagated semantic components. This leads to output semantic component variables which are not bound.

The current syntax for a native function call on a sort, recv.fun(args*) is not very pretty. This should be changed so that it is similar to the notation for constructors, meta-functions and native operators:

fun(rec, arg1, arg2, ...)

Explication and analysis should treat semantic components as labels rather than types. Proposed syntax:

arrows
  E Env |- Exp :: H Heap --> V :: H Heap

rules
  E env |- Box(v) :: H h --> BoxV(allocate(v)) :: H h.

  Program(e) -init-> v
  where
    E {} : Env |- e :: H {} : Heap --> v :: H _.

Handling of semantic components in this way requires that explication be done as part of the analysis and can no longer be purely syntactic.

The transformation to DynSem Core now depends on dynsem.properties. This is inconvenient and is probably unnecessary. The transformation should work without the configuration file.

The generation of the term library relies on a number of projections from DynSem types (sorts) to Java primitive types, non-primitive types and identifiers. This library of projections is non-reusable and hard to maintain. To allow further development we must refactor it.

Explication of the semantic components does not properly support the case pattern matching premise.

Changing the signatures used in a specification leads to a different set of Java classes to be generated for the term library. The target directory of the generated code should be cleaned before generation of the new library.

By default cleaning of the output directory should be enabled, but the developer should be able to disable this in the dynsem.properties configuration file.

@milosonator needs to apply a transformation (desugaring) to a Grace module before interpretation. How can this be done without copying the Java code generated from Stratego into the interpreter project?