113 lines
3.9 KiB
Plaintext
113 lines
3.9 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 (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.
|
|
**/
|