spoofax_prop/trans/prop-dnf3.str

/** 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.
**/