From 50dce6b265d34b2fd432abb5e7cbf6d5c52b79be Mon Sep 17 00:00:00 2001 From: Glen Whitney Date: Sun, 17 Jan 2021 10:15:32 -0800 Subject: [PATCH] docs: Document section 5.1.2 Note still need to implement and document command-line running of these strategies. --- docrefs/sec5.1.2.md | 1 + mkdocs.yml | 1 + trans/prop-dnf-rules.str | 2 +- trans/prop-dnf3.str | 83 ++++++++++++++++++++++++++++++++++++++- trans/prop-eval-rules.str | 3 +- 5 files changed, 87 insertions(+), 3 deletions(-) create mode 100644 docrefs/sec5.1.2.md diff --git a/docrefs/sec5.1.2.md b/docrefs/sec5.1.2.md new file mode 100644 index 0000000..dfe21f8 --- /dev/null +++ b/docrefs/sec5.1.2.md @@ -0,0 +1 @@ +[Section 5.1.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.html#attempt-2-functionalization) \ No newline at end of file diff --git a/mkdocs.yml b/mkdocs.yml index 2cbe8f2..41a15dd 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -12,6 +12,7 @@ nav: - syntax/Spoofax-Propositional-Language.md - trans/prop-eval-rules.md - trans/prop-dnf-rules.md +- trans/prop-dnf3.md theme: name: readthedocs markdown_extensions: diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str index bbce794..42e32ea 100644 --- a/trans/prop-dnf-rules.str +++ b/trans/prop-dnf-rules.str @@ -35,7 +35,7 @@ Now just importing `prop-dnf` in `trans/spoofax-propositional-language.str` and adding a menu item to `editor/Manual.esv`: ```ESV ... -{! ../editor/Manual.esv extract: {start: menus} !} +{! ../editor/Manual.esv extract: {start: menus, stop: dnf3} !} ``` should suffice to make the dnf strategy available in the "Spoofax > Manual" menu. diff --git a/trans/prop-dnf3.str b/trans/prop-dnf3.str index 6583969..6b9d0a3 100644 --- a/trans/prop-dnf3.str +++ b/trans/prop-dnf3.str @@ -1,3 +1,24 @@ +/** md +Title: Running a Strategy: the command line + +## Functionalizing reduction rules + +The {! ../docrefs/manual.md !} next goes on, in Chapter 5, to consider ways to +add the ability to also compute conjunctive normal forms for propositional +ASTs. The rules for this form cannot simply be added to those from the prior +chapter for disjunctive normal form, as they would produce a non-terminating +rewrite system. + +The first method for which working examples are provided is the method of +"functionalization" in {! ../docrefs/sec5.1.2.md !}. Although an anti-pattern +in the views of the Spoofax designers, the examples are still instructive and +of course we want to implement them here. + +So, we can grab the Stratego code given in the section as our +`trans/prop-dnf3.str`: +```Stratego +**/ +/** md Include this code in docs: */ module prop-dnf3 imports libstrategolib signatures/- signature @@ -28,4 +49,64 @@ strategies // Interface dnf3 strategy with editor services and file system do-dnf3: (selected, _, _, path, project-path) -> (filename, result) with filename := path - ; result := selected \ No newline at end of file + ; result := selected +/* End of code inclusion **/ +/** md Conclusion of documentation: +``` + +Notice the few minor differences from the manual. We import `signatures/-` as +before. We've used a fresh identifier for the `E` and `D` rules, because unlike +in the manual, all of our Stratego files are imported into the same main +`trans/spoofax_propositional_language.str` module. So they must live together, +but as noted in the manual, these functionalized rules do not "play together" +nicely with the evaluation `E` rules introduced [earlier](prop-eval-rules.md). +And we've renamed the `dnf` rule to `make-nf` -- for a reason that will +become clear in a moment -- but incorporated the wrapping by `Dnf` of the AST +we want to compute the DNF of into the `dnf3` strategy, since our concrete +syntax has no way of specifying such a wrapping. + +Also as before, we've created a `syntax/examples/sec_5_1_2_test1.spl` +(which it turns out is just the same as `sec_4_2_test3.spl`) +and a menu item and a `test/manual-suite.spt` case called `sec5_1_2_test1_ex` to +see that all is working well. Applying `dnf3` to the test file produces +``` +{! ../syntax/examples/sec5.1.2_test1.dnf.aterm !} +``` +which is correct. (Note the contrast with what's shown in +{! ../docrefs/sec5.1.2.md !} as the output of the `prop-dnf3` program, +in which the recurring "ATom" typo has blocked +the reductive elimination of some of the occurrences of the Dnf function +symbol. Of course, as the manual itself points out, in proper operation of +this functionalization approach, all of the function symbols must reduce away +to end up back in an AST of the subject language.) + +So now we can move on to the conjunctive normal form. The Stratego code +for the CNF is not given explicitly in the manual, but it consists of: +``` +{! prop-cnf3.str !} +``` + +Note in particular we have not repeated the `make-nf` strategy -- that's the +entire point of functionalization; we can use the same top-level reduction +scheme because the introduced function symbols keep track of what operations +are being performed. We also introduce a strategy `dcnf` for the simultaneous +construction of DNF and CNF, as noted in the manual. + +Again, there are menu items and SPT cases for the `cnf3` and `dcnf` strategies +as well. There's one caveat here, though. The test case for `dcnf`: +```SPT +{! ../test/manual-suite.spt extract: + start: '^(.*test.*both.*\n?)$' +!} +``` +does not actually work, because of what appears to be a bug in SPT: the `to` +in the expectation line is interpreted as part of the expected AST. However, +the error message does show that the transformation is operating properly. + +We can now use this example to show yet another way to try Stratego stragies +with the Spoofax IDE implementation. + +### Command-line Utilities + +[HERE] +**/ \ No newline at end of file diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str index c36d88f..5ee5638 100644 --- a/trans/prop-eval-rules.str +++ b/trans/prop-eval-rules.str @@ -114,7 +114,8 @@ by importing the `prop-eval` module in the main Stratego file for our language, in this case `trans/spoofax_propositional_language.str`: ```Stratego {! spoofax_propositional_language.str extract: - replace: ['prop-dnf'] + - stop: 'prop-dnf' + - start: '^(.*rule.*)$' terminate: debug-show !} [ ... rest of file suppressed. ]