(* ps2-framework.sml

   Framework for Problem 2 of Problem Set 2 *)

(********************************* Exception **********************************)

exception Error

(***************************** Symbols and Strings ****************************)

(* val zero : sym
   val one  : sym

   The symbols 0 and 1 *)

val zero = Sym.fromString "0"
val one  = Sym.fromString "1"

(* val isZero : sym -> bool

   Tests whether a symbol is 0 *)

fun isZero a = Sym.equal(a, zero)

(* val isOne : sym -> bool

   Tests whether a symbol is 1 *)

fun isOne a = Sym.equal(a, one)

(* val diffSym : sym -> int

   Computes the diff of an individual symbol, raising Error if the
   symbol isn't a zero or one *)

fun diffSym a =
      if isZero a
        then ~2
      else if isOne a
        then 1
      else raise Error

(* val diff : str -> int

   Computes the diff of an str, raising Error if one or more of the
   str's symbols isn't a zero or one *)

fun diff (nil : str) = 0
  | diff (b :: bs)   = diffSym b + diff bs

(* val validStr : bool -> str -> bool

   If w is in Y, then validStr verbose w silently returns true;
   otherwise, validStr false w silently returns false, and validStr
   true w prints an error message explaining why w is not in Y, and
   then returns false *)

fun validStr verbose w =
      let fun judge nil       = true
            | judge (v :: vs) =
                let val m = diff v
                in if m >= 0
                   then judge vs
                   else (if verbose
                         then (print "str has prefix ";
                               print(Str.toString v);
                               print " with negative diff: ";
                               print (Int.toString m); print "\n")
                         else ();
                         false)
                end
      in judge(Set.toList(StrSet.prefixes w)) end
        handle Error =>
                 (if verbose
                  then print "str has symbol other than 0/1\n"
                  else ();
                  false)

(******************************** Explanations ********************************)

(* Explanation of why an str is in X *)

datatype expl =
           Rule1                 (* % *)
         | Rule2                 (* 1 *)
         | Rule3 of expl * expl  (* 1x1y0 *)
         | Rule4 of expl * expl  (* xy *)

(* val strExplained : expl -> str

   Returns the str explained to be in X by an explanation *)

fun strExplained Rule1 : str           = nil
  | strExplained Rule2                 = [one]
  | strExplained (Rule3(expl1, expl2)) =
      [one] @ strExplained expl1 @ [one] @ strExplained expl2 @ [zero]
  | strExplained (Rule4(expl1, expl2)) =
      strExplained expl1 @ strExplained expl2

(* val printExplanation : expl -> unit

   Prints an explanation in an understandable form *)

local
  fun indent ind = print(StringCvt.padLeft #" " ind "")

  fun prExpl(ind, Rule1)               =
        (indent ind; print "% is in X, by rule (1)\n")
    | prExpl(ind, Rule2)               =
        (indent ind; print "1 is in X, by rule (2)\n")
    | prExpl(ind, Rule3(expl1, expl2)) =
        let val x1 = strExplained expl1
            val x2 = strExplained expl2
            val w  = strExplained(Rule3(expl1, expl2))
        in indent ind;
           print
           (Str.toString w ^ " = 1 @ " ^ Str.toString x1 ^ " @ 1 @ " ^
            Str.toString x2 ^ " @ 0 is in X, by rule (3)\n");
           prExpl(ind + 2, expl1);
           prExpl(ind + 2, expl2)
        end
    | prExpl(ind, Rule4(expl1, expl2)) =
        let val x1 = strExplained expl1
            val x2 = strExplained expl2
            val w  = strExplained(Rule4(expl1, expl2))
        in indent ind;
           print
           (Str.toString w ^ " = " ^ Str.toString x1 ^ " @ " ^
            Str.toString x2 ^ " is in X, by rule (4)\n");
           prExpl(ind + 2, expl1);
           prExpl(ind + 2, expl2)
        end
in
  fun printExplanation expl = prExpl(0, expl)
end

(* val test : (str -> expl) -> str -> unit

   If w is not in Y, then

     test explain w

   prints an explanation of why w is not in Y. Otherwise, it calls
   explain on w. If the resulting explanation, expl, explains why
   another string is in X, then it notes that discrepancy. Otherwise,
   it prints the explanation in an understandable form.

   (If explain raises an exception, then test reports that this
   occurred; if explain runs forever, then test runs forever *)

fun test explain w =
      if validStr true w
      then let val expl = explain w
               val w'   = strExplained expl
           in if Str.equal(w', w)
              then printExplanation expl
              else (print "explanation is for different str: ";
                    print(Str.toString w'); print "\n")
           end
             handle _ => print "explanation function raised exception\n"
      else ()