structure ES2Ex4 =
struct
(* val zero : sym is the symbol 0
val one : sym is the symbol 1 *)
val zero = Sym.fromString "0"
val one = Sym.fromString "1"
(* val isZero : sym -> bool
isZero a tests whether a is zero *)
fun isZero a = Sym.equal(a, zero)
(* val isOne : sym -> bool
isOne a tests whether a is one *)
fun isOne a = Sym.equal(a, one)
(* val diffSym : sym -> int
if diffSym is called with zero or one, then it returns the diff of
its argument; otherwise, it returns 0 *)
fun diffSym a =
if isZero a
then ~1
else if isOne a
then 1
else 0
(* val validStr : str -> bool
validStr w tests whether w is in Y, returning true if it is, and
false otherwise; when w is not in Y, it prints an explanation of
why w fails to be in Y on the standard output *)
fun validStr w =
let (* val valid : str * int * str -> bool
in a call valid(ds, n, cs), diff ds = n and w = ds @ cs
if every nonempty prefix of cs ends with a zero or one,
and has a diff that when added to n is <= 1, then
if n + diff cs = 1, then valid silently returns true
otherwise, valid complains that w has a diff of n
instead of 1, and returns false
otherwise, let es be the shortest nonempty prefix of cs
such that either es doesn't end with a zero or one, or
the n + diff es > 1
if the last symbol of es isn't a zero or one, then
valid complains about this symbol of w
otherwise, valid compains that ds @ es is a prefix of w
with a diff that is > 1 *)
fun valid(_, n, nil) =
if n = 1
then true
else (print "diff of string is ";
print(Int.toString n); print " not 1\n";
false)
| valid(ds, n, c :: cs) =
let val m = n + diffSym c
val ds = ds @ [c]
in if m = n
then (print "string has symbol other than 0/1 : ";
print(Sym.toString c); print "\n";
false)
else if m > 1
then (print "prefix "; print(Str.toString ds);
print " of string has diff "; print(Int.toString m);
print " which is greater-than 1\n";
false)
else valid(ds, m, cs)
end
in valid(nil, 0, w) end
(* val shortestPrefix : (int -> bool) -> str -> str * str
if w is an str of zeros and ones, and there is a prefix x of w such
that f(diff x), then shortestPrefix f w returns (x, y), where x
is the shortest such prefix, and y is such that x @ y = w *)
fun shortestPrefix f w =
let (* val short : str * int * str -> str * str
if cs is a list of zeros and ones, and there is a
prefix ds of cs such that f(n + diff ds), then
short(bs, n, cs) returns (bs @ ds, es), where ds is the
shortest such prefix, and es is such that cs = ds @ es *)
fun short(bs, n, nil) =
if f n then (bs, nil) else raise Fail "shouldn't happen"
| short(bs, n, c_cs as c :: cs) =
if f n
then (bs, c_cs)
else short(bs @ [c], n + diffSym c, cs)
in short(nil, 0, w) end
(* val splitPositive : str -> str * str
if w is an str of zeros and ones such that diff w >= 1, then
splitPositive w returns a pair (x, y) such that w = x @ y,
x is in Y and diff y = diff w - 1 *)
val splitPositive = shortestPrefix(fn n => n >= 1)
(* val indent : int -> unit
indent n prints n spaces *)
fun indent n = print(StringCvt.padLeft #" " n "")
(* val text1 : int -> unit
print explanation based on rule (1) of X's definition at given indentation *)
fun text1 ind = (indent ind; print "1 is in X, by (1)\n")
(* val text2 : int * str * str * str -> unit
print explanation based on rule (2) of X's definition at given indentation *)
fun text2(ind, w, x, y) =
(indent ind;
print(Str.toString w ^ " = " ^
Str.toString x ^ " @ 0 @ " ^
Str.toString y ^ " is in X, by (2)\n"))
(* val text3 : int * str * str * str -> unit
print explanation based on rule (3) of X's definition at given indentation *)
fun text3(ind, w, x, y) =
(indent ind;
print(Str.toString w ^ " = 0 @ " ^
Str.toString x ^ " @ " ^
Str.toString y ^ " is in X, by (3)\n"))
(* val expl : int * str -> unit
if ind >= 0 and w is in Y, then expl(ind, w) prints an explanation
of why w is in X, indented ind spaces; in recursive calls, the size
of the str goes down *)
fun expl(ind, w) =
if Str.isEmpty w
then raise Fail "cannot happen"
else if isZero(hd w)
then let val t = tl w (* w = [zero] @ t, diff t = 2 *)
val (x, y) = splitPositive t (* t = x @ y *)
(* x, y are in Y, w = [zero] @ x @ y *)
in text3(ind, w, x, y); expl(ind + 2, x); expl(ind + 2, y)
end
else (* isOne(hd w) *)
let val t = tl w (* w = [one] @ t, diff t = 0 *)
in if Str.isEmpty t (* w = [one] *)
then text1 ind
else if isZero(hd t)
then let val y = tl t (* t = [zero] @ y, w = [one, zero] @ y *)
(* y is in Y *)
in text2(ind, w, [one], y); text1(ind + 2);
expl(ind + 2, y)
end
else (* isOne(hd t), w begins with [one, one] *)
raise Fail "cannot happen"
end
(* val explain : unit -> unit
explain() reads an str from the standard input; if the str is not
in Y, it prints an error message; otherwise, it prints an
explanation of why the str is in X *)
fun explain() =
let val w = Str.input ""
in if validStr w then expl(0, w) else () end
end;