(* 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, x) counts the number of occurrences of a in x *)

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

(* val inLan : (int * int * int * int -> bool) -> str -> bool

   inLan f x tests whether x is in {0}^*{1}^*{2}^*{3}^* and f(i, j, k,
   l) holds, where i, j, k and l, respectively, are the numbers of 0s,
   1s, 2s and 3s, respectively, in x *)

fun inLan (f : int * int * int * int -> bool) (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 f(i, j, k, l) end;
      
(* val even : int -> bool

   even n tests whether n is even *)

fun even (n : int) = n mod 2 = 0

(* val odd : int -> bool

   odd n tests whether n is odd *)

fun odd (n : int) = n mod 2 = 1

(* val inYgen : bool -> str -> bool *)

fun inYgen (b : bool) =
      inLan
      (fn (i, j, k, l) =>
            i + j <= k + l andalso
            ((if b then odd else even) (i + j + k + l)))

(* val inY     : str -> bool
   val inYeven : str -> bool

   inY tests for membership of Y
   inYeven tests for membership of Y, but where the length is even *)

val inY     = inYgen true
val inYeven = inYgen false

(* val in123gen : bool -> str -> bool *)

fun in123gen (b : bool) =
      inLan
      (fn (i, j, k, l) =>
            i = 0 andalso l <= j andalso j - l <= k andalso
            ((if b then odd else even) (j + k + l)))

(* val in123     : str -> bool
   val in123even : str -> bool

   in123 tests for membership in {1^n1^j2^k3^n | j <= k and n + j + k + n
   is odd};
   in123even tests for membership in {1^n1^j2^k3^n | j <= k and n + j + k + n
   is even} *)

val in123     = in123gen true
val in123even = in123gen false

(* val in012gen : bool -> str -> bool *)

fun in012gen (b : bool) =
      inLan
      (fn (i, j, k, l) =>
            l = 0 andalso i <= k andalso j <= k - i andalso
            ((if b then odd else even) (i + j + k)))

(* val in012     : str -> bool
   val in012even : str -> bool

   in012 tests for membership in {0^n1^j2^k2^n | j <= k and n + j + k + n
   is odd};
   in012even tests for membership in {0^n1^j2^k2^n | j <= k and n + j + k + n
   is even} *)

val in012     = in012gen true
val in012even = in012gen false

(* val in12gen : bool -> str -> bool *)

fun in12gen (b : bool) =
      inLan
      (fn (i, j, k, l) =>
            i = 0 andalso l = 0 andalso j <= k andalso
            ((if b then odd else even) (j + k)))

(* val in12     : str -> bool
   val in12even : str -> bool

   in12 tests for membership in {1^j2^k | j <= k and j + k is odd};
   in12even tests for membership in {1^j2^k | j <= k and j + k is even} *)

val in12     = in12gen true
val in12even = in12gen false

(* 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 -> bool) -> str set * str set

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

   xs is all elements of upto n that are satisfied by p; and

   ys is all elements of upto n that are not satisfied by p *)

fun partition n (p : str -> bool) = Set.partition p (upto n);

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

   if n >= 0, then test n p 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 satisfied by p 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 satisfied by p but is generated by gram, then yOpt =
     SOME y for some such y; otherwise, yOpt = NONE. *)

fun test n (p : str -> bool) =
      let val (goods, bads) = partition n p
      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;

(* val changeStartVariable : gram * sym -> gram

   if q is a variable of gram, then changeStartVariable(gram, q)
   returns the simplification of the grammar formed by changing gram's
   start variables to be q; otherwise, it raises an exception *)

fun changeStartVariable(gram, q) =
      let val {vars, start, prods} = Gram.toConcr gram
      in if SymSet.memb(q, vars)
         then Gram.simplify
              (Gram.fromConcr{vars = vars, start = q, prods = prods})
         else raise Fail "symbol must be variable of grammar"
      end;

(* doit : int -> (str -> bool) -> gram -> sym -> str option * str option *)

fun doit n p gram q = test n p (changeStartVariable(gram, q));