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