#include "hnat_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 ()
{
  udatum m, n;

  (void) printf("m <- 0\n");
  m= zero();
  (void) printf("m := %s\n", ud_draw(nat, m));
  ud_free(nat, m);

  (void) printf("m <- 1\n");
  m= one();
  (void) printf("m := %s\n", ud_draw(nat, m));
  ud_free(nat, m);

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

  (void) printf("n <- succ(succ(succ(m)))\n");
  n= succ(succ(succ(ud_copy(nat, m))));
  (void) printf("n := %s\n", ud_draw(nat, n));

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

  ud_free(nat, m);
  ud_free(nat, 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;
}
