/***************************************************************************

  This is the grammar for the wff accepted by this parser, 'a' is an atom
  constant or variable, 'e' is the empty string.  The operators xor and
  then are also accepted having the same precedence as or and if.

  Start -> term5 $
  term5 -> term4 more4
  more4 -> iff term4 more4 | e
  term4 -> term3 more3
  more3 -> if term3 more3 | e
  term3 -> term2 more2
  more2 -> or term2 more2 | e
  term2 -> term1 more1
  more1 -> and term1 more1 | e
  term1 -> not term1 | some atom term5 | all atom term5 | (term5) | lit eq
  eq -> = lit | e
  lit -> atom | atom(lit arg) | atom()
  arg -> , lit arg | e

It calls the function GetToken to get the input.

***************************************************************************/

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include "glob.h"

static int next = 0;
static int
  tand,tand2,tor,tor2,txor,txor2,tif,tif2,tiff,tiff2,
  lpar,rpar,tnot,tnot2,teq,teq2,tall,tall2,tsome,tsome2,
  tthen,tthen2,comma,semi;

int InitParser()
{
  tand = AddSymbol("and");
  tand2 = AddSymbol("&");
  tor = AddSymbol("or");
  tor2 = AddSymbol("|");
  txor = AddSymbol("xor");
  txor2 = AddSymbol("^");
  tif = AddSymbol("if");
  tif2 = AddSymbol("<");
  tthen = AddSymbol("then");
  tthen2 = AddSymbol(">");
  tiff = AddSymbol("iff");
  tiff2 = AddSymbol("iff");
  lpar = AddSymbol("(");
  rpar = AddSymbol(")");
  tnot = AddSymbol("not");
  tnot2 = AddSymbol("-");
  teq = AddSymbol("=");
  teq2 = AddSymbol("=");
  tall = AddSymbol("all");
  tall2 = AddSymbol("every");
  tsome = AddSymbol("some");
  tsome2 = AddSymbol("exist");
  comma = AddSymbol(",");
  semi = AddSymbol(";");
  return 0;
}

#define NONSYM "(),;"

static int checksymbol(int x)    /* check if x is a valid atom */
{
  char *s;

  s = GetSymbol(x);
  if (strchr(NONSYM,*s) != NULL) {
    eprintf("A symbolic atom expected at '%s'",s,0,0);
    return 0;
  }
  return 1;
}

static lox *term5();

static lox *literal()
{
  lox *t,*u,*v;

  t = NewLox(TERM);
  t->id = next;
  checksymbol(next);
  u = NULL;

  next = GetToken();
  if (next == lpar) {
    next = GetToken();
    if (next == rpar) {
      next = GetToken();
      return t;
    }
    while (1) {
      v = literal();
      if (u == NULL) {
        u = v;  t->a = v;    /* first child */
      }
      else {
        u->b = v; u=v;       /* next sibling */
      }
      if (next == comma) next = GetToken();
      else break;
    }
    if (next != rpar) {
      eprintf("Right parenthesis expected at '%s'",GetSymbol(next),0,0);
      return t;
    }
    next = GetToken();
  }
  return t;
}

static lox *term1()
{
  lox *t,*u;

  if (next==tall || next==tall2) {
    t = NewLox(ALL);
    next = GetToken();
    u = NewLox(TERM);
    u->id = next;
    checksymbol(next);
    next = GetToken();
    t->a = u;
    t->b = term5();
  } else
  if (next==tsome || next==tsome2) {
    t = NewLox(SOME);
    next = GetToken();
    u = NewLox(TERM);
    u->id = next;
    checksymbol(next);
    next = GetToken();
    t->a = u;
    t->b = term5();
  } else
  if (next==tnot || next==tnot2) {
    t = NewLox(NOT);
    next = GetToken();
    t->a = term1();
  } else
  if (next==lpar) {
    next = GetToken();
    t = term5();
    if (next == rpar) next = GetToken();
    else
      eprintf("Right parenthesis expected at '%s'",GetSymbol(next),0,0);
  }
  else {
    t = literal();
    if (next == teq || next == teq2) {
      u = NewLox(TERM);
      u->id = teq;
      next = GetToken();
      u->a = t;
      t->b = literal();     /* jdh */
      t = u;
    }
  }
  return t;
}

static lox *term2()
{
  lox *t,*u;

  t = term1();
  while (next==tand || next==tand2) {
    next = GetToken();
    u = NewLox(AND);
    u->a = t;
    u->b = term1();
    t = u;
  }
  return t;
}

static lox *term3()
{
  lox *t,*u;

  t = term2();
  while (1) {
    if (next==tor || next==tor2) {
      next = GetToken();
      u = NewLox(OR);
      u->a = t;
      u->b = term2();
      t = u;
    } else
    if (next==txor || next==txor2) {
      next = GetToken();
      u = NewLox(XOR);
      u->a = t;
      u->b = term2();
      t = u;
    }
    else break;
  }
  return t;
}

static lox *term4()
{
  lox *t,*u;

  t = term3();
  while (1) {
    if (next==tif || next==tif2) {
      next = GetToken();
      u = NewLox(IF);
      u->a = t;
      u->b = term3();
      t = u;
    } else
    if (next==tthen || next==tthen2) {
      next = GetToken();
      u = NewLox(IF);
      u->b = t;
      u->a = term3();
      t = u;
    }
    else break;
  }
  return t;
}

static lox *term5()
{
  lox *t,*u;

  t = term4();
  while (next==tiff || next==tiff2) {
    next = GetToken();
    u = NewLox(IFF);
    u->a = t;
    u->b = term4();
    t = u;
  }
  return t;
}

lox *ParseLox()
{
  lox *t;
  next = GetToken();
  t = term5();
  if (next != semi) eprintf("Unknown operator '%s'",GetSymbol(next),0,0);
  return t;
}

int PrintLox(lox *t)
{
  if (t==NULL) return printf("<NULL>");

  switch (t->type) {
  case SKOL:
    printf("$%d",t->id);
    if (t->vc) printf("_%d",t->vc);
    if (t->a != NULL) {
      printf("(");
      PrintLox(t->a);
      printf(")");
    }
    if (t->b != NULL) {
      printf(",");
      PrintLox(t->b);   /* tail recursion */
    }
    break;
  case VAR:
    printf("%s_%d",GetSymbol(t->id),t->vc);
    if (t->a != NULL) {
      printf(" [");
  /*  PrintLox(t->a);   */
      printf("]");
    }
    if (t->b != NULL) {
      printf(",");
      PrintLox(t->b);   /* tail recursion */
    }
    break;
  case TERM:
    printf("%s",GetSymbol(t->id));
    if (t->vc) printf("_%d",t->vc);
    if (t->a != NULL) {
      printf("(");
      PrintLox(t->a);
      printf(")");
    }
    if (t->b != NULL) {
      printf(",");
      PrintLox(t->b);   /* tail recursion */
    }
    break;
  case ALL:
    printf("(all ");
    PrintLox(t->a);
    printf(" ");
    PrintLox(t->b);
    printf(")");
    break;
  case SOME:
    printf("(some ");
    PrintLox(t->a);
    printf(" ");
    PrintLox(t->b);
    printf(")");
    break;
  case NOT:
    printf("not ");
    PrintLox(t->a);
    break;
  case AND:
    printf("(");
    PrintLox(t->a);
    printf(" and ");
    PrintLox(t->b);
    printf(")");
    break;
  case OR:
    printf("(");
    PrintLox(t->a);
    printf(" or ");
    PrintLox(t->b);
    printf(")");
    break;
  case XOR:
    printf("(");
    PrintLox(t->a);
    printf(" xor ");
    PrintLox(t->b);
    printf(")");
    break;
  case IF:
    printf("(");
    printf("if ");
    PrintLox(t->b);
    printf(" then ");
    PrintLox(t->a);
    printf(")");
    break;
  case IFF:
    printf("(");
    PrintLox(t->a);
    printf(" iff ");
    PrintLox(t->b);
    printf(")");
    break;
  default:
    printf("<type=%d>",t->type);
  }
  return 0;
}