import java.io.*;
import com.mw.SystemInput;


// Logik og sprog, Modul 2, datalogi RUC      Henning Christiansen
//
// 
// En fortolker for Datalog i Java
//
// Appendix B i "Sprog og abstrakte maskiner"
//
// (c) 2000, Henning Christiansen


// Tak til Keld Helsgaun for at have skrevet dette program
// om fra Simula til Java!

//*********************************************
//   S y n t a x   o f   D a t a l o g
// *********************************************;


abstract class CATEGORY {
    // The class of syntactic objects in
    // the Datalog programming language
  	abstract void read(LEXICAL_SCANNER source);
  	abstract void pretty_print();
  	abstract CATEGORY new_copy(int level);
   	//the latter used by the interpreter;
}


class PROGRAM extends CATEGORY {
 	// Datalog programs

    // A list of CLAUSEs
    CLAUSE first;
    PROGRAM rest;

   	void read(LEXICAL_SCANNER source) {
   		first = new CLAUSE(); first.read(source);
      	if (!(source.look_ahead instanceof END_OF_FILE))
     		{ rest = new PROGRAM(); rest.read(source); }
   	}

    void pretty_print() {
   		first.pretty_print();
      	if (rest != null)
        	rest.pretty_print();
   	}

  	CATEGORY new_copy(int level) { return null; }

}

class CLAUSE extends CATEGORY {

	// Datalog clauses;

   	GOAL head;
   	GOAL_LIST body; // Empty body signifies a fact

    void read(LEXICAL_SCANNER source) {
      	head = new GOAL(); head.read(source);
     	if (source.look_ahead instanceof COLON_DASH) {
            source.read_symbol();
            body = new GOAL_LIST();
            body.read(source);
       	}
       	else if (!(source.look_ahead instanceof PERIOD))
      		throw new RuntimeException(":- or . expected");
      	if (source.look_ahead instanceof PERIOD)
       		source.read_symbol();
       	else
      		throw new RuntimeException(":- or . expected");
   	}

    void pretty_print() {
    	System.out.println();
      	head.pretty_print();
      	if (body != null)
        	{ System.out.print(":-"); body.pretty_print(); }
      	System.out.print(".");
  	}

   	// The following used by the interpreter

  	CATEGORY new_copy(int level) {
    	CLAUSE cl = new CLAUSE();
      	cl.head = (GOAL) head.new_copy(level);
      	cl.body = body == null ? null : (GOAL_LIST) body.new_copy(level);
      	return cl;
   	}

}


class GOAL extends CATEGORY {

    // Datalog goals

    ATOM predicate;
    ARGUMENT_LIST parameters;

    void read(LEXICAL_SCANNER source) {
      	predicate = new ATOM();
      	predicate.read(source);
      	if (source.look_ahead instanceof BEGIN_PAR)
        	source.read_symbol();
      	else
      		throw new RuntimeException("( expected");
      	parameters = new ARGUMENT_LIST();
      	parameters.read(source);
      	if (source.look_ahead instanceof END_PAR)
        	source.read_symbol();
      	else
      		throw new RuntimeException(") expected");
   	}

    void pretty_print() {
      	predicate.pretty_print();
      	System.out.print("(");
      	parameters.pretty_print();
      	System.out.print(")");
   	}

    // The following used by the interpreter

    CATEGORY new_copy(int level) {
      	GOAL g = new GOAL();
      	g.predicate = (ATOM) predicate.new_copy(level);
      	g.parameters = (ARGUMENT_LIST) parameters.new_copy(level);
     	return g;
   	}

}


class GOAL_LIST extends CATEGORY {

   	GOAL first;
   	GOAL_LIST rest;

    void read(LEXICAL_SCANNER source) {
      	first = new GOAL();
      	first.read(source);
      	if (source.look_ahead instanceof COMMA) {
          	source.read_symbol();
          	rest = new GOAL_LIST();
          	rest.read(source);
       	}
   	}

    void pretty_print() {
    	System.out.println();
    	System.out.print("    ");
      	first.pretty_print();
      	if (rest != null) {
          	System.out.print(",");
          	rest.pretty_print();
       	}
  	}

  	// The following used by the interpreter

   	CATEGORY new_copy(int level) {
      	GOAL_LIST gl = new GOAL_LIST();
      	gl.first = (GOAL) first.new_copy(level);
      	gl.rest = rest == null ? null : (GOAL_LIST) rest.new_copy(level);
     	return gl;
   	}

}


abstract class ARGUMENT extends CATEGORY {

  	// Arguments in Datalog goals

   	// The following used by the interpreter
   	abstract boolean equal(ARGUMENT arg);

   	// An ATOM or a VARIABLE
}


class ARGUMENT_LIST extends  CATEGORY {

  	ARGUMENT first;
   	ARGUMENT_LIST rest;

    void read(LEXICAL_SCANNER source) {
    	if (source.look_ahead instanceof ATOM_LEX) {
            first = new ATOM();
            first.read(source);
       	}
       	else if (source.look_ahead instanceof VARIABLE_LEX) {
            first = new VARIABLE();
            first.read(source);
      	}
      	else
      		throw new RuntimeException("argument expected");
      	if (source.look_ahead instanceof COMMA) {
          	source.read_symbol();
          	rest = new ARGUMENT_LIST();
          	rest.read(source);
      	}
  	}

    void pretty_print() {
      	first.pretty_print();
      	if (rest != null) {
          	System.out.print(", ");
          	rest.pretty_print();
       	}
   	}

    // The following used by the interpreter

   	CATEGORY new_copy(int level) {
      	ARGUMENT_LIST al = new ARGUMENT_LIST();
      	al.first = (ARGUMENT) first.new_copy(level);
      	al.rest = rest == null ? null : (ARGUMENT_LIST) rest.new_copy(level);
      	return al;
   	}

}


class ATOM extends ARGUMENT {;

 	// Atomic constant in Datalog

    String id;

   	void read(LEXICAL_SCANNER source) {
      	if (source.look_ahead instanceof ATOM_LEX)
        	id = ((ATOM_LEX) source.read_symbol()).lex;
      	else
      		throw new RuntimeException("atom expected");
   	}

    void pretty_print() {
      	System.out.print(id);
   	}

   	// The following used by the interpreter

    boolean equal(ARGUMENT arg) {
    	return arg instanceof ATOM && id.equals(((ATOM) arg).id);
   	}

    CATEGORY new_copy(int level) {
      	ATOM atm = new ATOM();
      	atm.id = id;
      	return atm;
   	}

}


class VARIABLE extends ARGUMENT {

  	// Variables in Datalog

    String id;

    void read(LEXICAL_SCANNER source) {
    	if (source.look_ahead instanceof VARIABLE_LEX)
        	id = ((VARIABLE_LEX) source.read_symbol()).lex;
      	else
      		throw new RuntimeException("variable expected");
   	}

    void pretty_print() {
     	System.out.print(id);
      	if (level != 0) {
          	System.out.print("/");
          	System.out.print(level);
       	}
  	}

    // The following used by the interpreter

    int level;

    boolean equal(ARGUMENT arg) {
   		return arg instanceof VARIABLE
               && id.equals(((VARIABLE) arg).id)
               && level == ((VARIABLE) arg).level;
  	}

    CATEGORY new_copy(int level) {
   		VARIABLE v = new VARIABLE();
      	v.level = level;
      	v.id = id;
      	return v;
   	}

}


class QUERY extends CATEGORY {

    // Query in Datalog

   	GOAL_LIST goals;

    void read(LEXICAL_SCANNER source) {
      	goals = new GOAL_LIST();
      	goals.read(source);
      	if (!(source.look_ahead instanceof PERIOD))
      		throw new RuntimeException(". expected");
      	else source.read_symbol();
   	}

    void pretty_print() {
      	goals.pretty_print();
      	System.out.println(".");
   	}

	CATEGORY new_copy(int level) { return null; }

}


//***************************************************************
//  L e x i c a l   s y n t a x   f o r  D a t a l o g
//***************************************************************


class LEXICAL_SYMBOL {
  	// The smallest syntactically and semantically
    //  significant objects
}

class ATOM_LEX extends LEXICAL_SYMBOL {
   	// The lexical symbol denoting an ATOM
	String lex;

  	ATOM_LEX(String lex) {this.lex = lex; }
}

class VARIABLE_LEX extends LEXICAL_SYMBOL {
   	// The lexical symbol denoting a VARIABLE

   	String lex;

  	VARIABLE_LEX(String lex) {this.lex = lex; }
}

class COLON_DASH extends LEXICAL_SYMBOL {
   	// The symbol ":-"
}

class COMMA extends LEXICAL_SYMBOL {
   	// The symbol ","
}

class PERIOD extends LEXICAL_SYMBOL {
   	// The symbol "."
}

class BEGIN_PAR extends LEXICAL_SYMBOL {
   	// The symbol "("
}

class END_PAR extends LEXICAL_SYMBOL {
   	// The symbol ")"
}

class END_OF_FILE extends LEXICAL_SYMBOL {
   	// Signals the end of a Datalog program file
}


//*****************************************
//  T h e   l e x i c a l   s c a n n e r
//*****************************************


class LEXICAL_SCANNER {

   	LEXICAL_SYMBOL look_ahead;
    char character_look_ahead;
    FileReader file;
    boolean endfile;

    LEXICAL_SCANNER(String file_name) {
    	try {
    		file = new FileReader(file_name);

    		// Initialize look_ahead:
    		character_read();
   			read_symbol();
    	}
    	catch (Exception e) {
    		throw new RuntimeException("File error: " + file_name);
    	}
   	}

    char character_read() {
      	char character = character_look_ahead;
      	try {
       		character_look_ahead = (char) file.read();
       		if (character_look_ahead == (char) -1) endfile = true;
       	}
       	catch (IOException e) { endfile = true; }
       	return character;
    }

   	LEXICAL_SYMBOL read_symbol()  {
      	LEXICAL_SYMBOL symbol = look_ahead;
      	// set look_ahead to the next LEXICAL_SYMBOL
      	while (!endfile && Character.isWhitespace(character_look_ahead))
        	character_read();
      	if (endfile) {
        	look_ahead = new END_OF_FILE();
        	return symbol;
        }
     	if ('a' <= character_look_ahead &&
     		character_look_ahead <= 'z') {
         	StringBuffer string = new StringBuffer();
      		while (Character.isLetter(character_look_ahead))
            	string.append(character_read());
          	look_ahead = new ATOM_LEX(new String(string));
      	}
      	else if ('A' <= character_look_ahead &&
              	 character_look_ahead <= 'Z') {
       		StringBuffer string = new StringBuffer();
      		while (Character.isLetter(character_look_ahead))
            	string.append(character_read());
          	look_ahead = new VARIABLE_LEX(new String(string));
      	}
      	else if (character_look_ahead == ',') {
          	look_ahead = new COMMA();
          	character_read();
      	}
      	else if (character_look_ahead == '.') {
          	look_ahead = new PERIOD();
          	character_read();
       	}
      	else if (character_look_ahead == '(') {
          	look_ahead = new BEGIN_PAR();
          	character_read();
       	}
      	else if (character_look_ahead == ')') {
          	look_ahead = new END_PAR();
          	character_read();
       	}
      	else if (character_look_ahead == ':') {
          	character_read();
          	if (character_look_ahead == '-') {
              	character_read();
              	look_ahead = new COLON_DASH();
           	}
        	else
            	throw new RuntimeException("- expected after :");
      	}
      	else throw new RuntimeException("illegal character");
      	return symbol;
 	}

 }

//*********************************
//  T h e   i n t e r p r e t e r
//*********************************

class BINDING_SET {
  	// Bindings of Datalog variables
}

class OK_BINDING_SET extends BINDING_SET {
	OK_BINDING_SET(VARIABLE var, ARGUMENT val, OK_BINDING_SET rest) {
		this.var = var; this.val = val; this.rest = rest;
	}

    VARIABLE var;
    ARGUMENT val;
   	OK_BINDING_SET rest;
}

class EMPTY_BINDING_SET extends OK_BINDING_SET {
   	// An empty or initial binding set
    // Attributes are ignored
    EMPTY_BINDING_SET(VARIABLE var, ARGUMENT val, OK_BINDING_SET rest) {
    	super(var, val, rest);
    }
}

class FAIL extends BINDING_SET {
  	// The result of an unsuccesful matching
}

class Exit extends Exception {}

class Interpreter {
	ARGUMENT dereference(ARGUMENT param, OK_BINDING_SET bindings) {
   	// returns the deepest value of param;
   		if (param instanceof ATOM)
   			return param;
   		if (param instanceof VARIABLE) {
        	OK_BINDING_SET rest_bindings = bindings;
        	while (!(rest_bindings instanceof EMPTY_BINDING_SET))
          		if(rest_bindings.var.equal(param))
            		return dereference(rest_bindings.val, bindings);
        		else rest_bindings = rest_bindings.rest;
       	}
        return param; // uninstantiated
 	}

 	BINDING_SET bind(OK_BINDING_SET old_bindings,
 		             VARIABLE the_var,
 		             ARGUMENT the_val) {
  	// produces an extension of this BINDING_SET,
    // the_var is expected not to be previously bound and
   	// the_val is expected to be an atom or an unbound variable
    	if (the_val instanceof VARIABLE &&
        	((VARIABLE) the_val).equal(the_var))
     		return old_bindings;
    	return new OK_BINDING_SET(the_var, the_val, old_bindings);
    }

  	BINDING_SET unify_goals(GOAL goal1, GOAL goal2,
  		     	            OK_BINDING_SET old_bindings) {
    // Match goal1 and goal2 in old_bindings,
    // producing an extended OK_BINDING_SET or FAIL
    	ARGUMENT_LIST param_list1, param_list2;
    	BINDING_SET current_bindings = null;
    	current_bindings = goal1.predicate.equal(goal2.predicate) ?
                           (BINDING_SET) old_bindings : new FAIL();
    	param_list1 = goal1.parameters;
    	param_list2 = goal2.parameters;
    	while (param_list1 != null && param_list2 != null &&
               !(current_bindings instanceof FAIL)) {
        	current_bindings = unify_arguments(param_list1.first,
                                     param_list2.first,
                                     (OK_BINDING_SET) current_bindings);
        	param_list1 = param_list1.rest;
        	param_list2 = param_list2.rest;
      	}
    	return param_list1 != null || param_list2 != null
                       ? new FAIL() : current_bindings;
  	}

 	BINDING_SET unify_arguments(ARGUMENT arg1, ARGUMENT arg2,
 		                        OK_BINDING_SET old_bindings) {
    	arg1 = dereference(arg1, old_bindings);
    	arg2 = dereference(arg2, old_bindings);
    	if (arg1 instanceof ATOM && arg2 instanceof ATOM)
      		return arg1.equal(arg2) ? (BINDING_SET) old_bindings : new
FAIL();
  		if (arg1 instanceof VARIABLE)
      		return bind(old_bindings, (VARIABLE) arg1, arg2);
      	return bind(old_bindings, (VARIABLE) arg2, arg1);
  	}

  	void print_out_solution(OK_BINDING_SET bindings) throws Exit {
    	OK_BINDING_SET rest_bindings = bindings;
    	while (!(rest_bindings instanceof EMPTY_BINDING_SET)) {
        	if (rest_bindings.var.level == 0) {
           		System.out.print("    ");
            	rest_bindings.var.pretty_print();
            	System.out.print(" = ");
            	dereference(rest_bindings.val, bindings).pretty_print();
            	System.out.println();
       		}
        	rest_bindings = rest_bindings.rest;
   		}
    	System.out.println("yes");
    	while (true) {
    		char answer;
    		DataInputStream input = new DataInputStream(System.in);
    		System.out.println("more solutions? (y/n)");
    		try {
    			answer = input.readLine().charAt(0);
    		}
    		catch(IOException e) { throw new Exit(); }
    		if (answer == 'y')
    			return;
    		if (answer == 'n')
    			throw new Exit();
   		}
   	}

 	void prove(GOAL_LIST list_of_goals, OK_BINDING_SET bindings,
 		       PROGRAM prog, int level) throws Exit {
    	PROGRAM rules_left;
    	if (list_of_goals == null) {
        	print_out_solution(bindings);
        	return;
       	}
   		rules_left = prog;
    	while (rules_left != null) {
        	BINDING_SET bindings1;
        	CLAUSE rule = (CLAUSE) rules_left.first.new_copy(level);
        	rules_left = rules_left.rest;
        	bindings1 = unify_goals(list_of_goals.first, rule.head,
bindings);
        	if (bindings1 instanceof OK_BINDING_SET)
         		prove(append_goals(rule.body, list_of_goals.rest),
         					       (OK_BINDING_SET)
bindings1,
                                   prog, level + 1);
       	}
   	}

  	void execute(QUERY question, PROGRAM prog) {
    // The top-level prove procedure;
    	OK_BINDING_SET initial_state;
    	initial_state = new EMPTY_BINDING_SET(null, null, null);
    	try {
    		prove(question.goals, initial_state, prog, 1);
    	}
    	catch (Exit e) {}
    	System.out.println("no (more) solutions");
   	}

	// ***** Auxiliary method used in the interpreter:

  	GOAL_LIST append_goals(GOAL_LIST goals1, GOAL_LIST goals2) {
  		if (goals1 == null)
  			return goals2;
  		GOAL_LIST result = new GOAL_LIST();
      	result.first = goals1.first;
       	result.rest = append_goals(goals1.rest, goals2);
      	return result;
  	}

}


public class Datalog {

	// ****************
   	//   Main program
 	// ****************

 	public static void main(String[] args) {
		LEXICAL_SCANNER source;
		PROGRAM datalog_program;
		QUERY question;

		System.out.println();
		System.out.print("Reading program from file TESTPROGRAM");
		System.out.flush();
		source = new LEXICAL_SCANNER("testprogram");
	        datalog_program = new PROGRAM();
		datalog_program.read(source);
		datalog_program.pretty_print();

		System.out.println(); System.out.println();
		System.out.print("Reading program from file TESTQUERY");
		System.out.flush();
		source = new LEXICAL_SCANNER("testquery");
		question = new QUERY();
		question.read(source);
		question.pretty_print();

		System.out.println();
		System.out.println("Executing...");

		SystemInput sysin = new SystemInput();
		new Interpreter().execute(question, datalog_program);
		sysin.dispose();
	}
}