%{
// Author : Gregory R. Olsen 
//          Center for Design Research, Stanford University
//          560 Panama Street
//          Stanford, CA 94305-2232
//          olsen@cs.stanford.edu
// Contributions by: Jim McGuire (Lockheed AI Center)

// Copyright (c) 1993 Stanford University. All rights reserved.
// Copyright (c) 1993 Lockheed Missiles and Space Co.

/*
 * Permission is hereby granted, without written agreement and without
 * license, to use, copy, modify, and distribute this software and its 
 * documentation for non-commercial use, provided that the above 
 * copyright notice and the following two paragraphs appear in
 * all copies of this software.
 * 
 * THIS SOFTWARE IS PROVIDED "AS-IS" AND WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS, IMPLIED OR OTHERWISE, INCLUDING WITHOUT LIMITATION, ANY
 * WARRANTY OF MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.
 * 
 * IN NO EVENT SHALL STANFORD UNIVERSITY OR LOCKHEED MISSILES AND SPACE 
 * COMPANY BE LIABLE FOR ANY SPECIAL, INCIDENTAL, INDIRECT OR 
 * CONSEQUENTIAL DAMAGES OF ANY KIND, OR ANY DAMAGES WHATSOEVER 
 * RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER OR NOT ADVISED
 * OF THE POSSIBILITY OF DAMAGE, AND ON ANY THEORY OF LIABILITY, ARISING 
 * OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 */

#include "KIFClass.h"
#include "KIFGrammar.tab.h"
#define min(a,b) ((a)<(b)?a:b)

char inputstring[MAXMESLEN];
char *inputstringptr; /* current position in inputstring */
int inputstringlim;  /* end of data */

int mywrap();
#undef yywrap()
#define yywrap()  mywrap()

int my_yyinput(char *buf,int max);
#undef YY_INPUT
#define YY_INPUT(buffer,result,maxsize) (result=my_yyinput(buffer,maxsize))

%}

/* regular definitions */

delim		[ \t\n]
ws		{delim}+
digit		[0-9]
number		\-?{digit}+(\.{digit}+)?((E|e)[+\-]?{digit}+)?
/*string		\"[[\\\"]|[^"]]*\"*/
string		\"([^"\\]|(\\.))*\"
/* string		\"[^"]*\" */
constant	[^ )(\t\n]+
indvar		\?{constant}+
seqvar		\@{constant}+

%%

{ws}			/* no action */
"("			{yylval.val = strdup(yytext); return('(');}
")"			{yylval.val = strdup(yytext); return(')');}
{indvar}		{yylval.val = strdup(yytext); return(INDVAR);}
{seqvar}		{yylval.val = strdup(yytext); return(SEQVAR);}
("true"|"TRUE")  	{yylval.val = strdup(yytext); return(TRUE);}
("false"|"FALSE")  	{yylval.val = strdup(yytext); return(FALSE);}
{string}		{yylval.val = strdup(yytext); return(STRING);}
{number}		{yylval.val = strdup(yytext); return(NUMBER);}
"="			{yylval.val = strdup(yytext); return(EQ);}
"/="			{yylval.val = strdup(yytext); return(NOTEQ);}
"=>"			{yylval.val = strdup(yytext); return(IMPLIES);}
"<="			{yylval.val = strdup(yytext); return(IMPLIED);}
"<=>"			{yylval.val = strdup(yytext); return(EQUIV);}
"=>>"			{yylval.val = strdup(yytext); return(RULELR);}
"<<="			{yylval.val = strdup(yytext); return(RULERL);}
("quote"|"QUOTE")	{yylval.val = strdup(yytext); return(QUOTE);}
"'"			{yylval.val = strdup(yytext); return(QUOTESYM);}
("and"|"AND")		{yylval.val = strdup(yytext); return(AND);}
("or"|"OR")		{yylval.val = strdup(yytext); return(OR);}
("not"|"NOT")		{yylval.val = strdup(yytext); return(NOT);}
("forall"|"FORALL")	{yylval.val = strdup(yytext); return(FORALL);}
("exists"|"EXISTS")	{yylval.val = strdup(yytext); return(EXISTS);}
("if"|"IF")		{yylval.val = strdup(yytext); return(IF);}
("listof"|"LISTOF")	{yylval.val = strdup(yytext); return(LISTOF);}	
("setof"|"SETOF")	{yylval.val = strdup(yytext); return(SETOF);}	
("setofall"|"SETOFALL")	{yylval.val = strdup(yytext); return(SETOFALL);}    
("defobject"|"DEFOBJECT")	{yylval.val = strdup(yytext); return(DEFOBJECT);}	
("deffunction"|"DEFFUNCTION")	{yylval.val = strdup(yytext); return(DEFFUNCTION);}	
("defrelation"|"DEFRELATION")	{yylval.val = strdup(yytext); return(DEFRELATION);}  
":="			{yylval.val = strdup(yytext); return(COLEQ);}
":=>"			{yylval.val = strdup(yytext); return(COLEQLT);}
":&"			{yylval.val = strdup(yytext); return(COLAMP);}
^":T"		        {yylval.val = strdup(yytext); return(TERMEXP);}
^":F"   		{yylval.val = strdup(yytext); return(FORMEXP);}
(consis|CONSIS)		{yylval.val = strdup(yytext); return(CONSIS);}
{constant}		{yylval.val = strdup(yytext); return(CONSTANT);}

%%

int mywrap()
{
extern FILE *yyin;
extern void yyrestart(FILE *);
yyrestart(yyin);
return 1;
}

int my_yyinput(char *buf, int max_size)
{
  int copylen = inputstringlim - (int) (inputstringptr - inputstring);
  int n = min(max_size, copylen);

  if (n > 0) {
    memcpy(buf, inputstringptr, n);
    inputstringptr += n;
  }
  return n;
}