/*----------------------------------------------------------------------------*/
/* Truth table evaluator                                                      */
/* LOG32LLC Assignment 4                                                      */
/* Sten M. Andersen                                                           */
/*                                                                            */
/* used and truevars are sets representing the used and true atoms of the     */
/* formula, where 'a' is 1, b, is 10, c is 100 and so on                      */
/*                                                                            */
/*----------------------------------------------------------------------------*/

#include <stdio.h>
#include <setjmp.h>
#include <string.h>


#define MAX_TOKEN_STRING_LENGTH     200
#define MAX_BUFF                    200
#define MAX_CODE					200
#define MAX_OUTPUT_BUFF				200

typedef enum 
{
	false,
	true
} BOOL;

/*----------------------------------------------------------------------------*/
/* Globals                                                                    */
/*----------------------------------------------------------------------------*/

char ch;							 // The next character
BOOL cont, debug, min, showcode;  	   	   	    
jmp_buf start;	     	 			 // On error: empty stack and go to start

BOOL exists_false, exists_true;		 // For the synopsis

// Input buffer stuff
char buff[ MAX_BUFF ];			     // Input buffer storage
char opvalues[ MAX_BUFF ];			 // Truth value of each opeator in formula
int  opindex[ MAX_BUFF ];		     // Cross-index of operators infix/postfix
int bufferpointer;                   // Keep a count, so we can point to error

// Output buffer
char obuff[ MAX_OUTPUT_BUFF ];
int obuffpointer;

int used, truevars;                  // Sets					 
char code[MAX_CODE];				 // Code to be evaluated
int codeindex;

// This idea for how to extract tokens is from
// Mak, R. (1991). Writing compilers and interpreters. An applied approach.
// Brisbane: John Wiley & Son, Inc;
char token_string[MAX_TOKEN_STRING_LENGTH]; // Token string
char *tokenp = token_string;				// Token string pointer

/*----------------------------------------------------------------------------*/
/* Function declarations                                                      */
/*----------------------------------------------------------------------------*/

void factor();
void term();
void expression();
void formula();
int gen( char c );

void get_token();
void get_word();
void get_char();

void printoutputbuffer();
void printinputbuffer();
void printopvalues();
void printresult(BOOL r);
void printused();
void printcode();
void output();

void error( char* e );

// Helper functions
BOOL in( char element, int set );	// Is element represented in set?
BOOL atom( char c );				// Is c an atom?

/*----------------------------------------------------------------------------*/
/* Application logic                                                          */
/*----------------------------------------------------------------------------*/

void factor() {
	int bp;
	if ( atom( ch ) ) {
		// put ch into the set of used atoms
		used = used | (1 << ch - 'a');
		gen( ch );
		get_token();
	} else 
		switch ( ch ) {
			case '-':
				bp = bufferpointer-1;
				get_token();
				formula();
				opindex[ bp ] = gen( 'N' );
				break;
			case '(':
				get_token();
				formula();
				if ( ch != ')' ) error("Expected ) at end of formula.");
				get_token();
				break;
			default:
					error("Atom a..z, -, or \( expected.");
		}
}

void term() {
	factor();
	while ( ch == '&' ) {
		int bp = bufferpointer-1;
		get_token();
		factor();
		opindex[ bp ] = gen( 'K' );
	}	
}	

void expression() {
	term();
	while ( ch == 'v' ) {
		int bp = bufferpointer-1;
		get_token();
		term();
		opindex[ bp ] = gen( 'A' );
	}
}

void formula() {
	char c;
	expression();
	if ( ch == '>' || ch == '=' ) {
		int bp = bufferpointer-1;
		c = ch;
		get_token();
		formula();
		if      ( c == '=' ) opindex[ bp ] = gen( 'E' );
		else if ( c == '>' ) opindex[ bp ] = gen( 'C' );	   	   
	}
}

int gen( char c ) {
	code[ ++codeindex ] = c;
	return codeindex;
}

BOOL val() {
	int x, 
		t = -1;			// top of stack
	BOOL s[100];		// stack
	
	for ( x = 0; x <= codeindex; x++ ) {
		if ( atom( code[ x ] ) ) {
			t++; 
			s[ t ] = in( code[ x ], truevars );
		} else {
			switch ( code[ x ] ) {
				case 'A':
					t--;
					s[ t ] = s[ t ] || s[ t+1 ];
					break;
				case 'C':
					t--;
					s[ t ] = s[ t ] <= s[ t+1 ];
					break;
				case 'E':
					t--;
					s[ t ] = s[ t ] == s[ t+1 ];
					break;
				case 'K':
					t--;
					s[ t ] = s[ t ] && s[ t+1 ];
					break;
				case 'N':
					s[ t ] = ! s[ t ];
					break;
				default:
					error("Unexpected error in val()");	   
			}
			int i;
			for (i = 0; i < bufferpointer; i++) {
				/* de-reference the op-values, so they can be printed
				   underneath the operators                           */
				if ( opindex[ i ] == x ) opvalues[ i ] = s[ t ] + '0';
			}
		}
	}
	return s[ t ];
}

void table( char v ) {
	while ( ! ( in( v, used ) ) ) v++;
	if ( v <= 'z' ) {
		int tv = truevars;
		truevars = truevars | ( 1 << v - 'a' );
		table( v+1 );
		truevars = tv;
		table( v+1 );
	} else {
		/* output current values and compute and output values of 
		   (postfix version of) formula */
		char c;
		for ( c = 'a'; c <= 'z'; c++ )
			if ( in ( c, used ) ) {
				obuff[ obuffpointer ] = '0' + in( c, truevars );
				obuffpointer+=2;
			}
		BOOL v = val();
		printopvalues();
		printresult( v );
		
		// Prepare for synopsis
		if ( v ) exists_true = true; else exists_false = true;
		
		obuff[ obuffpointer++ ] = '\n'; 
		printoutputbuffer(); 
		obuffpointer = 0;
	}
}

/*----------------------------------------------------------------------------*/
/* Helper functions, just for code readability                                */
/*----------------------------------------------------------------------------*/
BOOL atom( char c ) {
	return ( c >= 'a' && c <= 'z' ) ? 1 : 0;
}

// returns true if the element's representation is in the set
BOOL in( char element, int set ) {
	return ( set & ( 1 << element - 'a' ) ) ? 1 : 0;
}

/*int size( int set ) {
	char c; int s = 0;
	for ( c = 'a'; c < 'z'; c++ ) if ( in( c, set ) ) s++;
	return s;
}*/

/*----------------------------------------------------------------------------*/
/* Character routines                                                         */
/*----------------------------------------------------------------------------*/

void get_char() {  // Gets char into ch and skips blanks 
	ch = getchar();
	if ( !isprint( ch ) ) ch = ' ';
	if ( bufferpointer < MAX_BUFF ) 
		buff[ bufferpointer++ ] = ch;
	else error( "TOO_LONG_INPUT" );
}

void skip_blanks() {
	do { 
		get_char();
	} while ( ch == ' ');
}

void get_token() {
	skip_blanks();
	tokenp = token_string;
	if ( isupper( ch ) ) get_word();
}

void get_word() {
	while ( isupper( ch )  ) {
		*tokenp++ = ch;
		get_char();
	}

	*tokenp = '\0';
	
	/* The decrementing of bufferpointer is sort off an odd hack ;-)
	   It makes error messages ugly when WORDS have been used
	   instead of the character-operators. But it works.           */
	if ( strcmp( token_string, "AND") == 0 )  
		{ ch = '&'; bufferpointer-=4; buff[ bufferpointer++ ] = ch; }
	if ( strcmp( token_string, "OR" ) == 0 )
		{ ch = 'v'; bufferpointer-=3; buff[ bufferpointer++ ] = ch; }
	if ( strcmp( token_string, "NOT") == 0 )
		{ ch = '-'; bufferpointer-=4; buff[ bufferpointer++ ] = ch; }
	if ( strcmp( token_string, "IMP") == 0 )
		{ ch = '>'; bufferpointer-=4; buff[ bufferpointer++ ] = ch; }
	if ( strcmp( token_string, "IFF") == 0 ) 
		{ ch = '='; bufferpointer-=4; buff[ bufferpointer++ ] = ch; }
}

/*----------------------------------------------------------------------------*/
/* Printing routines                                                          */
/*----------------------------------------------------------------------------*/

void synopsis() {
	if ( exists_false )
		if ( exists_true )
			printf("Contingent\n\n");
		else
			printf("Self-contradictory\n\n");
	else
		printf("Tautology\n\n");
}

void output() { 
	printcode();
	printinputbuffer();
	printused();
	table('a');							  // do table
	synopsis();							  // print synopsis
}

void printcode() {
	if ( showcode ) {
		int i;
		printf("Code: ");
		for ( i = 0; i <= codeindex; i++ ) 
			printf("%c", code[ i ]);
		printf("\n");
	}	
}

void printused() {
	if ( !min ) {
		char u;
		printf("   ");
		for ( u = 'a'; u <= 'z'; u++ )
			if ( in( u, used ) ) printf("%c ", u); 
	printf("\n");
	}
}

void printinputbuffer() {
	if ( !min ) printf("%s", buff );
}

void printoutputbuffer() {
	if ( !min ) {
		printf("  ");
		int i;						
		for ( i = 0; i < obuffpointer; i++ )
			printf( "%c", obuff[ i ] );
	}
}

void printopvalues() {
	if ( !min ) {
		int i;
		for ( i = 0; i < bufferpointer; i++ )
			printf( "%c", opvalues[ i ] );
	}
}

void printresult(BOOL r) {
	if ( !min ) printf("%c", r + '0' );
}

void test() {
	// only prints out the int-values
	printf("used: %d\n", used);			
	printf("truevars: %d\n", truevars);
	
	printcode();
}

/*----------------------------------------------------------------------------*/
/* Print out error                                                            */
/*----------------------------------------------------------------------------*/

void print_blanks( int n ) {
	int i;			// There must be a better way, .e.g., a format-thingy
	for ( i = 0; i < n; i++ )
		printf(" ");
}

void error(char* e) {
	printf( "\n%s\n", e );
	printf("%s\n", buff );		     // print input buffer
	print_blanks( bufferpointer-1 ); // Better way?
	printf( "^\n" );
	fflush( stdin );;
	longjmp( start, 0 );
}

/*----------------------------------------------------------------------------*/
/* Initialise                                                                 */
/*----------------------------------------------------------------------------*/

void init() {
	exists_false = exists_true = false;
	cont = true;
	codeindex = -1;
	used = truevars = 0;
	used = used | ( 1 << ( 'z' - 'a' + 1 ) );		// add sentinel to used
	
	bufferpointer = obuffpointer = 0;
	
	int i;
	for ( i = 0; i < MAX_BUFF; i++ ) {
			opvalues[ i ] = ' ';
			opindex[ i ]  = -1;
			buff[ i ]     = NULL;
	}
	
	for ( i = 0; i < MAX_OUTPUT_BUFF; i++ ) {
		obuff[ i ]    = ' ';
	}	 
}

/*----------------------------------------------------------------------------*/
/* Clean up                                                                   */
/*----------------------------------------------------------------------------*/

void clean_up() {}

/*----------------------------------------------------------------------------*/
/* Main                                                                       */
/*----------------------------------------------------------------------------*/

int main(int argc, char **argv) {  
	min = debug = showcode = false; 
	int i;	// parse commands
	for ( i = 0; i < argc; i++ ) {
		switch( toupper( argv[i][0] ) ) {
			case 'M': min      = true; break;
	 		case 'D': debug    = true; break;
			case 'C': showcode = true; break;
		}
	}
	setjmp( start );
	do {
		init();
		get_token();			// one token look-ahead
		formula();	   	   
		if ( ch != '.' ) error("Unexpected end of formula. Expected '.'"); 
		output();
		if ( debug ) test();
	} while ( cont );
	clean_up();
	return (0);
}


/*


*/