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