#define KTYPE_IMP

#include "ldc.hh"

tSORT_TBL sort_tbl= {  { 0, FALSE, NULL, NULL, NULL, NULL, NULL },
  { 1, FALSE, "side", NULL, NULL, NULL, NULL },
  { 2, FALSE, "nat14", NULL, NULL, NULL, NULL }
};

unsigned sort_tbl_size= 3;

static int _arg_buf[]= {  2, 2, 2, 2
};

kdatum _eval_opn(_oid, _arg)
int _oid;
kdatum _arg[];
{
  return NULL;
}

tOPN_TBL opn_tbl= {  { 0, 0, 0, NULL, FALSE, FALSE, NULL, NULL },
  { 1, 1, 0, NULL, FALSE, FALSE, "left", (kdatum(*)())left },
  { 2, 1, 0, NULL, FALSE, FALSE, "right", (kdatum(*)())right },
  { 3, 2, 0, NULL, FALSE, FALSE, "n1", (kdatum(*)())n1 },
  { 4, 2, 0, NULL, FALSE, FALSE, "n2", (kdatum(*)())n2 },
  { 5, 2, 0, NULL, FALSE, FALSE, "n3", (kdatum(*)())n3 },
  { 6, 2, 0, NULL, FALSE, FALSE, "n4", (kdatum(*)())n4 },
  { 7, 2, 1, _arg_buf, FALSE, FALSE, "succ", (kdatum(*)())succ },
  { 8, 2, 1, _arg_buf + 1, FALSE, FALSE, "pred", (kdatum(*)())pred },
  { 9, 2, 2, _arg_buf + 2, FALSE, FALSE, "plus", (kdatum(*)())plus }
};

unsigned opn_tbl_size= 10;

/* left: -> side */
kdatum left()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= kd_alloc();
    _v->opn= 1;
    (void) kd_const(_v);
  }
  return _v;
}

/* right: -> side */
kdatum right()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= kd_alloc();
    _v->opn= 2;
    (void) kd_const(_v);
  }
  return _v;
}

/* _plus_: nat14, nat14 -> nat14 */
kdatum plus(_p1, _p2)
kdatum _p1;
kdatum _p2;
{  kdatum _v= NULL;
  klink _s1, _s2;

  switch (_p2->opn)
  {  case 7: /* succ */
      _v= succ(plus(kd_copy(_p1), kd_copy(_p2->lnk->arg)));
      break;
    case 3: /* n1 */
      _v= succ(kd_copy(_p1));
      break;
  }

  if (_v == NULL)
  {  put_error("non-constructor failure: (unable to build term of external sort)\n");
    put_error("                   name: plus (see line 74 of file \"phil3.lot\")\n");
    put_error("                  arg 1: %s\n", kd_draw(_p1));
    put_error("                  arg 2: %s\n", kd_draw(_p2));
    exit(1);
  }
  else
  {  kd_free(_p1);
    kd_free(_p2);
  }

  return _v;
}

/* succ: nat14 -> nat14 */
kdatum succ(_p1)
kdatum _p1;
{  kdatum _v= NULL;
  klink _s1;

  switch (_p1->opn)
  {  case 7: /* succ */
      switch (_p1->lnk->arg->opn)
      {  case 7: /* succ */
          switch (_p1->lnk->arg->lnk->arg->opn)
          {  case 7: /* succ */
              switch (_p1->lnk->arg->lnk->arg->lnk->arg->opn)
              {  case 3: /* n1 */
                  _v= n1();
                  break;
                case 7: /* succ */
                  _v= succ(kd_copy(_p1->lnk->arg->lnk->arg->lnk->arg->lnk->arg));
                  break;
              }
              break;
          }
          break;
      }
      break;
  }

  if (_v == NULL)
  {  _v= kd_alloc();
    _v->opn= 7;

    _s1= kd_link();
    _s1->arg= (kdatum)_p1;
    _v->lnk= _s1;
  }
  else
  {  kd_free(_p1);
  }

  return _v;
}

/* pred: nat14 -> nat14 */
kdatum pred(_p1)
kdatum _p1;
{  kdatum _v;

  _v= succ(succ(succ(kd_copy(_p1))));

  kd_free(_p1);

  return _v;
}

/* n1: -> nat14 */
kdatum n1()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= kd_alloc();
    _v->opn= 3;
    (void) kd_const(_v);
  }
  return _v;
}

/* n2: -> nat14 */
kdatum n2()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= succ(n1());
    (void) kd_const(_v);
  }
  return _v;
}

/* n3: -> nat14 */
kdatum n3()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= succ(succ(n1()));
    (void) kd_const(_v);
  }
  return _v;
}

/* n4: -> nat14 */
kdatum n4()
{  static kdatum _v= NULL;

  if (_v == NULL)
  {  _v= succ(succ(succ(n1())));
    (void) kd_const(_v);
  }
  return _v;
}

void ldcinit() {}
