package Token;
import java.util.ArrayList;
import java.util.List;
import java.util.Stack;

import Main.Expression;
import Automata.Automaton;

public class Word extends Token{
	Automaton W;
	String name;
	public Word(int position,String name,Automaton W,int number_of_indices) throws Exception{
		this.name = name;
		setPositionInPredicate(position);
		this.W = W;
		setArity(number_of_indices);
		if(W.getArity() != getArity())throw new Exception("word " + name + " requires " + W.getArity() +" indices: char at " + getPositionInPredicate());
	}
	public String toString(){
		return name;
	}
	public void act(Stack<Expression> S) throws Exception{
		if(S.size() < getArity())throw new Exception("word " + name + " requires " + getArity()+ " indices");
		
		Stack<Expression> temp = new Stack<Expression>();
		List<Expression> indices = new ArrayList<Expression>();
		for(int i = 1; i <= getArity();i++){
			temp.push(S.pop());
		}
		String stringValue = name;
		List<String> identifiers = new ArrayList<String>();
		List<String> quantify = new ArrayList<String>();
		Automaton M = new Automaton(true);
		for(int i = 0 ; i < getArity();i++){
			Expression currentIndex = temp.pop();
			indices.add(currentIndex);
			stringValue += "["+currentIndex+"]";
			/**
			 * type checking
			if(W.NS.get(i) == null && (currentIndex.is(Type.arithmetic) || currentIndex.is(Type.numberLiteral)))
				throw new Exception("index "+ (i+1) +" of word " + name + " cannot be of type arithmetic");	*/
			
			switch(currentIndex.T){
			case variable:
				identifiers.add(currentIndex.identifier);
				break;
			case arithmetic:
				identifiers.add(currentIndex.identifier);
				M = M.and(currentIndex.M);
				quantify.add(currentIndex.identifier);
				break;
			case automaton:
				if(currentIndex.M.getArity() != 1){
					throw new Exception("index " + (i+1) + " of word " + name + " cannot be an automaton with != 1 inputs");
				}
				if(!currentIndex.M.isBound()){
					throw new Exception("index " + (i+1) + " of word " + name + " cannot be an automaton with unlabeled input");					
				}
				M = M.and(currentIndex.M);
				identifiers.add(currentIndex.M.getLabel().get(0));
				break;
			case numberLiteral:
				Automaton constant = currentIndex.base.get(currentIndex.constant);
				String id = getUniqueString();
				constant.bind(id);
				identifiers.add(id);
				quantify.add(id);
				M = M.and(constant);
				break;
			default:
				throw new Exception("index "+ (i+1) +" of word " + name + " cannot be of type " +currentIndex.getType());			
			}	
		}
		W.bind(identifiers);
		S.push(new Expression(stringValue,W,M,quantify));
	}
}
