(* ps2-explain.sml *)
(* validStr' w (silently) tests whether w is in Y *)
val validStr' = validStr false
(* 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 : str) : str * str =
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 shortestNegativePrefix : str -> str * str
if w is an str of zeros and ones, and there is a prefix x of w
such that diff x <= ~1, then shortestNegativePref w returns (x, y),
where x is the shortest such prefix and y is such that x @ y = w *)
val shortestNegativePrefix = shortestPrefix(fn n => n <= ~1)
(* val shortestPositiveSuffix : str -> str * str
if w is an str of zeros and ones, and there is a suffix y of w
such that diff y >= 1, then shortestPositiveSuffix w returns (x, y),
where y is the shortest such suffix and x is such that x @ y = w *)
fun shortestPositiveSuffix (w : str) : str * str =
let val (x, y) = shortestPrefix (fn n => n >= 1) (rev w)
in (rev y, rev x) end
(* val splitPositiveValid : str -> str * str
if w is an str of zeros and ones such that diff w >= 1 and w is in
Y, then splitPositiveValid w returns a pair (x, y) such that w = x @
[one] @ y and x, y are in Y *)
fun splitPositiveValid (w : str) : str * str =
let val (x, z) = shortestPositiveSuffix w
(* z begins with one *)
in (x, tl z) end
(* val explain : str -> expl
if w is in Y, then strExplained(explain w) = w *)
fun explain (w : str) =
if null w
then Rule1
else if isZero(hd w)
then raise Fail "shouldn't happen"
else (* isOne(hd w) *)
let val s = tl w (* w = [one] @ s *)
in if validStr' s (* if s is in Y *)
then Rule4(Rule2, explain s)
else (* w is not in Y *)
let val (z, t) = shortestNegativePrefix s
(* s = z @ t *)
val u = ListAux.allButLast z
(* z = u @ [zero], diff u = 1, u is in Y
w = [one] @ u @ [zero] @ t, t is in Y *)
val (x, y) = splitPositiveValid u
(* u = x @ [one] @ y, x is in Y, y is in Y, t is in Y
w = ([one] @ x @ [one] @ y @ [zero]) @ t *)
in Rule4(Rule3(explain x, explain y), explain t) end
end