package parser;

import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.InputStream;
import java.net.URL;
import java.util.LinkedList;

import verifier.LogicSolver;

public class LogicNodeParser<Node extends LogicSolver> {

	/*
	 * Simple Logic Node Parser
	 * 
	 *    Syntax is based on Prolog implementation of LITE verifier, but
	 *    it is not an operator order grammer parser. Currently we use
	 *    object comparison, but it is better to use id, because we can
	 *    use switch statements.
	 *    
	 *    Tokenize is done by Scanner. Nested parsing (necesssary for macro
	 *    expansion) is done by scanner.push()/pop().
	 *    
	 *    Scope is handled by association linked list based scope. Use scope.push()/pop()
	 *    and scope.getLocalName(s).
	 *    
	 *    All nodes are created by logicnNodeFactory. In order to handle various
	 *    logic, constructed Node is parameterized.
	 *    
	 *               2007/12 Shinji Kono
	 */
	
	public LogicNodeFactoryInterface<Node> logicNodeFactory;
	public LogicNodeScanner<Node> scanner;
	public Dictionary<Node> dict;
	public LogicNodeScope<Node> scope;
	public int position;
	public int end;
	public Token<Node> nextToken;
	private ExecutorInterface<Node> exec = new NullExecutor<Node>();

	public LogicNodeParser() {
		super();
		initialize();
	}

	public LogicNodeParser(String string, LogicNodeFactoryInterface<Node> lf) {
		super();
		logicNodeFactory = lf;
		initialize();
		scanner.set(string);
	}

	public void initReservedWord() {
		dict.reserve(",",TokenID.And);
		dict.reserve(";",TokenID.Or);

		dict.reserve("(",TokenID.Paren);
		dict.reserve(")",TokenID.CloseParen);
		dict.reserve("{",TokenID.CurParen);
		dict.reserve("}",TokenID.CloseCurParen);
		dict.reserve("[",TokenID.BParen);
		dict.reserve("]",TokenID.CloseBParen);
		dict.reserve("~",TokenID.Not);
		dict.reserve(".",TokenID.Period);
		dict.reserve("?",TokenID.Question);
		dict.reserve(":",TokenID.Colon);
		dict.reserve("exists",TokenID.Exists);
		dict.reserve("true",TokenID.True);
		dict.reserve("false",TokenID.False);
	}

	public void initialize() {
		dict = new Dictionary<Node>();
		scope = new LogicNodeScope<Node>(null,dict);
		initReservedWord();
		scanner = new LogicNodeScanner<Node>(dict);
	}

	public Node parse() {
		if (scanner==null) return null;
		nextToken();
		return expr1();
	}

	public Node parse(String exp) {
		Node n;
		scanner = scanner.pushScanner(exp);
		n = parse();
		scanner = scanner.popScanner();
		nextToken = scanner.nextToken;
		return n;
		
	}

	public void parseFile(String file) {
		try {
			scanner = scanner.pushScannerFile(file);
		} catch (FileNotFoundException e) {
			error("Can't open "+file);
			return;
		}
		doParse();
	}
	
	public void parse(InputStream file) {
		scanner = scanner.pushScannerFile(file,null);
		doParse();
	}

	public void parse(InputStream in, String prompt) {
		scanner = scanner.pushScannerFile(in,prompt);
		doParse();
	}
	
	public Node doParse() {
		Node n;
		do {
			n=parse();
			exec.verify(n);
		} while(scanner.hasRemaining());
		scanner = scanner.popScanner();
		nextToken = scanner.nextToken;
		return n;
	}

	public Node expr1() {
	    Node n = expr2();
		while(nextToken.type == TokenID.Or) {
			nextToken();
			n = logicNodeFactory.orNode(n, expr2());
		}
		return n;
	}

	public Node expr2() {
		Node n = expr3();
		while(nextToken.type == TokenID.And) {
			nextToken();
			n = logicNodeFactory.andNode(n, expr3());
		}
		return n;
	}

	public Node expr3() {
		if (nextToken.type==TokenID.Not) {
			nextToken();
			return logicNodeFactory.notNode(expr3());
		} else if (nextToken.type==TokenID.Exists) {
			return quantifier();
		}
		return expr4();
	}

	/*
	 * exists(x,(x,a))
	 *      this operator has a local scope
	 */
	public Node quantifier() {
		LinkedList<Node> arg;
		nextToken();
		if (nextToken.type==TokenID.Paren) {
			// symbolc x havs been already converted to a variable when it was
			// evaluated as a macro argument. We cannot make it local here.
			// Do it in exists evaluation. 
			nextToken();
			arg = arguments();
			if (arg.size()!=2 /* || !arg.get(0).isVariable() */) {
				error("bad quantifier");
				return logicNodeFactory.trueNode();
			}
			return logicNodeFactory.existsNode(arg.get(0),arg.get(1));
		} else {
			error("( expected");
			return logicNodeFactory.trueNode();
		}
	}

	public Node expr4() {
		Node n = term();
		if (nextToken.type==TokenID.Paren) {
			// predicate ( or macro )
			nextToken();
			n = logicNodeFactory.predicateNode(n,arguments());
		}
		return n;
	}

	protected LinkedList<Node> arguments() {
		Node n;
		LinkedList<Node> arg = new LinkedList<Node>();
		while(nextToken.type!=TokenID.CloseParen) {
			n = expr3();
			arg.add(n);
			if (nextToken.type == TokenID.And)
				nextToken();
		}
		if (nextToken.type==TokenID.CloseParen) nextToken();
		else {
			scanner.error(") expected");
		}
		return arg;
	}

	protected Node term() {
		Node n = null;
		switch (nextToken.type) {
		case Paren:
			nextToken();
			n = expr1();
			if (nextToken.type==TokenID.CloseParen) {
			} else { // syntax error;
				scanner.error(") expected but got "+nextToken);
				return logicNodeFactory.trueNode();
			}
			break;
		case CurParen:
			nextToken();
			n = expr1();
			if (nextToken.type==TokenID.CloseCurParen) {
			} else { // syntax error;
				scanner.error("} expected");
			}
			break;
		case NUMBER:
			n = logicNodeFactory.numberNode(Integer.parseInt(nextToken.name));
			break;
		case True:
			n = logicNodeFactory.trueNode();
			break;
		case False:
			n = logicNodeFactory.falseNode();
			break;
		case NULL: case Period:
			break;
		default:
			if (nextToken.type.isVariable()) 
				n = makeVariable(nextToken);
			else {
				// error("Internal ununderstandable term '"+nextToken+"' type: "+nextToken.type+".");
				n = makeVariable(nextToken); // skip any
			}
		}
		nextToken();
		return n;
	}
	/*
	 * All names in LogicNode are variables. A token represents
	 * name. To get the variable, use this method.
	 */
	protected Node makeVariable(Token<Node> t) {
		Node n;
		if ((n=t.value())==null) {
			n =  logicNodeFactory.variableNode(t.realName(),true);
			t.setValue(n);
		}
		// n.token = t;
		return n;
	}

	/*
	 * Syntactical Short cut for scanner.textToken()
	 * 
	 * It never returns null, to check EOF, 
	 *     nextToken.type==TokenID.NULL
	 */
	public Token<Node> nextToken() {
		return nextToken = scanner.nextToken();
	}

	public void setExecutor(ExecutorInterface<Node> exec) {
		this.exec = exec;
	}

	public boolean getResource(String filename) {
		System.out.println("try to get resource ... "+filename);
		try {
			URL rsrc = getClass().getResource(filename);
			if (rsrc==null) throw new IOException();
			InputStream in = rsrc.openStream();
			parse(in);
			System.out.println("done.");
			return true;
		} catch (IOException e) {
			System.out.println("failed.");
			return false;
		}
	}

	public void showResourceFile(String file) {
		try {
			InputStream in;
			in = getClass().getResourceAsStream("/"+file);
			if (in==null) {
				in = new FileInputStream(file);
			}
			byte[] buf = new byte[4096];
			for(int len; (len=in.read(buf,0,4096))>0;) {
				System.out.write(buf,0,len);
			}
		} catch (IOException e) {
		}
	}
	
	public void error(String err) {
		scanner.error(err);
	}


	
}