%{
/* 
$Id: pvs_lexer.l,v 1.7 2001/01/11 11:45:47 sbeyer Exp $
$Log: pvs_lexer.l,v $
Revision 1.7  2001/01/11 11:45:47  sbeyer

added parameter_parse_verbose support

Revision 1.6  2001/01/09 13:42:19  sbeyer

corrected linenumber count (multiple files)
and added filename to error output

*/

#include "pvs_parser.tab.h"
#include "parser_typen.h"

int zeilennummer;
char* inputfile;

#define ECHO if (parameter_parse_verbose) fprintf(yyout, "%s", yytext);
%}
ZI   [0-9]
ID   [a-zA-Z][_?0-9a-zA-Z]*

%%
[\n]                    { ECHO; zeilennummer++; }
[\t ]+                  { ECHO; }

\".*\"                  { ECHO; yylval.string=(char *) strdup(yytext); yylval.string[0]='\''; yylval.string[strlen(yylval.string)-1]='\''; return STRING; }
ALL                     { ECHO; return ALL; }
AND                     { ECHO; return AND; }
ANDTHEN                 { ECHO; return ANDTHEN; }
ARRAY                   { ECHO; return ARRAY; }
ASSUMING                { ECHO; return ASSUMING; }
ASSUMPTION              { ECHO; return ASSUMPTION; }
AXIOM                   { ECHO; return AXIOM; }
ENDASSUMING             { ECHO; return ENDASSUMING; }
BEGIN                   { ECHO; return BEGINN; }
BUT                     { ECHO; return BUT; }
BY                      { ECHO; return BY; }
CASES                   { ECHO; return CASES; }
CHALLENGE               { ECHO; return CHALLENGE; }
CLAIM                   { ECHO; return CLAIM; }
CLOSURE                 { ECHO; return CLOSURE; }
COND                    { ECHO; return COND; }
CONJECTURE              { ECHO; return CONJECTURE; }
CONTAINING              { ECHO; return CONTAINING; }
CONVERSION              { ECHO; return CONVERSION; }
COROLLARY               { ECHO; return COROLLARY; }
DATATYPE                { ECHO; return DATATYPE; }
ELSE                    { ECHO; return ELSE; }
ELSIF                   { ECHO; return ELSIF; }
END                     { ECHO; return END; }
ENDCASES                { ECHO; return ENDCASES; }
ENDCOND                 { ECHO; return ENDCOND; }
ENDIF                   { ECHO; return ENDIF; }
ENDTABLE                { ECHO; return ENDTABLE; }
EXISTS                  { ECHO; return EXISTS; }
EXPORTING               { ECHO; return EXPORTING; }
FACT                    { ECHO; return FACT; }
FALSE                   { ECHO; return FALSE; }
FORALL                  { ECHO; return FORALL; }
FORMULA                 { ECHO; return FORMULA; }
FROM                    { ECHO; return FROM; }
FUNCTION                { ECHO; return FUNCTION; }
HAS_TYPE                { ECHO; return HAS_TYPE; }
IF                      { ECHO; return IF; }
IFF                     { ECHO; return IFF; }
IMPLIES                 { ECHO; return IMPLIES; }
IMPORTING               { ECHO; return IMPORTING; }
IN                      { ECHO; return IN; }
INDUCTIVE               { ECHO; return INDUCTIVE; }
JUDGEMENT               { ECHO; return JUDGEMENT; }
JUX                     { ECHO; return JUX; }
LAMBDA                  { ECHO; return LAMBDA; } 
LAW                     { ECHO; return LAW; }
LEMMA                   { ECHO; return LEMMA; }
LET                     { ECHO; return LET; }
LIBRARY                 { ECHO; return LIBRARY; } 
MEASURE                 { ECHO; return MEASURE; }
NONEMPTY_TYPE           { ECHO; return NONEMPTY_TYPE; }
NOT                     { ECHO; return NOT; }
OBLIGATION              { ECHO; return OBLIGATION; }
OF                      { ECHO; return OF; }
OR                      { ECHO; return OR; }
ORELSE                  { ECHO; return ORELSE; }
POSTULATE               { ECHO; return POSTULATE; }
PROPOSITION             { ECHO; return PROPOSITION; }
RECURSIVE               { ECHO; return RECURSIVE; }
SUBLEMMA                { ECHO; return SUBLEMMA; }
SUBTYPE_OF              { ECHO; return SUBTYPE_OF; }
SUBTYPES                { ECHO; return SUBTYPES; }
TABLE                   { ECHO; return TABLE; }
THEN                    { ECHO; return THEN; }
THEOREM                 { ECHO; return THEOREM; }
THEORY                  { ECHO; return THEORY; }
TRUE                    { ECHO; return TRUE; }
TYPE                    { ECHO; return TYPE; }
"TYPE+"                 { ECHO; return TYPEPLUS; }
VAR                     { ECHO; return VAR; }
WHEN                    { ECHO; return WHEN; }
WHERE                   { ECHO; return WHERE; } 
WITH                    { ECHO; return WITH; }
XOR                     { ECHO; return XOR; }
"o"                     { ECHO; return O_OPERATOR; }
"[#"                    { ECHO; return ECKKLAMMERAUF_RAUTE; }     
"#]"                    { ECHO; return RAUTE_ECKKLAMMERZU; }      
"(:"                    { ECHO; return KLAMMERAUF_DOPPELPUNKT; }  
":)"                    { ECHO; return DOPPELPUNKT_KLAMMERZU; }   
"[|"                    { ECHO; return ECKKLAMMERAUF_PIPE; }
"|]"                    { ECHO; return PIPE_ECKKLAMMERZU; }
"(#"                    { ECHO; return KLAMMERAUF_RAUTE; }
"#)"                    { ECHO; return RAUTE_KLAMMERZU; }
"::"                    { ECHO; return DOPPELPUNKT_DOPPELPUNKT; }
"->"                    { ECHO; return MINUS_GROESSER; }
":="                    { ECHO; return DOPPELPUNKT_GLEICH; }
"|->"                   { ECHO; return PIPE_MINUS_GROESSER; }
"|["                    { ECHO; return PIPE_ECKKLAMMERAUF; }
"]|"                    { ECHO; return ECKKLAMMERZU_PIPE; }
"||"                    { ECHO; return PIPE_PIPE; }
"[||]"                  { ECHO; return ECKKLAMMERAUF_PIPE_PIPE_ECKKLAMMERZU; }
"<=>"                   { ECHO; return KLEINER_GLEICH_GROESSER; }
"=>"                    { ECHO; return GLEICH_GROESSER; }
"++"                    { ECHO; return PLUS_PLUS; }
"**"                    { ECHO; return MAL_MAL; }
"//"                    { ECHO; return SLASH_SLASH; }
"^^"                    { ECHO; return DACH_DACH; }
"|-"                    { ECHO; return PIPE_MINUS; }
"|="                    { ECHO; return PIPE_GLEICH; }
"<|"                    { ECHO; return KLEINER_PIPE; }
"|>"                    { ECHO; return PIPE_GROESSER; }
"/="                    { ECHO; return SLASH_GLEICH; }
"=="                    { ECHO; return GLEICH_GLEICH; }
"<="                    { ECHO; return KLEINER_GLEICH; }
">="                    { ECHO; return GROESSER_GLEICH; }
"<<"                    { ECHO; return KLEINER_KLEINER; }
">>"                    { ECHO; return GROESSER_GROESSER; }
"<<="                   { ECHO; return KLEINER_KLEINER_GLEICH; }
">>="                   { ECHO; return GROESSER_GROESSER_GLEICH; }
"@@"                    { ECHO; return AT_AT; }
"##"                    { ECHO; return RAUTE_RAUTE; }
"[]"                    { ECHO; return ECKKLAMMERAUF_ECKKLAMMERZU; }
"<>"                    { ECHO; return KLEINER_GROESSER; }
{ZI}*                   { ECHO; yylval.zahl=(char *) strdup(yytext); return NUMBER; }
{ID}"@"                 { ECHO; yylval.identifier=(char *) strdup(yytext); return IDAT; } 
{ID}                    { ECHO; yylval.identifier=(char *) strdup(yytext); return ID; }       
%.*\n                   { ECHO; zeilennummer++; } /* Kommentare */
.                       { ECHO; return(*yytext); }                    
%%

void yyerror(char *errmsg)
{
  printf("\nDatei %s, Zeile %d: '%s' vor : %s\n",inputfile,zeilennummer,errmsg,yytext);
  exit(1);
}