From a33c1585d6e39e821671a587251d034a26fe9704 Mon Sep 17 00:00:00 2001 From: Glen Whitney Date: Tue, 19 Jan 2021 19:29:48 -0800 Subject: [PATCH] feat: Implement Sec 5.3.1 tests And put in generic documentation for all the remaining tests. If any particular tests need individual commentary, it can always be added later. --- mkdocs.yml | 1 + test/manual-suite.spt | 45 ++++++++++++++++++++++++ trans/prop-dnf-rules.str | 8 +++-- trans/prop-laws.str | 22 ++++++++++++ trans/spoofax_propositional_language.str | 1 + 5 files changed, 75 insertions(+), 2 deletions(-) create mode 100644 trans/prop-laws.str diff --git a/mkdocs.yml b/mkdocs.yml index 41a15dd..4f979df 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -13,6 +13,7 @@ nav: - trans/prop-eval-rules.md - trans/prop-dnf-rules.md - trans/prop-dnf3.md +- test/manual-suite.md theme: name: readthedocs markdown_extensions: diff --git a/test/manual-suite.spt b/test/manual-suite.spt index 5d22850..1e4f1d9 100644 --- a/test/manual-suite.spt +++ b/test/manual-suite.spt @@ -1,3 +1,38 @@ +/** 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. +**/ module manual-suite language Spoofax-Propositional-Language @@ -25,3 +60,13 @@ test sec5_1_2_test1_both_ex [[ 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")) diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str index 42e32ea..9bfab66 100644 --- a/trans/prop-dnf-rules.str +++ b/trans/prop-dnf-rules.str @@ -66,7 +66,9 @@ trying our different Stratego transformations. So, we can just take our `test3` expression above and make it a part of an SPT test suite, which we will call `test/manual-suite.spt`: ```SPT -{! ../test/manual-suite.spt terminate: '(.*run dnf)' !} +{! ../test/manual-suite.spt extract: + start: '\*\*/' +terminate: '(.*run dnf)' !} ``` Once we have saved this file, the tests run automatically. What does this mean? @@ -83,7 +85,9 @@ If we use an AST like `Atom("x")` that can't possibly be the actual output what the transformation actually produced. So we add just a bit to `test/manual-suite.spt`: ```SPT -{! ../test/manual-suite.spt terminate: '(.*run dnf.*)$' !} +{! ../test/manual-suite.spt extract: + start: '\*\*/' +terminate: '(.*run dnf.*)$' !} ``` and now sure enough a little error symbol appears next to the test. If you hover diff --git a/trans/prop-laws.str b/trans/prop-laws.str new file mode 100644 index 0000000..1f8987e --- /dev/null +++ b/trans/prop-laws.str @@ -0,0 +1,22 @@ +module prop-laws +imports libstrategolib signatures/- +rules + + DefI : Impl(x, y) -> Or(Not(x), y) + DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) + + DN : Not(Not(x)) -> x + + DMA : Not(And(x, y)) -> Or(Not(x), Not(y)) + DMO : Not(Or(x, y)) -> And(Not(x), Not(y)) + + DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) + DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) + + DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z)) + DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y)) + +strategies + + dnf4 = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO) + cnf4 = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO) \ No newline at end of file diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str index 4452125..f80a4f4 100644 --- a/trans/spoofax_propositional_language.str +++ b/trans/spoofax_propositional_language.str @@ -10,6 +10,7 @@ imports prop-dnf prop-dnf3 prop-cnf3 + prop-laws rules // Debugging