Tests for assignment 5, question 2 (unify)

use "hw5-q2.sml";

(* ------------------------------------------------------------
   Place this file in the same directory as hw5-q2.sml, and run "sml tests.sml".
   You must have a function called "occurs" (typ option ref -> typ -> bool) and
   a function called unify (typ * typ -> unit).
   If you don't have a function called "occurs", or if it's a different type,
   set the flag testOccurs below to false.
   ------------------------------------------------------------*)

Control.Print.printDepth := 100;

(* Define some type variables *)
val a1 : (typ option) ref = ref(NONE);
val a2 : (typ option) ref = ref(NONE);

val a3 : (typ option) ref = ref(NONE);
val a4 : (typ option) ref = ref(NONE);

val a5 : (typ option) ref = ref(NONE);
val a6 : (typ option) ref = ref(NONE);

val a7 : (typ option) ref = ref(NONE);
val a8 : (typ option) ref = ref(NONE);

val a9 : (typ option) ref = ref(NONE);
val a10 : (typ option) ref = ref(NONE);

val a11 : (typ option) ref = ref(NONE);
val a12 : (typ option) ref = ref(NONE);

(* Define some types *)
val t1 = Arrow(Product(TVar(a1), TVar(a1)), TVar(a2));
val t2 = Arrow(Product(Int, Int), TVar(a1));

val t3 = Arrow(Product(TVar(a3), TVar(a4)), TVar(a4));
val t4 = Arrow(Product(TVar(a4), TVar(a3)), TVar(a3));

val t5 = Arrow(Product(TVar(a5),TVar(a6)), TVar(a6));
val t6 = Arrow(TVar(a6), TVar(a5));

val t7 = Arrow(TVar a7, TVar a8);
val t8 = Arrow(TVar a8, TVar a7);

val t9 = Arrow(TVar a9, Int);
val t10 = TVar a10;

val t11 = Product(Arrow(TVar a11, Bool), Int);
val t12 = TVar a11;

(* Define the internal functions for testing *)
val num_pass = ref 0
val num_fail = ref 0

fun assert statement desc = let
      val test_num = Int.toString (!num_pass + !num_fail + 1);
      val _ = print ("Test " ^ test_num ^ " (" ^ desc ^ "): ")
    in
      if statement then
          (num_pass := !num_pass + 1;
          print "OK\n")
      else
          (num_fail := !num_fail + 1;
          print "FAIL ###############################\n")
    end

(* Define the callable testing functions *)
fun assertCanUnify (a, b) = (unify(a, b); assert (equal(a, b)) "assertCanUnify") handle UnifyError s => assert false "assertCanUnify"

fun assertNotUnified (a, b) = assert (not (equal (a, b))) "assertNotUnified"

fun assertCannotUnify (a, b) = (unify(a, b); assert false "assertCannotUnify") handle UnifyError s => assert true "assertCannotUnify"

fun printStats () = let
    val num_passed = Int.toString (!num_pass)
    val num_total = Int.toString (!num_pass + !num_fail)
    val _ = print ("*******************************************************************************\nPassed: " ^ num_passed ^ " out of " ^ num_total ^ "\n")
  in
      if !num_fail > 0 then
          print "Not all the tests passed. Check the failures above.\n"
      else
          ()
  end;

(* If your occurs function is not defined, or has a different signature, then
   comment out the section below!

   Beginning of section =====================================================*)
fun assertOccurs r thing = assert (occurs r thing) "assertOccurs";
fun assertNotOccurs r thing = assert (not (occurs r thing)) "assertNotOccurs";

assertOccurs a1 t1;
assertOccurs a2 t1;
assertNotOccurs a3 t1;

assertOccurs a1 t1;
assertNotOccurs a2 t2;

assertOccurs a3 t3;
assertOccurs a4 t3;

assertOccurs a3 t4;
assertOccurs a4 t4;
assertNotOccurs a1 t4;

(* End of section ===========================================================*)

assertNotUnified (t1, t2);
assertCanUnify (t1, t2);

assertNotUnified (t3, t4);
assertCanUnify (t3, t4);

assertNotUnified (t5, t6);
assertCannotUnify (t5, t6);

assertCanUnify (t7, t8);

assertCanUnify (t9, t10);

assertCannotUnify (t11, t12);

printStats();