package parser;

import java.util.LinkedList;

import verifier.LogicSolver;


public class MacroNodeParser<Node extends LogicSolver>
     extends LogicNodeParser<Node> 
	 implements MacroNodeParserInterface<Node> {

	/*
	 * Logic Node Parser with Macro Expansion
	 *       parser.define("head(var)","body = var");
	 *       "head(x+1)" is replcaed by "body = (x+1)" and parsed
	 *       
	 *  A macro definition is stored in MacroNode. The MacroNode is stored in
	 *  dict by MacroNodeFactory.predicateNode(); MacroNode has to know the parser
	 *  to parse expanded macro. It is possible to parse macro body before expansion,
	 *  but its implementation is sligtly complex.      
	 */
	
	public LogicNodeFactoryInterface<Node> logicNodeFactory;
	
	public MacroNodeParser() {
		super();
	}

	public MacroNodeParser(String str, LogicNodeFactoryInterface<Node> lf) {
		this();
		logicNodeFactory = lf;
		super.logicNodeFactory = logicNodeFactory;
		initialize();
		scanner = scanner.pushScanner(str);
	}
	
	public MacroNodeParser(LogicNodeFactoryInterface<Node> lf) {
		this();
		logicNodeFactory = lf;
		super.logicNodeFactory = logicNodeFactory;
		initialize();
	}

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

	/*
	 *   Recurseive Decent with operator order
	 *      n1 op n2 op2 ...
	 *      
	 *      When the nextToken is a macro, nextToken.type is
	 *      TokenID.VARIABLE, that is nextToken.type.order==1. 
	 *      MacroNode constructor assign the order in Token.order. 
	 *      Don't use Token.type.order.
	 */
	public Node exprM1() {
		return exprM2(expr3());
	}
	
	public Node exprM2(Node n1) {
		while (nextToken.isInfix()) {
			Node op = makeVariable(nextToken);
			LinkedList<Node> arg = new LinkedList<Node>();
			arg.add(n1);
			nextToken();
			Node n2 = expr3();
			if (!nextToken.isInfix()) {
				arg.add(n2);
				return logicNodeFactory.predicateNode(op, arg);
			} 
			if (op.order() > nextToken.order) {    // a + b * 
				arg.add(exprM2(n2));
				return logicNodeFactory.predicateNode(op, arg);
			} else if (op.isxfy() && op.order() == nextToken.order) {  
					arg.add(exprM2(n2));           // a + b *  "xfy" case  (odd order) 
					return logicNodeFactory.predicateNode(op, arg);
			} else {                               // a * b + 
				arg.add(n2);
				n1 = logicNodeFactory.predicateNode(op, arg);
			}
		}
		return n1;
	}


	@Override
	public Node expr3() {
		if (nextToken.type==TokenID.Not) {
			nextToken();
			return logicNodeFactory.notNode(expr3());
		} else if (nextToken.isPrefix()) {
			Node op = makeVariable(nextToken);
			LinkedList<Node> arg = new LinkedList<Node>();
			nextToken();
			if (nextToken.type!=TokenID.NULL&&nextToken.type!=TokenID.Period) { 
				Node n = expr3();
				arg.add(n);
			} else arg.add(null); // prefix can be null arity 
			return logicNodeFactory.predicateNode(op, arg );
		} else if (nextToken.type==TokenID.Exists) {
			return quantifier();
		}
		return expr4();
	}

	@Override
	public Node expr4() {
	    if (nextToken.syntax==TokenID.ALIAS) {
		    LinkedList<Node> arg = new LinkedList<Node>(); // empty
		    Node op = makeVariable(nextToken);
		    nextToken();
		    return logicNodeFactory.predicateNode(op, arg );
	    }
		Node n = term();
		if (nextToken.type==TokenID.Paren) {
			// predicate ( or macro )
			nextToken();
			n = logicNodeFactory.predicateNode(n,arguments());
		} else if (nextToken.syntax==TokenID.ALIAS) {
			LinkedList<Node> arg = new LinkedList<Node>(); // empty
			Node op = makeVariable(nextToken);
			nextToken();
			return logicNodeFactory.predicateNode(op, arg );
		}
		return n;
	}

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

	/*
	 * 
	 * Expand macro body with args. Called from PredicateNode Factory (if it is a macro)
	 */
	
	public Node eval(LinkedList<? extends Node> args, Node predicate, String body, 
			LinkedList<? extends Node> vars) {
		Node result;
		int i = 0;
		
		if (vars==null) {
			// TermMacro case
			return parse(body);
		}
		// prepare new scope
		scope = scope.push();
		for(Node var: vars) {
			Node value;
			if (i<args.size()) {
				value =	args.get(i++);
			} else {
				value =	logicNodeFactory.trueNode();
				scanner.error("Macro "+predicate+" Argument mismatch");
			}
			// make new token in the dictionary
			Token<Node> local = scope.getLocalName(var.toString());
			// assign new value
			local.setMacro(value);
		}
		// parse it in new bindings
		result = parse(body);
		scope = scope.pop();
		
		return result;
	}

	/*
	 * Make macro definition (store in the token in the dictionary)
	 */
	public void define(String macro, String body) {
		define(macro, body, 0, null);
	}

	public void define(String macro, String body, int order) {
		define(macro, body, order, null);
	}
	
	/* macro with command */
	public void define(String macro, String body, int order, Command<Node> command) {
		Node m = parseMarcoHead(macro,order);
		Node n = logicNodeFactory.macroNode(m, body, order, command, this);

		Token<Node> t;
		LogicSolver p = m.predicate();
		if (p!=null && (t = dict.get(p.toString()))!=null) {
			t.setMacro(n);
		} else {
			scanner.error("Internal error in define(\""+macro+"\",\""+n+"\")");
		}
	}

	/*
	 * Macro Head parser
	 */
	private Node parseMarcoHead(String exp, int order) {
		Node n;
		scanner = scanner.pushScanner(exp);
		nextToken();
		Token<Node> n1 = scanner.nextToken;
		n = term();

		if (nextToken.type==TokenID.Paren) {
			nextToken();
			n = logicNodeFactory.predicateNode(n,parameter());
			if (n.arguments().size()==1) {
				// all one argument predicates are prefix
				n1.setPrefix();
			}
		} else if (nextToken.type==TokenID.NULL) {
			// No parameter
			n = logicNodeFactory.predicateNode(n,null);
			n1.syntax = TokenID.ALIAS;
		} else {
			Token<Node> opToken = nextToken;
			Node op;
			nextToken();
			Token<Node> n2 = nextToken;
			LinkedList<Node> arg = new LinkedList<Node>();
			scope = scope.push();
			if (nextToken.type!=TokenID.NULL) {
				// Assuming infix operator
				opToken.setInfix();
				opToken.order = order;
				op = makeVariable(opToken);
				oneParameter(arg,n1);
				oneParameter(arg,n2);
			} else {
				op = makeVariable(n1);
				n1.setPrefix();
				n1.order = order;
				oneParameter(arg,opToken);
			}
			scope = scope.pop();
			n = logicNodeFactory.predicateNode(op,arg);
		}

		scanner = scanner.popScanner();
		nextToken = scanner.nextToken;
		return n;
	}

	/*
	 * Function parameter 
	 *    parameters are defined in local scope
	 */
	private LinkedList<Node> parameter() {
		LinkedList<Node> arg = new LinkedList<Node>();

		scope = scope.push();
		while(nextToken.type!=TokenID.CloseParen) {
			if (nextToken.type==TokenID.NULL) break;
			oneParameter(arg,nextToken);
			nextToken();
			if (nextToken.type == TokenID.And)
				nextToken();
		}
		if (nextToken.type==TokenID.CloseParen) nextToken();
		else {
			 scanner.error(") expected");
		}
		scope = scope.pop();
		return arg;
	}

	public void oneParameter(LinkedList<Node> arg, Token<Node> nextToken) {
		Token<Node> t;
		Node v;
		// If next token is a macro, parameter name is going to be replaced.
		// We have to know the real symbol name.
		
		// more check is necessary
		t = scope.getLocalName(nextToken.realName());
		t.setVariable(true);
		v = makeVariable(t);
		arg.add(v);
	}
}