/** 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 (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 dnf-laws 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 cnf-laws 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 {! ../docrefs/sec6.2.md !}. 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 within the IDE, 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 whether 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 dnf-laws 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`. (At least with these choices, all of the
transformations in the chapter remain valid in the usual semantics for the SPL
signature, even if a bit unorthodox.)
**/

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()))))

/** md
### Chapter 8

This chapter is even more just a collection of interactive examples. In this
repository we just give some examples of swapping and variable scope using the
SPL signature, and some free-form examples of term wrapping and projecting.
There's no attempt to do any of the arithmetic examples because SPL does not have
an integer type.
**/

test sec8_3_firstswap_ex [[
  p | 0
]] run SwapWithPat to Or(False(), Atom("p"))

test sec8_3_1_swap_ex [[
  p | 0
]] run SwapAnon to Or(False(), Atom("p"))

test sec8_3_2_variablescope_fails [[
  p | 0
]] run NoSwapTwice fails

test sec8_3_2_localscope_ex [[
  p | 0
]] run OkSwapTwice to Or(Atom("p"), False())

test sec8_5_1_wrap_ex [[
  p
]] run TermWrap to Or(Atom("p"), Not(Atom("p")))

test sec8_5_2_project_ex [[
  p | !p
]] run TermProj to Atom("p")

/** md
### Chapter 9

This chapter is much more in the style of the early chapters: there are several
explicit Stratego modules, and we incorporate each one into this repository. As
before, we need to differentiate the names in some modules since they all end
up being loaded at once; but we also take advantage of the common sections of
some of the modules and re-use rather than repeat the code. In addition, the
disjunctive and conjunctive normal forms of the same test expression as used
in Chapter Five are used for test cases in `trans/manual-suite.spt`.

**/

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

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

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

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

/** md
The key point to know about
[Chapter 9](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html),
however, is that there is a mistake that affects examples `prop-dnf8` through
`prop-dnf10`. The difficulty is in this definition:
```Stratego
strategies
  propbu(s) = proptr(propbu(s)); s
```

Recall that `proptr` is defined as follows: (Note that our implementation calls
it `proptr7` to distinguish it from different definitions for `proptr` in other
examples.)
```Stratego
{! ../trans/prop-dnf7.str extract:
  start: '(rules\n*)'
  stop: strategies
!}
```

So `propbu` must be defined as:
```Stratego
{! ../trans/prop-dnf8.str extract:
  start: strategies
  stop: '(.*propbu8.*)'
!}
```

The point is that `proptr` cannot apply to `Atom`s and logical constants, and so
fails when it reaches such nodes in the AST. Without the `try` in the definition
of the `propbu` traversal, any such failure propagates to a failure of the entire
strategy.
**/

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

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

/** md
Example `prop-dnf9` simply re-uses `propbu8`.
**/

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

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

/** md
And a similar fix is made to `prop-dnf10`:
```Stratego
{! ../trans/prop-dnf10.str !}
```

**/

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

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

/** md
There is another issue in the "Format Checking" example in section 9.1. It lies
with the strategy used to determine if an expression is an atom or the negation
of an atom. The expression shown is `Not(Atom(x)) <+ Atom(x)`. This appears to
be a left choice of two congruences. But a congruence expects a strategy as an
argument, whereas here `x` is simply a free variable. There are a couple of
fixes to write an expression that checks whether a term is just an `Atom()` call
or the negation of one. The first possibility is to use match expressions, e.g.
`?Not(Atom(x)) <+ ?Atom(x)`. However, as that can run into issues with the scoping
of the variable `x`, we opted for sticking with the congruences, just using a
strategy that always succeeds in the inner position, namely `id`:
```Stratego
{! ../trans/sec9_1.str terminate: exercise !}
```
**/

test sec9_1_disj-nf_fails [[
  (r -> p & q) & p
]] run disj-nf fails

test sec9_1_conj-nf_fails [[
  (r -> p & q) & p
]] run conj-nf fails

test sec9_1_disj-nf [[
  (!r & p) | (p & q & p)
]] run disj-nf

test sec9_1_conj-nf [[
  (!r | p) & (!r | q) & p
]] run conj-nf

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

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

/** md
Also note that the repository does not include `prop-dnf12` because at this
point the strategies there have become identical to the ones
in {! ../docrefs/sec6.2.md !} used to introduce the idea of splitting
transformations into local rewrite rules applied via a traversal strategy. So
they have already been implemented and tested above.

On the other hand, in `trans/sec9_1.str`, the repository does contain a
solution for the second exercise in
[Section 9.1.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#visiting-one-subterm).
**/

test sec9_1_2_second_exercise_inner_ex [[
  !!p | (!!q | r)
]] run inner-soln to Or(Atom("p"), Or(Atom("q"), Atom("r")))

test sec9_1_2_second_exercise_outer_ex [[
  !!p | (!!q | r)
]] run outer-soln to Impl(Not(Atom("p")), Impl(Not(Atom("q")), Atom("r")))

/* Note that the actual output of the following test matches
   the inner application. However, according to the manual, it would
   also be a correct implementation for it to produce
   `Impl(Not(Atom("p")), Or(Atom("q"), Atom("r")))`, which could not
   result from either outer or inner application.
*/
test sec9_1_2_second_exercise_random_ex [[
  !!p | (!!q | r)
]] run random-soln to Atom("x")

test sec9_2_eval_bottomup_ex [[
  1 & !(0 | 1)
]] run eval1 to False()

/* This test fails deliberately, to show that topdown evaluation
   does not go all the way to completion.
*/
test sec9_2_eval_topdown [[
  1 & !(0 | 1)
]] run eval2 to False()

test sec9_2_eval_exercise_bottomup_ex [[
  (1 | 0) & (0 | 1)
]] run eval1 to True()

/* Ditto for this one.*/
test sec9_2_eval_exercise_topdown [[
  (1 | 0) & (0 | 1)
]] run eval2 to True()

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

/* And ditto for this one. */
test sec9_2_desugar_bottomup [[
  p = q
]] run desugar2 to And(Or(Not(Atom("p")),Atom("q")),Or(Not(Atom("q")),Atom("p")))

test sec9_2_impl-nf_repeated_ex [[
  p & q
]] run impl-nf1 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())

/* And ditto for this one. */
test sec9_2_impl-nf_once [[
  p & q
]] run impl-nf2 to Impl(Impl(Atom("p"),Impl(Atom("q"),False())),False())

/** md
I couldn't think of a natural application of paramorphism in the context of
the Spoofax Propositional Language, so there is no solution provided for the
exercise just before
[Section 9.2.1](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.html#cascading-transformations).

The rest of Chapter 9 and all of the remaining chapters deal
either with signatures other than SPL or
just with abstract principles, so that concludes the Stratego examples provided
in this repository.
**/