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,6 +2,7 @@
 /bin
 /src-gen
 /target
+/site
 
 /.classpath
 /.project
@@ -10,3 +11,4 @@
 
 /.polyglot.metaborg.yaml
 *.aterm
+*~

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*:.*)'
+!}
+```
+<!-- /md -->
+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.

docrefs/manual.md

@@ -0,0 +1 @@
+[manual](http://www.metaborg.org/en/latest/source/langdev/meta/lang/stratego/strategoxt/index.html)

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)

editor/Main.esv

@@ -4,6 +4,7 @@ imports
 
   Syntax
   Analysis
+  Manual
 
 language
 

editor/Manual.esv

@@ -0,0 +1,7 @@
+module Manual
+
+menus
+
+  menu: "Manual" (openeditor)
+
+   action: "prop-eval" = do-eval

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
   

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: <!-- /md -->
+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

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>
@@ -33,3 +49,26 @@ context-free priorities
   > Prop.Or
   > Prop.Impl
   > 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.
+**/

syntax/examples/sec4.1_A.spl

@@ -0,0 +1 @@
+(1 -> 0) & 0

syntax/examples/sec4.1_B.spl

@@ -0,0 +1 @@
+p & 0

syntax/examples/sec4.1_test1.spl

@@ -0,0 +1 @@
+(1 -> 0 & 1) & 1

syntax/examples/sec4.1_test2.spl

@@ -0,0 +1 @@
+(1 -> p & q) & p

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]
+
+**/

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 := <guarantee-extension(|"eval.aterm")> path
+       ; result   := <eval> selected

trans/spoofax_propositional_language.str

@@ -6,6 +6,7 @@ imports
   pp
   outline
   analysis
+  prop-eval
 
 rules // Debugging