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