(* ps2-explain.sml
Solution to Problem 2 of Problem Set 2 *)
(* val shortestPref : (int -> bool) -> str -> str * str
If w is an str of zero's and one's, and there is a prefix x of w
such that f(diff x), then shortestPref f w returns (x, y), where x
is the shortest such prefix and y is such that x @ y = w *)
fun shortestPref f (w : str) : str * str =
let fun short(bs, n, nil) =
if f n then (bs, nil) else raise Fail "shouldn't happen"
| short(bs, n, c :: cs) =
if f n
then (bs, c :: cs)
else short(bs @ [c], n + diffSym c, cs)
in short(nil, 0, w) end
(* val shortestSuff : (int -> bool) -> str -> str * str
If w is an str of zero's and one's, and there is a suffix x of w
such that f(diff x), then shortestSuff f w returns (x, y), where x
is the shortest such suffix and y is such that y @ x = w *)
fun shortestSuff f (w : str) : str * str =
let val (x, y) = shortestPref f (rev w)
in (rev x, rev y) end
(* val shortestNegSuff : str -> str * str
If w is an str of zero's and one's, and there is a suffix x of w
such that diff x <= ~1, then shortestNegSuff w returns (x, y),
where x is the shortest such prefix and y is such that y @ x = w *)
val shortestNegSuff = shortestSuff(fn n => n <= ~1)
(* val explain : str -> expl
If w is in Y, then explain w returns an explanation expl such
that Str.equal(strExplained expl, w) *)
fun explain (w : str) =
if null w
then Rule1
else (* w ends with one *)
let val t = Str.allButLast w
(* w = t @ [one], diff t = ~1 *)
val (u, x) = shortestNegSuff t
(* t = x @ u, u begins with zero, diff u = ~1, all proper
suffixes of u have non-negative diffs, x is in Y *)
val y = tl u
(* w = x @ [zero] @ y @ [one], x, y are in Y *)
in Rule2(explain x, explain y) end