signature IFF_SOLVER =sig val decide : string -> boolendstructure IffSolver : IFF_SOLVER =structexception FAILdatatype formula = Atom of string | Iff of formula * formulafun 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) endfun 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)) endend