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

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

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)

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)

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
   

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:

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
 

syntax/examples/sec4.2_test3.spl

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

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

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

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*$']} !}
+{! ../editor/Main.esv extract:
-  [ ... rest of file suppressed for brevity. ]
+  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).
 **/

trans/spoofax_propositional_language.str

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