44 lines
1.4 KiB
Plaintext
44 lines
1.4 KiB
Plaintext
/** 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).
|
|
As the manual notes, another way to see what the `dnf` strategy does to a given
|
|
AST is to add a Spoofax Test Language test that claims it transforms to
|
|
something that it definitely does **not** parse to, e.g.
|
|
```SPT
|
|
{! ../test/manual-suite.spt extract:
|
|
start: '\*\*[/]'
|
|
terminate: '(.*run dnf.*)$' !}
|
|
```
|
|
|
|
The difficulty is that in a standard Spoofax language project, the error popup
|
|
showing what the transformation actually does is nearly unreadable due to
|
|
a tremendous amount of annotation produced by the default static analysis process.
|
|
|
|
Since in this repository we are not actually doing any (meaningful) static
|
|
analysis, it includes a hack which makes the editor popup much more readable.
|
|
Namely, it strips the annotation, by modifying the
|
|
`editor-analyze` rule in `trans/analysis.str` like so:
|
|
```Stratego
|
|
{! ../trans/analysis.str terminate: Debugging!} [rest of file omitted]
|
|
```
|
|
|
|
**/
|
|
|
|
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))
|