/** 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 !}. In this
repository, we've placed those rules in `trans/prop-eval-rules.str`,
and the glue strategies that call them in `trans/prop-eval.str`. This latter
module is imported by `trans/spoofax_propositional_language.str`.

(I am unclear on what triggers Editor Services 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.)

There's an Editor Services module `editor/Manual.esv` to invoke the eval strategy,
and it's included in in `editor/Main.esv.`

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 "test1"
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:
```
{! ../syntax/examples/sec4.1_test1.eval.aterm !}
```
You can do the same with test2:
```SPL
{! ../syntax/examples/sec4.1_test2.spl !}
```
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 !}.

One other note about the files provided in this repository. The "do-XXX" rule
used as boilerplate glue between ESV and a Stratego strategy in
`trans/prop-eval.str` is:

```Stratego
{! prop-eval.str extract: {start: '^(.*Interface.*\s*)$'} !}
```

The version of 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.
**/

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