(*  Auto-tester for wffstr and standardize functions.  *)
use "tester.sml";   (* common utility functions *)

(*  Avoid "unbound variable or constructor" errors.  *)
fun wffstr _ = raise Undefined;
fun standardize _ = raise Undefined;

(*  Load file.  *)
print "\n--> Loading file \"wff.sml\"\n";
use "../wff.sml" handle _ => ();

(***  The next function and bunch of values must be adjusted
      to use the student's constructor names for datatype wff.  ***)

(*  Since we can't rely on the student's version for testing...  *)
fun wff2string False = "F"
  | wff2string True = "T"
  | wff2string (Var v) = v
  | wff2string (NOT p) = "~" ^ wff2string p
  | wff2string (AND(p,q)) = "(" ^ wff2string p ^ " /\\ " ^ wff2string q ^ ")"
  | wff2string (OR(p,q)) = "(" ^ wff2string p ^ " \\/ " ^ wff2string q ^ ")"
  | wff2string (IMP(p,q)) = "(" ^ wff2string p ^ " => " ^ wff2string q ^ ")"
  | wff2string (IFF(p,q)) = "(" ^ wff2string p ^ " <=> " ^ wff2string q ^ ")"
  | wff2string (XOR(p,q)) = "(" ^ wff2string p ^ " <+> " ^ wff2string q ^ ")"

(*  Test cases: input and output for 'standardize'.  *)
val in01 = False;
val out01 = in01;
val in02 = True;
val out02 = in02;
val in03 = Var "p";
val out03 = in03;
val in04 = Var "blah";
val out04 = in04;
val in05 = NOT (Var "p");
val out05 = in05;
val in06 = AND (False, Var "p");
val out06 = in06;
val in07 = OR (Var "q", True);
val out07 = in07;
val in08 = IMP (Var "p", Var "q");
val out08 = in08;
val in09 = IFF (False, True);
val out09 = in09;
val in10 = XOR (Var "p", True);
val out10 = in10;
val in11 = NOT False;
val out11 = True;
val in12 = NOT True;
val out12 = False;
val in13 = NOT (NOT (Var "p"));
val out13 = Var "p";
val in14 = NOT (AND (Var "q", Var "p"));
val out14 = OR (NOT (Var "q"), NOT (Var "p"));
val in15 = NOT (OR (Var "p", Var "q"));
val out15 = AND (NOT (Var "p"), NOT (Var "q"));
val in16 = NOT (IMP (Var "q", Var "p"));
val out16 = AND (Var "q", NOT (Var "p"));
val in17 = NOT (IFF (Var "p", Var "q"));
val out17 = XOR (Var "p", Var "q");
val in18 = NOT (XOR (Var "q", Var "p"));
val out18 = IFF (Var "q", Var "p");
val in19 = NOT (IMP (AND (Var "p", Var "q"), IFF (Var "p", Var "q")));
val out19 = AND (AND (Var "p", Var "q"), XOR (Var "p", Var "q"));
val in20 = XOR (NOT (AND (True, NOT (Var "q"))),
    NOT (OR (IMP (NOT (Var "p"), False), XOR (Var "p", Var "q"))));
val out20 = XOR (OR (False, Var "q"),
    AND (AND (NOT (Var "p"), True), IFF (Var "p", Var "q")));

(***  Nothing below needs to be changed.  ***)

(*  Run test cases.  *)
( print "\n--> Beginning test cases for function 'wffstr'...\n";
  runtests total grade wffstr "wffstr"
    wff2string string2string (op =)
    [ (in01, wff2string in01, "(* constant *)", 0.1),
      (in02, wff2string in02, "(* constant *)", 0.1),
      (in03, wff2string in03, "(* variable with short name *)", 0.1),
      (in04, wff2string in04, "(* variable with long name *)", 0.1),
      (in05, wff2string in05, "(* simple negation *)", 0.2),
      (in06, wff2string in06, "(* simple conjunction *)", 0.2),
      (in07, wff2string in07, "(* simple disjunction *)", 0.2),
      (in08, wff2string in08, "(* simple implication *)", 0.2),
      (in09, wff2string in09, "(* simple bi-conditional *)", 0.2),
      (in10, wff2string in10, "(* simple exclusive-or *)", 0.2),
      (in19, wff2string in19, "(* complex wff *)", 0.2),
      (in20, wff2string in20, "(* complex wff *)", 0.2) ];
  print "\n--> Beginning test cases for function 'standardize'...\n";
  runtests total grade standardize "standardize"
    wff2string wff2string (op =)
    [ (in01, out01, "(* constant *)", 0.1),
      (in02, out02, "(* constant *)", 0.1),
      (in03, out03, "(* variable with short name *)", 0.1),
      (in04, out04, "(* variable with long name *)", 0.1),
      (in05, out05, "(* simple negation *)", 0.2),
      (in06, out06, "(* simple conjunction *)", 0.2),
      (in07, out07, "(* simple disjunction *)", 0.2),
      (in08, out08, "(* simple implication *)", 0.2),
      (in09, out09, "(* simple bi-conditional *)", 0.2),
      (in10, out10, "(* simple exclusive-or *)", 0.2),
      (in11, out11, "(* negation of constant *)", 0.2),
      (in12, out12, "(* negation of constant *)", 0.2),
      (in13, out13, "(* negation of simple negation *)", 0.2),
      (in14, out14, "(* negation of simple conjunction *)", 0.2),
      (in15, out15, "(* negation of simple disjunction *)", 0.2),
      (in16, out16, "(* negation of simple implication *)", 0.2),
      (in17, out17, "(* negation of simple bi-conditional *)", 0.2),
      (in18, out18, "(* negation of simple exclusive-or *)", 0.2),
      (in19, out19, "(* complex wff *)", 0.4),
      (in20, out20, "(* complex wff *)", 0.4) ] );

(*  Print total grade.  *)
print ("\n--> Grade = "
        ^ real2string (!grade) ^ " / " ^ real2string (!total) ^ "\n\n");

(*  Quit the SML interpreter.  *)
exit 0;