/** md
Title: The Remaining Tests

## Programmable Rewriting Strategies

The manual then begins to discuss "programmable rewriting strategies" in
[Section 5.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#programmable-rewriting-strategies)
and beyond to show how to use Stratego's various features to overcome the
difficulties with the last several examples.

The next example is in Section 5.3.1, which shows a unified treatment of
disjunctive and conjunctive normal forms that avoids the potential combinatorial
explosion of rules seen in the functionalized example. As usual, the example
Stratego module `prop-laws` is in `trans/prop-laws.str` and included in
`trans/spoofax_propositional_language.str`. Also as typical, some of the identifiers
in the module had to be changed to avoid namespace conflicts when they are all
imported into the main language module.

But after going through the previous examples, it seems that trying them is most
convenient with the Spoofax Testing Language:

* No glue transformation is needed and no ESV files need to be modified.
* It's not necessary to place the SPL expression to be tested in a separate file.
* The SPL expression, name of strategy to run, and results of that run are all
  kept together (in the `test/manual-suite.spt` file).

Hence, the test cases for Section 5.3.1 and beyond, through the end of the
Tutorial/Reference Manual, are captured in this repository solely in terms
of SPT Test Cases. You can of course clone the repository and create menu items
for any of them if you want to try them that way. Just remember to add a
"glue" strategy for them as shown in the [first example](../trans/prop-eval-rules.md).

Hopefully these examples are helpful to your exploration and understanding of
Stratego -- certainly creating them was to mine.

Additional notes on particular sections or tests follow.
**/
module manual-suite
language Spoofax-Propositional-Language

test sec4_2_test3 [[
  (r -> p & q) & p
]] run dnf to Atom("x")

test sec4_2_test3_ex [[
  (r -> p & q) & p
]] run dnf to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))

test sec5_1_2_test1_ex [[
  (r -> p & q) & p
]] run dnf3 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))

test sec5_1_2_test1_cnf_ex [[
  (r -> p & q) & p
]] run cnf3 to And(And(Or(Not(Atom("r")), Atom("p")),
                       Or(Not(Atom("r")), Atom("q"))),
                   Atom("p"))

test sec5_1_2_test1_both [[
  (r -> p & q) & p
]] run dcnf to Atom("x")
//(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")))

test sec5_3_1_test1_dnf_ex [[
  (r -> p & q) & p
]] run dnf4 to Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))

test sec5_3_1_test1_cnf_ex [[
  (r -> p & q) & p
]] run cnf4 to And(And(Or(Not(Atom("r")), Atom("p")),
                       Or(Not(Atom("r")), Atom("q"))),
                   Atom("p"))

test sec5_3_2_eval_up_ex [[
  (1 -> p & q) & p
]] run eval-up to And(And(Atom("p"),Atom("q")),Atom("p"))

test sec5_3_2_eval_down_ex [[
  (1 -> p & q) & p
]] run eval-down to And(And(Atom("p"),Atom("q")),Atom("p"))

test sec5_3_2_desugar_ex [[
  (1 -> p & q) & p
]] run desugar to And(Or(Not(True()),And(Atom("p"),Atom("q"))),Atom("p"))

test sec5_3_2_impl_nf_ex [[
  (1 -> p & q) & p
]] run impl-nf to Impl(Impl(Impl(True(),Impl(Impl(Atom("p"),
                                                  Impl(Atom("q"),False())),
                                             False())),
                            Impl(Atom("p"),False())),
                       False())

/** md
### Chapter 6

Many of the examples in
[Chapter 6](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/06-rules-and-strategies.html)
are in the form of interactive "Stratego shell" sessions. For this repository, we
have to convert them to rule definitions in a Stratego file (`chap6.str`) and
test cases for each of the executed examples.

Also, there are some examples for a Plus-Times signature; we transpose these
to Or-And for the sake of keeping everything within the SPL language project.

To illustrate extending a rule, we need to give the rule we're going to extend
a different identifier and add both definitions to that (otherwise our original
rule `SwapArgs` would already have been extended).

The `chap6.str` file also includes a solution to the exercise in
[Section 6.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/06-rules-and-strategies.html#what-is-a-strategy).
On the other hand, it is not clear whether the Spoofax Eclipse IDE has a "debug"
operator for Stratego, or if so how it would work, so the repository does not
attempt to implement the "debug" example.

The remainder of the chapter (from section 6.3 on) consists of general information
about Stratego syntax and information about the Stratego compiler. As it's not
clear if the latter applies to the Spoofax Eclipse IDE, there are no further test
cases in this repository beyond Section 6.2.
**/

test sec6_1_swap_ex [[
  p | 0
]] run SwapArgs to Or(False(), Atom("p"))

test sec6_1_swap_fails [[
  p & 0
]] run SwapArgs fails

test sec6_1_swap_subterm_fails [[
  (1 | p) & 0
]] run SwapArgs fails

test sec6_1_swap_only_outer_ex [[
  (1 | p) | 0
]] run SwapArgs to Or(False(), Or(True(), Atom("p")))

test sec6_1_swapboth_or_ex [[
  p | 0
]] run SwapBoth to Or(False(), Atom("p"))

test sec6_1_swapboth_and_ex [[
  p & 0
]] run SwapBoth to And(False(), Atom("p"))

test sec6_2_invoke_rule_ex [[
  1 -> p
]] run DefI to Or(Not(True()), Atom("p"))

test sec6_2_innermost_ex [[
  p = q
]] run dnf4 to Or(Or(And(Not(Atom("p")),Not(Atom("q"))),
                     And(Not(Atom("p")),Atom("p"))),
                  Or(And(Atom("q"),Not(Atom("q"))),
                     And(Atom("q"),Atom("p"))))

test sec6_2_dnf_exercise_ex [[
  p = q
]] run better-dnf to Or(And(Not(Atom("p")),Not(Atom("q"))),
                        And(Atom("q"),Atom("p")))

/** md
### Chapter 7

The content and style of chapter 7 are similar to chapter 6. Again, there is a
`trans/chap7.str` Stratego file defining several of the rules used in the examples
from the chapter. As before, the examples with a different signature are recast
into the SPL signature. Specifically, `Z` becomes `False`, `S(x)` becomes
`Impl(True(), x)`, and `P` becomes `Or`.
**/

test sec7_2_b_ex [[
  (1 -> 0) | 0
]] run B to Or(False(), Impl(True(), False()))

test sec7_2_b_a_ex [[
  (1 -> 0) | 0
]] run BthenA to Impl(True(), False())

test sec7_2_b_b_fails [[
  (1 -> 0) | 0
]] run Btwice fails

test sec7_2_local_choice_fails [[
  (1 -> 0) | 0
]] run maybeB-id-thenB fails

test sec7_2_seq_no_dist_over_choice_ex [[
  (1 -> 0) | 0
]] run maybeBtwice-idthenB to Or(False(), Impl(True(), False()))

test sec7_3_repeat_small_ex [[
  (1 -> 0) | 0
]] run repeatmaybeAB to Impl(True(), False())

test sec7_3_repeat_big_ex [[
  (1 -> (1 -> (1 -> (1 -> 0)))) | 0
]] run repeatmaybeAB to Impl(True(), Impl(True(), Impl(True(),
                                                       Impl(True(), False()))))