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

import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection
import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
import java.util.HashMap
import java.util.LinkedHashSet
import java.util.LinkedList
import java.util.List
import java.util.Map
import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
import org.eclipse.viatra.query.runtime.emf.EMFScope
import org.eclipse.xtend.lib.annotations.Data

import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
	implements Logic2AlloyLanguageMapper_TypeMapperTrace {
	public var ALSSignatureDeclaration declaredSupertype
	public var ALSSignatureDeclaration definedSupertype
	public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
	
	public val Map<TypeDefinition,  ALSSignatureDeclaration> definition2definition = new HashMap
	public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap
	public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap
	public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap
	
	def getAllDefinedTypes() {
		return (definition2definition.values) +
		       (declaration2definition.values) +
		       (undefined2definition.values)
	}
	def getAllDeclaredTypes() {
		return new2declaration.values
	}
	
	public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap;
}

@Data
class DynamicTypeConstraints {
	List<List<Type>> positiveCNF
	LinkedHashSet<Type> negative
	public new() {
		this.positiveCNF = new LinkedList
		this.negative = new LinkedHashSet
	}
	def public void addPositiveTypeOptions(List<Type> typeDisjunction) {
		this.positiveCNF.add(typeDisjunction)
	}
	def public void addNegativeTypes(Iterable<Type> negativeTypes) {
		this.negative.addAll(negativeTypes)
	}
}

/**
 * Dynamic types are represented by disjoint sets, and 
 * static types are represented by the union of the dynamic type sets.
 * 
 * Definition                         Declaration
 *     |                              /         \
 *     |                  W/DefinedSuper       Wo/DefinedSuper
 *     |                     |                  /           \
 *     |                     |      undefined2declaration  new2declaration
 * definition2definition  definition2declaration
 * +----------------------------------------------------+  +-------------+
 *        Defined                                              Declared
 */
class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{
	private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
	private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
	
	override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		// 0. Creating the traces
		val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
		trace.typeMapperTrace = typeTrace
		/**
		 * Static type -> list of possible dynamic type map
		 */
		val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace)
		
		
		
		// 1. Transforming the types
		
		// There are two kind of types:
		// A: one with defined supertypes (including itself), that only has defined elements
		// Those types can have instances only from the defined elements, ie they are subset of problem.elements
		// B: one without defined supertypes 
		// Those types can have instances from two sources
		// B.1 from elements that dont have definitions
		// B.2 from newly created elements
		val allConcreteTypes = problem.types.filter[!it.isAbstract]
		val definitions = allConcreteTypes.filter(TypeDefinition).toList
		val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList
		val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList
		
		// 2. If there are defined elements
		if(trace.typeTrace.definedSupertype != null) {
			// 3 mapping the elements
			problem.elements.transformDefinedSupertype(trace)
			// 4. if there are elements that are added to types, then it have to be mapped to defined parts
			if(problem.elements.exists[!it.definedInType.empty]) {
				definitions.forEach[it.transformDefinition2Definition(trace)]
				declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)]
			}
			// 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions
			if(problem.elements.exists[it.definedInType.empty]) {
				declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)]
			}
			
			definedConcreteTypesAreFull(trace)
			definedConcreteTypesAreDisjoint(trace)
			problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace)
		}
		
		// Transforming the declared and defined concrete types
		problem.elements.transformDefinedSupertype(trace)
		if(trace.typeTrace.definedSupertype != null) {
			problem.elements.transformDefinedElements(trace)
			declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)]
		}
		
		// 2: Caching the types by filling type2AllSignatures
		for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) {
			val type = typeToConcreteSubtypesEntry.key
			val List<ALSSignatureDeclaration> signatures = new LinkedList
			
		}
	}
	
	def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
		val res = trace.typeMapperTrace
		if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) {
			return res
		} else {
			throw new IllegalArgumentException('''
			Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name»,
			but found «res.class.name»''')
		}
	}
	
	private def boolean hasDefinedSupertype(Type type) {
		if(type instanceof TypeDefinition) {
			return true
		} else {
			if(type.supertypes.empty) return false
			else return type.supertypes.exists[it.hasDefinedSupertype]
		}
	}
	
	private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) {
		trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [
			it.name = support.toID(#["util","defined","Object"])
		]
		trace.specification.signatureBodies += createALSSignatureBody => [
			it.abstract = true
			it.declarations += trace.typeTrace.definedSupertype
		]
	}
	
	private def transformDefinedElements(List<DefinedElement> elements,
		Logic2AlloyLanguageMapperTrace trace){
		if(trace.typeTrace.definedSupertype != null) {			
			// 2. Create elements as singleton signatures subtype of definedSupertype
			val elementBodies = createALSSignatureBody => [
				it.multiplicity = ALSMultiplicity::ONE
				it.supertype = trace.typeTrace.definedSupertype
			]
			trace.specification.signatureBodies += elementBodies
			for(element : elements) {
				val elementDeclaration = createALSSignatureDeclaration => [
					it.name = support.toIDMultiple(#["element"],element.name)
				]
				elementBodies.declarations += elementDeclaration
				trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration)
			}
			// 3. Specify that definedSupertype is equal to the union of specified
			/*trace.specification.factDeclarations += createALSFactDeclaration => [
				it.name = support.toID(#["util","typehierarchy","definitionOfElements"])
				it.term = createALSEquals => [
					it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
					it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[
						it.referred = element.lookup(trace.typeTrace.definedElement2Declaration)
					]])
				]
			]*/
		}
	}
	
	///// Type definitions
	
	protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) {
		val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)]
		val body = createALSSignatureBody => [
			it.declarations += sig
			it.superset += trace.typeTrace.definedSupertype
		]
		trace.specification.signatureBodies += body
		trace.typeTrace.definition2definition.put(type,sig)
	}
	protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
		val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)]
		val body = createALSSignatureBody => [
			it.declarations += sig
			it.superset += trace.typeTrace.definedSupertype
		]
		trace.specification.signatureBodies += body
		trace.typeTrace.declaration2definition.put(type,sig)
	}
	protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
		val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)]
		val body = createALSSignatureBody => [
			it.declarations += sig
			it.supertype = trace.typeTrace.definedSupertype
		]
		trace.specification.signatureBodies += body
		trace.typeTrace.undefined2definition.put(type,sig)
	}
	protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
		val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)]
		val body = createALSSignatureBody => [
			it.declarations += sig
			it.supertype = trace.typeTrace.declaredSupertype
		]
		trace.specification.signatureBodies += body
		trace.typeTrace.new2declaration.put(type,sig)
	}
	
	/**
	 * The dynamic types cover each concrete types
	 */
	protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) {
		trace.specification.factDeclarations += createALSFactDeclaration => [
			it.name = support.toID(#["util","typehierarchy","elementFull"])
				it.term = createALSEquals => [
					it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
					it.rightOperand = support.unfoldPlus(
						trace.typeTrace.allDefinedTypes.map[type|
							createALSReference=>[referred = type]
						].toList
					)
				]
		]
		
	}
	/**
	 * The dynamic types are disjoint
	 */
	protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) {
		val types = trace.getTypeTrace.allDefinedTypes.toList
		if (types.size >= 2) {
			trace.specification.factDeclarations += createALSFactDeclaration => [
				it.name = support.toID(#["util", "typehierarchy", "elementFull"])
				it.term = types.disjointSets
			]
		}
	}
	/**
	 * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not
	 */
	protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) {
		val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes)
		for(constraintOnElement : constraintOnElements.entrySet) {
			val element = constraintOnElement.key
			val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration)
			val constraint = constraintOnElement.value
			
			var ALSTerm negativeConstraints;
			if(constraint.negative.isEmpty) {
				negativeConstraints = null
			} else {
				negativeConstraints = support.unfoldAnd(constraint.negative.map[type|
					createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ]
				].toList)
			}
			
			var ALSTerm positiveTypeConstraints
			if(constraint.positiveCNF.isEmpty) {
				positiveTypeConstraints = null
			} else {
				positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition |
					support.unfoldOr(typeConstraintFromDefinition.map[type |
						elementInDefinedType(elementSignature,type,trace)
					].toList,trace)
				])
			}
			
			var ALSTerm typeConstraint
			if(negativeConstraints != null && positiveTypeConstraints == null) {
				typeConstraint = negativeConstraints
			} else if (negativeConstraints == null && positiveTypeConstraints != null) {
				typeConstraint = positiveTypeConstraints
			} else if (negativeConstraints != null && positiveTypeConstraints != null) {
				val and = createALSAnd
				and.leftOperand = positiveTypeConstraints
				and.rightOperand = negativeConstraints
				typeConstraint = and
			} else {
				typeConstraint = null
			}
			
			if(typeConstraint != null) {
				val fact =  createALSFactDeclaration => [
					name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name)
				]
				fact.term = typeConstraint
				trace.specification.factDeclarations +=fact
			}
			// otherwise there is no type constraint on element
		}
	}
	
	private def elementInDefinedType(
		ALSSignatureDeclaration elementSignature,
		Type type,
		Logic2AlloyLanguageMapperTrace trace)
	{
		var ALSSignatureDeclaration signature
		if(type instanceof TypeDeclaration) {
			if(trace.typeTrace.declaration2definition.containsKey(type)) {
				signature = type.lookup(trace.typeTrace.declaration2definition)
			} else if(trace.typeTrace.undefined2definition.containsKey(type)) {
				signature = type.lookup(trace.typeTrace.undefined2definition)
			} else {
				return null
			}
		} else if(type instanceof TypeDefinition) {
			if(trace.typeTrace.definition2definition.containsKey(type)) {
				signature = type.lookup(trace.typeTrace.definition2definition)
			} else {
				return null
			}
		} else throw new IllegalArgumentException('''Unknownt type «type.class.name»''')
		
		val finalSignature = signature
		return createALSSubset => [
			leftOperand = createALSReference => [
				referred = elementSignature
			]
			rightOperand = createALSReference => [
				referred = finalSignature
			]
		]
	}
	
	def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) {
		if(trace.incqueryEngine == null) {
			trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
		}
		val matcher = SupertypeStarMatcher.on(trace.incqueryEngine)
		val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap
		for(supertype : problem.types) {
			typeToConcreteSubtypes.put(
				supertype,
				matcher.getAllValuesOfsubtype(supertype)
					.filter[!it.isIsAbstract].toList)
		}
		return typeToConcreteSubtypes
	}
	
	/**
	 * Gives type constraints in a form of CNF 
	 */
	def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) {
		val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap
		elements.forEach[constraints.put(it,new DynamicTypeConstraints)]
		
		for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) {
			val subtypes = type.lookup(typeToConcreteSubtypes)
			for(elementInType:type.elements) {
				elementInType.lookup(constraints).addPositiveTypeOptions(subtypes)
			}
			for(elementNotInType:elements.filter[!type.elements.contains(it)]) {
				elementNotInType.lookup(constraints).addNegativeTypes(subtypes)
			}
		}
		
		return constraints
	}
	
	private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) {
		if(signatures.size >= 2){
			val top = createALSEquals => [
				it.leftOperand = signatures.intersectionOfTypes
				it.rightOperand = createALSNone
			]
			if(signatures.size > 2) {
				return createALSAnd => [
					it.leftOperand = top
					it.rightOperand = signatures.subList(1,signatures.size).disjointSets
				]
			} else{
				return top
			}
		} else {
			throw new UnsupportedOperationException()
		}
	}
	
	private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) {
		if(signatures.size == 2) {
			return createALSIntersection => [
				leftOperand = createALSReference => [it.referred = signatures.get(0)]
				rightOperand = createALSReference => [it.referred = signatures.get(1)]
			]
		} else if(signatures.size > 2) {
			return createALSIntersection => [
				leftOperand = createALSReference => [it.referred = signatures.get(0)]
				rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes
			]
		} else throw new UnsupportedOperationException()
	}
	
	
	override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		//trace.typeTrace.
	}
}