%{
#include <string.h>
#include <stdlib.h>
#include "y.tab.h"

#define TPTP_STORE_SIZE 32768
/* Compile with -DP_VERBOSE=2 to list tokens as they are seen. */
#ifndef P_VERBOSE
#  define P_VERBOSE 0
#  endif
int verbose2 = P_VERBOSE;
extern int tptp_store_size;
extern char* tptp_lval[];
int tptp_store_size = TPTP_STORE_SIZE;
/* If tptp_prev_tok == PERIOD, you are outside any sentence.*/
#ifndef PERIOD
#  define PERIOD 46
#  endif
int tptp_prev_tok = PERIOD;
int tptp_next_store = 0;
char* tptp_lval[TPTP_STORE_SIZE];
void tptp_print_tok(char* lval);
int tptp_update_lval(char* lval);
int tptp_update_lval(char* lval)
  { int next = tptp_next_store;
    free(tptp_lval[tptp_next_store]);
    tptp_lval[tptp_next_store] = strdup(lval);
    tptp_next_store = (tptp_next_store+1)%TPTP_STORE_SIZE;
    if (verbose2==2) tptp_print_tok(lval);
    return next; }

void tptp_print_tok(char* lval)
  { printf("%3d:%s;\n", tptp_prev_tok, lval);
    return; }

/* %Start: INITIAL begin sentence, B before formula. No others. */
%}
comment                 {comment_line}|{comment_block}
comment_line            [%]{printable_char}*
comment_block           [/][*]{not_star_slash}[*][*]*[/]
not_star_slash          ([^*]*[*][*]*[^/*])*[^*]*
single_quoted           [']([^\\']|[\\][']|[\\][\\])*[']
distinct_object         ["]([^\\"]|[\\]["]|[\\][\\])*["]
dollar_word             [$]{lower_word}
dollar_dollar_word      {dollar_dollar}{lower_word}
upper_word              {upper_alpha}{alpha_numeric}*
lower_word              {lower_alpha}{alpha_numeric}*
plus                    [+]
real                    ({signed_decimal}|{unsigned_decimal}){fraction_decimal}
signed_integer          {sign}{unsigned_integer}
unsigned_integer        {unsigned_decimal}
signed_decimal          {sign}{unsigned_decimal}
sign                    [+-]
unsigned_decimal        ([0]|{non_zero_numeric}{numeric}*)
fraction_decimal        [.]{numeric}{numeric}*
numeric                 [0-9]
non_zero_numeric        [1-9]
lower_alpha             [a-z]
upper_alpha             [A-Z]
alpha_numeric           ({lower_alpha}|{upper_alpha}|{numeric}|[_])
dollar_dollar           [$][$]
printable_char          .
vline                   [|]
star                    [*]
%Start B FF SQ1 SQ2 Q1 Q2
%%

"&"    {tptp_prev_tok=AMPERSAND; yylval.ival = tptp_update_lval(yytext); return(AMPERSAND);}
"@"    {tptp_prev_tok=AT_SIGN; yylval.ival = tptp_update_lval(yytext); return(AT_SIGN);}
"^"    {tptp_prev_tok=CARET; yylval.ival = tptp_update_lval(yytext); return(CARET);}
":"    {tptp_prev_tok=COLON; yylval.ival = tptp_update_lval(yytext); return(COLON);}
":="    {tptp_prev_tok=COLON_EQUALS; yylval.ival = tptp_update_lval(yytext); return(COLON_EQUALS);}
","    {tptp_prev_tok=COMMA; yylval.ival = tptp_update_lval(yytext); return(COMMA);}
"="    {tptp_prev_tok=EQUALS; yylval.ival = tptp_update_lval(yytext); return(EQUALS);}
"=>"    {tptp_prev_tok=EQUALS_GREATER; yylval.ival = tptp_update_lval(yytext); return(EQUALS_GREATER);}
"!"    {tptp_prev_tok=EXCLAMATION; yylval.ival = tptp_update_lval(yytext); return(EXCLAMATION);}
"!="    {tptp_prev_tok=EXCLAMATION_EQUALS; yylval.ival = tptp_update_lval(yytext); return(EXCLAMATION_EQUALS);}
">"    {tptp_prev_tok=GREATER; yylval.ival = tptp_update_lval(yytext); return(GREATER);}
"["    {tptp_prev_tok=LBRKT; yylval.ival = tptp_update_lval(yytext); return(LBRKT);}
"<="    {tptp_prev_tok=LESS_EQUALS; yylval.ival = tptp_update_lval(yytext); return(LESS_EQUALS);}
"<=>"    {tptp_prev_tok=LESS_EQUALS_GREATER; yylval.ival = tptp_update_lval(yytext); return(LESS_EQUALS_GREATER);}
"<~>"    {tptp_prev_tok=LESS_TILDE_GREATER; yylval.ival = tptp_update_lval(yytext); return(LESS_TILDE_GREATER);}
"("    {tptp_prev_tok=LPAREN; yylval.ival = tptp_update_lval(yytext); return(LPAREN);}
"->"    {tptp_prev_tok=MINUS_GREATER; yylval.ival = tptp_update_lval(yytext); return(MINUS_GREATER);}
"."    {BEGIN INITIAL; tptp_prev_tok=PERIOD; yylval.ival = tptp_update_lval(yytext); return(PERIOD);}
"?"    {tptp_prev_tok=QUESTION; yylval.ival = tptp_update_lval(yytext); return(QUESTION);}
"]"    {tptp_prev_tok=RBRKT; yylval.ival = tptp_update_lval(yytext); return(RBRKT);}
")"    {tptp_prev_tok=RPAREN; yylval.ival = tptp_update_lval(yytext); return(RPAREN);}
"*"    {tptp_prev_tok=STAR; yylval.ival = tptp_update_lval(yytext); return(STAR);}
"~"    {tptp_prev_tok=TILDE; yylval.ival = tptp_update_lval(yytext); return(TILDE);}
"~&"    {tptp_prev_tok=TILDE_AMPERSAND; yylval.ival = tptp_update_lval(yytext); return(TILDE_AMPERSAND);}
"~|"    {tptp_prev_tok=TILDE_VLINE; yylval.ival = tptp_update_lval(yytext); return(TILDE_VLINE);}
"|"    {tptp_prev_tok=VLINE; yylval.ival = tptp_update_lval(yytext); return(VLINE);}
"$false"    {tptp_prev_tok=_DLR_false; yylval.ival = tptp_update_lval(yytext); return(_DLR_false);}
"$i"    {tptp_prev_tok=_DLR_i; yylval.ival = tptp_update_lval(yytext); return(_DLR_i);}
"$iType"    {tptp_prev_tok=_DLR_iType; yylval.ival = tptp_update_lval(yytext); return(_DLR_iType);}
"$o"    {tptp_prev_tok=_DLR_o; yylval.ival = tptp_update_lval(yytext); return(_DLR_o);}
"$oType"    {tptp_prev_tok=_DLR_oType; yylval.ival = tptp_update_lval(yytext); return(_DLR_oType);}
"$t"    {tptp_prev_tok=_DLR_t; yylval.ival = tptp_update_lval(yytext); return(_DLR_t);}
"$tType"    {tptp_prev_tok=_DLR_tType; yylval.ival = tptp_update_lval(yytext); return(_DLR_tType);}
"$true"    {tptp_prev_tok=_DLR_true; yylval.ival = tptp_update_lval(yytext); return(_DLR_true);}
<INITIAL>"cnf"    {BEGIN B; tptp_prev_tok=_LIT_cnf; yylval.ival = tptp_update_lval(yytext); return(_LIT_cnf);}
<INITIAL>"fof"    {BEGIN B; tptp_prev_tok=_LIT_fof; yylval.ival = tptp_update_lval(yytext); return(_LIT_fof);}
<INITIAL>"include"    {BEGIN B; tptp_prev_tok=_LIT_include; yylval.ival = tptp_update_lval(yytext); return(_LIT_include);}
"lambda"    {tptp_prev_tok=_LIT_lambda; yylval.ival = tptp_update_lval(yytext); return(_LIT_lambda);}
"letrec"    {tptp_prev_tok=_LIT_letrec; yylval.ival = tptp_update_lval(yytext); return(_LIT_letrec);}
<INITIAL>"tff"    {BEGIN B; tptp_prev_tok=_LIT_tff; yylval.ival = tptp_update_lval(yytext); return(_LIT_tff);}
<INITIAL>"thf"    {BEGIN B; tptp_prev_tok=_LIT_thf; yylval.ival = tptp_update_lval(yytext); return(_LIT_thf);}
{single_quoted}      {tptp_prev_tok=single_quoted; yylval.ival = tptp_update_lval(yytext); return(single_quoted);}
{distinct_object}      {tptp_prev_tok=distinct_object; yylval.ival = tptp_update_lval(yytext); return(distinct_object);}
{dollar_word}      {tptp_prev_tok=dollar_word; yylval.ival = tptp_update_lval(yytext); return(dollar_word);}
{dollar_dollar_word}      {tptp_prev_tok=dollar_dollar_word; yylval.ival = tptp_update_lval(yytext); return(dollar_dollar_word);}
{upper_word}      {tptp_prev_tok=upper_word; yylval.ival = tptp_update_lval(yytext); return(upper_word);}
{lower_word}      {tptp_prev_tok=lower_word; yylval.ival = tptp_update_lval(yytext); return(lower_word);}
{plus}      {tptp_prev_tok=plus; yylval.ival = tptp_update_lval(yytext); return(plus);}
{real}      {tptp_prev_tok=real; yylval.ival = tptp_update_lval(yytext); return(real);}
{signed_integer}      {tptp_prev_tok=signed_integer; yylval.ival = tptp_update_lval(yytext); return(signed_integer);}
{unsigned_integer}      {tptp_prev_tok=unsigned_integer; yylval.ival = tptp_update_lval(yytext); return(unsigned_integer);}
{comment}    tptp_update_lval(yytext);
[ \t\n]    ;
[\000-\040]|[\177]    ;
[\041-\176]    return(unrecognized);
%%