package parser;

import java.util.LinkedList;
import java.util.TreeMap;

import lite.ITLNodeFactoryInterface;
import lite.ITLSolver;
import lite.NumberSolver;


import sbdd.BDDDiagnosis;
import sbdd.BDDSatisfier;
import sbdd.SBDDEntry;

public class ITLCommander<Node extends ITLSolver> implements Command<Node> {


	private ITLNodeFactoryInterface<Node> lf;
	private ITLNodeParser<Node> parser;
	public BDDSatisfier sat;
	private TreeMap<Integer,Node> examples;
	private BDDDiagnosis diag;

	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
		this.lf = lf;
		this.parser = parser;
		this.examples = new TreeMap<Integer,Node>();
		
		parser.addHelp(
			"do(p).                     verify formula p or a numberd example, try do(10).\n"+
			"ex(N,p).                   register numbered examle p\n"+
			"ls.                        list predefined example\n"+
			"verbose(TF).               set verbose mode (true/false)\n"+
			"include(File).             read from File\n"+
			"def('head(p)','body(p)').  define macro\n"+
			"exe.                       execute last verifed formula\n"+
			"diag.                      counter example of last verifed formula\n"+
			"clear.                     clear state database\n"+
			"show.                      show state statistics\n"+
			"readme.                    show README\n"+
			"help.                      show this\n"+
			""
				);
	}

	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
		
		// All names used here have to be reserved. Otherwise, parser generated name becomes 
		// different string at run time, as a result, name=="less" will fail even if name contains "less". 
		// If we reserve it, paredicateNode.varaibleNode.name contains pregenerated String which is 
		// equivalent to used here. Of course name.equal("less") works fine, but it is time consuming. 
		// Although it is practically allowed but I cannot accept.
		
		// We can also define Command as internal interface class in ITLNodeParser. In this case
		// reserve operation is not required, like "length" macro.

		// I put most interpretive command here, because it is easy to do so. But it should
		// be in Executer. Otherwise, all other expressions remain unchecked.
		
		String name = predicate.toString();
		
		if (name=="less") {
			Node n = lf.falseNode();
			int length = atoi(args);
			for(int i =0;i<length;i++) {
				n = lf.nextNode(n);
			}
			return (Node)n;
		} else if (name == "ex"|| name=="do") {
			checkSat();
			if (args.size()<1) {
				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
				return lf.trueNode();
			}
			int index = atoi(args);
			if (args.size()==1) {
				Node n = args.get(0);
				if (index>=0) {
					// do(10) case
					n = examples.get(index);
					if (n==null) {
						parser.error("Unknown registered example");
						return lf.trueNode();
					}
				}
				System.out.println(n);
				sat.verify(n);
			} else if (args.size()==2 && index>=0){
				examples.put(index, args.get(1));
			}
		} else if (name == "ls") {
			// this is not human readable...
			//for(int i:examples.keySet()) {
			// System.out.println(i+":"+examples.get(i));
			//}
			parser.showResourceFile("data/example");
		} else if (name == "readme") {
			parser.showResourceFile("data/README");
		} else if (name == "help") {
			parser.help();
		} else if (name == "def") {
			parser.define(args.get(0).toString(),args.get(1).toString());
		} else if (name == "verbose") {
			// verbose(true) / verbose(off)
			checkSat();
			Node n;
			if (args.size()==0 || (n=args.get(0))==null) n = lf.trueNode();
			sat.verbose = (n==lf.trueNode())?true:false;
		} else if (name == "include") {
			String file = args.getFirst().toString();
			parser.parseFile(file);
		} else if (name == "exe") {
			int length = 0;
			if (args.size()>1) length = atoi(args);
			checkSat();
			diag.execute(sat.last, length );
		} else if (name == "diag") {
			int length = 0;
			if (args.size()>1) length = atoi(args);
			checkSat();
			diag.counterExample(sat.last, length);
		} else if (name == "clear") {
			sat = null;
			checkSat();
		} else if (name == "states") {
			// System.out.println(sat.sf.hash); too large
			for(SBDDEntry e: sat.sf.hash.sbddArray) {
				if (e==null) continue;
				System.out.println(e);
			}
		} else if (name == "show") {
			checkSat();
			diag.showState(sat.last);
		} else
			parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
		return lf.trueNode();
	}

	private int atoi(LinkedList<Node> args) {
		// should have more strict check..
		int i=-1;
		if (args.size()==0) return i;
		Node n = args.get(0);
		if (n==null) return 0;
		if (n.getClass()==NumberSolver.class) {
			i = Integer.parseInt(n.toString()); 
		}
		return i;
	}

	private void checkSat() {
		if (sat==null) {
			sat = new BDDSatisfier();
			diag = new BDDDiagnosis(sat);
		}
	}

}