144 lines
5.7 KiB
Plaintext
144 lines
5.7 KiB
Plaintext
/** 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 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 we want to implement them here.
|
|
|
|
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
|
|
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
|
|
/* End of code inclusion **/
|
|
/** md Conclusion of documentation:
|
|
```
|
|
|
|
Notice the few minor differences from the manual. We import `signatures/-` as
|
|
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
|
|
|
|
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`:
|
|
```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.
|
|
**/
|