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

#define TPTP_STORE_SIZE 32768
extern int tptp_ff;
extern int tptp_store_size;
extern char* tptp_lval[];
int tptp_ff = 0;
int tptp_store_size = TPTP_STORE_SIZE;
/* If tptp_prev_tok == PERIOD, you are outside any sentence.*/
int tptp_prev_tok = PERIOD;
int tptp_next_store = 0;
char* tptp_lval[TPTP_STORE_SIZE];
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;
    return next; }

/* %Start: INITIAL begin sentence, B before formula, FF formula finished. */
/* For now, FF is unreachable; tptp_ff always 0; example only. */
%}
digit                   [0-9]
lower                   [a-z]
upper                   [A-Z]
alphanum                ({lower}|{upper}|{digit}|[_])
any_char                (.|\n)
ddollar                 [$][$]
real                    ({signed_integer}|{unsigned_integer}){decimal_part}
signed_integer          [+-]{unsigned_integer}
unsigned_integer        {digit}{digit}*
decimal_part            [.]{digit}{digit}*
upper_word              {upper}{alphanum}*
lower_word              {lower}{alphanum}*
atomic_system_word      {ddollar}{lower}{alphanum}*
system_comment          {system_comment_one}|{system_comment_multi}
comment                 {comment_one}|{comment_multi}
system_comment_one      [%][ ]*{ddollar}.*
system_comment_multi    [/][*][ ]*{ddollar}([^*]*[*][*]*[^/*])*[^*]*[*][*]*[/]
comment_one             [%].*
comment_multi           [/][*]([^*]*[*][*]*[^/*])*[^*]*[*][*]*[/]
single_quoted           [']([^\\']|[\\][']|[\\][\\])*[']
distinct_object         ["]([^\\"]|[\\]["]|[\\][\\])*["]
%Start B FF SQ1 SQ2 Q1 Q2
%%

"&"    {tptp_prev_tok=AMPERSAND; yylval.ival = tptp_update_lval(yytext); return(AMPERSAND);}
<INITIAL>"cnf"    {BEGIN B; tptp_prev_tok=CNF; yylval.ival = tptp_update_lval(yytext); return(CNF);}
":"    {tptp_prev_tok=COLON; yylval.ival = tptp_update_lval(yytext); return(COLON);}
","    {if (tptp_ff){BEGIN FF;} 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=EXCLAMATION; yylval.ival = tptp_update_lval(yytext); return(EXCLAMATION);}
<INITIAL>"fof"    {BEGIN B; tptp_prev_tok=FOF; yylval.ival = tptp_update_lval(yytext); return(FOF);}
"<="    {tptp_prev_tok=IF; yylval.ival = tptp_update_lval(yytext); return(IF);}
"<=>"    {tptp_prev_tok=IFF; yylval.ival = tptp_update_lval(yytext); return(IFF);}
"=>"    {tptp_prev_tok=IMPLIES; yylval.ival = tptp_update_lval(yytext); return(IMPLIES);}
<INITIAL>"include"    {BEGIN B; tptp_prev_tok=INCLUDE; yylval.ival = tptp_update_lval(yytext); return(INCLUDE);}
"input_clause"    {tptp_prev_tok=INPUT_CLAUSE; yylval.ival = tptp_update_lval(yytext); return(INPUT_CLAUSE);}
"input_formula"    {tptp_prev_tok=INPUT_FORMULA; yylval.ival = tptp_update_lval(yytext); return(INPUT_FORMULA);}
"["    {tptp_prev_tok=LBRKT; yylval.ival = tptp_update_lval(yytext); return(LBRKT);}
"("    {tptp_prev_tok=LPAREN; yylval.ival = tptp_update_lval(yytext); return(LPAREN);}
"--"    {tptp_prev_tok=MMINUS; yylval.ival = tptp_update_lval(yytext); return(MMINUS);}
"~&"    {tptp_prev_tok=NAMPERSAND; yylval.ival = tptp_update_lval(yytext); return(NAMPERSAND);}
"!="    {tptp_prev_tok=NEQUALS; yylval.ival = tptp_update_lval(yytext); return(NEQUALS);}
"<~>"    {tptp_prev_tok=NIFF; yylval.ival = tptp_update_lval(yytext); return(NIFF);}
"~|"    {tptp_prev_tok=NVLINE; yylval.ival = tptp_update_lval(yytext); return(NVLINE);}
"."    {BEGIN INITIAL; tptp_ff = 0; tptp_prev_tok=PERIOD; yylval.ival = tptp_update_lval(yytext); return(PERIOD);}
"++"    {tptp_prev_tok=PPLUS; yylval.ival = tptp_update_lval(yytext); return(PPLUS);}
"?"    {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=TILDE; yylval.ival = tptp_update_lval(yytext); return(TILDE);}
"$false"    {tptp_prev_tok=TOK_FALSE; yylval.ival = tptp_update_lval(yytext); return(TOK_FALSE);}
"$true"    {tptp_prev_tok=TOK_TRUE; yylval.ival = tptp_update_lval(yytext); return(TOK_TRUE);}
"|"    {tptp_prev_tok=VLINE; yylval.ival = tptp_update_lval(yytext); return(VLINE);}
{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);}
{decimal_part}      {tptp_prev_tok=decimal_part; yylval.ival = tptp_update_lval(yytext); return(decimal_part);}
{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);}
{atomic_system_word}      {tptp_prev_tok=atomic_system_word; yylval.ival = tptp_update_lval(yytext); return(atomic_system_word);}
{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);}
{comment}    tptp_update_lval(yytext);
[ \t\n]    ;
[\000-\040]|[\177]    ;
[\041-\176]    return(unrecognized);
%%