signature IFF_SOLVER =

sig

  val decide : string -> bool

end

structure IffSolver : IFF_SOLVER =

struct

exception FAIL

datatype formula = Atom of string | Iff of formula * formula

fun scan s =

  let

    fun push yss = [] :: yss 

    fun add x (ys :: yss) = (x :: ys) :: yss

      | add _ _ = raise FAIL

    fun pop ([a, b] :: yss) = add (Iff (b, a)) yss

      | pop _ = raise FAIL

    fun formula [] acc = acc

      | formula ("(" :: xs) acc = formula xs (push acc)

      | formula (")" :: xs) acc = formula xs (pop acc)

      | formula ("<=>" :: xs) acc = formula xs acc

      | formula (x :: xs) acc = formula xs (add (Atom x) acc)

    val tokens = String.tokens (fn c => c = #" ") s

  in

    (case formula tokens [[]] of

      [[f]] => f

    | _ => raise FAIL)

  end

fun decide s =

  let

    fun fold_atoms f (Atom n) = f s

      | fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q

    fun collect s tab =

      (case Symtab.lookup tab s of

        NONE => Symtab.update (s, false) tab

      | SOME v => Symtab.update (s, not v) tab)

    fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true

  in 

    (case try scan s of

      NONE => false

    | SOME f => check (fold_atoms collect f Symtab.empty))

  end

end