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