404 lines
13 KiB
Cheetah
404 lines
13 KiB
Cheetah
/** 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"))
|
|
|
|
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"))
|
|
|
|
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"))
|
|
|
|
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"))
|
|
|
|
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
|
|
Note that this 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
|
|
On the other hand 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.
|
|
**/
|