package de.dhbwstuttgart.syntaxtree.statement;

import java.util.Hashtable;
import de.dhbwstuttgart.typeinference.Menge;

import de.dhbwstuttgart.myexception.CTypeReconstructionException;
import de.dhbwstuttgart.myexception.JVMCodeException;
import de.dhbwstuttgart.myexception.SCStatementException;
import de.dhbwstuttgart.syntaxtree.Class;
import de.dhbwstuttgart.syntaxtree.ClassHelper;
import de.dhbwstuttgart.syntaxtree.FormalParameter;
import de.dhbwstuttgart.syntaxtree.Method;
import de.dhbwstuttgart.syntaxtree.ParameterList;
import de.dhbwstuttgart.syntaxtree.SyntaxTreeNode;
import de.dhbwstuttgart.syntaxtree.type.DoubleType;
import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType;
import de.dhbwstuttgart.syntaxtree.type.GenericTypeVar;
import de.dhbwstuttgart.syntaxtree.type.ObjectType;
import de.dhbwstuttgart.syntaxtree.type.RefType;
import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType;
import de.dhbwstuttgart.syntaxtree.type.Type;
import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
import de.dhbwstuttgart.syntaxtree.type.WildcardType;
import de.dhbwstuttgart.typeinference.ConstraintsSet;
import de.dhbwstuttgart.typeinference.FunN;
import de.dhbwstuttgart.typeinference.JavaCodeResult;
import de.dhbwstuttgart.typeinference.OderConstraint;
import de.dhbwstuttgart.typeinference.ResultSet;
import de.dhbwstuttgart.typeinference.SingleConstraint;
import de.dhbwstuttgart.typeinference.Typeable;
import de.dhbwstuttgart.typeinference.assumptions.ParameterAssumption;
import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException;
import de.dhbwstuttgart.typeinference.unify.CSubstitutionSet;

/**
 * @author A10023 - Andreas Stadelmeier
 * Momentan erweitert LambdaExpression noch Expr und erbt dadurch auch von ExprStatement ist also auch ein Statement
 * 
 * LambdaExpression Aufbau:
 * ( ParameterList ) -> { method_body };
 */
public class LambdaExpression extends Expr{ 
	
	private Block method_body;
	private ParameterList params;
	
	public LambdaExpression(int offset, int variableLength) {
		super(offset, variableLength);
		setParameterList(new ParameterList());//default is empty parameterlist
	}
	
	public void setBody(Block block){
		method_body = block;
	}
	
	public void setExpr(Expr expression){
		Block bl = new Block();
		Return returnStmt = new Return(0, 0);
		returnStmt.retexpr = expression;
		bl.set_Statement(returnStmt);
		this.setBody(bl);
	}
	
	public void setParameterList(ParameterList params){
		ParameterList lambdaParameter = new ParameterList();
		for(FormalParameter fp : params){
			lambdaParameter.formalparameter.add(new LambdaParameter(fp));
		}
		this.params = lambdaParameter;
	}

	@Override
	public void wandleRefTypeAttributes2GenericAttributes(
			Menge<Type> paralist,
			Menge<GenericTypeVar> genericMethodParameters) {
		Block block = this.method_body;
		// Zuerst Returntype untersuchen
        Type returnType=getType();
        Type pendantReturnType = null;
        if(returnType instanceof RefType)
        	pendantReturnType = ((RefType)returnType).findGenericType(paralist, new Menge<GenericTypeVar>());
        //GenericTypeVar pendantReturnType=ClassHelper.findGenericType(returnType, paralist,genericMethodParameters);
        if(pendantReturnType!=null){    //Wenn generisch, dann modifizieren
            setType(pendantReturnType);
        }                                       
        
        // Dann parameterlist untersuchen
        for(FormalParameter fp : params){
            Type fpType=fp.getType();
            // Nur wenn es sich um ein RefType-Field handelt
            Type pendantPara = null;
            if(fpType instanceof RefType)
            	pendantPara = ((RefType)fpType).findGenericType(paralist, new Menge<GenericTypeVar>());
            //GenericTypeVar pendantPara=ClassHelper.findGenericType(fpType,paralist,genericMethodParameters);
            if(pendantPara!=null){  //Wenn generisch, dann modifizieren
                fp.setType(pendantPara);
            }                       
        }
        
        // Zuletzt alle Lokalen Variablendeklarationen durchgehen
        if(block!=null){
            block.wandleRefTypeAttributes2GenericAttributes(paralist,genericMethodParameters);
        }
	}

	@Override
	public String get_Name() {
		// TODO Auto-generated method stub
		return null;
	}


	
	/**
	  * Spezifikation:
	  * 
	  * TYPEExpr( Ass, Lambda( (x1 , . . . , xN ), expr|stmt ) ) =
	  * let
	  * AssArgs = { xi : ai | ai fresh type variables }
	  * (exprt : rty, ConS) = TYPEExpr( Ass ∪ AssArgs, expr )
	  * | (stmtt : rty, ConS) = TYPEStmt( Ass u AssArgs, stmt )
	  * in
	  * (Lambda( (x1 : a1 , . . . , xN : aN ), exprt : rty|stmtt : rty ) : a,
	  * ConS ∪ { (FunN<rty, a1 , . . . , aN > a) }),
	  * where a is a fresh type variable 
	 */
	@Override
	public ConstraintsSet TYPEExpr(TypeAssumptions assumptions) {
		ConstraintsSet ret = new ConstraintsSet();
		//Die Assumptions für die Parameter der LambdaExpression
		TypeAssumptions ArgumentAssumptions = new TypeAssumptions(this.getParentClass().getName());
		Menge<Type> paramTypes =  new Menge<Type>();
		
		for(FormalParameter param : params.formalparameter){
			if(param.getType()==null)param.setType(TypePlaceholder.fresh(this));
			int offset = 0;
			//Jeder Parameter der LambdaExpression wird als CParaTypeAssumption der Assumption liste hinzugefügt:
			ArgumentAssumptions.addAssumption(new ParameterAssumption(param));
			paramTypes.add(param.getType());
		}
		this.setType(TypePlaceholder.fresh(this));
		//ArgumentAssumptions + assumptions ergeben die Assumptions für die Statements innerhalb des Lambda-Bodys:
		ret.add(method_body.TYPEStmt(ArgumentAssumptions.add(assumptions))); //Es gibt die LambdaExpression nur mit einem Block als Method Body, nicht mit einer einzelnen Expression
		
		//Die Constraints für ParameterTypen und Ret Typ erstellen:
		Menge<Type> modifiedParamTypes = new Menge<>();
		for(Type pT : paramTypes){
			if(pT instanceof WildcardType){
				//Auf Typfehler kontrollieren. Siehe Bug #12 Kommentar 3
				if(pT instanceof ExtendsWildcardType){
					throw new TypeinferenceException("Typfehler von Parametertyp "+pT,this);
				}else{
					modifiedParamTypes.add(pT);
				}
			}else{
				modifiedParamTypes.add(new SuperWildcardType((ObjectType) pT));
			}
		}
		Type retType = method_body.getType();
		// PN < TPH PN
		if(retType instanceof WildcardType){
			//Auf Typfehler kontrollieren. Siehe Bug #12 Kommentar 3
				if(retType instanceof SuperWildcardType){
					throw new TypeinferenceException("Typfehler von Parametertyp "+retType,this);
				}else{
					//retType bleibt unverändert
				}
			}else{
				retType = new ExtendsWildcardType((ObjectType) retType);
		}
		
		ret.add(new SingleConstraint(new FunN(retType, modifiedParamTypes).TYPE(assumptions, this),this.getType().TYPE(assumptions, this)));
		return ret;
	}
	
	@Override
	public ConstraintsSet TYPEStmt(TypeAssumptions ass){
		throw new TypeinferenceException("Eine LambdaExpression darf nicht als Statement verwendet werden.", this);
	}
	
	@Override
	public String getTypeInformation(){
		return this.getType().toString()+" :: ("+this.params.getTypeInformation()+ ") -> " +this.method_body.getTypeInformation();
	}
	
	@Override
	public String toString(){
		//return "LambdaExpression, Parameter: "+this.params+ ", Body: " +this.method_body;
		return this.getType() +  " (("+this.params+ ") -> "+this.method_body + ")";
	}
	
	@Override
	public JavaCodeResult printJavaCode(ResultSet resultSet){
		JavaCodeResult ret = new JavaCodeResult();
		ret.attach( "(").attach(this.params.printJavaCode(resultSet)).attach(")");
		ret.attach( " -> ").attach( this.method_body.printJavaCode(resultSet));
		return ret;
	}

	@Override
	public Menge<SyntaxTreeNode> getChildren() {
		Menge<SyntaxTreeNode> ret = new Menge<SyntaxTreeNode>();
		ret.add(this.method_body);
		for(FormalParameter fp : this.params)ret.add(fp);
		return ret;
	}

}