(* val upto : int -> str set

   if n >= 0, then upto n returns all strings over the alphabet {0, 1}
   of length no more than n *)

fun upto 0 : str set = Set.sing nil
  | upto n           =
      let val xs = upto(n - 1)
          val ys = Set.filter (fn x => length x = n - 1) xs
      in StrSet.union
         (xs, StrSet.concat(StrSet.fromString "0, 1", ys))
      end;

(* val occs : str * str -> (str * str)list

   if x, w in {0, 1}*, then occs(x, w) returns the list of all pairs
   (u, v) such that w = u @ x @ v *)

fun occs(ds : str, nil : str) : (str * str)list =
      if null ds
      then [(nil, nil)]
      else nil
  | occs(ds,       cs)                          =
      let val b  = hd cs
          val bs = tl cs
      in (if Str.prefix(ds, cs)
          then [(nil, List.drop(cs, length ds))]
          else nil) @      
         map (fn (es, fs) => (b :: es, fs)) (occs(ds, bs))
      end;

(* val inDCS : str * str -> str -> bool

   if x, y, w in {0, 1}*, inDCS (x, y) w tests whether w is in
   DCS(x, y) *)

fun inDCS (x, y) w =
      List.all
      (fn (u, v) => Str.substr(y, u) orelse Str.substr(y, v))
      (occs(x, w))
      andalso
      List.all
      (fn (u, v) => Str.substr(x, u) orelse Str.substr(x, v))
      (occs(y, w));

(* val all2 : ('a * 'a -> bool) -> 'a set -> bool

   all2 f xs tests whether f(x, y) for all x, y in xs *)

fun all2 f xs =
      Set.all
      (fn x =>
            Set.all
            (fn y => f(x, y))
            xs)
      xs

(* val test : int * int -> int * int * ((str * str -> dfa) -> bool)

   if n, m >= 0, then test(n, m) binds xs and ys to upto n and upto m,
   respectively, and then returns

     (Set.size xs * Set.size xs, Set.size ys, f),

   where f is the function that, when called with argument
   g : str * str -> dfa, tests whether, for all x, y in xs, g(x, y)
   returns a DFA dfa such that dfa is minimized (isomorphic to
   the minimization of itself) and, for all w in ys,

     if w is in DCS(x, y), then dfa accepts w; and

     if w is not in DCS(x, y), then dfa does not accept w *)

fun test(n, m) =
      let val xs = upto n
          val ys = upto m
      in (Set.size xs * Set.size xs,
          Set.size ys,
          fn g =>
               all2
               (fn (x, y) =>
                     let val dfa           = g(x, y)
                         val accepted      = DFA.determAccepted dfa
                         val (goods, bads) = Set.partition (inDCS(x, y)) ys
                     in DFA.isomorphic(DFA.minimize dfa, dfa) andalso
                        Set.all accepted goods                andalso
                        Set.all (not o accepted) bads
                     end)
               xs)
      end;