glen/spoofax_prop
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

docs: Update to reflect pending changes in the Spoofax Tutorial/Reference

Browse Source
This commit is contained in:
Glen Whitney 2021-02-03 16:24:47 -08:00
parent ba130ecb0f
commit ae0a798c7b
8 changed files with 107 additions and 385 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
README.md
View File

@ -12,18 +12,9 @@ of those facilities can be created from more primitive operations of
term matching and replacement. Every step of the way is illustrated with actual, term matching and replacement. Every step of the way is illustrated with actual,
working Stratego programs. working Stratego programs.
There are, however, two catches for a newcomer trying to learn Spoofax and This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop)
Stratego for the first time: provides a working implementation of most of the examples in the manual.
It can be cloned as an Eclipse project (note the git root
1. All of the examples are worked in an older framework ("Stratego/XT") which
has a rather different collection of tools than the current implementation
of Spoofax in the Eclipse IDE.
1. Unlike with the Calc example language used for the explication of the
Syntax Definition Language SDF3, there does not seem to be any publicly
available repository containing the worked examples to follow along with.
This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop) aims
to fill both gaps. It can be cloned as an Eclipse project (note the git root
is at the project level rather than in the directory above the project, as may is at the project level rather than in the directory above the project, as may
be more common; in other words, this repository should be cloned within be more common; in other words, this repository should be cloned within
an existing Eclipse workspace, rather than as the workspace itself). Within that an existing Eclipse workspace, rather than as the workspace itself). Within that
@ -34,19 +25,15 @@ dealing with an arithmetical/imperative language (except in a couple of
isolated instances in which the relevant phenomenon is recast in the isolated instances in which the relevant phenomenon is recast in the
propositional language). propositional language).
This (Mkdocs-generated) documentation seeks to clarify the ways that Stratego
transformations may be run in the Spoofax/Eclipse IDE environment, serving as
a supplement/replacement for the portions of the manual that are
specific to Stratego/XT.
## Preliminaries ## Preliminaries
I recommend working with a complete pre-built Eclipse installation of Spoofax I recommend working with a complete pre-built Eclipse installation of Spoofax
as provided by the Spoofax project, as provided by the Spoofax project,
for example one that you can download from their for example one that you can download from their
[development release page](https://www.metaborg.org/en/latest/source/release/development.html). [development release page](https://www.metaborg.org/en/latest/source/release/development.html).
I have been unable to get the examples in this repository working starting from Sometimes I have had difficulty getting the examples in this repository working
plain Eclipse and installing Spoofax in it using the Spoofax update site. starting from plain Eclipse and installing Spoofax in it using the Spoofax
update site.
If at any point in using the examples things appear to stop working, and If at any point in using the examples things appear to stop working, and
especially if the Spoofax menu item disappears or the Spoofax menu turns into especially if the Spoofax menu item disappears or the Spoofax menu turns into
@ -68,9 +55,10 @@ operation at some point in the above process.
## Abstract syntax ## Abstract syntax
With the preliminaries out of the way, let's begin delving into Stratego With the preliminaries out of the way, note that the examples in the Stratego
transformations by recalling the abstract syntax of the manual deal exclusively with Abstract Syntax Trees (ASTs). The trees used
Spoofax Propositional Language (SPL), as defined are primarily for a language concerning propositional logic, which we dub the
Spoofax Propositional Language (SPL). It is defined
at the top of {! docrefs/sec4.1.md !} of the manual. at the top of {! docrefs/sec4.1.md !} of the manual.
It consists of the following signature of constructors: It consists of the following signature of constructors:

2
docrefs/sec4.2.md
View File

@ -1 +1 @@
[Section 4.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#adding-rules-to-a-rewrite-system) [Section 4.3](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#adding-rules-to-a-rewrite-system)

1
mkdocs.yml
View File

@ -21,3 +21,4 @@ markdown_extensions:
- pymdownx.superfences - pymdownx.superfences
- pymdownx.highlight: - pymdownx.highlight:
use_pygments: true use_pygments: true
- smarty

3
syntax/Spoofax-Propositional-Language.sdf3
View File

@ -68,7 +68,4 @@ you can visit the file `syntax/examples/sec4.1_A.spl` (or ...`_B.spl`) and from
Spoofax menu select "Syntax > Show parsed AST" to see the AST generation Spoofax menu select "Syntax > Show parsed AST" to see the AST generation
in action.) in action.)
This concrete syntax actually makes it easier to construct the example
expressions used throughout the tutorial manual as examples for Stratego
processing.
**/ **/

67
test/manual-suite.spt
View File

@ -267,40 +267,6 @@ test chap9_cnf7_ex [[
Or(Not(Atom("r")), Atom("q"))), Or(Not(Atom("r")), Atom("q"))),
Atom("p")) Atom("p"))
/** md
The key point to know about
[Chapter 9](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html),
however, is that there is a mistake that affects examples `prop-dnf8` through
`prop-dnf10`. The difficulty is in this definition:
```Stratego
strategies
propbu(s) = proptr(propbu(s)); s
```
Recall that `proptr` is defined as follows: (Note that our implementation calls
it `proptr7` to distinguish it from different definitions for `proptr` in other
examples.)
```Stratego
{! ../trans/prop-dnf7.str extract:
start: '(rules\n*)'
stop: strategies
!}
```
So `propbu` must be defined as:
```Stratego
{! ../trans/prop-dnf8.str extract:
start: strategies
stop: '(.*propbu8.*)'
!}
```
The point is that `proptr` cannot apply to `Atom`s and logical constants, and so
fails when it reaches such nodes in the AST. Without the `try` in the definition
of the `propbu` traversal, any such failure propagates to a failure of the entire
strategy.
**/
test chap9_dnf8_ex [[ test chap9_dnf8_ex [[
(r -> p & q) & p (r -> p & q) & p
]] run dnf8 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))) ]] run dnf8 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@ -311,10 +277,6 @@ test chap9_cnf8_ex [[
Or(Not(Atom("r")), Atom("q"))), Or(Not(Atom("r")), Atom("q"))),
Atom("p")) Atom("p"))
/** md
Example `prop-dnf9` simply re-uses `propbu8`.
**/
test chap9_dnf9_ex [[ test chap9_dnf9_ex [[
(r -> p & q) & p (r -> p & q) & p
]] run dnf9 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))) ]] run dnf9 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@ -325,14 +287,6 @@ test chap9_cnf9_ex [[
Or(Not(Atom("r")), Atom("q"))), Or(Not(Atom("r")), Atom("q"))),
Atom("p")) Atom("p"))
/** md
And a similar fix is made to `prop-dnf10`:
```Stratego
{! ../trans/prop-dnf10.str !}
```
**/
test sec9_1_dnf10_ex [[ test sec9_1_dnf10_ex [[
(r -> p & q) & p (r -> p & q) & p
]] run dnf10 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))) ]] run dnf10 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
@ -343,22 +297,6 @@ test sec9_1_cnf10_ex [[
Or(Not(Atom("r")), Atom("q"))), Or(Not(Atom("r")), Atom("q"))),
Atom("p")) Atom("p"))
/** md
There is another issue in the "Format Checking" example in section 9.1. It lies
with the strategy used to determine if an expression is an atom or the negation
of an atom. The expression shown is `Not(Atom(x)) <+ Atom(x)`. This appears to
be a left choice of two congruences. But a congruence expects a strategy as an
argument, whereas here `x` is simply a free variable. There are a couple of
fixes to write an expression that checks whether a term is just an `Atom()` call
or the negation of one. The first possibility is to use match expressions, e.g.
`?Not(Atom(x)) <+ ?Atom(x)`. However, as that can run into issues with the scoping
of the variable `x`, we opted for sticking with the congruences, just using a
strategy that always succeeds in the inner position, namely `id`:
```Stratego
{! ../trans/sec9_1.str terminate: exercise !}
```
**/
test sec9_1_disj-nf_fails [[ test sec9_1_disj-nf_fails [[
(r -> p & q) & p (r -> p & q) & p
]] run disj-nf fails ]] run disj-nf fails
@ -386,7 +324,7 @@ test sec9_1_cnf11_ex [[
Atom("p")) Atom("p"))
/** md /** md
Also note that the repository does not include `prop-dnf12` because at this Note that this repository does not include `prop-dnf12` because at this
point the strategies there have become identical to the ones point the strategies there have become identical to the ones
in {! ../docrefs/sec6.2.md !} used to introduce the idea of splitting in {! ../docrefs/sec6.2.md !} used to introduce the idea of splitting
transformations into local rewrite rules applied via a traversal strategy. So transformations into local rewrite rules applied via a traversal strategy. So
@ -454,8 +392,7 @@ test sec9_2_impl-nf_once [[
]] run impl-nf2 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False()) ]] run impl-nf2 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())
/** md /** md
I couldn't think of a natural application of paramorphism in the context of On the other hand there is no solution provided for the
the Spoofax Propositional Language, so there is no solution provided for the
exercise just before exercise just before
[Section 9.2.1](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#cascading-transformations). [Section 9.2.1](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#cascading-transformations).

140
trans/prop-dnf-rules.str
View File

@ -5,11 +5,29 @@ Title: Running a Strategy, continued
The next Stratego example, in {! ../docrefs/sec4.2.md !}, extends The next Stratego example, in {! ../docrefs/sec4.2.md !}, extends
`prop-eval-rules` to convert SPL propositions into disjunctive normal form (DNF). `prop-eval-rules` to convert SPL propositions into disjunctive normal form (DNF).
Once again, we can place the Stratego code in `trans/prop-dnf-rules.str`: As the manual notes, another way to see what the `dnf` strategy does to a given
AST is to add a Spoofax Test Language test that claims it transforms to
something that it definitely does **not** parse to, e.g.
```SPT
{! ../test/manual-suite.spt extract:
start: '\*\*[/]'
terminate: '(.*run dnf.*)$' !}
```
The difficulty is that in a standard Spoofax language project, the error popup
showing what the transformation actually does is nearly unreadable due to
a tremendous amount of annotation produced by the default static analysis process.
Since in this repository we are not actually doing any (meaningful) static
analysis, it includes a hack which makes the editor popup much more readable.
Namely, it strips the annotation, by modifying the
`editor-analyze` rule in `trans/analysis.str` like so:
```Stratego ```Stratego
{! ../trans/analysis.str terminate: Debugging!} [rest of file omitted]
```
**/ **/
/** md Include this code in documentation: */
module prop-dnf-rules module prop-dnf-rules
imports prop-eval-rules imports prop-eval-rules
rules rules
@ -23,121 +41,3 @@ rules
E : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) E : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))
/* end of code inclusion **/
/** md rest of documentation
```
and create a `trans/prop-dnf.str` that defines a strategy for applying the
DNF rules and supplies the glue needed between ESV and Stratego:
```Stratego
{! prop-dnf.str !}
```
Now just importing `prop-dnf` in `trans/spoofax-propositional-language.str`
and adding a menu item to `editor/Manual.esv`:
```ESV
...
{! ../editor/Manual.esv extract: {start: menus, stop: dnf3} !}
```
should suffice to make the dnf strategy available in the "Spoofax > Manual"
menu.
Indeed, we can try it out on `syntax/examples/sec4.2_test3.spl`:
```SPL
{! ../syntax/examples/sec4.2_test3.spl !}
```
to produce
```
{! ../syntax/examples/sec4.2_test3.dnf.aterm !}
```
as verified in the manual (again, modulo the "ATom" typo in the manual).
However, we also want to use this second example to show another method of
running Stratego strategies from the Eclipse IDE.
### Spoofax Testing Language
The
[Spoofax Testing Language](http://www.metaborg.org/en/latest/source/langdev/meta/lang/spt/index.html)
(SPT) is a declarative language that provides for a full range of tests
for a Spoofax language project. As such, it includes the ability to run an
arbitrary Stratego strategy on the results of parsing an arbitrary piece of
the language you're working with -- seemingly perfect for our interest in
trying our different Stratego transformations.
So, we can just take our `test3` expression above and make it a part of
an SPT test suite, which we will call `test/manual-suite.spt`:
```SPT
{! ../test/manual-suite.spt extract:
start: '\*\*[/]'
terminate: '(.*run dnf)' !}
```
Once we have saved this file, the tests run automatically. What does this mean?
The file seems to be just "sitting there;" there's no indication that anything
is happening. That's because this test we've just written **succeeds**. All we
asked is that Spoofax run the `dnf` transformation on the results of parsing
the test expression. It did that, and the transformation succeeded. So all is
well, and no output is generated.
But of course, we want to see what the _result_ of the transformation was. One
way of arranging that is to ask that SPT compare that result to a given AST.
If we use an AST like `Atom("x")` that can't possibly be the actual output
(since "x" does not occur in the input), then the error message will show
what the transformation actually produced. So we add just a bit to
`test/manual-suite.spt`:
```SPT
{! ../test/manual-suite.spt extract:
start: '\*\*[/]'
terminate: '(.*run dnf.*)$' !}
```
and now sure enough a little error symbol appears next to the test. If you hover
over it, a popup will show up, indicating that SPT was expecting `Atom("x")`,
but got... wait! What's this monstrosity?
```
Got: Or(And(Not(Atom("r"{TermIndex("test/manual-suite.spt",1)}){TermIndex
("test/manual-suite.spt",2)}),Atom("p"{TermIndex("test/manual-suite.spt",9)})
{TermIndex("test/manual-suite.spt",10)}),And(And(Atom("p"{TermIndex("test/manual-
suite.spt",3)}){TermIndex("test/manual-suite.spt",4)},Atom("q"{TermIndex
("test/manual-suite.spt",5)}){TermIndex("test/manual-suite.spt",6)}){TermIndex
("test/manual-suite.spt",7)},Atom("p"{TermIndex("test/manual-suite.spt",9)})
{TermIndex("test/manual-suite.spt",10)}))
```
Well, it is actually the result of running the `dnf` strategy on the result of
parsing ` {! ../syntax/examples/sec4.2_test3.spl !} `. It's just that Spoofax
automatically annotates every subterm of the parsed term with its location in
the input, and those annotations are carried through the Stratego
transformation. While this can be very helpful in figuring out exactly what
happened in the course of the transformation, it can also make the output
practically unreadable.
Fortunately, we can strip this annotation if we like, by modifying the
`editor-analyze` rule in `trans/analysis.str` like so:
```Stratego
{! ../trans/analysis.str terminate: Debugging!} [rest of file omitted]
```
Now rebuild the project and re-run the SPT manual suite. (You may need to
do an irrelevant edit and save of the `test/manual-suite.spt` file, or
you can select this file in the project explorer and select the menu item
"Spoofax (meta) > Run all selected tests" to pop up a convenient window of
all test results.) Now you should see the much more readable
```
Got: Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
```
in the error message for the `sec4_2_test3` test.
Of course, if you know the AST you expect to generate with your transformation,
you can also just tell SPT to compare against that, for example in our case
by adding a test to the manual suite like this:
```SPT
{! ../test/manual-suite.spt extract:
start: '(test sec4_2_test3_ex.*\n?)$'
stop: '^(.*run.*)$'
!}
```
Now if there is no error or warning on this test then you know the
`dnf` strategy produced the result shown in the `to` clause, and otherwise,
the actual result will be shown in the error popup.
**/

75
trans/prop-dnf3.str
View File

@ -4,7 +4,7 @@ Title: Running a Strategy: the command line
## Functionalizing reduction rules ## Functionalizing reduction rules
The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to
add the ability to also compute conjunctive normal forms for propositional add the ability to also compute conjunctive normal forms (CNF) for propositional
ASTs. The rules for this form cannot simply be added to those from the prior ASTs. The rules for this form cannot simply be added to those from the prior
chapter for disjunctive normal form, as they would produce a non-terminating chapter for disjunctive normal form, as they would produce a non-terminating
rewrite system. rewrite system.
@ -12,13 +12,26 @@ rewrite system.
The first method for which working examples are provided is the method of The first method for which working examples are provided is the method of
"functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern "functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern
in the views of the Spoofax designers, the examples are still instructive and in the views of the Spoofax designers, the examples are still instructive and
of course we want to implement them here. of course they are implemented here.
In fact, the Stratego code
for the CNF is not given explicitly in the manual, but it consists of:
```
{! prop-cnf3.str !}
```
Note in particular we have not repeated the `make-nf` strategy from
`trans/prop-dnf3.str` here --- that's the
entire point of functionalization; we can use the same top-level reduction
scheme because the introduced function symbols keep track of what operations
are being performed. We also introduce a strategy `dcnf` for the simultaneous
construction of DNF and CNF, as noted in the manual.
Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies
as well. All operate just as in the previous sections.
So, we can grab the Stratego code given in the section as our
`trans/prop-dnf3.str`:
```Stratego
**/ **/
/** md Include this code in docs: */
module prop-dnf3 module prop-dnf3
imports libstrategolib signatures/- imports libstrategolib signatures/-
signature signature
@ -50,53 +63,8 @@ strategies
do-dnf3: (selected, _, _, path, project-path) -> (filename, result) do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
with filename := <guarantee-extension(|"dnf.aterm")> path with filename := <guarantee-extension(|"dnf.aterm")> path
; result := <dnf3> selected ; result := <dnf3> selected
/* End of code inclusion **/
/** md Conclusion of documentation:
```
Notice the few minor differences from the manual. We import `signatures/-` as /** md
before. We've used a fresh identifier for the `E` and `D` rules, because unlike
in the manual, all of our Stratego files are imported into the same main
`trans/spoofax_propositional_language.str` module. So they must live together,
but as noted in the manual, these functionalized rules do not "play together"
nicely with the evaluation `E` rules introduced [earlier](prop-eval-rules.md).
And we've renamed the `dnf` rule to `make-nf` -- for a reason that will
become clear in a moment -- but incorporated the wrapping by `Dnf` of the AST
we want to compute the DNF of into the `dnf3` strategy, since our concrete
syntax has no way of specifying such a wrapping.
Also as before, we've created a `syntax/examples/sec_5_1_2_test1.spl`
(which it turns out is just the same as `sec_4_2_test3.spl`)
and a menu item and a `test/manual-suite.spt` case called `sec5_1_2_test1_ex` to
see that all is working well. Applying `dnf3` to the test file produces
```
{! ../syntax/examples/sec5.1.2_test1.dnf.aterm !}
```
which is correct. (Note the contrast with what's shown in
{! ../docrefs/sec5.1.2.md !} as the output of the `prop-dnf3` program,
in which the recurring "ATom" typo has blocked
the reductive elimination of some of the occurrences of the Dnf function
symbol. Of course, as the manual itself points out, in proper operation of
this functionalization approach, all of the function symbols must reduce away
to end up back in an AST of the subject language.)
So now we can move on to the conjunctive normal form. The Stratego code
for the CNF is not given explicitly in the manual, but it consists of:
```
{! prop-cnf3.str !}
```
Note in particular we have not repeated the `make-nf` strategy -- that's the
entire point of functionalization; we can use the same top-level reduction
scheme because the introduced function symbols keep track of what operations
are being performed. We also introduce a strategy `dcnf` for the simultaneous
construction of DNF and CNF, as noted in the manual.
Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies
as well. All operate just as in the previous two sections.
We can now use this example to show yet another way to try Stratego stragies
with the Spoofax IDE implementation.
### Command-line Utilities ### Command-line Utilities
@ -105,7 +73,8 @@ The Spoofax project offers an executable jar called
that allows several different Spoofax actions to be invoked from the command line. that allows several different Spoofax actions to be invoked from the command line.
Let's say you have downloaded it to the path `SUNSHINE_JAR`. Then you can see a Let's say you have downloaded it to the path `SUNSHINE_JAR`. Then you can see a
summary of the available actions with `java -jar $SUNSHINE_JAR -h`. In the summary of the available actions with `java -jar $SUNSHINE_JAR -h`. In the
repository there's a convenience bash script `bin/spoofax-menu`: repository there's a convenience bash script `bin/spoofax-menu` you can use to
run the Sunshine jar:
```bash ```bash
{! ../bin/spoofax-menu extract: {! ../bin/spoofax-menu extract:
- stop: --help - stop: --help

172
trans/prop-eval-rules.str
View File

@ -5,17 +5,60 @@ Title: Running a Strategy
The first example of running a Stratego strategy The first example of running a Stratego strategy
in the {! ../docrefs/manual.md !} is that of _evaluating_ an AST, in the {! ../docrefs/manual.md !} is that of _evaluating_ an AST,
via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. This page via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. In this
describes the most straightforward way to run this same strategy repository, we've placed those rules in `trans/prop-eval-rules.str`,
in the Spoofax Eclipse IDE. and the glue strategies that call them in `trans/prop-eval.str`. This latter
module is imported by `trans/spoofax_propositional_language.str`.
In the current project structure, Stratego transformations and strategies go in (I am unclear on what triggers Editor Services to use this particular Stratego
the `trans` directory. So, you can place the Stratego code for file, but in any automatically-generated Spoofax project there will be a
this module in `trans/prop-eval-rules.str`, with the following contents: main language Stratego file in the `trans` directory, and that's the file
from which the rule specified in an ESV `action` has to be visible.)
There's an Editor Services module `editor/Manual.esv` to invoke the eval strategy,
and it's included in in `editor/Main.esv.`
With all of these elements in place, you should now be able to invoke
the `eval` rule from the "Spoofax" menu. For example, to execute the "test1"
example from the Spoofax Tutorial/Reference
{! ../docrefs/sec4.1.md !}, navigate to the
file `syntax/examples/sec4.1_test1.spl`:
```SPL
{! ../syntax/examples/sec4.1_test1.spl !}
```
and select "Spoofax > Manual > prop-eval" from the menu bar to produce:
```
{! ../syntax/examples/sec4.1_test1.eval.aterm !}
```
You can do the same with test2:
```SPL
{! ../syntax/examples/sec4.1_test2.spl !}
```
to produce
```
{! ../syntax/examples/sec4.1_test2.eval.aterm !}
```
Both of these results match the expected output of the `eval` transformation
as shown in {! ../docrefs/sec4.1.md !}.
One other note about the files provided in this repository. The "do-XXX" rule
used as boilerplate glue between ESV and a Stratego strategy in
`trans/prop-eval.str` is:
```Stratego ```Stratego
[End the documentation block to avoid the comment close in the code] **/ {! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
/** md [restart processing to include the code in the documentation] */ ```
The version of this glue being used here corresponds to what's used in the example
[Calc language project](https://github.com/MetaBorgCube/metaborg-calc),
but is slightly different from what is described in the
[Menus section](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html#menus)
of the ESV Manual. I am unclear on the significance of this difference or which
form is "better" -- I simply modeled this Stratego code after the code in the
working Calc repository, and all seems to be well.
**/
module prop-eval-rules module prop-eval-rules
imports signatures/- imports signatures/-
rules rules
@ -37,116 +80,3 @@ rules
E : Eq(x, False()) -> Not(x) E : Eq(x, False()) -> Not(x)
E : Eq(True(), x) -> x E : Eq(True(), x) -> x
E : Eq(x, True()) -> x E : Eq(x, True()) -> x
/* [stop to avoid the open-comment in the code block] **/
/** md [conclusion of the documentation]
```
Note an important difference between this code and the `prop-eval-rules` block
in {! ../docrefs/sec4.1.md !}: here, we import `signatures/-` rather than `prop`.
That's because the Spoofax IDE automatically generates the Spoofax Propositional
Language AST signature for us, from its concrete syntax definition. (The
evaluation rules in {! ../docrefs/sec4.1.md !} also happen to be missing the
fourth `Impl` rule, but that's less material; unsurprisingly, none of the examples
given in the manual happen to rely on that rule, but we include it here for the
sake of completeness.)
As in the {! ../docrefs/manual.md !}, we need an additional module, which we can
place in `trans/prop-eval.str`, to describe the strategy by which we want
to apply the above evaluation rules and to facilitate actually invoking
the strategy on an AST. This file starts out much like its counterpart in
{! ../docrefs/sec4.1.md !}:
```Stratego
{! prop-eval.str {terminate: '^\s*$'} !}
```
So far, we've included the evaluation rules and defined a strategy `eval` to
apply them exhaustively to an AST starting with inner subterms. Now we want to
be able to "run" this strategy on an actual AST.
### Editor Services
The most straightforward mechanism to execute a Stratego transformation
in the Spoofax IDE is by use of Editor Services (ESV). ESV is actually a full
declarative language in its own right, covering syntax coloring, menu items,
hover texts, and more, and with its own
[manual](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html).
We will not delve into the details of ESV here, but merely provide a recipe
for using it to add an item to the "Spoofax" Eclipse menu for running Stratego.
Actually, we'll create a submenu "Manual" for our examples. It's
cleanest to put our additions in a separate ESV module, which then must be
included into the `editor/Main.esv` file, like so:
```esv
{! ../editor/Main.esv extract:
replace: ['^\s*$']
terminate: 'provider\s*:' !} [ ... rest of file suppressed for brevity. ]
```
It's just the one line "Manual" in the `imports` section that we have added. The
`editor/Manual.esv` implementing the submenu is also very simple:
```esv
{! ../editor/Manual.esv terminate: dnf !}
```
Note that the quoted string on the `action` line is the text label of the menu
item in the "Manual" submenu, and the identifier on its right-hand side is the
Stratego action to call. But note that `do-eval` is not the same identifier as
`eval` in our last Stratego file above. That's because the Stratego invocation
caused by an ESV action item has a specific, multi-item argument list, whereas
`eval` above expects only a single Spoofax Propositional Language AST to operate
on. To bridge this gap, we must add one more item to `trans/prop-eval.str`,
namely:
```Stratego
{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
```
This "do-XXX" rule is pretty much boilerplate glue between ESV and your Stratego
strategy of interest. (Note that this "glue" being used here corresponds to
what's used in the example
[Calc language project](https://github.com/MetaBorgCube/metaborg-calc),
but is slightly different from what is described in the
[Menus section](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html#menus)
of the ESV Manual. I am unclear on the significance of this difference or which
form is "better" -- I simply modeled this Stratego code after the code in the
working Calc repository, and all seems to be well.)
There's one last step before you can run `eval` from inside the IDE.
Editor Services has to be able to find the `do-eval` rule. You can enable that
by importing the `prop-eval` module in the main Stratego file for our language,
in this case `trans/spoofax_propositional_language.str`:
```Stratego
{! spoofax_propositional_language.str extract:
- stop: 'prop-dnf'
- start: '^(.*rule.*)$'
terminate: debug-show
!}
[ ... rest of file suppressed. ]
```
(I am unclear on what triggers ESV to use this particular Stratego file, but
in any automatically-generated Spoofax project there will be a main language
Stratego file in the `trans` directory, and that's the file from which
the rule specified in an ESV `action` has to be visible.)
Ok, with all of these elements in place, you should now be able to invoke
the `eval` rule from the "Spoofax" menu. For example, to execute the next example
from the Spoofax Tutorial/Reference
{! ../docrefs/sec4.1.md !}, navigate to the
file `syntax/examples/sec4.1_test1.spl`:
```SPL
{! ../syntax/examples/sec4.1_test1.spl !}
```
and select "Spoofax > Manual > prop-eval" from the menu bar to produce:
```
{! ../syntax/examples/sec4.1_test1.eval.aterm !}
```
You can do the same with test2:
```SPL
{! ../syntax/examples/sec4.1_test2.spl !}
```
to produce
```
{! ../syntax/examples/sec4.1_test2.eval.aterm !}
```
Both of these results match the expected output of the `eval` transformation
as shown in {! ../docrefs/sec4.1.md !} (allowing for the typo "ATom" in the
manual in the latter case).
**/