(* ps2-explain.sml *)

(* validStrSilent w (silently) tests whether w is in Y *)

val validStrSilent = 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 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 shortestNegativePrefix 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)

(* longestPrefix : (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 longestPrefix f w returns (x, y), where x is
   the longest such prefix and y is such that x @ y = w *)

fun longestPrefix f (w : str) : str * str =
      let fun long(bs, n, lngstOpt, nil)             =
                if f n
                then (bs, nil)
                else (case lngstOpt of
                           NONE      => raise Fail "shouldn't happen"
                         | SOME long => long)
            | long(bs, n, lngstOpt, c_cs as c :: cs) =
                long(bs @ [c], n + diffSym c,
                     if f n then SOME(bs, c_cs) else lngstOpt,
                     cs)
      in long(nil, 0, NONE, w) end

(* val longestNonPositivePrefix : str -> str * str

   if w is an str of zeros and ones, then longestNonPositivePrefix w
   returns (x, y), where x is the longest prefix such that diff x <= 0
   and y is such that x @ y = w *)

val longestNonPositivePrefix = longestPrefix(fn n => n <= 0)

(* 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) = longestNonPositivePrefix w
      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 validStrSilent 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      = Str.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