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