/** 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. There's one caveat here, though. The test case for `dcnf`:
```SPT
{! ../test/manual-suite.spt extract:
  start: '^(.*test.*both.*\n?)$'
!}
```
does not actually work, because of what appears to be a bug in SPT: the `to`
in the expectation line is interpreted as part of the expected AST. However,
the error message does show that the transformation is operating properly.

We can now use this example to show yet another way to try Stratego stragies
with the Spoofax IDE implementation.

### Command-line Utilities

[HERE]
**/