package lite;

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

import parser.Command;

import sbdd.BDDDiagnosis;
import sbdd.BDDSatisfier;

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"+
			"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 reseve 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.

		String name = predicate.toString();
		
		if (name=="less") {
			Node n = lf.falseNode();
			int length = Integer.parseInt(args.get(0).toString());
			for(int i =0;i<length;i++) {
				n = lf.nextNode(n);
			}
			return (Node)n;
		} else if (name == "ex"|| name=="do") {
			checkSat();
			Node n = args.get(0);
			if (args.size()<1||n==null) {
				parser.error("ex(1) or ex(<>p) or ex(10,[]p)");
				return lf.trueNode();
			}
			int index = -1;
			if (n.getClass()==NumberSolver.class) {
				index = Integer.parseInt(n.toString()); 
			}
			if (args.size()==1) {
				// System.out.println(args.get(0)+":"+args.get(1));
				if (index>=0) {
					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 human unreadable...
			//for(int i:examples.keySet()) {
			// System.out.println(i+":"+examples.get(i));
			//}
			parser.showResourceFile("data/example");
		} 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)
			Node n= null;
			checkSat();
			try {
				int i = Integer.parseInt((n=args.get(0)).toString());
				sat.verbose =  (i==0)? false:true;
			} catch (NumberFormatException e) {
				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 = Integer.parseInt(args.get(0).toString());
			checkSat();
			diag.execute(sat.last, length );
		} else if (name == "diag") {
			int length = 0;
			if (args.size()>1) length = Integer.parseInt(args.get(0).toString());
			checkSat();
			diag.counterExample(sat.last, length);
		} else if (name == "clear") {
			sat = new BDDSatisfier();
		} else if (name == "states") {
			System.out.println(sat.sf.hash);
		} else if (name == "show") {
			checkSat();
			diag.showState(sat.last);
		} else
			parser.error("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
		return lf.trueNode();
	}

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

}