Compare commits
13 Commits
| Author | SHA1 | Date |
|---|---|---|
 Glen Whitney
|
ae0a798c7b | |
|
Glen Whitney
|
ba130ecb0f | |
|
Glen Whitney
|
fddc94a906 | |
|
Glen Whitney
|
98bb2088e4 | |
|
Glen Whitney
|
76456b2c21 | |
|
Glen Whitney
|
d5a19e0d69 | |
|
Glen Whitney
|
a33c1585d6 | |
|
Glen Whitney
|
19076a5163 | |
|
Glen Whitney
|
50dce6b265 | |
|
Glen Whitney
|
347afef2e5 | |
|
Glen Whitney
|
28a3370d03 | |
|
Glen Whitney
|
2357e1f220 | |
|
Glen Whitney
|
8536d6a469 |
|
|
@ -5,6 +5,7 @@
|
|||
/site
|
||||
|
||||
/.classpath
|
||||
/.project
|
||||
/.settings
|
||||
/.factorypath
|
||||
|
||||
|
|
|
|||
48
.project
48
.project
|
|
@ -1,48 +0,0 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<projectDescription>
|
||||
<name>spoofax_prop</name>
|
||||
<comment></comment>
|
||||
<projects>
|
||||
</projects>
|
||||
<buildSpec>
|
||||
<buildCommand>
|
||||
<name>org.eclipse.m2e.core.maven2Builder</name>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
<buildCommand>
|
||||
<name>org.metaborg.spoofax.eclipse.meta.builder.generatesources</name>
|
||||
<triggers>clean,full,</triggers>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
<buildCommand>
|
||||
<name>org.metaborg.spoofax.eclipse.builder</name>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
<buildCommand>
|
||||
<name>org.metaborg.spoofax.eclipse.meta.builder.prejava</name>
|
||||
<triggers>clean,full,</triggers>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
<buildCommand>
|
||||
<name>org.eclipse.jdt.core.javabuilder</name>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
<buildCommand>
|
||||
<name>org.metaborg.spoofax.eclipse.meta.builder.postjava</name>
|
||||
<triggers>clean,full,</triggers>
|
||||
<arguments>
|
||||
</arguments>
|
||||
</buildCommand>
|
||||
</buildSpec>
|
||||
<natures>
|
||||
<nature>org.eclipse.m2e.core.maven2Nature</nature>
|
||||
<nature>org.eclipse.jdt.core.javanature</nature>
|
||||
<nature>org.metaborg.spoofax.eclipse.nature</nature>
|
||||
<nature>org.metaborg.spoofax.eclipse.meta.nature</nature>
|
||||
</natures>
|
||||
</projectDescription>
|
||||
76
README.md
76
README.md
|
|
@ -1,26 +1,82 @@
|
|||
Title: The Spoofax Propositional Language
|
||||
Next: syntax/Spoofax-Propositional-Language.sdf3
|
||||
|
||||
# Stratego Transformations in the Spoofax Eclipse IDE
|
||||
|
||||
The Stratego Tutorial/Reference {! docrefs/manual.md !} in the official Spoofax documentation presents a comprehensive overview of the Stratego approach to abstract syntax tree (AST) transformations. It employs a running example of an abstract syntax intended to represent classical Propositional Logic, which we will dub here the "Spoofax Propositional Language." The manual introduces the concepts of rules and strategies for applying them, and then shows how both of those facilities can be created from more primitive operations of term matching and replacement. Every step of the way is illustrated with actual, working Stratego programs.
|
||||
The Stratego Tutorial/Reference {! docrefs/manual.md !} in the official Spoofax
|
||||
documentation presents a comprehensive overview of the Stratego approach to
|
||||
abstract syntax tree (AST) transformations. It employs a running example of an
|
||||
abstract syntax intended to represent classical Propositional Logic, which we
|
||||
will dub here the "Spoofax Propositional Language." The manual introduces the
|
||||
concepts of rules and strategies for applying them, and then shows how both
|
||||
of those facilities can be created from more primitive operations of
|
||||
term matching and replacement. Every step of the way is illustrated with actual,
|
||||
working Stratego programs.
|
||||
|
||||
There are, however, two catches for a newcomer trying to learn Spoofax and Stratego for the first time:
|
||||
This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop)
|
||||
provides a working implementation of most of the examples in the manual.
|
||||
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
|
||||
be more common; in other words, this repository should be cloned within
|
||||
an existing Eclipse workspace, rather than as the workspace itself). Within that
|
||||
project, all of the examples from the Stratego Tutorial manual that employ the
|
||||
propositional language (see below), starting from Section 4 on, can be executed
|
||||
directly. This repository does not attempt to implement the portion of examples
|
||||
dealing with an arithmetical/imperative language (except in a couple of
|
||||
isolated instances in which the relevant phenomenon is recast in the
|
||||
propositional language).
|
||||
|
||||
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.
|
||||
## Preliminaries
|
||||
|
||||
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 be more common; in other words, this repository should be cloned within an existing Eclipse workspace, rather than as the workspace itself). Within that project, (ultimately) every example from the Stratego Tutorial manual starting from Section 4 on can be executed directly. And 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 were specific to Stratego/XT.
|
||||
I recommend working with a complete pre-built Eclipse installation of Spoofax
|
||||
as provided by the Spoofax project,
|
||||
for example one that you can download from their
|
||||
[development release page](https://www.metaborg.org/en/latest/source/release/development.html).
|
||||
Sometimes I have had difficulty getting the examples in this repository working
|
||||
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
|
||||
especially if the Spoofax menu item disappears or the Spoofax menu turns into
|
||||
a thin white rectangle with no items to select, try the following:
|
||||
|
||||
* Build the project and try again.
|
||||
* Clean the workspace, and when it is done, build the project again and try
|
||||
again.
|
||||
* Right click on the project, select Maven > Update Project, make sure
|
||||
everything is checked except "Offline" and
|
||||
"Force update of Snapshots/Releases", and then click "OK". When it is done,
|
||||
clean the workspace, then build the project and try again.
|
||||
* If that still hasn't done it, restart (the Spoofax version of!) Eclipse and
|
||||
clean the workspace, then build the project and try again.
|
||||
|
||||
Running with a version of Spoofax _later_ than 2.5.13 (I was using a 2.6.0
|
||||
development snapshot), the Spoofax menu would always come back into proper
|
||||
operation at some point in the above process.
|
||||
|
||||
## Abstract syntax
|
||||
|
||||
Let's begin by recalling the abstract syntax of the Spoofax Propositional Language (SPL), as defined at the top of {! docrefs/sec4.1.md !} of the manual. It consists of the following signature of constructors:
|
||||
With the preliminaries out of the way, note that the examples in the Stratego
|
||||
manual deal exclusively with Abstract Syntax Trees (ASTs). The trees used
|
||||
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.
|
||||
It consists of the following signature of constructors:
|
||||
|
||||
```stratego
|
||||
{! src-gen/signatures/Spoofax-Propositional-Language-sig.str ---
|
||||
{! src-gen/signatures/Spoofax-Propositional-Language-sig.str extract:
|
||||
start: '(signature[\s]*)$'
|
||||
end: '^(\s*Eq\s*:.*)'
|
||||
stop: '^(\s*Eq\s*:.*)'
|
||||
!}
|
||||
```
|
||||
<!-- /md -->
|
||||
Continue reading in the latest released [SPL documentation](http://studioinfinity.org/SPL) to see how to define and run Stratego transformations on ASTs of this language.
|
||||
Continue reading in the latest released
|
||||
[SPL documentation](http://studioinfinity.org/SPL)
|
||||
to see how to define and run Stratego transformations on ASTs of this language.
|
||||
|
||||
### Building the documentation
|
||||
|
||||
In order to build the documentation from a clone of this repository, you must
|
||||
install [MkDocs](http://mkdocs.org) and the `semiliterate` plug-in for MkDocs,
|
||||
which is available in
|
||||
[pre-release form](https://code.studioinfinity.org/glen/mkdocs-semiliterate). Then
|
||||
you can execute `mkdocs build` in the top-level directory of this project.
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
[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)
|
||||
|
|
@ -0,0 +1 @@
|
|||
[Section 5.1.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#attempt-2-functionalization)
|
||||
|
|
@ -0,0 +1 @@
|
|||
[Section 6.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/06-rules-and-strategies.html#what-is-a-strategy)
|
||||
|
|
@ -1,7 +1,8 @@
|
|||
module Manual
|
||||
|
||||
menus
|
||||
|
||||
menu: "Manual" (openeditor)
|
||||
|
||||
action: "prop-eval" = do-eval
|
||||
menu: "Manual" (openeditor) (source)
|
||||
action: "prop-eval" = do-eval
|
||||
action: "prop-dnf" = do-dnf
|
||||
action: "prop-dnf3" = do-dnf3
|
||||
action: "prop-cnf3" = do-cnf3
|
||||
action: "both-nf3" = do-dcnf
|
||||
|
|
|
|||
|
|
@ -20,7 +20,6 @@ menus
|
|||
|
||||
action: "Format" = editor-format (source)
|
||||
action: "Show parsed AST" = debug-show-aterm (source)
|
||||
action: "Test action" = debug-show-aterm
|
||||
|
||||
views
|
||||
|
||||
|
|
|
|||
|
|
@ -11,6 +11,9 @@ nav:
|
|||
- README.md
|
||||
- syntax/Spoofax-Propositional-Language.md
|
||||
- trans/prop-eval-rules.md
|
||||
- trans/prop-dnf-rules.md
|
||||
- trans/prop-dnf3.md
|
||||
- test/manual-suite.md
|
||||
theme:
|
||||
name: readthedocs
|
||||
markdown_extensions:
|
||||
|
|
@ -18,3 +21,4 @@ markdown_extensions:
|
|||
- pymdownx.superfences
|
||||
- pymdownx.highlight:
|
||||
use_pygments: true
|
||||
- smarty
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ Title: Concrete Syntax
|
|||
The current Spoofax/Eclipse IDE is oriented around individual language
|
||||
projects. Therefore in order to work with ASTs of the SPL
|
||||
[abstract syntax](../README.md#abstract-syntax) that we just saw, it's easiest to
|
||||
define a concrete syntax for SPL, with the following SDF3 definition:
|
||||
define a concrete syntax for SPL, via the following SDF3 definition:
|
||||
|
||||
*[SPL]: Spoofax Propositional Language
|
||||
|
||||
|
|
@ -34,10 +34,10 @@ context-free syntax
|
|||
Prop.False = <0>
|
||||
Prop.Atom = String
|
||||
Prop.Not = <!<Prop>>
|
||||
Prop.And = <<Prop> & <Prop>>
|
||||
Prop.Or = <<Prop> | <Prop>>
|
||||
Prop.Impl = [[Prop] -> [Prop]]
|
||||
Prop.Eq = <<Prop> = <Prop>>
|
||||
Prop.And = <<Prop> & <Prop>> {left}
|
||||
Prop.Or = <<Prop> | <Prop>> {left}
|
||||
Prop.Impl = [[Prop] -> [Prop]] {right}
|
||||
Prop.Eq = <<Prop> = <Prop>> {non-assoc}
|
||||
Prop = <(<Prop>)> {bracket}
|
||||
|
||||
String = ID
|
||||
|
|
@ -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
|
||||
in action.)
|
||||
|
||||
This concrete syntax actually makes it easier to construct the example
|
||||
expressions used throughout the tutorial manual as examples for Stratego
|
||||
processing.
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -0,0 +1 @@
|
|||
(r -> p & q) & p
|
||||
|
|
@ -0,0 +1 @@
|
|||
(r -> p & q) & p
|
||||
|
|
@ -0,0 +1,403 @@
|
|||
/** md
|
||||
Title: The Remaining Tests
|
||||
|
||||
## Programmable Rewriting Strategies
|
||||
|
||||
The manual then begins to discuss "programmable rewriting strategies" in
|
||||
[Section 5.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#programmable-rewriting-strategies)
|
||||
and beyond to show how to use Stratego's various features to overcome the
|
||||
difficulties with the last several examples.
|
||||
|
||||
The next example is in Section 5.3.1, which shows a unified treatment of
|
||||
disjunctive and conjunctive normal forms that avoids the potential combinatorial
|
||||
explosion of rules seen in the functionalized example. As usual, the example
|
||||
Stratego module `prop-laws` is in `trans/prop-laws.str` and included in
|
||||
`trans/spoofax_propositional_language.str`. Also as typical, some of the identifiers
|
||||
in the module had to be changed to avoid namespace conflicts when they are all
|
||||
imported into the main language module.
|
||||
|
||||
But after going through the previous examples, it seems that trying them is most
|
||||
convenient with the Spoofax Testing Language:
|
||||
|
||||
* No glue transformation is needed and no ESV files need to be modified.
|
||||
* It's not necessary to place the SPL expression to be tested in a separate file.
|
||||
* The SPL expression, name of strategy to run, and results of that run are all
|
||||
kept together (in the `test/manual-suite.spt` file).
|
||||
|
||||
Hence, the test cases for Section 5.3.1 and beyond, through the end of the
|
||||
Tutorial/Reference Manual, are captured in this repository solely in terms
|
||||
of SPT Test Cases. You can of course clone the repository and create menu items
|
||||
for any of them if you want to try them that way. Just remember to add a
|
||||
"glue" strategy for them as shown in the [first example](../trans/prop-eval-rules.md).
|
||||
|
||||
Hopefully these examples are helpful to your exploration and understanding of
|
||||
Stratego -- certainly creating them was to mine.
|
||||
|
||||
Additional notes on particular sections or tests follow.
|
||||
**/
|
||||
module manual-suite
|
||||
language Spoofax-Propositional-Language
|
||||
|
||||
test sec4_2_test3 [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf to Atom("x")
|
||||
|
||||
test sec4_2_test3_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test sec5_1_2_test1_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf3 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test sec5_1_2_test1_cnf_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf3 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test sec5_1_2_test1_both [[
|
||||
(r -> p & q) & p
|
||||
]] run dcnf to (Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p"))),
|
||||
And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p")))
|
||||
|
||||
test sec5_3_1_test1_dnf_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf-laws to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test sec5_3_1_test1_cnf_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf-laws to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test sec5_3_2_eval_up_ex [[
|
||||
(1 -> p & q) & p
|
||||
]] run eval-up to And(And(Atom("p"),Atom("q")),Atom("p"))
|
||||
|
||||
test sec5_3_2_eval_down_ex [[
|
||||
(1 -> p & q) & p
|
||||
]] run eval-down to And(And(Atom("p"),Atom("q")),Atom("p"))
|
||||
|
||||
test sec5_3_2_desugar_ex [[
|
||||
(1 -> p & q) & p
|
||||
]] run desugar to And(Or(Not(True()),And(Atom("p"),Atom("q"))),Atom("p"))
|
||||
|
||||
test sec5_3_2_impl_nf_ex [[
|
||||
(1 -> p & q) & p
|
||||
]] run impl-nf to Impl(Impl(Impl(True(),Impl(Impl(Atom("p"),
|
||||
Impl(Atom("q"),False())),
|
||||
False())),
|
||||
Impl(Atom("p"),False())),
|
||||
False())
|
||||
|
||||
/** md
|
||||
### Chapter 6
|
||||
|
||||
Many of the examples in
|
||||
[Chapter 6](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/06-rules-and-strategies.html)
|
||||
are in the form of interactive "Stratego shell" sessions. For this repository, we
|
||||
have to convert them to rule definitions in a Stratego file (`chap6.str`) and
|
||||
test cases for each of the executed examples.
|
||||
|
||||
Also, there are some examples for a Plus-Times signature; we transpose these
|
||||
to Or-And for the sake of keeping everything within the SPL language project.
|
||||
|
||||
To illustrate extending a rule, we need to give the rule we're going to extend
|
||||
a different identifier and add both definitions to that (otherwise our original
|
||||
rule `SwapArgs` would already have been extended).
|
||||
|
||||
The `chap6.str` file also includes a solution to the exercise
|
||||
in {! ../docrefs/sec6.2.md !}. On the other hand, it is not clear whether
|
||||
the Spoofax Eclipse IDE has a "debug" operator for Stratego, or if so how
|
||||
it would work within the IDE, so the repository does not
|
||||
attempt to implement the "debug" example.
|
||||
|
||||
The remainder of the chapter (from section 6.3 on) consists of general information
|
||||
about Stratego syntax and information about the Stratego compiler. As it's not
|
||||
clear whether the latter applies to the Spoofax Eclipse IDE, there are no further test
|
||||
cases in this repository beyond Section 6.2.
|
||||
**/
|
||||
|
||||
test sec6_1_swap_ex [[
|
||||
p | 0
|
||||
]] run SwapArgs to Or(False(), Atom("p"))
|
||||
|
||||
test sec6_1_swap_fails [[
|
||||
p & 0
|
||||
]] run SwapArgs fails
|
||||
|
||||
test sec6_1_swap_subterm_fails [[
|
||||
(1 | p) & 0
|
||||
]] run SwapArgs fails
|
||||
|
||||
test sec6_1_swap_only_outer_ex [[
|
||||
(1 | p) | 0
|
||||
]] run SwapArgs to Or(False(), Or(True(), Atom("p")))
|
||||
|
||||
test sec6_1_swapboth_or_ex [[
|
||||
p | 0
|
||||
]] run SwapBoth to Or(False(), Atom("p"))
|
||||
|
||||
test sec6_1_swapboth_and_ex [[
|
||||
p & 0
|
||||
]] run SwapBoth to And(False(), Atom("p"))
|
||||
|
||||
test sec6_2_invoke_rule_ex [[
|
||||
1 -> p
|
||||
]] run DefI to Or(Not(True()), Atom("p"))
|
||||
|
||||
test sec6_2_innermost_ex [[
|
||||
p = q
|
||||
]] run dnf-laws to Or(Or(And(Not(Atom("p")),Not(Atom("q"))),
|
||||
And(Not(Atom("p")),Atom("p"))),
|
||||
Or(And(Atom("q"),Not(Atom("q"))),
|
||||
And(Atom("q"),Atom("p"))))
|
||||
|
||||
test sec6_2_dnf_exercise_ex [[
|
||||
p = q
|
||||
]] run better-dnf to Or(And(Not(Atom("p")),Not(Atom("q"))),
|
||||
And(Atom("q"),Atom("p")))
|
||||
|
||||
/** md
|
||||
### Chapter 7
|
||||
|
||||
The content and style of chapter 7 are similar to chapter 6. Again, there is a
|
||||
`trans/chap7.str` Stratego file defining several of the rules used in the examples
|
||||
from the chapter. As before, the examples with a different signature are recast
|
||||
into the SPL signature. Specifically, `Z` becomes `False`, `S(x)` becomes
|
||||
`Impl(True(), x)`, and `P` becomes `Or`. (At least with these choices, all of the
|
||||
transformations in the chapter remain valid in the usual semantics for the SPL
|
||||
signature, even if a bit unorthodox.)
|
||||
**/
|
||||
|
||||
test sec7_2_b_ex [[
|
||||
(1 -> 0) | 0
|
||||
]] run B to Or(False(), Impl(True(), False()))
|
||||
|
||||
test sec7_2_b_a_ex [[
|
||||
(1 -> 0) | 0
|
||||
]] run BthenA to Impl(True(), False())
|
||||
|
||||
test sec7_2_b_b_fails [[
|
||||
(1 -> 0) | 0
|
||||
]] run Btwice fails
|
||||
|
||||
test sec7_2_local_choice_fails [[
|
||||
(1 -> 0) | 0
|
||||
]] run maybeB-id-thenB fails
|
||||
|
||||
test sec7_2_seq_no_dist_over_choice_ex [[
|
||||
(1 -> 0) | 0
|
||||
]] run maybeBtwice-idthenB to Or(False(), Impl(True(), False()))
|
||||
|
||||
test sec7_3_repeat_small_ex [[
|
||||
(1 -> 0) | 0
|
||||
]] run repeatmaybeAB to Impl(True(), False())
|
||||
|
||||
test sec7_3_repeat_big_ex [[
|
||||
(1 -> 1 -> 1 -> 1 -> 0) | 0
|
||||
]] run repeatmaybeAB to Impl(True(), Impl(True(), Impl(True(),
|
||||
Impl(True(), False()))))
|
||||
|
||||
/** md
|
||||
### Chapter 8
|
||||
|
||||
This chapter is even more just a collection of interactive examples. In this
|
||||
repository we just give some examples of swapping and variable scope using the
|
||||
SPL signature, and some free-form examples of term wrapping and projecting.
|
||||
There's no attempt to do any of the arithmetic examples because SPL does not have
|
||||
an integer type.
|
||||
**/
|
||||
|
||||
test sec8_3_firstswap_ex [[
|
||||
p | 0
|
||||
]] run SwapWithPat to Or(False(), Atom("p"))
|
||||
|
||||
test sec8_3_1_swap_ex [[
|
||||
p | 0
|
||||
]] run SwapAnon to Or(False(), Atom("p"))
|
||||
|
||||
test sec8_3_2_variablescope_fails [[
|
||||
p | 0
|
||||
]] run NoSwapTwice fails
|
||||
|
||||
test sec8_3_2_localscope_ex [[
|
||||
p | 0
|
||||
]] run OkSwapTwice to Or(Atom("p"), False())
|
||||
|
||||
test sec8_5_1_wrap_ex [[
|
||||
p
|
||||
]] run TermWrap to Or(Atom("p"), Not(Atom("p")))
|
||||
|
||||
test sec8_5_2_project_ex [[
|
||||
p | !p
|
||||
]] run TermProj to Atom("p")
|
||||
|
||||
/** md
|
||||
### Chapter 9
|
||||
|
||||
This chapter is much more in the style of the early chapters: there are several
|
||||
explicit Stratego modules, and we incorporate each one into this repository. As
|
||||
before, we need to differentiate the names in some modules since they all end
|
||||
up being loaded at once; but we also take advantage of the common sections of
|
||||
some of the modules and re-use rather than repeat the code. In addition, the
|
||||
disjunctive and conjunctive normal forms of the same test expression as used
|
||||
in Chapter Five are used for test cases in `trans/manual-suite.spt`.
|
||||
|
||||
**/
|
||||
|
||||
test chap9_dnf4_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf4 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test chap9_dnf6_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf6 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test chap9_dnf7_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf7 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test chap9_cnf7_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf7 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test chap9_dnf8_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf8 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test chap9_cnf8_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf8 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test chap9_dnf9_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf9 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test chap9_cnf9_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf9 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test sec9_1_dnf10_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf10 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test sec9_1_cnf10_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf10 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
test sec9_1_disj-nf_fails [[
|
||||
(r -> p & q) & p
|
||||
]] run disj-nf fails
|
||||
|
||||
test sec9_1_conj-nf_fails [[
|
||||
(r -> p & q) & p
|
||||
]] run conj-nf fails
|
||||
|
||||
test sec9_1_disj-nf [[
|
||||
(!r & p) | (p & q & p)
|
||||
]] run disj-nf
|
||||
|
||||
test sec9_1_conj-nf [[
|
||||
(!r | p) & (!r | q) & p
|
||||
]] run conj-nf
|
||||
|
||||
test sec9_1_dnf11_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run dnf11 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
|
||||
|
||||
test sec9_1_cnf11_ex [[
|
||||
(r -> p & q) & p
|
||||
]] run cnf11 to And(And(Or(Not(Atom("r")), Atom("p")),
|
||||
Or(Not(Atom("r")), Atom("q"))),
|
||||
Atom("p"))
|
||||
|
||||
/** md
|
||||
Note that this repository does not include `prop-dnf12` because at this
|
||||
point the strategies there have become identical to the ones
|
||||
in {! ../docrefs/sec6.2.md !} used to introduce the idea of splitting
|
||||
transformations into local rewrite rules applied via a traversal strategy. So
|
||||
they have already been implemented and tested above.
|
||||
|
||||
On the other hand, in `trans/sec9_1.str`, the repository does contain a
|
||||
solution for the second exercise in
|
||||
[Section 9.1.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#visiting-one-subterm).
|
||||
**/
|
||||
|
||||
test sec9_1_2_second_exercise_inner_ex [[
|
||||
!!p | (!!q | r)
|
||||
]] run inner-soln to Or(Atom("p"), Or(Atom("q"), Atom("r")))
|
||||
|
||||
test sec9_1_2_second_exercise_outer_ex [[
|
||||
!!p | (!!q | r)
|
||||
]] run outer-soln to Impl(Not(Atom("p")), Impl(Not(Atom("q")), Atom("r")))
|
||||
|
||||
/* Note that the actual output of the following test matches
|
||||
the inner application. However, according to the manual, it would
|
||||
also be a correct implementation for it to produce
|
||||
`Impl(Not(Atom("p")), Or(Atom("q"), Atom("r")))`, which could not
|
||||
result from either outer or inner application.
|
||||
*/
|
||||
test sec9_1_2_second_exercise_random_ex [[
|
||||
!!p | (!!q | r)
|
||||
]] run random-soln to Atom("x")
|
||||
|
||||
test sec9_2_eval_bottomup_ex [[
|
||||
1 & !(0 | 1)
|
||||
]] run eval1 to False()
|
||||
|
||||
/* This test fails deliberately, to show that topdown evaluation
|
||||
does not go all the way to completion.
|
||||
*/
|
||||
test sec9_2_eval_topdown [[
|
||||
1 & !(0 | 1)
|
||||
]] run eval2 to False()
|
||||
|
||||
test sec9_2_eval_exercise_bottomup_ex [[
|
||||
(1 | 0) & (0 | 1)
|
||||
]] run eval1 to True()
|
||||
|
||||
/* Ditto for this one.*/
|
||||
test sec9_2_eval_exercise_topdown [[
|
||||
(1 | 0) & (0 | 1)
|
||||
]] run eval2 to True()
|
||||
|
||||
test sec9_2_desugar_topdown_ex [[
|
||||
p = q
|
||||
]] run desugar to And(Or(Not(Atom("p")),Atom("q")),Or(Not(Atom("q")),Atom("p")))
|
||||
|
||||
/* And ditto for this one. */
|
||||
test sec9_2_desugar_bottomup [[
|
||||
p = q
|
||||
]] run desugar2 to And(Or(Not(Atom("p")),Atom("q")),Or(Not(Atom("q")),Atom("p")))
|
||||
|
||||
test sec9_2_impl-nf_repeated_ex [[
|
||||
p & q
|
||||
]] run impl-nf1 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())
|
||||
|
||||
/* And ditto for this one. */
|
||||
test sec9_2_impl-nf_once [[
|
||||
p & q
|
||||
]] run impl-nf2 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())
|
||||
|
||||
/** md
|
||||
On the other hand there is no solution provided for the
|
||||
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).
|
||||
|
||||
The rest of Chapter 9 and all of the remaining chapters deal
|
||||
either with signatures other than SPL or
|
||||
just with abstract principles, so that concludes the Stratego examples provided
|
||||
in this repository.
|
||||
**/
|
||||
|
|
@ -4,6 +4,7 @@ imports
|
|||
|
||||
nabl2/api
|
||||
nabl2/runtime
|
||||
nabl2/shared/-
|
||||
|
||||
statics
|
||||
|
||||
|
|
@ -11,7 +12,9 @@ imports
|
|||
|
||||
rules // Analysis
|
||||
|
||||
editor-analyze = nabl2-analyze(id)
|
||||
// editor-analyze = nabl2-analyze(id)
|
||||
strip-indices : AnalysisResult([(r,Full(y,a,l,m,n))]) -> AnalysisResult([(r,Full(<nabl2--erase-ast-indices>y,a,l,m,n))])
|
||||
editor-analyze = nabl2-analyze(id); strip-indices
|
||||
|
||||
rules // Debugging
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,18 @@
|
|||
module chap6
|
||||
imports prop-laws prop-eval2 signatures/-
|
||||
|
||||
rules
|
||||
|
||||
SwapArgs : Or(e1,e2) -> Or(e2,e1)
|
||||
|
||||
SwapBoth : Or(e1,e2) -> Or(e2,e1)
|
||||
SwapBoth : And(e1,e2) -> And(e2,e1)
|
||||
|
||||
ExMid: And(Not(x),x) -> False()
|
||||
ExMid: And(x,Not(x)) -> False()
|
||||
|
||||
strategies
|
||||
|
||||
better-dnf =
|
||||
innermost(DefI <+ DefE <+ ExMid <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO); eval-down
|
||||
|
||||
|
|
@ -0,0 +1,15 @@
|
|||
module chap7
|
||||
imports libstrategolib signatures/-
|
||||
|
||||
rules
|
||||
|
||||
A : Or(False(), x) -> x
|
||||
B : Or(Impl(True(),x), y) -> Or(x, Impl(True(), y))
|
||||
|
||||
strategies
|
||||
|
||||
BthenA = B; A
|
||||
Btwice = B; B
|
||||
maybeB-id-thenB = (B <+ id); B
|
||||
maybeBtwice-idthenB = Btwice <+ (id; B)
|
||||
repeatmaybeAB = repeat(A <+ B)
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
module chap8
|
||||
imports signatures/-
|
||||
|
||||
rules
|
||||
|
||||
SwapWithPat = ?Or(e1,e2); !Or(e2,e1)
|
||||
SwapAnon = (Or(e1,e2) -> Or(e2,e1))
|
||||
NoSwapTwice = (Or(e1,e2) -> Or(e2,e1)); (Or(e1,e2) -> Or(e2,e1))
|
||||
OkSwapTwice =
|
||||
{e3,e4 : (Or(e3,e4) -> Or(e4,e3))}; {e3,e4 : (Or(e3,e4) -> Or(e4,e3))}
|
||||
TermWrap = !Or(<id>, Not(<id>))
|
||||
TermProj = ?Or(_, Not(<id>))
|
||||
|
|
@ -0,0 +1,35 @@
|
|||
module prop-cnf3
|
||||
imports libstrategolib prop-dnf3 signatures/-
|
||||
signature
|
||||
constructors
|
||||
Cnf : Prop -> Prop
|
||||
CnfR : Prop -> Prop
|
||||
rules
|
||||
E3 : Cnf(Atom(x)) -> Atom(x)
|
||||
E3 : Cnf(Not(x)) -> CnfR(Not(Cnf(x)))
|
||||
E3 : Cnf(Or(x, y)) -> CnfR(Or(Cnf(x), Cnf(y)))
|
||||
E3 : Cnf(And(x, y)) -> And(Cnf(x), Cnf(y))
|
||||
E3 : Cnf(Impl(x, y)) -> Cnf(Not(And(x, Not(y))))
|
||||
E3 : Cnf(Eq(x, y)) -> Cnf(And(Impl(x, y), Impl(y, x)))
|
||||
|
||||
E3 : CnfR(Not(Not(x))) -> x
|
||||
E3 : CnfR(Not(Or(x, y))) -> And(Cnf(Not(x)), Cnf(Not(y)))
|
||||
E3 : CnfR(Not(And(x, y))) -> Cnf(Or(Not(x), Not(y)))
|
||||
D3 : CnfR(Not(x)) -> Not(x)
|
||||
|
||||
E3 : CnfR(Or(And(x, y), z)) -> And(Cnf(Or(x, z)), Cnf(Or(y, z)))
|
||||
E3 : CnfR(Or(z, And(x, y))) -> And(Cnf(Or(z, x)), Cnf(Or(z, y)))
|
||||
D3 : CnfR(Or(x, y)) -> Or(x, y)
|
||||
|
||||
strategies
|
||||
cnf3 : x -> <make-nf> Cnf(x)
|
||||
dcnf : x -> <make-nf> (Dnf(x), Cnf(x))
|
||||
|
||||
// Interface cnf3 strategy with editor services and file system
|
||||
do-cnf3: (selected, _, _, path, project-path) -> (filename, result)
|
||||
with filename := <guarantee-extension(|"cnf.aterm")> path
|
||||
; result := <cnf3> selected
|
||||
|
||||
do-dcnf: (selected, _, _, path, project-path) -> (filename, result)
|
||||
with filename := <guarantee-extension(|"dc.aterm")> path
|
||||
; result := <dcnf> selected
|
||||
|
|
@ -0,0 +1,22 @@
|
|||
module prop-desugar
|
||||
imports libstrategolib signatures/-
|
||||
|
||||
rules
|
||||
|
||||
DefN : Not(x) -> Impl(x, False())
|
||||
DefI : Impl(x, y) -> Or(Not(x), y)
|
||||
DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x))
|
||||
DefO1 : Or(x, y) -> Impl(Not(x), y)
|
||||
DefO2 : Or(x, y) -> Not(And(Not(x), Not(y)))
|
||||
DefA1 : And(x, y) -> Not(Or(Not(x), Not(y)))
|
||||
DefA2 : And(x, y) -> Not(Impl(x, Not(y)))
|
||||
|
||||
IDefI : Or(Not(x), y) -> Impl(x, y)
|
||||
|
||||
IDefE : And(Impl(x, y), Impl(y, x)) -> Eq(x, y)
|
||||
|
||||
strategies
|
||||
|
||||
desugar = topdown(try(DefI <+ DefE))
|
||||
|
||||
impl-nf = topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE))
|
||||
|
|
@ -0,0 +1,43 @@
|
|||
/** md
|
||||
Title: Running a Strategy, continued
|
||||
|
||||
## Disjunctive Normal Form
|
||||
|
||||
The next Stratego example, in {! ../docrefs/sec4.2.md !}, extends
|
||||
`prop-eval-rules` to convert SPL propositions into disjunctive normal form (DNF).
|
||||
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
|
||||
{! ../trans/analysis.str terminate: Debugging!} [rest of file omitted]
|
||||
```
|
||||
|
||||
**/
|
||||
|
||||
module prop-dnf-rules
|
||||
imports prop-eval-rules
|
||||
rules
|
||||
E : Impl(x, y) -> Or(Not(x), y)
|
||||
E : Eq(x, y) -> And(Impl(x, y), Impl(y, x))
|
||||
|
||||
E : Not(Not(x)) -> x
|
||||
|
||||
E : Not(And(x, y)) -> Or(Not(x), Not(y))
|
||||
E : Not(Or(x, y)) -> And(Not(x), Not(y))
|
||||
|
||||
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))
|
||||
|
|
@ -0,0 +1,9 @@
|
|||
module prop-dnf
|
||||
imports libstrategolib prop-dnf-rules
|
||||
strategies
|
||||
dnf = innermost(E)
|
||||
|
||||
// Interface dnf strategy with editor services and file system
|
||||
do-dnf: (selected, _, _, path, project-path) -> (filename, result)
|
||||
with filename := <guarantee-extension(|"dnf.aterm")> path
|
||||
; result := <dnf> selected
|
||||
|
|
@ -0,0 +1,9 @@
|
|||
module prop-dnf10
|
||||
imports libstrategolib signatures/- prop-laws
|
||||
|
||||
strategies
|
||||
proptr10(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s)
|
||||
propbu10(s) = try(proptr10(propbu10(s))); s
|
||||
strategies
|
||||
dnf10 = propbu10(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf10))
|
||||
cnf10 = propbu10(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf10))
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
module prop-dnf11
|
||||
imports libstrategolib prop-laws
|
||||
|
||||
strategies
|
||||
dnf11 = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf11))
|
||||
cnf11 = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf11))
|
||||
|
|
@ -0,0 +1,112 @@
|
|||
/** md
|
||||
Title: Running a Strategy: the command line
|
||||
|
||||
## Functionalizing reduction rules
|
||||
|
||||
The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to
|
||||
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
|
||||
chapter for disjunctive normal form, as they would produce a non-terminating
|
||||
rewrite system.
|
||||
|
||||
The first method for which working examples are provided is the method of
|
||||
"functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern
|
||||
in the views of the Spoofax designers, the examples are still instructive and
|
||||
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.
|
||||
|
||||
**/
|
||||
|
||||
module prop-dnf3
|
||||
imports libstrategolib signatures/-
|
||||
signature
|
||||
constructors
|
||||
Dnf : Prop -> Prop
|
||||
DnfR : Prop -> Prop
|
||||
rules
|
||||
E3 : Dnf(Atom(x)) -> Atom(x)
|
||||
E3 : Dnf(Not(x)) -> DnfR(Not(Dnf(x)))
|
||||
E3 : Dnf(And(x, y)) -> DnfR(And(Dnf(x), Dnf(y)))
|
||||
E3 : Dnf(Or(x, y)) -> Or(Dnf(x), Dnf(y))
|
||||
E3 : Dnf(Impl(x, y)) -> Dnf(Or(Not(x), y))
|
||||
E3 : Dnf(Eq(x, y)) -> Dnf(And(Impl(x, y), Impl(y, x)))
|
||||
|
||||
E3 : DnfR(Not(Not(x))) -> x
|
||||
E3 : DnfR(Not(And(x, y))) -> Or(Dnf(Not(x)), Dnf(Not(y)))
|
||||
E3 : DnfR(Not(Or(x, y))) -> Dnf(And(Not(x), Not(y)))
|
||||
D3 : DnfR(Not(x)) -> Not(x)
|
||||
|
||||
E3 : DnfR(And(Or(x, y), z)) -> Or(Dnf(And(x, z)), Dnf(And(y, z)))
|
||||
E3 : DnfR(And(z, Or(x, y))) -> Or(Dnf(And(z, x)), Dnf(And(z, y)))
|
||||
D3 : DnfR(And(x, y)) -> And(x, y)
|
||||
|
||||
strategies
|
||||
make-nf = innermost(E3 <+ D3)
|
||||
dnf3 : x -> <make-nf> Dnf(x)
|
||||
|
||||
// Interface dnf3 strategy with editor services and file system
|
||||
do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
|
||||
with filename := <guarantee-extension(|"dnf.aterm")> path
|
||||
; result := <dnf3> selected
|
||||
|
||||
/** md
|
||||
|
||||
### Command-line Utilities
|
||||
|
||||
The Spoofax project offers an executable jar called
|
||||
[Sunshine](http://www.metaborg.org/en/latest/source/release/development.html#command-line-utilities)
|
||||
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
|
||||
summary of the available actions with `java -jar $SUNSHINE_JAR -h`. In the
|
||||
repository there's a convenience bash script `bin/spoofax-menu` you can use to
|
||||
run the Sunshine jar:
|
||||
```bash
|
||||
{! ../bin/spoofax-menu extract:
|
||||
- stop: --help
|
||||
- start: ';;'
|
||||
!}
|
||||
```
|
||||
(You can also get a usage explanation, elided from the listing above, via
|
||||
`bin/spoofax-menu -h`.)
|
||||
|
||||
To use this, you must have a Spoofax menu item set up to run the strategy you
|
||||
want, but then you can invoke it on an arbitrary file from the command line like
|
||||
so:
|
||||
```
|
||||
spoofax_prop> export SUNSHINE_JAR=~/software/org.metaborg.sunshine2-2.6.0-20210119.175231-1.jar
|
||||
spoofax_prop> export ECLIPSE_INSTALL=~/software/spoofax
|
||||
spoofax_prop> export SPOOFAX_PROJECT=~/code/neweclipse/spoofax_prop
|
||||
spoofax_prop> bin/spoofax-menu syntax/examples/sec5.1.2_test1.spl both-nf3
|
||||
( Or(
|
||||
And(Not(Atom("r")), Atom("p"))
|
||||
, And(And(Atom("p"), Atom("q")), Atom("p"))
|
||||
)
|
||||
, And(
|
||||
And(
|
||||
Or(Not(Atom("r")), Atom("p"))
|
||||
, Or(Not(Atom("r")), Atom("q"))
|
||||
)
|
||||
, Atom("p")
|
||||
)
|
||||
)
|
||||
```
|
||||
|
||||
In our case, the Sunshine jar doesn't really give us any new capabilities, and
|
||||
the ESV menu items still have to be set up, but it could make running examples
|
||||
more convenient for you.
|
||||
**/
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
module prop-dnf4
|
||||
imports libstrategolib prop-laws
|
||||
|
||||
rules
|
||||
dnf4 : True() -> True()
|
||||
dnf4 : False() -> False()
|
||||
dnf4 : Atom(x) -> Atom(x)
|
||||
dnf4 : Not(x) -> <dnfred4> Not (<dnf4>x)
|
||||
dnf4 : And(x, y) -> <dnfred4> And (<dnf4>x, <dnf4>y)
|
||||
dnf4 : Or(x, y) -> Or (<dnf4>x, <dnf4>y)
|
||||
dnf4 : Impl(x, y) -> <dnfred4> Impl(<dnf4>x, <dnf4>y)
|
||||
dnf4 : Eq(x, y) -> <dnfred4> Eq (<dnf4>x, <dnf4>y)
|
||||
strategies
|
||||
dnfred4 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf4)
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
module prop-dnf5
|
||||
imports libstrategolib prop-laws
|
||||
|
||||
rules
|
||||
dnft5 : Not(x) -> <dnfred5> Not (<dnf5>x)
|
||||
dnft5 : And(x, y) -> <dnfred5> And (<dnf5>x, <dnf5>y)
|
||||
dnft5 : Or(x, y) -> Or (<dnf5>x, <dnf5>y)
|
||||
dnft5 : Impl(x, y) -> <dnfred5> Impl(<dnf5>x, <dnf5>y)
|
||||
dnft5 : Eq(x, y) -> <dnfred5> Eq (<dnf5>x, <dnf5>y)
|
||||
strategies
|
||||
dnf5 = try(dnft5)
|
||||
dnfred5 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf5)
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
module prop-dnf6
|
||||
imports libstrategolib prop-laws
|
||||
|
||||
rules
|
||||
dnft6 : Not(x) -> Not (<dnf6>x)
|
||||
dnft6 : And(x, y) -> And (<dnf6>x, <dnf6>y)
|
||||
dnft6 : Or(x, y) -> Or (<dnf6>x, <dnf6>y)
|
||||
dnft6 : Impl(x, y) -> Impl(<dnf6>x, <dnf6>y)
|
||||
dnft6 : Eq(x, y) -> Eq (<dnf6>x, <dnf6>y)
|
||||
strategies
|
||||
dnf6 = try(dnft6); dnfred6
|
||||
dnfred6 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf6)
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
module prop-dnf7
|
||||
imports libstrategolib prop-laws
|
||||
|
||||
rules
|
||||
proptr7(s) : Not(x) -> Not (<s>x)
|
||||
proptr7(s) : And(x, y) -> And (<s>x, <s>y)
|
||||
proptr7(s) : Or(x, y) -> Or (<s>x, <s>y)
|
||||
proptr7(s) : Impl(x, y) -> Impl(<s>x, <s>y)
|
||||
proptr7(s) : Eq(x, y) -> Eq (<s>x, <s>y)
|
||||
strategies
|
||||
dnf7 = try(proptr7(dnf7)); dnfred7
|
||||
dnfred7 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf7)
|
||||
cnf7 = try(proptr7(cnf7)); cnfred7
|
||||
cnfred7 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf7)
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
module prop-dnf8
|
||||
imports libstrategolib prop-laws prop-dnf7
|
||||
|
||||
strategies
|
||||
propbu8(s) = try(proptr7(propbu8(s))); s
|
||||
strategies
|
||||
dnf8 = propbu8(dnfred8)
|
||||
dnfred8 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf8)
|
||||
cnf8 = propbu8(cnfred8)
|
||||
cnfred8 = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf8)
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
module prop-dnf9
|
||||
imports libstrategolib prop-laws prop-dnf8
|
||||
|
||||
strategies
|
||||
dnf9 = propbu8(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf9))
|
||||
cnf9 = propbu8(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf9))
|
||||
|
|
@ -4,18 +4,61 @@ Title: Running a Strategy
|
|||
## Running a Strategy
|
||||
|
||||
The first example of running a Stratego strategy
|
||||
in the {! ../docrefs/manual.md !} } is that of _evaluating_ an AST,
|
||||
via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. This page
|
||||
describes the most straightforward way to run this same strategy
|
||||
in the Spoofax Eclipse IDE.
|
||||
in the {! ../docrefs/manual.md !} is that of _evaluating_ an AST,
|
||||
via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. In this
|
||||
repository, we've placed those rules in `trans/prop-eval-rules.str`,
|
||||
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
|
||||
the `trans` directory. So, you can place the Stratego code for
|
||||
this module in `trans/prop-eval-rules.str`, with the following contents:
|
||||
(I am unclear on what triggers Editor Services 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.)
|
||||
|
||||
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
|
||||
[End the documentation block to avoid the comment close in the code] **/
|
||||
/** md [restart processing to include the code in the documentation] */
|
||||
{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
|
||||
```
|
||||
|
||||
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
|
||||
imports signatures/-
|
||||
rules
|
||||
|
|
@ -37,99 +80,3 @@ rules
|
|||
E : Eq(x, False()) -> Not(x)
|
||||
E : Eq(True(), x) -> 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 {terminate: 'provider\s*:', replace: ['^\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 !}
|
||||
```
|
||||
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 {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 including 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 {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:
|
||||
|
||||
[CONTINUE HERE ONCE THIS WORKS]
|
||||
|
||||
**/
|
||||
|
|
|
|||
|
|
@ -0,0 +1,27 @@
|
|||
module prop-eval2
|
||||
imports libstrategolib signatures/-
|
||||
rules
|
||||
|
||||
Eval : Not(True()) -> False()
|
||||
Eval : Not(False()) -> True()
|
||||
Eval : And(True(), x) -> x
|
||||
Eval : And(x, True()) -> x
|
||||
Eval : And(False(), x) -> False()
|
||||
Eval : And(x, False()) -> False()
|
||||
Eval : Or(True(), x) -> True()
|
||||
Eval : Or(x, True()) -> True()
|
||||
Eval : Or(False(), x) -> x
|
||||
Eval : Or(x, False()) -> x
|
||||
Eval : Impl(True(), x) -> x
|
||||
Eval : Impl(x, True()) -> True()
|
||||
Eval : Impl(False(), x) -> True()
|
||||
Eval : Impl(x, False()) -> Not(x)
|
||||
Eval : Eq(False(), x) -> Not(x)
|
||||
Eval : Eq(x, False()) -> Not(x)
|
||||
Eval : Eq(True(), x) -> x
|
||||
Eval : Eq(x, True()) -> x
|
||||
|
||||
strategies
|
||||
|
||||
eval-up = bottomup(repeat(Eval))
|
||||
eval-down = downup(repeat(Eval))
|
||||
|
|
@ -0,0 +1,22 @@
|
|||
module prop-laws
|
||||
imports libstrategolib signatures/-
|
||||
rules
|
||||
|
||||
DefI : Impl(x, y) -> Or(Not(x), y)
|
||||
DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x))
|
||||
|
||||
DN : Not(Not(x)) -> x
|
||||
|
||||
DMA : Not(And(x, y)) -> Or(Not(x), Not(y))
|
||||
DMO : Not(Or(x, y)) -> And(Not(x), Not(y))
|
||||
|
||||
DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
|
||||
DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))
|
||||
|
||||
DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
|
||||
DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))
|
||||
|
||||
strategies
|
||||
|
||||
dnf-laws = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO)
|
||||
cnf-laws = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO)
|
||||
|
|
@ -0,0 +1,18 @@
|
|||
module sec9_1
|
||||
imports libstrategolib signatures/- prop-laws prop-desugar
|
||||
|
||||
strategies
|
||||
conj(s) = And(conj(s), conj(s)) <+ s
|
||||
disj(s) = Or (disj(s), disj(s)) <+ s
|
||||
|
||||
// Conjunctive normal form
|
||||
conj-nf = conj(disj(Not(Atom(id)) <+ Atom(id)))
|
||||
|
||||
// Disjunctive normal form
|
||||
disj-nf = disj(conj(Not(Atom(id)) <+ Atom(id)))
|
||||
|
||||
// Second exercise, Section 9.1.2
|
||||
path-dep-xform = DN <+ IDefI
|
||||
inner-soln = repeat(oncebu(path-dep-xform))
|
||||
outer-soln = repeat(oncetd(path-dep-xform))
|
||||
random-soln = repeat(rec x(one(x) + path-dep-xform))
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
module sec9_2
|
||||
imports prop-eval2 prop-desugar
|
||||
|
||||
rules
|
||||
DefT : True() -> Impl(False(), False())
|
||||
|
||||
strategies
|
||||
eval1 = bottomup(try(Eval))
|
||||
eval2 = topdown(try(Eval))
|
||||
|
||||
desugar2 = bottomup(try(DefI <+ DefE))
|
||||
|
||||
impl-nf1 = topdown(repeat(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
|
||||
impl-nf2 = topdown(try(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))
|
||||
|
|
@ -7,6 +7,25 @@ imports
|
|||
outline
|
||||
analysis
|
||||
prop-eval
|
||||
prop-dnf
|
||||
prop-dnf3
|
||||
prop-cnf3
|
||||
prop-laws
|
||||
prop-eval2
|
||||
prop-desugar
|
||||
chap6
|
||||
chap7
|
||||
chap8
|
||||
prop-dnf4
|
||||
prop-dnf5
|
||||
prop-dnf6
|
||||
prop-dnf7
|
||||
prop-dnf8
|
||||
prop-dnf9
|
||||
prop-dnf10
|
||||
sec9_1
|
||||
prop-dnf11
|
||||
sec9_2
|
||||
|
||||
rules // Debugging
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue