(* 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));