package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

import java.util.Map
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import java.util.List
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant
import edu.mit.csail.sdg.alloy4compiler.ast.Expr
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall
import java.util.HashMap
import edu.mit.csail.sdg.alloy4compiler.ast.Decl
import java.util.ArrayList
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import edu.mit.csail.sdg.alloy4compiler.ast.Attr
import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
import javax.naming.OperationNotSupportedException
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant
import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification
import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity
import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

class AlloyInput{
	public val List<PrimSig> typeDeclarations=new ArrayList
	public val List<Expr> functionDeclarations=new ArrayList
	public val List<Expr> assertions=new ArrayList
	public val List<Expr> multiplicityConstraints=new ArrayList
	public val List<Expr> inverseConstraints=new ArrayList
}

class Logic2AlloyApiMapperTrace {
	val Map<Type, PrimSig> typeMap
	val Map<DefinedElement, PrimSig> elementMap
	//val Map<Function, SMTFunctionDeclaration> functionMap
	val Map<Relation,Expr> relationMap
	//val Map<Constant,SMTFunctionDeclaration> constantMap
	
	new () {
		this.typeMap = new HashMap
		this.elementMap = new HashMap
		//this.functionMap = new HashMap
		this.relationMap = new HashMap
		//this.constantMap = new HashMap
	}
	new (Map<Type, PrimSig> typeMap,
		 Map<DefinedElement, PrimSig> elementMap,
		 //Map<Function, SMTFunctionDeclaration> functionMap,
		 Map<Relation,Expr> relationMap/*,
		 Map<Constant,SMTFunctionDeclaration> constantMap*/)
	{
		this.typeMap = typeMap
		this.elementMap = elementMap
		//this.functionMap = functionMap
		this.relationMap = relationMap
		//this.constantMap = constantMap
	}
	
	def types() { typeMap }
	def elements() { elementMap }
	//def functions() { functionMap }
	def relations() { relationMap }
	//def constants() { constantMap }
}

class Logic2AlloyApiMapper{
	//TODO output
	public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) {
		val documentInput = new AlloyInput()
		//createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand]
		//val document = createSMTDocument => [input = documentInput]
		val List<PrimSig> document=new ArrayList
		val trace = new Logic2AlloyApiMapperTrace
		
		// Trafo
		documentInput.typeDeclarations		+= problem.types.map[transformType(trace)]
		//documentInput.functionDeclarations	+= problem.functions.map[transformFunction(trace)]
		documentInput.functionDeclarations	+= problem.relations.map[transformRelation(trace)]
		//documentInput.functionDeclarations	+= problem.constants.map[transformConstant(trace)]
		documentInput.assertions			+= problem.assertions.map[transformAssertion(trace)]
		
		
		val alloySpecification = problem.specifications.filter(AlloySpecification).head
		
		for(mult: alloySpecification.multiplicities){
			if(mult.min>0){
				documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace)
			}
			if(mult.max!=-1){
				documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace)
			}
		}
		
		for(inv: alloySpecification.inverses){
			documentInput.inverseConstraints += inv.transformInverse(trace)
		}
		// End trafo
		
		return new TracedOutput(document,trace)
	}
	
	def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
		
		val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
		return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable)
		
	}
	
	def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){
		
		val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl
		return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable)
		
	}
	
	def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){
		return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose)	
	}
	
	private def toID(List<String> names) {names.join("!") }
	
	def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) {
		val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT)
		trace.types.put(declaration,result)
		return result
	}
	
	def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) {
		val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE)
		trace.elements.put(element,result)
		return result
	}
		
	def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) {
		//TODO �r�kles, absztrakt
		val result = new PrimSig(declaration.name.toID)
		trace.types.put(declaration,result)
		return result
	}
	
	def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) {
		throw new UnsupportedOperationException("BoolTypeReference is not supported.")
	}
	def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) {
		return PrimSig.SIGINT
	}
	def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) {
		throw new UnsupportedOperationException("RealTypeReference is not supported.")
	}
	def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) {
		return trace.types.get(complexTypeReference.referred)
	}
	
	/*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) {
		val functionDeclaration = createSMTFunctionDeclaration => [
			name = declaration.name.toID
			range = declaration.range.transformTypeReference(trace)
			parameters+= declaration.parameters.map[transformTypeReference(trace)]
		]
		trace.functions.put(declaration,functionDeclaration)
		return functionDeclaration
	}*/
	
	def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) {
		if(relation.parameters.size==2){
			trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf))
		} else{
			throw new OperationNotSupportedException("More parameters are not supported.")
		} 
	}
	
	/*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) {
		val smtConstant = createSMTFunctionDeclaration => [
			name = constant.name.toID
			range = transformTypeReference(constant.type, trace)
		]
		trace.constants.put(constant,smtConstant)
		return smtConstant
	}*/
	
	def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) {
		
		return assertion.value.transformTerm(trace,emptyMap)
	}
	
	def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		throw new UnsupportedOperationException("Bool is not supported")
		//open util/boolean, autoPay: Bool
		//https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142
	}
	def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)  {
		return ExprConstant.makeNUMBER(literal.value)
	}
	def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		throw new UnsupportedOperationException("Real number is not supported")
	}
	def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return not.operand.transformTerm(trace,variables).not}
	def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		val List<Expr> operands= and.operands.map[transformTerm(trace,variables)]
		var andTerm=operands.get(0)
		for(Integer i: 1..(operands.size-1)){
			andTerm=andTerm.and(operands.get(i))
		}
		return andTerm
	}
	def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		val List<Expr> operands= or.operands.map[transformTerm(trace,variables)]
		var orTerm=operands.get(0)
		for(Integer i: 1..(operands.size-1)){
			orTerm=orTerm.or(operands.get(i))
		}
		return orTerm
	}
	def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables))
	}
	/*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) {
		createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/
	def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables))
	}
	def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		throw new UnsupportedOperationException("Modulo is not supported.")
	}
	def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return configureForall(forall,trace,variables) 
	}
	def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return configureExists(exists,trace,variables)
	}
	def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) }
	
	def private configureForall(
		Forall quantifiedExpression,
		Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
	{
		val allVariables = new HashMap(variables)
		val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
		
		for(logicVariable: quantifiedExpression.quantifiedVariables) {
			val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
			allVariables.put(logicVariable, newAlloyVariable)
			newAlloyVariables += newAlloyVariable
		}
		val variable0=newAlloyVariables.get(0)
		newAlloyVariables.remove(0)
		return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables)
	}
	
	def private configureExists(
		Exists quantifiedExpression,
		Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables)
	{
		val allVariables = new HashMap(variables)
		val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size)
		
		for(logicVariable: quantifiedExpression.quantifiedVariables) {
			val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl
			allVariables.put(logicVariable, newAlloyVariable)
			newAlloyVariables += newAlloyVariable
		}
		val variable0=newAlloyVariables.get(0)
		newAlloyVariables.remove(0)
		return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables)
	}
	
	def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return trace.elements.get(referred)
	}
	def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return variables.get(variable).get
	}
	/*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)]
		for(paramSubstitution : parameterSubstitutions) {
			result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables))
		}
		return result
	}*/
	def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		return trace.relations.get(relation)
	}
	def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) {
		//createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)]
		throw new UnsupportedOperationException("Constant is not supported")
	}
}