(* 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 1
      else if isOne a
        then ~2
      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 : str -> bool

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

fun validStr w =
      let val n = diff w
      in if n = 0
         then true
         else (print "str has non-zero diff : "; print(Int.toString n);
               print "\n"; false)
      end
        handle Error =>
                 (print "str has symbol other than 0/1\n"; false)

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

(* Explanation of why a string is in X. *)

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

(* val strExplained : expl -> str

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

fun strExplained Rule1 : str           = nil
  | strExplained (Rule2(expl1, expl2)) =
      [zero] @ strExplained expl1 @ [zero] @ strExplained expl2 @ [one]
  | strExplained (Rule3(expl1, expl2)) =
      [zero] @ strExplained expl1 @ [one]  @ strExplained expl2 @ [zero]
  | strExplained (Rule4(expl1, expl2)) =
      [one] @ strExplained expl1 @ [zero] @ strExplained expl2 @ [zero]
  | strExplained (Rule5(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(expl1, expl2)) =
        rules2To4(ind, 2, zero, expl1, zero, expl2, one)
    | prExpl(ind, Rule3(expl1, expl2)) =
        rules2To4(ind, 3, zero, expl1, one, expl2, zero)
    | prExpl(ind, Rule4(expl1, expl2)) =
        rules2To4(ind, 4, one, expl1, zero, expl2, zero)
    | prExpl(ind, Rule5(expl1, expl2)) = rule5(ind, expl1, expl2)

  and rules2To4(ind, rul, sym1, expl1, sym2, expl2, sym3) =
        let val x1 = strExplained expl1
            val x2 = strExplained expl2
            val w  = [sym1] @ x1 @ [sym2] @ x2 @ [sym3]
        in indent ind;
           print
           (Str.toString w ^ " = " ^ Sym.toString sym1 ^ " @ " ^
            Str.toString x1 ^ " @ " ^ Sym.toString sym2 ^ " @ " ^
            Str.toString x2 ^ " @ " ^ Sym.toString sym3 ^
            " is in X, by rule (" ^ Int.toString rul ^ ")\n");
           prExpl(ind + 2, expl1); prExpl(ind + 2, expl2)
        end

  and rule5(ind, expl1, expl2) =
        let val x1 = strExplained expl1
            val x2 = strExplained expl2
            val w  = x1 @ x2
        in indent ind;
           print
           (Str.toString w ^ " = " ^ Str.toString x1 ^ " @ " ^
            Str.toString x2 ^ " is in X, by rule (5)\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 in Y, then

     test explain w

   prints in an understandable form the result of calling explain with
   w; otherwise, it explains why w is not in Y.  (If explain w raises
   an exception, then test reports that this occurred; if explain w
   runs forever, then test runs forever. *)

fun test explain w =
      if validStr w
      then let val expl = explain w
           in printExplanation expl end
             handle _ => print "explanation function raised exception\n"
      else ()