/**CFile*******************************************************************
  PackageName [mc]
  Synopsis    [Package 'mc' provides a symbolic ACTLW model checker]

  FileName    [mcParser.l]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si)]
  Description [File  mcParser.y is a flex file for ACTLW parser.]
  SeeAlso     [mc.h, mcInt.h, mcParser.y]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

%{
#define MAX_MACRO_DEPTH 255
YY_BUFFER_STATE macro_stack[MAX_MACRO_DEPTH] = {0};
int macro_depth = 0;
%}

NAME            [-_A-Za-z0-9][-_A-Za-z0-9]*
ACTION          {NAME}[?!]|[?!]{NAME}
VALTRUE         true|True|TRUE
VALFALSE        false|False|FALSE
NOT             not|Not|NOT
AND             and|And|AND
OR              or|Or|OR
EQV             eqv|Eqv|EQV
IMPL            impl|Impl|IMPL
TAU             tau|tAu|taU|tAU|Tau|TAu|TaU|TAU
EPSILON         eps|Eps|EPS|epsilon|Epsilon|EPSILON
MACRO 	        \${NAME}
OUTLINE 	^#.*
OUTLINE1 	#.*

%%
"/*" {
       int ch, inComm;
       for (inComm=1; inComm; ) {
          switch (ch=input()) {
            case '\n' : break;
            case '*'  : if (( ch=input()) == '/') {
                          inComm=0;
                        } else {
                          unput(ch);
                        }
                        break;
          }
       }
     }

[ \t\n\r] {/* empty space is ignored */}

"'" {/* qoutes are ignored */}

"\"" {/* qoutes are ignored */}

E   {return E;}
A   {return A;}
U   {return UNTIL;}
EX  {return EX;}
AX  {return AX;}
EF  {return EF;}
AF  {return AF;}
EG  {return EG;}
AG  {return AG;}

EE  {return EE;}
AA  {return AA;}
W   {return UNLESS;}
UU  {return UNLESS;}
EEX {return EEX;}
AAX {return AAX;}
EEF {return EEF;}
AAF {return AAF;}
EEG {return EEG;}
AAG {return AAG;}

"~"		{return NOT;}
"*"		{return AND;}
"&"		{return AND;}
"+"		{return OR;}
"|"		{return OR;}
"<->"		{return EQV;}
"->"		{return IMPL;}

{NOT}   {return NOT;}
{AND}   {return AND;}
{OR}    {return OR;}
{EQV}   {return EQV;}
{IMPL}  {return IMPL;}

"("  {return yytext[0];}
")"  {return yytext[0];}
"{"  {return yytext[0];}
"}"  {return yytext[0];}
"["  {return yytext[0];}
"]"  {return yytext[0];}
"<"  {return yytext[0];}
">"  {return yytext[0];}
";"  {return yytext[0];}

{ACTION} {
  yylval.name = strdup(yytext);
  return ACTION;
}

{VALTRUE} {
  yylval.name = strdup("true");
  return VALTRUE;
}

{VALFALSE} {
  yylval.name = strdup("false");
  return VALFALSE;
}

{TAU} {
  yylval.name = strdup("TAU");
  return TAU;
}

{EPSILON} {
  yylval.name = strdup("EPSILON");
  return EPSILON;
}

{OUTLINE}	{
  char *text,*name,*body;
  int len;

  text = strdup(yytext);
  if (strncmp(text,"#define",7)) {
    yylval.name = text;
    return OUTLINE;
  } else {
    name = strdup(strtok(&text[7]," "));
    len = 8+strlen(&text[7]);
    if (len > strlen(yytext)) {
      body = strdup("");
    } else {
      body = strdup(&text[len]);
    }
    free(text);

    /*
    fprintf(stderr,"Definition: <%s> <%s>\n",name,body);
    */

    McAddMacro(name,body);
  }
}

{OUTLINE1} {
  yylval.name = strdup(yytext);
  return OUTLINE;
}

{MACRO} {
  YY_BUFFER_STATE buffer;
  int i;

  /*
  fprintf(stderr,"Macro: %s\n",yytext);
  */

  if (macro_depth >= MAX_MACRO_DEPTH) {
    fprintf(stderr,"Macros nested too deeply!");
    exit(1);
  } else {
    macro_stack[macro_depth++] = YY_CURRENT_BUFFER;
    i = McFindMacro(&yytext[1]);
    if (i == -1) {
      fprintf(stderr,"Macro not defined!");
      exit(1);
    } else {

      /* VARIANT 1 */
      /*
      char *text;
      int len;
      text = strdup(mcMacroTable[i].body);
      len = strlen(text);
      text = (char *) realloc(text,len+2);
      text[len+1] = 0;
      buffer = yy_scan_buffer(text,len+2);
      */

      /* VARIANT 2 */
      /**/
      buffer = yy_scan_string(mcMacroTable[i].body);
      /**/

      yy_switch_to_buffer(buffer);
    }
  }
}

<<EOF>> {
  if (macro_depth == 0 ) {
    yyterminate();
  } else {
    yy_delete_buffer(YY_CURRENT_BUFFER);
    yy_switch_to_buffer(macro_stack[--macro_depth]);
  }
}
%%
