From 56b8b921dce783d7159146ca903442bd9cbd4457 Mon Sep 17 00:00:00 2001 From: Glen Whitney Date: Tue, 12 Jan 2021 08:41:01 -0800 Subject: [PATCH] docs: Initiate building documentation with mkdocs Also lay out the structure of the documentation and supply a decent introduction. Also (unsuccessfully) attempt to get the first example of a Stratego transformation from the manual implemented and documented. --- .gitignore | 2 + README.md | 26 +++- docrefs/manual.md | 1 + docrefs/sec4.1.md | 1 + editor/Main.esv | 1 + editor/Manual.esv | 7 ++ editor/Syntax.esv | 1 + mkdocs.yml | 20 +++ syntax/Spoofax-Propositional-Language.sdf3 | 49 +++++++- syntax/examples/sec4.1_A.spl | 1 + syntax/examples/sec4.1_B.spl | 1 + syntax/examples/sec4.1_test1.spl | 1 + syntax/examples/sec4.1_test2.spl | 1 + trans/prop-eval-rules.str | 135 +++++++++++++++++++++ trans/prop-eval.str | 9 ++ trans/spoofax_propositional_language.str | 1 + 16 files changed, 251 insertions(+), 6 deletions(-) create mode 100644 docrefs/manual.md create mode 100644 docrefs/sec4.1.md create mode 100644 editor/Manual.esv create mode 100644 mkdocs.yml create mode 100644 syntax/examples/sec4.1_A.spl create mode 100644 syntax/examples/sec4.1_B.spl create mode 100644 syntax/examples/sec4.1_test1.spl create mode 100644 syntax/examples/sec4.1_test2.spl create mode 100644 trans/prop-eval-rules.str create mode 100644 trans/prop-eval.str diff --git a/.gitignore b/.gitignore index 0735fdd..8b845af 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ /bin /src-gen /target +/site /.classpath /.project @@ -10,3 +11,4 @@ /.polyglot.metaborg.yaml *.aterm +*~ diff --git a/README.md b/README.md index 1f46858..35e6f73 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,26 @@ -# Spoofax-Propositional-Language Language Specification +Title: The Spoofax Propositional Language +Next: syntax/Spoofax-Propositional-Language.sdf3 +# Stratego Transformations in the Spoofax Eclipse IDE + +The Stratego Tutorial/Reference {! docrefs/manual.md !} in the official Spoofax documentation presents a comprehensive overview of the Stratego approach to abstract syntax tree (AST) transformations. It employs a running example of an abstract syntax intended to represent classical Propositional Logic, which we will dub here the "Spoofax Propositional Language." The manual introduces the concepts of rules and strategies for applying them, and then shows how both of those facilities can be created from more primitive operations of term matching and replacement. Every step of the way is illustrated with actual, working Stratego programs. + +There are, however, two catches for a newcomer trying to learn Spoofax and Stratego for the first time: + +1. All of the examples are worked in an older framework ("Stratego/XT") which has a rather different collection of tools than the current implementation of Spoofax in the Eclipse IDE. +1. Unlike with the Calc example language used for the explication of the Syntax Definition Language SDF3, there does not seem to be any publicly available repository containing the worked examples to follow along with. + +This [Gitea repository](https://code.studioinfinity.org/glen/spoofax_prop) aims to fill both gaps. It can be cloned as an Eclipse project (note the git root is at the project level rather than in the directory above the project, as may be more common; in other words, this repository should be cloned within an existing Eclipse workspace, rather than as the workspace itself). Within that project, (ultimately) every example from the Stratego Tutorial manual starting from Section 4 on can be executed directly. And this (Mkdocs-generated) documentation seeks to clarify the ways that Stratego transformations may be run in the Spoofax/Eclipse IDE environment, serving as a supplement/replacement for the portions of the manual that were specific to Stratego/XT. + +## Abstract syntax + +Let's begin by recalling the abstract syntax of the Spoofax Propositional Language (SPL), as defined 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 --- + start: '(signature[\s]*)$' + end: '^(\s*Eq\s*:.*)' +!} +``` + +Continue reading in the latest released [SPL documentation](http://studioinfinity.org/SPL) to see how to define and run Stratego transformations on ASTs of this language. diff --git a/docrefs/manual.md b/docrefs/manual.md new file mode 100644 index 0000000..e2fa432 --- /dev/null +++ b/docrefs/manual.md @@ -0,0 +1 @@ +[manual](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/index.html) diff --git a/docrefs/sec4.1.md b/docrefs/sec4.1.md new file mode 100644 index 0000000..0ff5d58 --- /dev/null +++ b/docrefs/sec4.1.md @@ -0,0 +1 @@ +[Section 4.1](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.html#transformation-with-rewrite-rules) diff --git a/editor/Main.esv b/editor/Main.esv index 82989d9..7572ab4 100644 --- a/editor/Main.esv +++ b/editor/Main.esv @@ -4,6 +4,7 @@ imports Syntax Analysis + Manual language diff --git a/editor/Manual.esv b/editor/Manual.esv new file mode 100644 index 0000000..a4613d7 --- /dev/null +++ b/editor/Manual.esv @@ -0,0 +1,7 @@ +module Manual + +menus + + menu: "Manual" (openeditor) + + action: "prop-eval" = do-eval diff --git a/editor/Syntax.esv b/editor/Syntax.esv index 3d65405..c92a6b9 100644 --- a/editor/Syntax.esv +++ b/editor/Syntax.esv @@ -20,6 +20,7 @@ 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 new file mode 100644 index 0000000..ef1b344 --- /dev/null +++ b/mkdocs.yml @@ -0,0 +1,20 @@ +site_name: spoofax_prop +docs_dir: target #dummy +plugins: +- search +- semiliterate: + merge_docs_dir: false + ignore_folders: ['target', 'docrefs'] + extract_standard_markdown: + terminate: +nav: +- README.md +- syntax/Spoofax-Propositional-Language.md +- trans/prop-eval-rules.md +theme: + name: readthedocs +markdown_extensions: +- abbr +- pymdownx.superfences +- pymdownx.highlight: + use_pygments: true diff --git a/syntax/Spoofax-Propositional-Language.sdf3 b/syntax/Spoofax-Propositional-Language.sdf3 index 50859a4..e085f2b 100644 --- a/syntax/Spoofax-Propositional-Language.sdf3 +++ b/syntax/Spoofax-Propositional-Language.sdf3 @@ -1,17 +1,33 @@ module Spoofax-Propositional-Language +/** md: +Title: Concrete Syntax + +## 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: + +*[SPL]: Spoofax Propositional Language + +```sdf3 +**/ + imports Common -context-free start-symbols - - Prop - context-free sorts Prop String +context-free start-symbols + + Prop + +/** md (include the following code in the documentation) */ context-free syntax Prop.True = <1> @@ -32,4 +48,27 @@ context-free priorities > Prop.And > Prop.Or > Prop.Impl - > Prop.Eq \ No newline at end of file + > Prop.Eq +/* [stop to avoid the open-comment in the extracted markdown] **/ + +/** md [conclusion of the documentation] +``` + +Thus, the first two example AST expressions + +`A: {! examples/sec4.1_A.aterm !}` and +`B: {! examples/sec4.1_B.aterm !}` + +from {! ../docrefs/sec4.1.md !} can be generated by the following much more +compact SPL expressions: + +`A: {! examples/sec4.1_A.spl !}` and +`B: {! examples/sec4.1_B.spl !}`. (If you are following along in the repository, +you can visit the file `syntax/examples/sec4.1_A.spl` (or ...`_B.spl`) and from the +Spoofax menu select "Syntax > Show parsed AST" to see the AST generation +in action.) + +This concrete syntax actually makes it easier to construct the example +expressions used throughout the tutorial manual as examples for Stratego +processing. +**/ diff --git a/syntax/examples/sec4.1_A.spl b/syntax/examples/sec4.1_A.spl new file mode 100644 index 0000000..cb3acfd --- /dev/null +++ b/syntax/examples/sec4.1_A.spl @@ -0,0 +1 @@ +(1 -> 0) & 0 diff --git a/syntax/examples/sec4.1_B.spl b/syntax/examples/sec4.1_B.spl new file mode 100644 index 0000000..4f60ecf --- /dev/null +++ b/syntax/examples/sec4.1_B.spl @@ -0,0 +1 @@ +p & 0 diff --git a/syntax/examples/sec4.1_test1.spl b/syntax/examples/sec4.1_test1.spl new file mode 100644 index 0000000..20ec26d --- /dev/null +++ b/syntax/examples/sec4.1_test1.spl @@ -0,0 +1 @@ +(1 -> 0 & 1) & 1 diff --git a/syntax/examples/sec4.1_test2.spl b/syntax/examples/sec4.1_test2.spl new file mode 100644 index 0000000..dc3d2b9 --- /dev/null +++ b/syntax/examples/sec4.1_test2.spl @@ -0,0 +1 @@ +(1 -> p & q) & p diff --git a/trans/prop-eval-rules.str b/trans/prop-eval-rules.str new file mode 100644 index 0000000..8bfe6f4 --- /dev/null +++ b/trans/prop-eval-rules.str @@ -0,0 +1,135 @@ +/** md +Title: Running a Strategy + +## Running a Strategy + +The first example of running a Stratego strategy +in the {! ../docrefs/manual.md !} } is that of _evaluating_ an AST, +via the `prop-eval-rules` module in {! ../docrefs/sec4.1.md !}. This page +describes the most straightforward way to run this same strategy +in the Spoofax Eclipse IDE. + +In the current project structure, Stratego transformations and strategies go in +the `trans` directory. So, you can place the Stratego code for +this module in `trans/prop-eval-rules.str`, with the following contents: + +```Stratego +[End the documentation block to avoid the comment close in the code] **/ +/** md [restart processing to include the code in the documentation] */ +module prop-eval-rules +imports signatures/- +rules + E : Not(True()) -> False() + E : Not(False()) -> True() + E : And(True(), x) -> x + E : And(x, True()) -> x + E : And(False(), x) -> False() + E : And(x, False()) -> False() + E : Or(True(), x) -> True() + E : Or(x, True()) -> True() + E : Or(False(), x) -> x + E : Or(x, False()) -> x + E : Impl(True(), x) -> x + E : Impl(x, True()) -> True() + E : Impl(False(), x) -> True() + E : Impl(x, False()) -> Not(x) + E : Eq(False(), x) -> Not(x) + E : Eq(x, False()) -> Not(x) + E : Eq(True(), x) -> x + E : Eq(x, True()) -> x +/* [stop to avoid the open-comment in the code block] **/ +/** md [conclusion of the documentation] +``` + +Note an important difference between this code and the `prop-eval-rules` block +in {! ../docrefs/sec4.1.md !}: here, we import `signatures/-` rather than `prop`. +That's because the Spoofax IDE automatically generates the Spoofax Propositional +Language AST signature for us, from its concrete syntax definition. (The +evaluation rules in {! ../docrefs/sec4.1.md !} also happen to be missing the +fourth `Impl` rule, but that's less material; unsurprisingly, none of the examples +given in the manual happen to rely on that rule, but we include it here for the +sake of completeness.) + +As in the {! ../docrefs/manual.md !}, we need an additional module, which we can +place in `trans/prop-eval.str`, to describe the strategy by which we want +to apply the above evaluation rules and to facilitate actually invoking +the strategy on an AST. This file starts out much like its counterpart in +{! ../docrefs/sec4.1.md !}: + +```Stratego +{! prop-eval.str {terminate: '^\s*$'} !} +``` + +So far, we've included the evaluation rules and defined a strategy `eval` to +apply them exhaustively to an AST starting with inner subterms. Now we want to +be able to "run" this strategy on an actual AST. + +### Editor Services + +The most straightforward mechanism to execute a Stratego transformation +in the Spoofax IDE is by use of Editor Services (ESV). ESV is actually a full +declarative language in its own right, covering syntax coloring, menu items, +hover texts, and more, and with its own +[manual](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html). +We will not delve into the details of ESV here, but merely provide a recipe +for using it to add an item to the "Spoofax" Eclipse menu for running Stratego. + +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. ] +``` +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 !} +``` +Note that the quoted string on the `action` line is the text label of the menu +item in the "Manual" submenu, and the identifier on its right-hand side is the +Stratego action to call. But note that `do-eval` is not the same identifier as +`eval` in our last Stratego file above. That's because the Stratego invocation +caused by an ESV action item has a specific, multi-item argument list, whereas +`eval` above expects only a single Spoofax Propositional Language AST to operate +on. To bridge this gap, we must add one more item to `trans/prop-eval.str`, +namely: +```Stratego +{! prop-eval.str {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 +what's used in the example +[Calc language project](https://github.com/MetaBorgCube/metaborg-calc), +but is slightly different from what is described in the +[Menus section](http://www.metaborg.org/en/latest/source/langdev/meta/lang/esv.html#menus) +of the ESV Manual. I am unclear on the significance of this difference or which +form is "better" -- I simply modeled this Stratego code after the code in the +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, +in this case `trans/spoofax_propositional_language.str`: +```Stratego +{! spoofax_propositional_language.str {terminate: debug-show} !} + [ ... rest of file suppressed. ] +``` +(I am unclear on what triggers ESV to use this particular Stratego file, but +in any automatically-generated Spoofax project there will be a main language +Stratego file in the `trans` directory, and that's the file from which +the rule specified in an ESV `action` has to be visible.) + +Ok, with all of these elements in place, you should now be able to invoke +the `eval` rule from the "Spoofax" menu. For example, to execute the next example +from the Spoofax Tutorial/Reference +{! ../docrefs/sec4.1.md !}, navigate to the +file `syntax/examples/sec4.1_test1.spl`: +```SPL +{! ../syntax/examples/sec4.1_test1.spl !} +``` +and select "Spoofax > Manual > prop-eval" from the menu bar to produce: + +[CONTINUE HERE ONCE THIS WORKS] + +**/ diff --git a/trans/prop-eval.str b/trans/prop-eval.str new file mode 100644 index 0000000..31d4db3 --- /dev/null +++ b/trans/prop-eval.str @@ -0,0 +1,9 @@ +module prop-eval +imports libstrategolib prop-eval-rules +strategies + eval = innermost(E) + + // Interface eval strategy with editor services and file system + do-eval: (selected, _, _, path, project-path) -> (filename, result) + with filename := path + ; result := selected diff --git a/trans/spoofax_propositional_language.str b/trans/spoofax_propositional_language.str index 08b5603..945407b 100644 --- a/trans/spoofax_propositional_language.str +++ b/trans/spoofax_propositional_language.str @@ -6,6 +6,7 @@ imports pp outline analysis + prop-eval rules // Debugging