Merge pull request #41 from gwhitney/stratego-fixes

fix: correct typos and errors in Stratego Tutorial/Reference

source/langdev/meta/lang/stratego/strategoxt/04-term-rewriting.md

@@ -54,6 +54,7 @@ Now we can create similar evaluation rules for all constructors of sort `Prop`:
       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
@@ -84,10 +85,10 @@ This results in an executable `prop-eval` that can be used to evaluate Boolean e
     False
 
     $ cat test2.prop
-    And(Impl(True(),And(Atom("p"),Atom("q"))),ATom("p"))
+    And(Impl(True(),And(Atom("p"),Atom("q"))),Atom("p"))
 
     $ ./prop-eval -i test2.prop
-    And(And(Atom("p"),Atom("q")),ATom("p"))
+    And(And(Atom("p"),Atom("q")),Atom("p"))
 
 We can also import these definitions in the Stratego Shell, as illustrated by the following session:
 
@@ -100,14 +101,14 @@ We can also import these definitions in the Stratego Shell, as illustrated by th
     stratego> eval
     False
 
-    stratego> !And(Impl(True(),And(Atom("p"),Atom("q"))),ATom("p"))
-    And(Impl(True,And(Atom("p"),Atom("q"))),ATom("p"))
+    stratego> !And(Impl(True(),And(Atom("p"),Atom("q"))),Atom("p"))
+    And(Impl(True,And(Atom("p"),Atom("q"))),Atom("p"))
 
     stratego> eval
-    And(And(Atom("p"),Atom("q")),ATom("p"))
+    And(And(Atom("p"),Atom("q")),Atom("p"))
 
     stratego> :quit
-    And(And(Atom("p"),Atom("q")),ATom("p"))
+    And(And(Atom("p"),Atom("q")),Atom("p"))
     $
 
 The first command imports the `prop-eval` module, which recursively loads the evaluation rules and the library, thus making its definitions available in the shell. The `!` commands replace the current term with a new term. (This _build_ strategy will be properly introduced in [Chapter 8][1].)
@@ -131,12 +132,12 @@ Next we extend the rewrite rules above to rewrite a Boolean expression to disjun
 
 We use this signature only to describe what a disjunctive normal form is, not in an the actual Stratego program. This is not necessary, since terms conforming to the DNF signature are also `Prop` terms as defined before. For example, the disjunctive normal form of
 
-    And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p"))
+    And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),Atom("p"))
 
 is
 
-    Or(And(Not(Atom("r")),ATom("p")),
-       And(And(Atom("p"),Atom("q")),ATom("p")))
+    Or(And(Not(Atom("r")),Atom("p")),
+       And(And(Atom("p"),Atom("q")),Atom("p")))
 
 Module `prop-dnf-rules` extends the rules defined in `prop-eval-rules` with rules to achieve disjunctive normal forms:
 
@@ -171,8 +172,8 @@ compile it in the usual way
 so that we can use it to transform terms:
 
     $ cat test3.prop
-    And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p"))
+    And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),Atom("p"))
     $ ./prop-dnf -i test3.prop
-    Or(And(Not(Atom("r")),ATom("p")),And(And(Atom("p"),Atom("q")),ATom("p")))
+    Or(And(Not(Atom("r")),Atom("p")),And(And(Atom("p"),Atom("q")),Atom("p")))
 
 [1]: 08-creating-and-analyzing-terms.md "Creating and Analyzing Terms"

source/langdev/meta/lang/stratego/strategoxt/05-rewriting-strategies.md

@@ -108,11 +108,11 @@ The `Dnf` function mimics the innermost normalization strategy by recursively tr
 In order to compute the disjunctive normal form of a term, we have to _apply_ the `Dnf` function to it, as illustrated in the following application of the `prop-dnf3` program:
 
     $ cat test1.dnf
-    Dnf(And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p")))
+    Dnf(And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),Atom("p")))
 
     $ ./prop-dnf3 -i test1.dnf
-    Or(And(Not(Atom("r")),Dnf(Dnf(ATom("p")))),
-       And(And(Atom("p"),Atom("q")),Dnf(Dnf(ATom("p")))))
+    Or(And(Not(Atom("r")),Atom("p")),
+       And(And(Atom("p"),Atom("q")),Atom("p")))
 
 For conjunctive normal form we can create a similar definition, which can now co-exist with the definition of DNF. Indeed, we could then simultaneously rewrite one subterm to DNF and the other to CNF.
 
@@ -223,6 +223,7 @@ Module `prop-eval2` defines the evaluation rules for Boolean expressions and a s
       Eval : Impl(True(), x)  -> x
       Eval : Impl(x, True())  -> True()
       Eval : Impl(False(), x) -> True()
+      Eval : Impl(x, False()) -> Not(x)
       Eval : Eq(False(), x)   -> Not(x)
       Eval : Eq(x, False())   -> Not(x)
       Eval : Eq(True(), x)    -> x

source/langdev/meta/lang/stratego/strategoxt/09-traversal-strategies.md

@@ -125,7 +125,7 @@ But we can do better, and also make the _composition_ of this strategy reusable.
       proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y)
       proptr(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
     strategies
-      propbu(s) = proptr(propbu(s)); s
+      propbu(s) = try(proptr(propbu(s))); s
     strategies
       dnf    = propbu(dnfred)
       dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
@@ -147,7 +147,7 @@ Come to think of it, `dnfred` and `cnfred` are somewhat useless now and can be i
       proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y)
       proptr(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
     strategies
-      propbu(s) = proptr(propbu(s)); s
+      propbu(s) = try(proptr(propbu(s))); s
     strategies
       dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf))
       cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))
@@ -203,7 +203,7 @@ can be written by the congruence `And(s,s)`. Applying this to the `prop-dnf` pro
       main = io-wrap(dnf)
     strategies
       proptr(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s)
-      propbu(s) = proptr(propbu(s)); s
+      propbu(s) = try(proptr(propbu(s))); s
     strategies
       dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf))
       cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))
@@ -252,10 +252,10 @@ As an example, consider checking the output of the `dnf` and `cnf` transformatio
     disj(s) = Or (disj(s), disj(s)) <+ s
 
     // Conjunctive normal form
-    conj-nf = conj(disj(Not(Atom(x)) <+ Atom(x)))
+    conj-nf = conj(disj(Not(Atom(id)) <+ Atom(id)))
 
     // Disjunctive normal form
-    disj-nf = disj(conj(Not(Atom(x)) <+ Atom(x)))
+    disj-nf = disj(conj(Not(Atom(id)) <+ Atom(id)))
 
 The strategies `conj(s)` and `disj(s)` check that the subject term is a conjunct or a disjunct, respectively, with terms satisfying `s` at the leaves. The strategies `conj-nf` and `disj-nf` check that the subject term is in conjunctive or disjunctive normal form, respectively.