#include "anat_ldc.hh"
#include "test.h"

static void test_bool ()
{
  kdatum t, f;

  (void) printf("t <- true\n");
  t= true();
  (void) printf("t := %s\n", kd_draw(t));

  (void) printf("f <- false\n");
  f= false();
  (void) printf("f := %s\n", kd_draw(f));

  kd_free(t);
  kd_free(f);
}

static void test_nat ()
{
  kdatum m, n;

  (void) printf("m <- 0\n");
  m= zero();
  (void) printf("m := %s\n", kd_draw(m));
  kd_free(m);

  (void) printf("m <- 1\n");
  m= one();
  (void) printf("m := %s\n", kd_draw(m));
  kd_free(m);

  (void) printf("m <- succ(succ(0))\n");
  m= succ(succ(zero()));
  (void) printf("m := %s\n", kd_draw(m));

  (void) printf("n <- succ(succ(succ(m)))\n");
  n= succ(succ(succ(kd_copy(m))));
  (void) printf("n := %s\n", kd_draw(n));

  (void) printf("succ(m) := %s\n", kd_gdraw(succ(kd_copy(m)), 0x1));
  (void) printf("pred(m) := %s\n", kd_gdraw(pred(kd_copy(m)), 0x1));
  (void) printf("m + n := %s\n", kd_gdraw(plus(kd_copy(m),
					       kd_copy(n)), 0x1));
  (void) printf("m < n := %s\n", kd_gdraw(lt(kd_copy(m),
					     kd_copy(n)), 0x1));
  (void) printf("m == n := %s\n", kd_gdraw(eq(kd_copy(m),
					      kd_copy(n)), 0x1));
  (void) printf("m /= n := %s\n", kd_gdraw(ne(kd_copy(m),
					      kd_copy(n)), 0x1));

  kd_free(m);
  kd_free(n);
}

void test ()
{
  kaos.debug= TRUE;
  (void) printf("*** testing bool sort ***\n");
  test_bool();
  (void) printf("\n");
  (void) printf("*** testing nat sort ***\n");
  test_nat();
  kaos.debug= FALSE;
}
