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