/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */

/*
 *  Main authors:
 *     Guido Tack <guido.tack@monash.edu>
 */

/* This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/. */

%option reentrant
%option bison-bridge bison-locations
%option noyywrap
%option stack

%top{
#include <cstdint>
}

%{
#if defined __GNUC__
#pragma GCC diagnostic ignored "-Wunused-function"
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wsign-compare"
#pragma GCC diagnostic ignored "-Wdeprecated"
#elif defined _MSC_VER
#pragma warning(push, 1)
#endif

namespace MiniZinc{ class ParserLocation; }
#define YYLTYPE MiniZinc::ParserLocation
#define YYLTYPE_IS_DECLARED 1
#define YYLTYPE_IS_TRIVIAL 0

#include <minizinc/parser.hh>

namespace MiniZinc {

  int utf8len(const char* s) {
    int l=0;
    for (int i=0; s[i] != '\0'; i++)
      if ((s[i] & 0xc0) != 0x80)
        l++;
    return l;
  }

  int yy_input_proc(char* buf, int size, yyscan_t yyscanner);
}

#define YY_INPUT(buf, result, max_size) \
  result = ::MiniZinc::yy_input_proc(buf, max_size, yyscanner);

#define YY_USER_ACTION \
  { MiniZinc::ParserState* parm =  \
      static_cast<MiniZinc::ParserState*>(yyget_extra(yyscanner)); \
    yylloc->firstLine(yylloc->lastLine()); \
    yylloc->firstColumn(yylloc->lastColumn()+1); \
    if(parm->hadNewline) { \
      parm->hadNewline=false; \
      parm->lineStartPos += parm->nTokenNextStart; \
      parm->nTokenNextStart=1; \
      yylloc->lastLine(yylloc->lastLine()+1); \
      yylloc->firstLine(yylloc->lastLine()); \
      yylloc->firstColumn(1); \
    } \
    if(yytext[0] == '\n') { \
      parm->hadNewline=true; \
      parm->nTokenNextStart+=0; \
    } else { \
      parm->nTokenNextStart+=yyleng; \
    } \
    yylloc->lastColumn(yylloc->firstColumn()+::MiniZinc::utf8len(yytext)-1); \
  }

namespace MiniZinc {
  
  bool hexstrtointval(const char* s, long long int& v) {
    std::istringstream iss(s);
    iss >> std::hex >> v;
    return !iss.fail();
  }

  bool octstrtointval(const char* s, long long int& v) {
    std::istringstream iss(s);
    iss >> std::oct >> v;
    return !iss.fail();
  }

  bool fast_strtointval(const char* s, long long int& v) {
    MiniZinc::IntVal x = 0;
    try {
      for (; *s != '\0'; ++s) {
        x = (x*10) + (*s - '0');
      }
    } catch (MiniZinc::ArithmeticError&) {
      return false;
    }
    v = x.toInt();
    return true;
  }

  bool strtofloatval(const char* s, double& v) {
    std::istringstream iss(s);
    iss >> v;
    return !iss.fail();
  }

  void clearBuffer(void* parm) {
    MiniZinc::ParserState* pp =
      static_cast<MiniZinc::ParserState*>(parm);
    pp->stringBuffer = "";
  }

  void appendBufferString(void* parm, const char* s) {
    MiniZinc::ParserState* pp =
    static_cast<MiniZinc::ParserState*>(parm);
    pp->stringBuffer += s;
  }

  void appendBufferChar(void* parm, char s) {
    MiniZinc::ParserState* pp =
    static_cast<MiniZinc::ParserState*>(parm);
    pp->stringBuffer += s;
  }

  char* bufferData(void* parm) {
    MiniZinc::ParserState* pp =
      static_cast<MiniZinc::ParserState*>(parm);
    return strdup(pp->stringBuffer.c_str());
  }
}

%}

%x string
%x string_quote
%x multilinecomment
%x doccomment
%x doccomment_file
%s bracket_exp
%s quoted_exp

%%

<*>\x0               { return MZN_INVALID_NULL; }

\xa               { }
[ \f\xd\t]        { /* ignore whitespace */ }

"/**"             { yy_push_state(doccomment,yyscanner); ::MiniZinc::clearBuffer(yyget_extra(yyscanner)); }
<doccomment>{
  "*/"            { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
                    yy_pop_state(yyscanner); return MZN_DOC_COMMENT; }
  [^*\xa]+        { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
  "*"             { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
  \xa             { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
}

"/***"             { yy_push_state(doccomment_file,yyscanner); ::MiniZinc::clearBuffer(yyget_extra(yyscanner)); }
<doccomment_file>{
  "*/"             { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
    yy_pop_state(yyscanner); return MZN_DOC_FILE_COMMENT; }
  [^*\xa]+         { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
  "*"              { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
  \xa              { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
}

"/*"              { yy_push_state(multilinecomment,yyscanner); }
<multilinecomment>{
  "*/"            { yy_pop_state(yyscanner); }
  [^*\xa]+        { }
  "*"             { }
  \xa             { }
}


"["               { return MZN_LEFT_BRACKET; }
"[|"              { return MZN_LEFT_2D_BRACKET; }
"]"               { return MZN_RIGHT_BRACKET; }
"|]"              { return MZN_RIGHT_2D_BRACKET; }
%[^\xa]*          { /* ignore comments */ }

"true"            { yylval->iValue = 1; return MZN_BOOL_LITERAL; }
"false"           { yylval->iValue = 0; return MZN_BOOL_LITERAL; }

0[xX]([0-9a-fA-F]*\.[0-9a-fA-F]+|[0-9a-fA-F]+\.)([pP][+-]?[0-9]+)|(0[xX][0-9a-fA-F]+[pP][+-]?[0-9]+)  {
                  if (::MiniZinc::strtofloatval(yytext, yylval->dValue))
                  return MZN_FLOAT_LITERAL;
                  else
                  return MZN_INVALID_FLOAT_LITERAL;
                }

0[xX][0-9A-Fa-f]+  {
                    if (::MiniZinc::hexstrtointval(yytext+2, yylval->iValue))
                      return MZN_INTEGER_LITERAL;
                    else
                      return MZN_INVALID_INTEGER_LITERAL;
                }
0o[0-7]+        {
                  if (::MiniZinc::octstrtointval(yytext+2, yylval->iValue))
                    return MZN_INTEGER_LITERAL;
                  else
                    return MZN_INVALID_INTEGER_LITERAL;
                }
"9223372036854775808" {
                  return MZN_MAX_NEGATIVE_INTEGER_LITERAL;
                }
[0-9]+          {
                  if (::MiniZinc::fast_strtointval(yytext, yylval->iValue))
                    return MZN_INTEGER_LITERAL;
                  else
                    return MZN_INVALID_INTEGER_LITERAL;
                }

[0-9]+\.[0-9]+  {
                  if (::MiniZinc::strtofloatval(yytext, yylval->dValue))
                  return MZN_FLOAT_LITERAL;
                  else
                  return MZN_INVALID_FLOAT_LITERAL;
                }
[0-9]+\.[0-9]+[Ee][+-]?[0-9]+  {
                    if (::MiniZinc::strtofloatval(yytext, yylval->dValue))
                      return MZN_FLOAT_LITERAL;
                    else
                      return MZN_INVALID_FLOAT_LITERAL;
                  }
[0-9]+[Ee][+-]?[0-9]+  {
                    if (::MiniZinc::strtofloatval(yytext, yylval->dValue))
                      return MZN_FLOAT_LITERAL;
                    else
                      return MZN_INVALID_FLOAT_LITERAL;
                  }
[:;|{},\[\]]      { return *yytext; }
([ \f\xd\t]*\.[ \f\xd\t]*(([0-9]+)|(_?[A-Za-z][A-Za-z0-9_]*)|('[^\\'\xa\xd\x0]+')))+ { yylval->sValue = strdup(yytext); return MZN_FIELD_TAIL; }
\.\.              { return MZN_DOTDOT; }
"'\.\.'"          { return MZN_DOTDOT_QUOTED; }
"\.\.<"           { return MZN_DOTDOT_LE; }
"'\.\.<'"         { return MZN_DOTDOT_LE_QUOTED; }
"<\.\."           { return MZN_LE_DOTDOT; }
"'<\.\.'"         { return MZN_LE_DOTDOT_QUOTED; }
"<\.\.<"          { return MZN_LE_DOTDOT_LE; }
"'<\.\.<'"        { return MZN_LE_DOTDOT_LE_QUOTED; }
::                { return MZN_COLONCOLON; }
_                 { return MZN_UNDERSCORE; }
"ann"             { return MZN_ANN; }
"annotation"      { return MZN_ANNOTATION; }
"any"             { return MZN_ANY; }
"array"           { return MZN_ARRAY; }
"bool"            { return MZN_BOOL; }
"case"            { return MZN_CASE; }
"constraint"      { return MZN_CONSTRAINT; }
"default"         { return MZN_DEFAULT; }
"div"             { return MZN_IDIV; }
"'div'"           { return MZN_IDIV_QUOTED; }
"diff"            { return MZN_DIFF; }
"'diff'"          { return MZN_DIFF_QUOTED; }
"else"            { return MZN_ELSE; }
"elseif"          { return MZN_ELSEIF; }
"endif"           { return MZN_ENDIF; }
"enum"            { return MZN_ENUM; }
"float"           { return MZN_FLOAT; }
"function"        { return MZN_FUNCTION; }
"if"              { return MZN_IF; }
"include"         { return MZN_INCLUDE; }
"infinity"        { return MZN_INFINITY; }
"intersect"       { return MZN_INTERSECT; }
"'intersect'"     { return MZN_INTERSECT_QUOTED; }
"in"              { return MZN_IN; }
"'in'"            { return MZN_IN_QUOTED; }
"int"             { return MZN_INT; }
"let"             { return MZN_LET; }
"list"            { return MZN_LIST; }
"maximize"        { yylval->bValue = false; return MZN_MAXIMIZE; }
"minimize"        { yylval->bValue = true; return MZN_MINIMIZE; }
"mod"             { return MZN_MOD; }
"'mod'"           { return MZN_MOD_QUOTED; }
"not"             { return MZN_NOT; }
"'not'"           { return MZN_NOT_QUOTED; }
"of"              { return MZN_OF; }
"output"          { return MZN_OUTPUT; }
"opt"             { return MZN_OPT; }
"par"             { return MZN_PAR; }
"predicate"       { return MZN_PREDICATE; }
"record"          { return MZN_RECORD; }
"satisfy"         { return MZN_SATISFY; }
"set"             { return MZN_SET; }
"solve"           { return MZN_SOLVE; }
"string"          { return MZN_STRING; }
"subset"          { return MZN_SUBSET; }
"'subset'"        { return MZN_SUBSET_QUOTED; }
"superset"        { return MZN_SUPERSET; }
"'superset'"      { return MZN_SUPERSET_QUOTED; }
"symdiff"         { return MZN_SYMDIFF; }
"'symdiff'"       { return MZN_SYMDIFF_QUOTED; }
"test"            { return MZN_TEST; }
"then"            { return MZN_THEN; }
"tuple"           { return MZN_TUPLE; }
"type"            { return MZN_TYPE; }
"union"           { return MZN_UNION; }
"'union'"         { return MZN_UNION_QUOTED; }
"var"             { return MZN_VAR; }
"variant_record"  { return MZN_VARIANT_RECORD; }
"where"           { return MZN_WHERE; }
"xor"             { return MZN_XOR; }
"'xor'"           { return MZN_XOR_QUOTED; }
"+"               { return MZN_PLUS; }
"'+'"             { return MZN_PLUS_QUOTED; }
"-"               { return MZN_MINUS; }
"'-'"             { return MZN_MINUS_QUOTED; }
"*"               { return MZN_MULT; }
"'*'"             { return MZN_MULT_QUOTED; }
"/"               { return MZN_DIV; }
"'/'"             { return MZN_DIV_QUOTED; }
"^-1"             { return MZN_POW_MINUS1; }
"^"               { return MZN_POW; }
"'^'"             { return MZN_POW_QUOTED; }
"++"              { return MZN_PLUSPLUS; }
"'++'"            { return MZN_PLUSPLUS_QUOTED; }
"<>"              { return MZN_ABSENT; }
"<"               { return MZN_LE; }
"'<'"             { return MZN_LE_QUOTED; }
"<="              { return MZN_LQ; }
"'<='"            { return MZN_LQ_QUOTED; }
">"               { return MZN_GR; }
"'>'"             { return MZN_GR_QUOTED; }
">="              { return MZN_GQ; }
"'>='"            { return MZN_GQ_QUOTED; }
"=="              { return MZN_EQ; }
"'=='"            { return MZN_EQ_QUOTED; }
"="               { return MZN_EQ; }
"'='"             { return MZN_EQ_QUOTED; }
"!="              { return MZN_NQ; }
"'!='"            { return MZN_NQ_QUOTED; }
"->"              { return MZN_IMPL; }
"'->'"            { return MZN_IMPL_QUOTED; }
"<-"              { return MZN_RIMPL; }
"'<-'"            { return MZN_RIMPL_QUOTED; }
"<->"             { return MZN_EQUIV; }
"'<->'"           { return MZN_EQUIV_QUOTED; }
"\\/"             { return MZN_OR; }
"'\\/'"           { return MZN_OR_QUOTED; }
"/\\"             { return MZN_AND; }
"'/\\'"           { return MZN_AND_QUOTED; }

"~+"              { return MZN_WEAK_PLUS; }
"~*"              { return MZN_WEAK_MULT; }
"~="              { return MZN_WEAK_EQ; }
"~!="             { return MZN_WEAK_NQ; }
"~-"              { return MZN_WEAK_MINUS; }
"~/"              { return MZN_WEAK_DIV; }
"~div"            { return MZN_WEAK_IDIV; }

"'~"[+*=/-]"'"    {
                    yylval->sValue = strdup(yytext+1);
                    yylval->sValue[strlen(yytext)-2] = 0;
                    return MZN_IDENTIFIER; }

"_objective"      { yylval->sValue = strdup(yytext); return MZN_IDENTIFIER; }

_?[A-Za-z][A-Za-z0-9_]* {
                    yylval->sValue = strdup(yytext); return MZN_IDENTIFIER; }
"'"[^'\xa\xd\x0]+"'" {
                    MiniZinc::ParserState* parm = 
                    static_cast<MiniZinc::ParserState*>(yyget_extra(yyscanner));
                    if (parm->isFlatZinc) {
                      return QUOTED_IDENTIFIER;
                    } else {
                      yylval->sValue = strdup(yytext + 1);
                      yylval->sValue[strlen(yytext)-2] = 0;
                      return MZN_IDENTIFIER;
                    }
                    }

"\xE2\x88\x80"      { yylval->sValue = strdup("forall"); return MZN_IDENTIFIER; }
"\xE2\x88\x83"      { yylval->sValue = strdup("exists"); return MZN_IDENTIFIER; }
"\xE2\x88\x88"      { return MZN_IN; }
"\xE2\x8A\x86"      { return MZN_SUBSET; }
"\xE2\x8A\x87"      { return MZN_SUPERSET; }
"\xE2\x88\x9E"      { return MZN_INFINITY; }
"\xC2\xAC"          { return MZN_NOT; }
"\xE2\x86\x90"      { return MZN_RIMPL; }
"\xE2\x86\x92"      { return MZN_IMPL; }
"\xE2\x86\x94"      { return MZN_EQUIV; }
"\xE2\x88\xA7"      { return MZN_AND; }
"\xE2\x88\xA8"      { return MZN_OR; }
"\xE2\x89\xA0"      { return MZN_NQ; }
"\xE2\x89\xA4"      { return MZN_LQ; }
"\xE2\x89\xA5"      { return MZN_GQ; }
"\xE2\x88\xAA"      { return MZN_UNION; }
"\xE2\x88\xA9"      { return MZN_INTERSECT; }
"\xE2\x81\xBB\xC2\xB9" { return MZN_POW_MINUS1; }

$$[A-Za-z][A-Za-z0-9_]* {
  yylval->sValue = strdup(yytext+1); return MZN_TI_ENUM_IDENTIFIER; }

$[A-Za-z][A-Za-z0-9_]* {
                    yylval->sValue = strdup(yytext+1); return MZN_TI_IDENTIFIER; }

"(" { yy_push_state(bracket_exp,yyscanner); return *yytext; }
<bracket_exp>")" { yy_pop_state(yyscanner); return *yytext; }
<quoted_exp>")" { yy_pop_state(yyscanner); yy_pop_state(yyscanner); yy_push_state(string_quote,yyscanner);
                  ::MiniZinc::clearBuffer(yyget_extra(yyscanner)); }

\"                { yy_push_state(string,yyscanner); ::MiniZinc::clearBuffer(yyget_extra(yyscanner)); }
<string,string_quote>[^\\"\xa\xd\x0]* { ::MiniZinc::appendBufferString(yyget_extra(yyscanner), yytext); }
<string,string_quote>\\n         { ::MiniZinc::appendBufferChar(yyget_extra(yyscanner), '\n'); }
<string,string_quote>\\t         { ::MiniZinc::appendBufferChar(yyget_extra(yyscanner), '\t'); }
<string,string_quote>\\x[0-9a-fA-F][0-9a-fA-F]? {
  long long int hexVal;
  if (::MiniZinc::hexstrtointval(yytext+2, hexVal)) {
    ::MiniZinc::appendBufferChar(yyget_extra(yyscanner), static_cast<char>(hexVal));
  } else {
    return MZN_INVALID_STRING_LITERAL;
  }
}
<string,string_quote>\\[0-7][0-7]?[0-7]? {
  long long int octVal;
  if (::MiniZinc::octstrtointval(yytext+1, octVal)) {
    ::MiniZinc::appendBufferChar(yyget_extra(yyscanner), static_cast<char>(octVal));
  } else {
    return MZN_INVALID_STRING_LITERAL;
  }
}

<string,string_quote>\\[\\"']     { ::MiniZinc::appendBufferChar(yyget_extra(yyscanner), yytext[1]); }
<string>\\"("       { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
                      yy_push_state(quoted_exp,yyscanner); return MZN_STRING_QUOTE_START; }
<string_quote>\\"(" { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
                      yy_push_state(quoted_exp,yyscanner); return MZN_STRING_QUOTE_MID; }
<string>\"          { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
                      yy_pop_state(yyscanner); return MZN_STRING_LITERAL; }
<string_quote>\"          { yylval->sValue = ::MiniZinc::bufferData(yyget_extra(yyscanner));
                            yy_pop_state(yyscanner); return MZN_STRING_QUOTE_END; }
<string,string_quote>. { return (unsigned char)yytext[0]; }
<string,string_quote>[\xa\xd\x0] { return MZN_END_OF_LINE_IN_STRING; }
<string,string_quote><<EOF>> { yy_pop_state(yyscanner); return MZN_UNTERMINATED_STRING; }

`[A-Za-z][A-Za-z0-9_]*` {
                    yylval->sValue = strdup(yytext+1);
                    yylval->sValue[strlen(yytext)-2] = 0; 
                    return MZN_QUOTED_IDENTIFIER; }

.                 { return (unsigned char)yytext[0]; }

%%
namespace MiniZinc {
  int yy_input_proc(char* buf, int size, yyscan_t yyscanner) {
    MiniZinc::ParserState* parm =
      static_cast<MiniZinc::ParserState*>(yyget_extra(yyscanner));
    return static_cast<int>(parm->fillBuffer(buf, size));
    // work around warning that yyunput is unused
    yyunput (0,buf,yyscanner);
  }
}