-- Sergio Antoy and Michael Hanus
-- Wed Apr  6 16:15:41 PDT 2011
-- Map coloring with the Quantifiers pattern.

import SetFunctions
import Quantification

data State = WA | OR | ID | BC

states = [WA,OR,ID,BC]

adjacent = [(WA,OR),(WA,ID),(WA,BC),(OR,ID),(ID,BC)]

data Color = Red | Green | Blue

color x = (x, Red ? Green ? Blue)

solve | exists cMap (\map -> 
           forall someAdj'set (\(st1,st2) -> 
               lookup st1 map /= lookup st2 map))
      = cMap
      where cMap = map color states
            someAdj = foldr1 (?) adjacent
            someAdj'set = set0 someAdj

solven | exists cMap (\map -> 
            not_exists someAdj'set (\(st1,st2) -> 
                lookup st1 map == lookup st2 map))
      = cMap
      where cMap = map color states
            someAdj = foldr1 (?) adjacent
            someAdj'set = set0 someAdj


solve' | forall (set0 someAdj)
               (\ (st1,st2) -> lookup st1 aMap /= lookup st2 aMap)
      = aMap
 where aMap = map color states
       someAdj = foldr1 (?) adjacent