/* Lexer for proof.log files, C version.
   Copyright (C) 2004 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 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, or (at your option)
   any later version.

   h1 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 h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*/
%{
#include <stdlib.h>
#include <stdio.h>
#ifdef HAVE_LIBZ
#include <zlib.h>
  typedef gzFile fp;
fp yygzin = NULL;
#else
  typedef FILE *fp;
#endif
#include "cproof.tab.h"

#ifdef HAVE_LIBZ
#define YY_INPUT(buf,result,max_size) \
if ( ((result = gzread(yygzin, buf, max_size)) < 0)) \
YY_FATAL_ERROR( "input in flex scanner failed" );
#endif

extern void *xmalloc (size_t n);

#ifdef OBSOLETE
char *unstringify (char *from)
{
  size_t len = strlen (from);
  char *to = xmalloc (len+1);
  char *s, *t, c;

  for (s=from+1, t=to; (c = *s++)!=0; )
    switch (c)
      {
      case '\\':
	switch (c = *s++)
	  {
	  case '\"': case '\\':
	    *t++ = c; break;
	  case 'n': *t++ = '\n'; break;
	  case 't': *t++ = '\t'; break;
	  case 'v': *t++ = 11; break;
	  case 'f': *t++ = 12; break;
	  case '^': *t++ = (*s++) - '@'; break;
	  default:
	    if (c>='0' && c<='9')
	      {
		int n = 100*(int)(c-'0');

		n += 10*(int)(*s++ - '0');
		n+= (int) (*s++ - '0');
		*t++ = n;
	      }
	    else
	      {
		while (*s++ != '\\');
	      }
	    break;
	  }
	break;
      case '"':
	goto end;
      default: *t++ = c; break;
      }
 end:
  *t = 0;
  return t;
}
#endif

%}

%option noyywrap

SPACE [\ \t\f\n\r]+
FMT [\ \t\n\f]
DIG [0-9]+
CAPITAL [A-Z]
SMALL [a-z]
LETTER ({CAPITAL}|{SMALL})
ALPHA [A-Za-z0-9\'\_]
SYMB [\!\%\&\$\#\+\-\/\:\<\=\>\?\@\\\~\'\^\|\*\`]

%x COMMENT

%%

{SPACE}	;
"%".*\n	;
"/*"	{ BEGIN(COMMENT); }
<COMMENT>{
  [^*]*	{ ; /* eat anything that's not a '*' */ }
  "*"+[^*/]*  { ; /* eat up '*'s not followed by '/'s */ }
  "*"+"/"       { BEGIN (INITIAL); }
  <<EOF>>	{ BEGIN (0); YY_FLUSH_BUFFER;
  fprintf (stderr, "Unterminated comment: stop.\n");
  fflush (stderr);
  exit (10); }
}
\#ne\([^()]*\) { return kw_ne; }
\#false\([^()]*\) { return kw_false; }

"<source>" return kw_open_source;
"</source>" return kw_close_source;
"<clause"{SPACE}+"name"{SPACE}*"="{SPACE}* return kw_open_clause;
"</clause>" return kw_close_clause;
"<definitions>" return kw_open_definitions;
"</definitions>" return kw_close_definitions;
"<approximation>" return kw_open_approximation;
"</approximation>" return kw_close_approximation;
"<justifications>" return kw_open_justifications;
"</justifications>" return kw_close_justifications;

\[({ALPHA}|\-)+\] return kw_axiom;
\[({ALPHA}|\-)+: return kw_open_rule;
\] return kw_close_rule;

\"([^\"\\]|(\\([\"\\ntvf]|(\^[\@A-Z\[\\\]\^\_])|({DIG}{DIG}{DIG})|({FMT}*\\))))*\"	{
  return string_constant; }
{DIG}:	{
          return kw_clause_def; }
{DIG};	{
          return kw_clause_use; }

\(	return kw_open_paren;
\)	return kw_close_paren;
\{[^{}]*\}	return kw_subst;
:-	return kw_provided;
\,	return kw_comma;
\;	return kw_semicolon;
\.	return kw_period;
\?	return kw_question_mark;
\>	return kw_end_tag;
\_*{SMALL}{ALPHA}*	{ return identifier; }
\_*{DIG}		{ return identifier; }
\_*{CAPITAL}{ALPHA}*	{ return VAR; }
\*			{ return identifier; }
\#q{DIG}*		{ return identifier; }
.	{ fprintf (stderr, "Unrecognized character: %s\n", yytext);
          fflush (stderr); }

%%
