%{
// 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 <stdlib.h>
#include <ctype.h> 
#include "KIFClass.h"
#define YYDEBUG 1
extern int yylex(void);
void yyerror(char *s);
expression *kif_result;

%}
%union {
  char *val;
  sentence *sen; 
  term *ter;
  definition *def;
  form *frm;
  expression *exp;
  sequence *seq;
}

%token <val> INDVAR SEQVAR CONSTANT CONSIS ')' '(' 
%token <val> AND NOT OR FORALL EXISTS STRING NUMBER FALSE TRUE 
%token <val> EQ NOTEQ IMPLIES IMPLIED EQUIV RULELR RULERL
%token <val> IF LISTOF SETOF QUOTE QUOTESYM
%token <val> COND THE SETOFALL KAPPA LAMBDA /* not fully supported */
%token <val> DEFOBJECT DEFFUNCTION DEFRELATION COLEQ COLEQLT COLAMP /* := :=> :& */
%token <val> TERMEXP FORMEXP /* term sentence rule definition */
%type <frm> form rule 
%type <def> definition complete partial
%type <sen> sentence relsent logconst equation inequality logsent quantsent
%type <ter> term functerm listterm logterm quoterm setterm quanterm 
%type <exp> express word list operator defop termop sentop ruleop premise kifexp
%type <seq> sequence sentenceseq indvarseq termseq premiseseq
%start kifexp
%%

kifexp  :	FORMEXP form      	{kif_result = $2;}
	|	TERMEXP term		{kif_result = $2;}
	|	error			{kif_result = NULL;yyclearin;}
	;
form	:	sentence        {$$=$1;}
	|	definition 	{$$=$1;}
	|	rule 		{$$=$1;}
	; 
rule	:	'(' RULELR premiseseq sentence ')'	
                {$$=new rule($3,$4);}
	|	'(' RULERL sentence premiseseq ')'	
                {$$=new rule($4,$3);}
	;
premiseseq	:	premise			
                        {$$=new sequence($1);}
		|	premiseseq premise	
                        {$1->add($2);$$=$1;}
		;
premise	:	sentence			
                {$$=$1;}
	|	'(' CONSIS sentence ')'		
                {$$=new consis($3);}
	; 
definition:	complete	{$$ = $1;} 
	|	partial		{$$ = $1;}
	;
complete:	'(' DEFOBJECT CONSTANT COLEQ term ')'
                {objconst *o=new objconst($3); 
		 $$=new objectdef(o,$5);}
	|	'(' DEFFUNCTION CONSTANT '(' indvarseq ')' COLEQ term ')'	
                {funconst *f=new funconst($3); 
		 $$=new functiondef(f,$5,$8);}
	|	'(' DEFRELATION CONSTANT '(' indvarseq ')' COLEQ sentence ')'	
                {relconst *r=new relconst($3); 
		 $$=new relationdef(r,$5,$8);}
	;
partial:	'(' DEFOBJECT CONSTANT ')'				
                {objconst *o=new objconst($3); 
		 $$=new objectdef(o,(term *) kifobj::nullmarker);}
	|	'(' DEFFUNCTION CONSTANT '(' indvarseq ')' ')'	        
                {funconst *f=new funconst($3); 
		 $$=new functiondef(f,$5,(term *) kifobj::nullmarker);}
	|	'(' DEFRELATION CONSTANT '(' indvarseq ')' ')'	        
                {relconst *r=new relconst($3); 
		 $$=new relationdef(r,$5,(sentence *) kifobj::nullmarker);}
	;
sentenceseq	:	sentence		{$$=new sequence($1);}
		|	sentenceseq sentence	{$1->add($2);$$=$1;}
		;
sentence	:	equation		{$$=$1;}
		|	inequality		{$$=$1;}
		|	logsent			{$$=$1;}
		|	quantsent		{$$=$1;}
		|	logconst		{$$=$1;}
		|	relsent			{$$=$1;}
		;
equation	:	'(' EQ term term ')'		
                        {$$=new equation($3,$4);}
		;
inequality	:	'(' NOTEQ term term ')'		
                        {$$=new inequality($3,$4);}
		;
logsent	:	'(' NOT sentence ')'			
                {$$=new negation($3);}
	|	'(' AND sentenceseq ')'			
                {$$=new conjunction($3);}
	|	'(' OR sentenceseq ')'			
                {$$=new disjunction($3);}
	|	'(' IMPLIES sentenceseq sentence ')'	
                {$$=new implication($3,$4);}
	|	'(' IMPLIED sentence sentenceseq ')'	
                {$$=new implication($4,$3);}
	|	'(' EQUIV sentence sentence ')'		
                {$$=new equivalence($3,$4);}
	;
quantsent	:	'(' FORALL INDVAR sentence ')'   
                        {indvar *iv=new indvar($3);
			 sequence *t=new sequence(iv);
			 $$=new universent(t,$4);}
		|	'(' FORALL '(' indvarseq ')' sentence ')'   
                        {$$=new universent($4,$6);}
		|	'(' EXISTS INDVAR sentence ')'	 
                        {indvar *iv=new indvar($3); 
			 sequence *t=new sequence(iv);
			 $$=new existensent(t,$4);}
		|	'(' EXISTS '(' indvarseq ')' sentence ')'	
                        {$$=new existensent($4,$6);}
		;
relsent	:	'(' CONSTANT termseq ')'	
                {relconst *rel=new relconst($2); 
		 $$=new relsent(rel,$3);}
	|	'(' CONSTANT ')'		
                {relconst *rel=new relconst($2); 
		 $$=new relsent(rel,(sequence *) kifobj::nullmarker);}
	|	'(' TRUE termseq ')'		
                {relconst *rel=new relconst($2); 
                 $$=new relsent(rel,$3);}
	;
termseq	:	SEQVAR  		
                {seqvar *e = new seqvar($1); 
		 $$=new sequence(e);}
        |	term			
                {$$=new sequence($1);}
        |	termseq SEQVAR		
                {seqvar *e = new seqvar($2); 
		 $1->add(e); $$=$1;}
        |	termseq term		
                {$1->add($2); $$=$1;}
	;
term	:	INDVAR			{$$ = new indvar($1);}
	|	CONSTANT		{$$ = new objconst($1);}
	|	STRING			{$$ = new string($1);}
	|	NUMBER			{$$ = new number($1);}
	|	functerm		{$$ = $1;}
	|	listterm		{$$ = $1;}
	|	setterm			{$$ = $1;}
	|	logterm			{$$ = $1;}
	|	quoterm			{$$ = $1;} 
	|	quanterm 		{$$ = $1;} 
	;
functerm	:	'(' CONSTANT termseq ')'	
                        {funconst *c=new funconst($2);
			 $$ = new functerm(c,$3);}
		|	'(' CONSTANT ')'		
                        {funconst *c=new funconst($2);
			 $$ = new functerm(c,(sequence *) kifobj::nullmarker);}
		;
listterm	:	'(' LISTOF ')'		                
                        {$$ = new listterm((sequence *) kifobj::nullmarker);}
		|	'(' LISTOF termseq ')'			
                        {$$ = new listterm($3);}
		;
setterm		:	'(' SETOF  ')'			        
                        {$$ = new setterm((sequence *) kifobj::nullmarker);}
		|	'(' SETOF termseq ')'			
                        {$$ = new setterm($3);}
		;
quoterm		:	'(' QUOTE term ')'	 	        
                        {$$ = new quoterm($3);}
		|	'(' QUOTE sentence ')'		        
                        {$$ = new quoterm($3);}
		|	'(' QUOTE rule ')'	                
                        {$$ = new quoterm($3);}
		|	'(' QUOTE operator ')'	                
                        {$$ = new quoterm($3);}
		|	'(' QUOTE definition ')'	        
                        {$$ = new quoterm($3);}
		; 
logterm		:	'(' IF sentence term ')'		
                        {$$ = new ifterm($3,$4,(term *) kifobj::nullmarker);}
		|	'(' IF sentence term term ')'		
                        {$$ = new ifterm($3,$4,$5);}
		;
indvarseq	:	INDVAR			
                        {indvar *iv=new indvar($1);
			 $$=new sequence(iv);}
		|	indvarseq INDVAR	
                        {indvar *iv=new indvar($2);
                         $1->add(iv);$$=$1;}
		;
logconst:	TRUE		{$$ = new logconst((unsigned) 1);}
	|	FALSE		{$$ = new logconst((unsigned) 0);}
	;
quanterm:	'(' SETOFALL term sentence ')'	 
                {$$ = new setofallterm($3,$4);}
		; 
express	:	word	{$$ = $1;}
	|	list	{$$ = $1;}
	;
list	:	'(' ')'	    {$$ = new list((sequence *) kifobj::nullmarker);}
	|	'(' sequence ')'	{$$ = new list($2);}
/*	|	'(' SEQVAR ')'
       	|	'(' sequence SEQVAR ')'	*/
	;
word	:	CONSTANT	{$$ = new ukconst($1);}
  	|	INDVAR		{$$ = new ukconst($1);}
	|	STRING		{$$ = new ukconst($1);}
	|	NUMBER		{$$ = new ukconst($1);}
	|	operator	{$$ = $1;}
	;
sequence:	express			{$$=new sequence($1);}
	|	sequence express	{$1->add($2);$$=$1;}
	;
operator:	termop		{$$ = $1;}
	|	sentop		{$$ = $1;}
	|	ruleop 		{$$ = $1;}
	|	defop  		{$$ = $1;}
	;
defop	:	DEFOBJECT	{$$ = new defop($1);}
	|	DEFFUNCTION	{$$ = new defop($1);}
	|	DEFRELATION	{$$ = new defop($1);}
	|	COLEQ		{$$ = new defop($1);}
	|	COLEQLT		{$$ = new defop($1);}
	|	COLAMP		{$$ = new defop($1);}
	; 
termop	:	LISTOF		{$$ = new termop($1);}
	|	SETOF		{$$ = new termop($1);}
	|	QUOTE		{$$ = new termop($1);}
	|	QUOTESYM	{$$ = new termop($1);}
	|	IF 		{$$ = new termop($1);}
	|	COND		{$$ = new termop($1);}
	|	SETOFALL	{$$ = new termop($1);}
	|	KAPPA		{$$ = new termop($1);}
	|	LAMBDA 		{$$ = new termop($1);}
	;
sentop	:	EQ		{$$ = new sentop($1);}
	|	NOTEQ		{$$ = new sentop($1);}
	|	NOT		{$$ = new sentop($1);}
	|	AND		{$$ = new sentop($1);}
	|	OR		{$$ = new sentop($1);}
	|	IMPLIES		{$$ = new sentop($1);}
	|	IMPLIED		{$$ = new sentop($1);}
	|	EQUIV		{$$ = new sentop($1);}
	|	FORALL		{$$ = new sentop($1);}
	|	EXISTS		{$$ = new sentop($1);}
	;

ruleop	:	RULELR		{$$ = new ruleop($1);}
	|	RULERL		{$$ = new ruleop($1);}
	|	CONSIS		{$$ = new ruleop($1);}
	; 
%%

void yyerror(char *s)

{
	fprintf( stderr, "%s\n",s );
}