Functionalizing reduction rules

The manual next goes on, in Chapter 5, to consider ways to add the ability to also compute conjunctive normal forms (CNF) for propositional ASTs. The rules for this form cannot simply be added to those from the prior chapter for disjunctive normal form, as they would produce a non-terminating rewrite system.

The first method for which working examples are provided is the method of “functionalization” in Section 5.1.2. Although an anti-pattern in the views of the Spoofax designers, the examples are still instructive and of course they are implemented here.

In fact, the Stratego code for the CNF is not given explicitly in the manual, but it consists of: 

module prop-cnf3
imports libstrategolib prop-dnf3 signatures/-
signature
  constructors
    Cnf  : Prop -> Prop
    CnfR : Prop -> Prop
rules
  E3 : Cnf(Atom(x))    -> Atom(x)
  E3 : Cnf(Not(x))     -> CnfR(Not(Cnf(x)))
  E3 : Cnf(Or(x, y))   -> CnfR(Or(Cnf(x), Cnf(y)))
  E3 : Cnf(And(x, y))  -> And(Cnf(x), Cnf(y))
  E3 : Cnf(Impl(x, y)) -> Cnf(Not(And(x, Not(y))))
  E3 : Cnf(Eq(x, y))   -> Cnf(And(Impl(x, y), Impl(y, x)))

  E3 : CnfR(Not(Not(x)))      -> x
  E3 : CnfR(Not(Or(x, y)))    -> And(Cnf(Not(x)), Cnf(Not(y)))
  E3 : CnfR(Not(And(x, y)))   -> Cnf(Or(Not(x), Not(y)))
  D3 : CnfR(Not(x))           -> Not(x)

  E3 : CnfR(Or(And(x, y), z)) -> And(Cnf(Or(x, z)), Cnf(Or(y, z)))
  E3 : CnfR(Or(z, And(x, y))) -> And(Cnf(Or(z, x)), Cnf(Or(z, y)))
  D3 : CnfR(Or(x, y))         -> Or(x, y)

strategies
  cnf3 : x -> <make-nf> Cnf(x)
  dcnf : x -> <make-nf> (Dnf(x), Cnf(x))

  // Interface cnf3 strategy with editor services and file system
  do-cnf3: (selected, _, _, path, project-path) -> (filename, result)
    with filename := <guarantee-extension(|"cnf.aterm")> path
       ; result   := <cnf3> selected

  do-dcnf: (selected, _, _, path, project-path) -> (filename, result)
    with filename := <guarantee-extension(|"dc.aterm")> path
       ; result   := <dcnf> selected

Note in particular we have not repeated the make-nf strategy from trans/prop-dnf3.str here — that’s the entire point of functionalization; we can use the same top-level reduction scheme because the introduced function symbols keep track of what operations are being performed. We also introduce a strategy dcnf for the simultaneous construction of DNF and CNF, as noted in the manual.

Again, there are menu items and SPT cases for the cnf3 and dcnf strategies as well. All operate just as in the previous sections.

Command-line Utilities

The Spoofax project offers an executable jar called Sunshine that allows several different Spoofax actions to be invoked from the command line. Let’s say you have downloaded it to the path SUNSHINE_JAR. Then you can see a summary of the available actions with java -jar $SUNSHINE_JAR -h. In the repository there’s a convenience bash script bin/spoofax-menu you can use to run the Sunshine jar: 

#!/bin/bash
SUPPRESS_ERR=YES
while [[ $1 = -* ]]
do
  case $1 in
    -d)
      SUPPRESS_ERR=''
      ;;
  esac
  shift
done

if [[ $SUPPRESS_ERR ]]
then
  exec 2>/dev/null
fi

java -jar $SUNSHINE_JAR transform -i $1 -n $2 -p $SPOOFAX_PROJECT -l $SPOOFAX_PROJECT -l "${ECLIPSE_INSTALL}/plugins"
(You can also get a usage explanation, elided from the listing above, via bin/spoofax-menu -h.)

To use this, you must have a Spoofax menu item set up to run the strategy you want, but then you can invoke it on an arbitrary file from the command line like so: 

spoofax_prop> export SUNSHINE_JAR=~/software/org.metaborg.sunshine2-2.6.0-20210119.175231-1.jar
spoofax_prop> export ECLIPSE_INSTALL=~/software/spoofax
spoofax_prop> export SPOOFAX_PROJECT=~/code/neweclipse/spoofax_prop
spoofax_prop> bin/spoofax-menu syntax/examples/sec5.1.2_test1.spl both-nf3
( Or(
    And(Not(Atom("r")), Atom("p"))
  , And(And(Atom("p"), Atom("q")), Atom("p"))
  )
, And(
    And(
      Or(Not(Atom("r")), Atom("p"))
    , Or(Not(Atom("r")), Atom("q"))
    )
  , Atom("p")
  )
)

In our case, the Sunshine jar doesn’t really give us any new capabilities, and the ESV menu items still have to be set up, but it could make running examples more convenient for you.