package lite;

import java.util.LinkedList;

import sbdd.SBDDFactory;

import logicNode.parser.Command;
import logicNode.parser.Dictionary;
import logicNode.parser.LogicNodeScope;
import logicNode.parser.MacroNodeParser;
import logicNode.parser.Token;
import logicNode.parser.TokenID;

public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> {

	public ITLNodeFactoryInterface<Node> logicNodeFactory;
	public ITLNodeScanner<Node> scanner;
	public ITLCommander<Node> parseCommand;
	public Node emptyNode;
	private Node periodNode;
	
	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {

		super(lf);
		logicNodeFactory = lf;
		initialize();

		Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty);
		emptyNode = emptyToken.value = logicNodeFactory.emptyNode();
		
		parseCommand = new ITLCommander<Node>(lf,this);
		
			define("not(P)","~P");                               // not
			define("P->Q","(not(P);Q))");                         // imply
			define("P<->Q","((not(P);Q),(P; not(Q)))");            // equiv
			define("P=Q","((not(P);Q),(P; not(Q)))");              // equiv 
			define("P && Q","((not(empty),P) & Q))");             // strong chop
			define("'<>'(Q)","(true & Q))");                        // sometime
			define("'#'(Q)"," not(true & not(Q)))");                // always
			define("'[]'(Q)"," not(true & not(Q)))");               // always
			define("'[a]'(Q)"," not(true & not(Q) & true))");       // always with arbitary fin
			define("'<a>'(Q)"," (true & Q & true))");       // sometime with arbitary fin
			define("fin(Q)","(true & (empty,Q)))");                 // final state in the interval
			define("keep(Q)"," not(true & not((empty ; Q))))");     // except final state
			define("halt(Q)"," '[]'(empty=Q))");    
			define("more"," not(empty))");                          // non empty interval
// discrete stuff
			define("skip"," @(empty))");                            // 1 length interval
			define("infinite"," (true & false))");                  // 
			define("finite"," ~((true & false)))");                 // 
			// define("length(I)", "true",50,command);            // length operator
			define("length(I)", "empty",50,                          // length operator
					new Command<Node>() {
						public Node exec(Node predicate, Node value, LinkedList<Node> args) {
	                        Node n = value;
	                        int length = Integer.parseInt(args.get(0).toString());
	                        for(int i =0;i<length;i++) {
	                                n = logicNodeFactory.nextNode(n);
	                        }
	                        return n;
						}
			});
			define("less(I)","false",50,parseCommand);               // less than N length
			define("next(P)","(empty; @(P)))");
// temporal assignments
			define("gets(A,B)","keep(@A<->B))");
			define("stable(A)","keep(@A<->A))");
			// define("state(A)","(share(A),'[]'(L))):- def_state(A,L)");
// def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R))))");
//   easier one
            define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))");
// def(P<=Q,Q=>P)");
// loop stuff and quantifiers
			define("*(A) ","proj(A,true),fin(A)");  // weak closure
			// define("+(A) ","A& *(empty;A)");   // strong closure (difficult one)
			define("+(A) ","A & proj(A,true)");   // strong closure
			define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
			define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
			define("all(P,Q)","not(exists(P,not(Q)))");
			define("local(P)"," (P = (P&true))");
// test predicates
//			define("trace(X,List),L) :- !,make_trace(List,X,L)");
			define("even(P)","exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P)))))");
			define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))"); 
			define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");

			define("ex(N,Exp)","true",50,parseCommand);
			define("do(N)","true",50,parseCommand);
			define("def(Head,Body)","true",50,parseCommand);
			define("include(path)","true",50,parseCommand);
			
			define("ex0(N,Exp)","skipped");
			define("verbose(I)", "true",50,parseCommand);                    
			
			define("^(r)","r"); // interval variable (we cannot handle now)
			
			periodNode = logicNodeFactory.variableNode(".", true);
			// only one of the is true (should allow all false case?)
			define("share(L)","[](share0(L))");
			define("share0(L)","true",50, new Command<Node>() {
				@SuppressWarnings({ "unchecked", "unchecked" })
				public Node exec(Node predicate, Node value, LinkedList<Node> args) {
					Node allFalse = (Node)SBDDFactory.trueSolver;
					value= (Node)SBDDFactory.falseSolver;
					LinkedList<ITLSolver> list = args.get(0).arguments();
					if (list==null) {
						error("sahre: missing [] argument");
						return value;
					}
					if (list.isEmpty()) return value;
					for(ITLSolver n:  list) {
						Node n1 = (Node)n;
						value = logicNodeFactory.bddNode(n1, allFalse, value);
						allFalse = logicNodeFactory.bddNode(n1, 
								(Node)SBDDFactory.falseSolver,allFalse);
					}
					return value;
				}
			});

	}

	public ITLNodeParser() {
		super();
	}
	

	@Override
	public void initialize() {
		dict = new Dictionary<Node>();
		scope = new LogicNodeScope<Node>(null,dict);
		initReservedWord();
		scanner = new ITLNodeScanner<Node>(dict);
		super.scanner = scanner;

		dict.reserve("&",TokenID.Chop);
		dict.reserve("@",TokenID.Next);
		dict.reserve("proj",TokenID.Projection);
		
		// parseCommand requires reserved word for string comparison
		dict.reserve("less");
		dict.reserve("ex");
		dict.reserve("do");
		dict.reserve("include");
		dict.reserve("def");
		dict.reserve("verbose");
	}

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

	@Override
	public Node expr3() {
		if (nextToken.type == TokenID.Next) {
			nextToken();
			return logicNodeFactory.nextNode(expr3());
		}
		Node n = super.expr3();
		while(nextToken.type==TokenID.Question) {
			nextToken();
			Node cond = n;
			Node high = expr3();
			if (nextToken.type!=TokenID.Colon) {
				error(": expected");
				return logicNodeFactory.trueNode();
			}
			nextToken();
			Node low = expr3();
			n = logicNodeFactory.orNode(
					logicNodeFactory.andNode(cond, high),
					logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low));
		}
		return n;
	}

	
	@Override
	public Node term() {
		if (nextToken.type==TokenID.BParen) {
			Node predicate = periodNode;
			nextToken();
			LinkedList<Node> arg = arguments();
			return logicNodeFactory.predicateNode(predicate, arg);
		}
		return super.term();
	}
	
	public Node exprI2() {
		Node n = exprM1();
		while(nextToken.type == TokenID.Chop) {
			nextToken();
			n = logicNodeFactory.chopNode(n, exprM1());
		}
		return n;
	}


	@Override
	protected LinkedList<Node> arguments() {
		Node n;
		LinkedList<Node> arg = new LinkedList<Node>();
		while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) {
			if (nextToken.type==TokenID.NULL) break;
			n = exprI2();
			arg.add(n);
			if (nextToken.type == TokenID.And)
				nextToken();
		}
		if (nextToken.type==TokenID.CloseParen||
				nextToken.type==TokenID.CloseBParen) nextToken();
		else {
			scanner.error(") expected");
		}
		return arg;
	}
	
	public ITLSolver emptyNode() {
		return emptyNode;
	}


}