From d5a19e0d6942fa307e91e14159b0f9fce06f557c Mon Sep 17 00:00:00 2001 From: Glen Whitney Date: Tue, 19 Jan 2021 21:00:56 -0800 Subject: [PATCH] feat: Finish Chapter 5 --- test/manual-suite.spt | 33 +++++++++++++++++++----- trans/prop-desugar.str | 22 ++++++++++++++++ trans/prop-dnf-rules.str | 4 +-- trans/prop-eval2.str | 27 +++++++++++++++++++ trans/prop-laws.str | 2 +- trans/spoofax_propositional_language.str | 2 ++ 6 files changed, 81 insertions(+), 9 deletions(-) create mode 100644 trans/prop-desugar.str create mode 100644 trans/prop-eval2.str diff --git a/test/manual-suite.spt b/test/manual-suite.spt index 1e4f1d9..59b35da 100644 --- a/test/manual-suite.spt +++ b/test/manual-suite.spt @@ -1,7 +1,7 @@ /** md Title: The Remaining Tests -## Programmable Rewriting strategies +## 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) @@ -54,12 +54,13 @@ test sec5_1_2_test1_cnf_ex [[ Or(Not(Atom("r")), Atom("q"))), Atom("p")) -test sec5_1_2_test1_both_ex [[ +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"))) +]] 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 @@ -70,3 +71,23 @@ test sec5_3_1_test1_cnf_ex [[ ]] 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()) diff --git a/trans/prop-desugar.str b/trans/prop-desugar.str new file mode 100644 index 0000000..45f70a7 --- /dev/null +++ b/trans/prop-desugar.str @@ -0,0 +1,22 @@ +module prop-desugar +imports libstrategolib signatures/- + +rules + + DefN : Not(x) -> Impl(x, False()) + DefI : Impl(x, y) -> Or(Not(x), y) + DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) + DefO1 : Or(x, y) -> Impl(Not(x), y) + DefO2 : Or(x, y) -> Not(And(Not(x), Not(y))) + DefA1 : And(x, y) -> Not(Or(Not(x), Not(y))) + DefA2 : And(x, y) -> Not(Impl(x, Not(y))) + + IDefI : Or(Not(x), y) -> Impl(x, y) + + IDefE : And(Impl(x, y), Impl(y, x)) -> Eq(x, y) + +strategies + + desugar = topdown(try(DefI <+ DefE)) + + impl-nf = topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE)) diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str index 9bfab66..dcf6a86 100644 --- a/trans/prop-dnf-rules.str +++ b/trans/prop-dnf-rules.str @@ -67,7 +67,7 @@ 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 extract: - start: '\*\*/' + start: '\*\*[/]' terminate: '(.*run dnf)' !} ``` @@ -86,7 +86,7 @@ what the transformation actually produced. So we add just a bit to `test/manual-suite.spt`: ```SPT {! ../test/manual-suite.spt extract: - start: '\*\*/' + start: '\*\*[/]' terminate: '(.*run dnf.*)$' !} ``` diff --git a/trans/prop-eval2.str b/trans/prop-eval2.str new file mode 100644 index 0000000..9861aff --- /dev/null +++ b/trans/prop-eval2.str @@ -0,0 +1,27 @@ +module prop-eval2 +imports libstrategolib signatures/- +rules + + Eval : Not(True()) -> False() + Eval : Not(False()) -> True() + Eval : And(True(), x) -> x + Eval : And(x, True()) -> x + Eval : And(False(), x) -> False() + Eval : And(x, False()) -> False() + Eval : Or(True(), x) -> True() + Eval : Or(x, True()) -> True() + Eval : Or(False(), x) -> x + Eval : Or(x, False()) -> x + Eval : Impl(True(), x) -> x + Eval : Impl(x, True()) -> True() + Eval : Impl(False(), x) -> True() + Eval : Impl(x, False()) -> Not(x) + Eval : Eq(False(), x) -> Not(x) + Eval : Eq(x, False()) -> Not(x) + Eval : Eq(True(), x) -> x + Eval : Eq(x, True()) -> x + +strategies + + eval-up = bottomup(repeat(Eval)) + eval-down = downup(repeat(Eval)) diff --git a/trans/prop-laws.str b/trans/prop-laws.str index 1f8987e..570f8ba 100644 --- a/trans/prop-laws.str +++ b/trans/prop-laws.str @@ -19,4 +19,4 @@ rules 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 + cnf4 = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO) diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str index f80a4f4..1017ff8 100644 --- a/trans/spoofax_propositional_language.str +++ b/trans/spoofax_propositional_language.str @@ -11,6 +11,8 @@ imports prop-dnf3 prop-cnf3 prop-laws + prop-eval2 + prop-desugar rules // Debugging