(* val inOrder : sym list -> bool

   inOrder x tests whether an element of {0, 1, 2, 3}^* is in
   {0}^*{1}^*{2}^*{3}^* *)

fun inOrder (b :: c :: ds) =
      Sym.compare(b, c) <> GREATER andalso inOrder(c :: ds)
  | inOrder _              = true;

(* val count : sym * sym list -> int

   count(a, bs) counts the number of occurrences of a in bs *)

fun count(_, nil)     = 0
  | count(a, b :: bs) =
      (if Sym.equal(a, b) then 1 else 0) + count(a, bs);

(* val inX : str -> bool

   inX x tests whether an element x of {0, 1, 2, 3}^* is in X *)

fun inX (x : str) =
      inOrder x andalso
      let val i = count(Sym.fromString "0", x)
          val j = count(Sym.fromString "1", x)
          val k = count(Sym.fromString "2", x)
          val l = count(Sym.fromString "3", x)
      in i + j <= k + l end;

(* val upto : int -> str set

   if n >= 0, then upto n returns all strings over alphabet {0, 1, 2,
   3} 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, 2, 3", ys))
      end;

(* val partition : int -> str set * str set

   if n >= 0, then partition n returns (xs, ys) where:

   xs is all elements of upto n that are in X; and

   ys is all elements of upto n that are not in X *)

fun partition n = Set.partition inX (upto n);

(* val test : int -> gram -> str option * str option

   if n >= 0, then test n returns a function f such that, for all grammars
   gram, f gram returns a pair (xOpt, yOpt) such that:

     If there is an element of {0, 1, 2, 3}^* of length no more than n
     that is in X but is not generated by gram, then xOpt = SOME x
     for some such x; otherwise, xOpt = NONE.

     If there is an element of {0, 1, 2, 3}^* of length no more than n
     that is not in X but is generated by gram, then yOpt = SOME y
     for some such y; otherwise, yOpt = NONE. *)

fun test n =
      let val (goods, bads) = partition n
      in fn gram =>
              let val generated     = Gram.generated gram
                  val goodNotGenOpt = Set.position (not o generated) goods
                  val badGenOpt     = Set.position generated bads
              in ((case goodNotGenOpt of
                        NONE   => NONE
                      | SOME i => SOME(ListAux.sub(Set.toList goods, i))),
                  (case badGenOpt of
                        NONE   => NONE
                      | SOME i => SOME(ListAux.sub(Set.toList bads, i))))
              end
      end;