239 lines
8.1 KiB
Cheetah
239 lines
8.1 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 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`. (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")
|