(* val zero : sym
val one : sym
the symbols 0 and 1 *)
val zero = Sym.fromString "0";
val one = Sym.fromString "1";
(* val diff : str -> int
the diff function *)
fun diff (nil : str) = 0
| diff (b :: bs) =
if Sym.equal(b, zero)
then ~1 + diff bs
else 1 + diff bs;
(* val prefixes : str -> str set
returns the set of all prefixes of a string *)
fun prefixes (nil : str) : str set = Set.sing nil
| prefixes (b :: bs) =
StrSet.union
(Set.sing nil,
StrSet.map (fn cs => b :: cs) (prefixes bs));
(* val substrings : str -> str set
returns the set of all substrings of a string *)
fun substrings (nil : str) : str set = Set.sing nil
| substrings (b :: bs) =
StrSet.union
(substrings bs,
StrSet.map (fn cs => b :: cs) (prefixes bs));
(* val allSubstringsGood : str -> bool
tests whether all substrings of a string have diff's between
~2 and 2, inclusive *)
fun allSubstringsGood x =
Set.all
(fn y =>
let val n = diff y
in ~2 <= n andalso n <= 2 end)
(substrings x);
(* 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 partition : int -> str set * str set
if n >= 0, then partition n returns (xs, ys) where:
xs is all elements w of upto n such that every substring of w
has a diff between ~2 and 2, inclusive; and
ys is all elements w of upto n such that at least one substring of
w has a diff that's not between ~2 and 2, inclusive *)
fun partition n = Set.partition allSubstringsGood (upto n);
(* val test : int -> int * int * (dfa -> bool)
if n >= 0, then test n returns
(m, l, f) : int * int * (dfa -> bool),
where m is the size of #1(partition n), l is the size of
#2(partition n), and f is the function that takes in a DFA dfa, and
tests whether dfa accepts all the elements of #1(partition n), but
rejects all the elements of #2(partition n) *)
fun test n =
let val (goods, bads) = partition n
in (Set.size goods, Set.size bads,
fn dfa =>
let val determAccepted = DFA.determAccepted dfa
in Set.all determAccepted goods andalso
Set.all (not o determAccepted) bads
end)
end;