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

  E3 : DnfR(Not(Not(x)))      -> x
  E3 : DnfR(Not(And(x, y)))   -> Or(Dnf(Not(x)), Dnf(Not(y)))
  E3 : DnfR(Not(Or(x, y)))    -> Dnf(And(Not(x), Not(y)))
  D3 : DnfR(Not(x))           -> Not(x)

  E3 : DnfR(And(Or(x, y), z)) -> Or(Dnf(And(x, z)), Dnf(And(y, z)))
  E3 : DnfR(And(z, Or(x, y))) -> Or(Dnf(And(z, x)), Dnf(And(z, y)))
  D3 : DnfR(And(x, y))        -> And(x, y)

strategies
  make-nf  = innermost(E3 <+ D3)
  dnf3 : x -> <make-nf> Dnf(x)
  
  // Interface dnf3 strategy with editor services and file system
  do-dnf3: (selected, _, _, path, project-path) -> (filename, result)
    with filename := <guarantee-extension(|"dnf.aterm")> path
       ; result   := <dnf3> selected