--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/external_solver.ML	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,56 @@
+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