/***** tl_spin: tl_lex.c *****/

/* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A.               */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
/* Send bug-reports and/or questions to: [email protected]    */

#include <stdlib.h>
#include <ctype.h>
#include "tl.h"

static Symbol   *symtab[Nhash+1];
static int      tl_lex(void);

extern YYSTYPE  tl_yylval;
extern char     yytext[];

#define Token(y)        tl_yylval = tl_nn(y,ZN,ZN); return y

static void
getword(int first, int (*tst)(int))
{       int i=0; char c;

       yytext[i++]= (char ) first;
       while (tst(c = tl_Getchar()))
               yytext[i++] = c;
       yytext[i] = '\0';
       tl_UnGetchar();
}

static int
follow(int tok, int ifyes, int ifno)
{       int c;
       char buf[32];
       extern int tl_yychar;

       if ((c = tl_Getchar()) == tok)
               return ifyes;
       tl_UnGetchar();
       tl_yychar = c;
       sprintf(buf, "expected '%c'", tok);
       tl_yyerror(buf);        /* no return from here */
       return ifno;
}

int
tl_yylex(void)
{       int c = tl_lex();
#if 0
       printf("c = %d\n", c);
#endif
       return c;
}

static int
tl_lex(void)
{       int c;

       do {
               c = tl_Getchar();
               yytext[0] = (char ) c;
               yytext[1] = '\0';

               if (c <= 0)
               {       Token(';');
               }

       } while (c == ' ');     /* '\t' is removed in tl_main.c */

       if (islower(c))
       {       getword(c, isalnum_);
               if (strcmp("true", yytext) == 0)
               {       Token(TRUE);
               }
               if (strcmp("false", yytext) == 0)
               {       Token(FALSE);
               }
               tl_yylval = tl_nn(PREDICATE,ZN,ZN);
               tl_yylval->sym = tl_lookup(yytext);
               return PREDICATE;
       }
       if (c == '<')
       {       c = tl_Getchar();
               if (c == '>')
               {       Token(EVENTUALLY);
               }
               if (c != '-')
               {       tl_UnGetchar();
                       tl_yyerror("expected '<>' or '<->'");
               }
               c = tl_Getchar();
               if (c == '>')
               {       Token(EQUIV);
               }
               tl_UnGetchar();
               tl_yyerror("expected '<->'");
       }

       switch (c) {
       case '/' : c = follow('\\', AND, '/'); break;
       case '\\': c = follow('/', OR, '\\'); break;
       case '&' : c = follow('&', AND, '&'); break;
       case '|' : c = follow('|', OR, '|'); break;
       case '[' : c = follow(']', ALWAYS, '['); break;
       case '-' : c = follow('>', IMPLIES, '-'); break;
       case '!' : c = NOT; break;
       case 'U' : c = U_OPER; break;
       case 'V' : c = V_OPER; break;
#ifdef NXT
       case 'X' : c = NEXT; break;
#endif
       default  : break;
       }
       Token(c);
}

Symbol *
tl_lookup(char *s)
{       Symbol *sp;
       int h = hash(s);

       for (sp = symtab[h]; sp; sp = sp->next)
               if (strcmp(sp->name, s) == 0)
                       return sp;

       sp = (Symbol *) tl_emalloc(sizeof(Symbol));
       sp->name = (char *) tl_emalloc(strlen(s) + 1);
       strcpy(sp->name, s);
       sp->next = symtab[h];
       symtab[h] = sp;

       return sp;
}

Symbol *
getsym(Symbol *s)
{       Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));

       n->name = s->name;
       return n;
}