package lite;

import java.util.LinkedList;

import logicNode.parser.Command;
import logicNode.parser.MacroNodeParserInterface;

import verifier.Backtrack;

public class MacroSolver extends ITLSolver {


	private ITLSolver predicate;
	private String body;
	private MacroNodeParserInterface<ITLSolver> parser;
	private Command<ITLSolver> command;
	public int order;


	public MacroSolver(ITLSolver macro, String body, int order,
			Command<ITLSolver> command,
			MacroNodeParserInterface<ITLSolver> parser) {
		this.predicate = macro;
		this.body = body;
		this.parser = parser;
		this.command = command;
		this.order = order;
	}


	@Override
	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
		// TODO Auto-generated method stub
		return null;
	}

	@Override
	public String toString() {
		return predicate.toString();
	}

	

	@Override
	public boolean isMacro() {
		return true;
	}
	
	@Override
	public LinkedList<ITLSolver> arguments() {
		return predicate.arguments();
	}

	/* 
	 * Macro Expansion
	 *      locally define parameters by given arguments
	 */
	@Override
	public ITLSolver eval(LinkedList<ITLSolver> args) {
		ITLSolver value = parser.eval(args, predicate, body,predicate.arguments());
		if (command!=null) {
			return command.exec(predicate,value, args);
		}
		return value;
	}
	
	@Override
	public int order() {
		return order;
	}

}