From 2357e1f220d695e404023a58186c43ec50cb2b65 Mon Sep 17 00:00:00 2001 From: Glen Whitney Date: Fri, 15 Jan 2021 09:57:30 -0800 Subject: [PATCH] docs: Add section 4.2 Also update to latest revision of mkdocs semiliterate plugin. Up next: using SPT as an alternate means of running Stratego. --- README.md | 4 +- docrefs/sec4.2.md | 1 + editor/Manual.esv | 1 + editor/Syntax.esv | 1 - mkdocs.yml | 1 + syntax/Spoofax-Propositional-Language.sdf3 | 2 +- syntax/examples/sec4.2_test3.spl | 1 + trans/prop-dnf-rules.str | 59 ++++++++++++++++++++++ trans/prop-dnf.str | 9 ++++ trans/prop-eval-rules.str | 20 +++++--- trans/spoofax_propositional_language.str | 1 + 11 files changed, 90 insertions(+), 10 deletions(-) create mode 100644 docrefs/sec4.2.md create mode 100644 syntax/examples/sec4.2_test3.spl create mode 100644 trans/prop-dnf-rules.str create mode 100644 trans/prop-dnf.str diff --git a/README.md b/README.md index 1c13c00..602a5a1 100644 --- a/README.md +++ b/README.md @@ -60,9 +60,9 @@ at the top of {! docrefs/sec4.1.md !} of the manual. It consists of the following signature of constructors: ```stratego -{! src-gen/signatures/Spoofax-Propositional-Language-sig.str --- +{! src-gen/signatures/Spoofax-Propositional-Language-sig.str extract: start: '(signature[\s]*)$' - end: '^(\s*Eq\s*:.*)' + stop: '^(\s*Eq\s*:.*)' !} ``` diff --git a/docrefs/sec4.2.md b/docrefs/sec4.2.md new file mode 100644 index 0000000..8328565 --- /dev/null +++ b/docrefs/sec4.2.md @@ -0,0 +1 @@ +[Section 4.2](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#adding-rules-to-a-rewrite-system) diff --git a/editor/Manual.esv b/editor/Manual.esv index 0c773a8..fae7b1b 100644 --- a/editor/Manual.esv +++ b/editor/Manual.esv @@ -2,3 +2,4 @@ module Manual menus menu: "Manual" (openeditor) action: "prop-eval" = do-eval (source) + action: "prop-dnf" = do-dnf (source) diff --git a/editor/Syntax.esv b/editor/Syntax.esv index c92a6b9..3d65405 100644 --- a/editor/Syntax.esv +++ b/editor/Syntax.esv @@ -20,7 +20,6 @@ menus action: "Format" = editor-format (source) action: "Show parsed AST" = debug-show-aterm (source) - action: "Test action" = debug-show-aterm views diff --git a/mkdocs.yml b/mkdocs.yml index ef1b344..2cbe8f2 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -11,6 +11,7 @@ nav: - README.md - syntax/Spoofax-Propositional-Language.md - trans/prop-eval-rules.md +- trans/prop-dnf-rules.md theme: name: readthedocs markdown_extensions: diff --git a/syntax/Spoofax-Propositional-Language.sdf3 b/syntax/Spoofax-Propositional-Language.sdf3 index e085f2b..71bd2f7 100644 --- a/syntax/Spoofax-Propositional-Language.sdf3 +++ b/syntax/Spoofax-Propositional-Language.sdf3 @@ -8,7 +8,7 @@ Title: Concrete Syntax The current Spoofax/Eclipse IDE is oriented around individual language projects. Therefore in order to work with ASTs of the SPL [abstract syntax](../README.md#abstract-syntax) that we just saw, it's easiest to -define a concrete syntax for SPL, with the following SDF3 definition: +define a concrete syntax for SPL, via the following SDF3 definition: *[SPL]: Spoofax Propositional Language diff --git a/syntax/examples/sec4.2_test3.spl b/syntax/examples/sec4.2_test3.spl new file mode 100644 index 0000000..cfce111 --- /dev/null +++ b/syntax/examples/sec4.2_test3.spl @@ -0,0 +1 @@ +(r -> p & q) & p diff --git a/trans/prop-dnf-rules.str b/trans/prop-dnf-rules.str new file mode 100644 index 0000000..dad4386 --- /dev/null +++ b/trans/prop-dnf-rules.str @@ -0,0 +1,59 @@ +/** md +Title: Running a Strategy, continued + +## Disjunctive Normal Form + +The next Stratego example, in {! ../docrefs/sec4.2.md !}, extends +`prop-eval-rules` to convert SPL propositions into disjunctive normal form (DNF). +Once again, we can place the Stratego code in `trans/prop-dnf-rules.str`: + +```Stratego +**/ +/** md Include this code in documentation: */ +module prop-dnf-rules +imports prop-eval-rules +rules + E : Impl(x, y) -> Or(Not(x), y) + E : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) + + E : Not(Not(x)) -> x + + E : Not(And(x, y)) -> Or(Not(x), Not(y)) + E : Not(Or(x, y)) -> And(Not(x), Not(y)) + + E : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) + E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y)) +/* end of code inclusion **/ +/** md rest of documentation +``` +and create a `trans/prop-dnf.str` that defines a strategy for applying the +DNF rules and supplies the glue needed between ESV and Stratego: +```Stratego +{! prop-dnf.str !} +``` +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} !} +``` +should suffice to make the dnf strategy available in the "Spoofax > Manual" +menu. + +Indeed, we can try it out on `syntax/examples/sec4.2_test3.spl`: +```SPL +{! ../syntax/examples/sec4.2_test3.spl !} +``` +to produce +``` +{! ../syntax/examples/sec4.2_test3.dnf.aterm !} +``` +as verified in the manual (again, modulo the"ATom" typo in the manual). + +However, we also want to use this second example to show another method of +running Stratego strategies from the Eclipse IDE. + +## Spoofax Testing Language + +CONTINUE FROM HERE +**/ \ No newline at end of file diff --git a/trans/prop-dnf.str b/trans/prop-dnf.str new file mode 100644 index 0000000..f00f246 --- /dev/null +++ b/trans/prop-dnf.str @@ -0,0 +1,9 @@ +module prop-dnf +imports libstrategolib prop-dnf-rules +strategies + dnf = innermost(E) + + // Interface dnf strategy with editor services and file system + do-dnf: (selected, _, _, path, project-path) -> (filename, result) + with filename := path + ; result := selected diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str index 1af7eaf..e0cd1eb 100644 --- a/trans/prop-eval-rules.str +++ b/trans/prop-eval-rules.str @@ -78,13 +78,14 @@ Actually, we'll create a submenu "Manual" for our examples. It's cleanest to put our additions in a separate ESV module, which then must be included into the `editor/Main.esv` file, like so: ```esv -{! ../editor/Main.esv {terminate: 'provider\s*:', replace: ['^\s*$']} !} - [ ... rest of file suppressed for brevity. ] +{! ../editor/Main.esv extract: + replace: ['^\s*$'] +terminate: 'provider\s*:' !} [ ... rest of file suppressed for brevity. ] ``` It's just the one line `Manual` in the `imports` section that we have added. The `editor/Manual.esv` implementing the submenu is also very simple: ```esv -{! ../editor/Manual.esv !} +{! ../editor/Manual.esv terminate: dnf !} ``` Note that the quoted string on the `action` line is the text label of the menu item in the "Manual" submenu, and the first identifier on its right-hand side is the @@ -95,7 +96,7 @@ caused by an ESV action item has a specific, multi-item argument list, whereas on. To bridge this gap, we must add one more item to `trans/prop-eval.str`, namely: ```Stratego -{! prop-eval.str {start: '^(.*Interface.*\s*)$'} !} +{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !} ``` This "do-XXX" rule is pretty much boilerplate glue between ESV and your Stratego strategy of interest. (Note that this "glue" being used here corresponds to @@ -109,10 +110,13 @@ working Calc repository, and all seems to be well.) There's one last step before you can run `eval` from inside the IDE. Editor Services has to be able to find the `do-eval` rule. You can enable that -by including the `prop-eval` module in the main Stratego file for our language, +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 {terminate: debug-show} !} +{! spoofax_propositional_language.str extract: + replace: ['prop-dnf'] +terminate: debug-show +!} [ ... rest of file suppressed. ] ``` (I am unclear on what triggers ESV to use this particular Stratego file, but @@ -140,4 +144,8 @@ to produce ``` {! ../syntax/examples/sec4.1_test2.eval.aterm !} ``` + +Both of these results match the expected output of the `eval` transformation +as shown in {! ../docrefs/sec4.1.md !} (allowing for the typo "ATom" in the +manual in the latter case). **/ diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str index 945407b..3374459 100644 --- a/trans/spoofax_propositional_language.str +++ b/trans/spoofax_propositional_language.str @@ -7,6 +7,7 @@ imports outline analysis prop-eval + prop-dnf rules // Debugging