/*Title: Tefkat trnasformation rules between Ecore and Object-Z
* Author: Soon-Kyeong Kim
* Last Modified: 28 February 2006 
* <copyright>
* Information Technology and Electrical Engineering
* The University of Queensland, St. Lucia, 4072, Australia
* </copyright>
*/

TRANSFORMATION EcoretoOZ : Ecore -> ObjectZ

IMPORT http:///ecoreTracking
IMPORT http:///oz.ecore
IMPORT http://www.eclipse.org/emf/2002/Ecore
//IMPORT http://www.itee.uq.edu.au/~mdavv/1.0.0/oz.ecore

	// Produces an OZ specification for each Ecore package (root of OZ spec)
	// 
	RULE EPackage2OZSpec(ep, ozs)
		FORALL 	EPackage ep
		MAKE 	OZSpecification ozs
		SET	ozs.name = ep.name 
		LINKING	EPackOZSpec
		WITH	ozspec = ozs, epack = ep
		;
	
	// Mapping Ecore types to OZ types

	// For ecore data types (except enumeration types and 
	// those predefined data types that have corresponding data types in OZ, e.g.
	// EInt, EBoolean, EFloat)
	// makes a given type in OZ.	
	RULE EOtherDataType2OZOtherType(et, gt, ozs, ep)
		FORALL	EDataType et
		WHERE	EPackOZSpec LINKS ozspec = ozs, epack = ep
		AND	NOT isEEnum(et) 
		//need to check all otherpredefined ecore types
		AND	NOT isEClassType(et)
		AND	ep.eClassifiers = et
		MAKE	GivenType gt
		SET	gt.name = et.name, gt.owner = ozs
		LINKING	EDataTypeOZOtherType
		WITH	other = gt, edata= et, ozspec = ozs, epack = ep
		;
	
		
	// Maps ecore enumeration types to OZ free types
	// 	
	RULE EEnum2OZFreeType(ft, et, ozs, ep)
		FORALL	EEnum et 
		WHERE	EPackOZSpec LINKS ozspec = ozs, epack = ep
		AND	ep.eClassifiers = et 
		MAKE	FreeType ft
		SET	ft.name = et.name, ft.owner = ozs
		LINKING	EEnumFreeType
		WITH	free = ft, enum = et, ozspec = ozs, epack = ep
		;

	// Maps ecore enumeration literals to OZ free type braches
	// 
	RULE EEnumLiteral2OZBranch(el, br, ozf, ee)
		FORALL	EEnumLiteral el 
		WHERE	EEnumFreeType LINKS free = ozf, enum = ee
		AND	ee.eLiterals = el 
		MAKE	Branch br
		SET	br.name = el.name, br.freetype = ozf
		//br.name = el.value
		LINKING	EEnumLiteralBranch
		WITH	branch = br, eliteral = el, free = ozf, enum = ee
		;
	
	
	// Patterns to check types of Ecore elements 
	// 
	PATTERN isEClassType(etype)
	    FORALL  EClass etype;
	
	PATTERN isEDataType(etype)
	    FORALL  EDataType etype;
	
	PATTERN isEEnum(etype)
	    FORALL  EEnum etype;
	    
	// Produces a Class for each Ecore class
	// 
	RULE EClass2OZClass(ep, ozs, ozc, ec, com)
		FORALL	EClass ec
		WHERE	EPackOZSpec LINKS ozspec = ozs, epack = ep
		AND	ep.eClassifiers = ec
		MAKE	OZClass ozc
		SET 	ozc.name = ec.name, ozc.owner = ozs,
		IF 	isAbstract(ec) THEN MAKE OZComment com, OZExpression exp, OZPredicate pre
		SET 	//constain formalizing the abstract class concept in UML 
			exp.name = "ECore abstract class",
			com.body = "ECore abstract class",
			ozc.comment = com,		
			exp.body = append(ozc.name, " = \\emptyset"),
				pre.specification = exp, ozc.invariant = pre
		ENDIF		
		LINKING	EClassOZClass
		WITH	ozclass = ozc, eclass = ec, ozspec = ozs, epack = ep
		;
	
	// Maps Ecore supertypes to the general class set of the correspoing OZ class
	//
	RULE ESuperType2OZInherit(ec, ozs, ozg, est)
		FORALL 	EClass ec, EClass est 
		WHERE	lookupClass(ozs, ec)
		AND	lookupClass(ozg, est)
		AND	ec.eSuperTypes = est 
		SET	ozs.general = ozg
		;
	
	// Pattern to lookup classes
	//	
	PATTERN lookupClass(ozc, ec)
		WHERE 	EClassOZClass LINKS ozclass = ozc, eclass = ec
		;


	
	// Pattern to map parameter kinds
	//
	PATTERN lookupParamKind(ozparkind)
		WHERE	ozo = <http:///oz.ecore#//ParameterKind/output>
		AND	ozparkind = ozo.instance
		;
		
			
	// Produces an OZ operation for each Ecore Operation
	// Also produces a return paramter for each Ecore Operation
	// This is because in Ecore, operations are a typed element including 
	// the semantics of a return parameter as part of the operation semanitcs
	RULE EOperation2OZOperation(ec, ozc, ozo, eo, ep, ozop, ozs, epa)
		FORALL  EOperation eo	
		WHERE	lookupClass(ozc, ec)
		AND	ec.eOperations = eo 
		AND	EPackOZSpec LINKS ozspec = ozs, epack = epa
		AND	EClassOZClass LINKS ozclass = ozc, eclass = ec, ozspec = ozs, epack = epa
		AND 	lookupParamKind(ozpkind)
		AND 	et = eo.eType
		MAKE    OZOperation ozo, OZParameter ozp 
		SET	ozo.name = eo.name, ozc.operation = ozo,
			
			//mapping properties to the return parameter  
			ozp.name = eo.name,
			ozp.isOrdered = eo.ordered, 
			ozp.lower = eo.lowerBound, ozp.upper = eo.upperBound,
			ozp.owner = ozo,
			//mapping parameter kind as output
			ozp.kind = ozpkind,
			
			IF lookupType(ozt, et) THEN 
			SET ozp.type = ozt 
			ENDIF,
			
			//If the class type is abstract, set the isPolymorphic feature of the OZ attribute true
			IF isEClassType(et) AND isAbstract(et) THEN
			SET	ozp.isPolymorphic = true 
			ENDIF,
			
			//From Ecore to OZ, we need to create datatypes in each instance model 
			//From OZ to Ecore, we can map OZ types to Ecore predefined data types. 
			//Creates an OZ basic type for Ecore EInt, EFloat and EBoolean types  	
			IF et.name = "EInt" OR et.name = "EFloat" OR et.name = "EBoolean" THEN
				MAKE println("test", et.name), BasicType bt FROM basicTypeFromEcoreType(et.name) 
				SET IF (et.name = "EInt") THEN SET bt.name = "Integer", ozp.type = bt
				    ELSEIF (et.name = "EFloat") THEN SET bt.name = "Real", ozp.type = bt
				    ELSEIF (et.name = "EBoolean") THEN SET bt.name = "Boolean", ozp.type = bt
				    ENDIF,
				    ozs.type = bt
				LINKING	EDataTypeBasicType
				WITH	basic = bt, edata= et, ozspec = ozs, epack = epa
			ENDIF,
				
			//Creates an OZ given type if the type is not Ecore EInt, EFloat and EBoolean types  
			IF NOT (isEEnum(et) OR isEClassType(et) OR et.name = "EInt" OR et.name = "EFloat" OR
				et.name = "EBoolean") THEN
				MAKE GivenType gt FROM givenTypeFromEcoreType(et.name) 
				SET gt.name = et.name, ozp.type = gt,
				ozs.type = gt
				LINKING	EDataTypeOZOtherType
				WITH	other = gt, edata= et, ozspec = ozs, epack = epa
			ENDIF	
		
//		LINKING	EParameterOZParameter
//		WITH	ozop = ozo, eop = eo, ozpar = ozp, epar = ep
				
		LINKING	EOpOZOp
		WITH	ozop = ozo, eop = eo, ozclass = ozc, eclass = ec
		;
		
	// Pattern to map enumeration or class types
	//		
	PATTERN lookupType(ozt, et)
		WHERE  	EEnumFreeType LINKS free = ozt, enum = et
		OR	EClassOZClass LINKS ozclass = ozt, eclass = et
		;
		
	// Produces an OZ Parameter for each Ecore Parameter
	// 	
	RULE EParam2OZParam(ozo, eo, ozp, ep, ozt, et, ec, oc, ozs, epa)
		FORALL 	EParameter ep 
		WHERE	EOpOZOp LINKS ozop = ozo, eop = eo, ozclass = ozc, eclass = ec
		AND	EPackOZSpec LINKS ozspec = ozs, epack = epa
		AND	EClassOZClass LINKS ozclass = ozc, eclass = ec, ozspec = ozs, epack = epa
		AND	eo.eParameters = ep
		AND 	et = ep.eType
		MAKE    OZParameter ozp 
		SET	ozp.name = ep.name,
			ozp.isOrdered = ep.ordered, 
			ozp.lower = ep.lowerBound, ozp.upper = ep.upperBound,
			ozp.owner = ozo,

			IF lookupType(ozt, et) THEN 
			SET ozp.type = ozt 
			ENDIF,
			
			//If the class type is abstract, set the isPolymorphic feature of the OZ attribute true
			IF isEClassType(et) AND isAbstract(et) THEN
			SET	ozp.isPolymorphic = true 
			ENDIF,
			
			//From Ecore to OZ, we need to create datatypes in each instance model 
			//From OZ to Ecore, we can map OZ types to Ecore predefined data types. 
			//Creates an OZ basic type for Ecore EInt, EFloat and EBoolean types  	
			IF et.name = "EInt" OR et.name = "EFloat" OR et.name = "EBoolean" THEN
				MAKE println("test", et.name), BasicType bt FROM basicTypeFromEcoreType(et.name) 
				SET IF (et.name = "EInt") THEN SET bt.name = "Integer", ozp.type = bt
				    ELSEIF (et.name = "EFloat") THEN SET bt.name = "Real", ozp.type = bt
				    ELSEIF (et.name = "EBoolean") THEN SET bt.name = "Boolean", ozp.type = bt
				    ENDIF,
				    ozs.type = bt
				LINKING	EDataTypeBasicType
				WITH	basic = bt, edata= et, ozspec = ozs, epack = epa
			ENDIF,
				
			//Creates an OZ given type if the type is not Ecore EInt, EFloat and EBoolean types  
			IF NOT (isEEnum(et) OR isEClassType(et) OR et.name = "EInt" OR et.name = "EFloat" OR
				et.name = "EBoolean") THEN
				MAKE GivenType gt FROM givenTypeFromEcoreType(et.name) 
				SET gt.name = et.name, ozp.type = gt,
				ozs.type = gt
				LINKING	EDataTypeOZOtherType
				WITH	other = gt, edata= et, ozspec = ozs, epack = epa
			ENDIF	
		
		LINKING	EParameterOZParameter
		WITH	ozop = ozo, eop = eo, ozpar = ozp, epar = ep
		;
	
	

	// Produces an OZ attribute for each Ecore attribute
	//
	RULE EAttribute2OZPureAttribute(ozc, ec, et, oza, ea, ozt, ozot, ep, ozs)
		FORALL 	EAttribute ea 
		WHERE	lookupClass(ozc, ec)
		AND	EPackOZSpec LINKS ozspec = ozs, epack = ep
		AND	EClassOZClass LINKS ozclass = ozc, eclass = ec, ozspec = ozs, epack = ep
		AND	ec.eAttributes = ea
		AND 	ea.eAttributeType = et
		AND	ozs.type = ozc
		AND	ep.eClassifiers = ec
		MAKE    PureAttribute oza, println("test", et.name)
		SET	oza.name = ea.name, oza.owner = ozc,
			//mapping multiplicity feature
			oza.lower = ea.lowerBound, oza.upper = ea.upperBound,
			//mapping ordered feature
			oza.isOrdered = ea.ordered,
			
			//mapping changeability feature in ecore
			IF (ea.changeable = true) THEN
			SET oza.isConstant = false
			ELSEIF oza.isConstant = true
			ENDIF,
			
			//mapping derived feature in ecore
			oza.isSecondary = ea.derived,
			
			//mapping type
			IF lookupType(ozt, et) THEN 
			MAKE println("test", ozt.eClass().name, ozt.name, et.name) 
			SET oza.type = ozt 
			ENDIF,
			
			//mapping initial values 
			IF isDefaultValue(ea.defaultValueLiteral)
			THEN MAKE OZExpression initial 
			SET initial.body = ea.defaultValueLiteral,
				oza.initialValue = initial
			ENDIF,
			
			//Creates an OZ basic type for Ecore EInt, EFloat and EBoolean types  	
			IF et.name = "EInt" OR et.name = "EFloat" OR et.name = "EBoolean" THEN
				MAKE println("test", et.name), BasicType bt FROM basicTypeFromEcoreType(et.name) 
				SET IF (et.name = "EInt") THEN SET bt.name = "Integer", oza.type = bt
				    ELSEIF (et.name = "EFloat") THEN SET bt.name = "Real", oza.type = bt
				    ELSEIF (et.name = "EBoolean") THEN SET bt.name = "Boolean", oza.type = bt
				    ENDIF,
				    ozs.type = bt 
				LINKING	EDataTypeBasicType
				WITH	basic = bt, edata= et, ozspec = ozs, epack = ep
			ENDIF, 
			
			//Creates an OZ given type if the type is not Ecore EInt, EFloat and EBoolean types  
			IF NOT (isEEnum(et) OR isEClassType(et) OR et.name = "EInt" OR et.name = "EFloat" OR
				et.name = "EBoolean") THEN
				MAKE GivenType gt FROM givenTypeFromEcoreType(et.name) 
				SET gt.name = et.name, oza.type = gt,
					ozs.type = gt
				LINKING	EDataTypeOZOtherType
				WITH	other = gt, edata= et, ozspec = ozs, epack = ep
			ENDIF	
									
			LINKING	EAttributeOZPureAttribute
			WITH	ozatt = oza, eatt = ea, ozclass = ozc, eclass = ec
		;
	
	// Pattern to check the existence of initial values
	//
	PATTERN isDefaultValue(exp)
		FORALL 	EString exp
		;
	
	// Pattern to check abstract classes
	//	
	PATTERN isAbstract(ec)
		FORALL 	EClass ec
		WHERE ec.abstract = true
		;
		
	// Pattern to check the existence of Ecore opposite
	//	
	PATTERN isEOpposite(eop)
		FORALL 	EReference eop 
		;
		
	PATTERN hasEOpposite(er)
		FORALL 	EReference er, EReference eop
		WHERE	er.EOpposite = eop 
		;
		
	// Produces an OZ relationship attribute for each Ecore reference
	//
	RULE EReferences2OZRelAttr(ozc, ot, ec, ozra, er, et)
		FORALL 	EReference er 
		WHERE	lookupClass(ozc, ec)
		AND	ec.eReferences = er 
		// convert attribute type
		AND	er.eReferenceType = et
		MAKE    RelationshipAttribute ozra 
		SET	ozra.name = er.name, ozra.owner = ozc,
			//mapping multiplicity feature
			ozra.lower = er.lowerBound, ozra.upper = er.upperBound,
			//mapping ordered feature
			ozra.isOrdered = er.ordered,

			// mapping containment feature
			ozra.isContainment = er.containment,
			
			//mapping changeability feature
			IF (er.changeable = true) THEN
			SET ozra.isConstant = false
			ELSEIF ozra.isConstant = true
			ENDIF,
			
			//mapping derived feature
			ozra.isSecondary = er.derived,

			//mapping types
			IF lookupType(ozt, et) THEN 
			MAKE println("test", er.eContainingClass.name, er.name, er.lowerBound, er.upperBound, er.eOpposite.name, er.eOpposite.lowerBound, er.eOpposite.upperBound) 
			SET ozra.type = ozt 
			ENDIF,
			
			//checking abstract classes and making the relationship attribute polimorphic 
			IF isAbstract(et) THEN
			SET 	ozra.isPolymorphic = true 
			ENDIF,
				
			//mapping initial values 
			IF isDefaultValue(er.defaultValueLiteral)
			THEN MAKE OZExpression initial 
			SET initial.body = er.defaultValueLiteral,
				ozra.initialValue = initial
			ENDIF,
			
			//mapping eOpposite
			//prodiuces constraints formalizing the object references according to the properties of the eOpposite
			// 
			IF isEOpposite(er.eOpposite) THEN
			MAKE println("test EPoosite", er.eContainingClass.name, er.name, er.lowerBound, er.upperBound, er.eOpposite.name, er.eOpposite.lowerBound, er.eOpposite.upperBound),
			OZExpression exp, OZPredicate pre, OZComment com
			SET exp.name = "ECore eOpposite", com.body = "ECore eOpposite", exp.comment = com,
						
			// 1 to 1 relationship 
			IF (er.lowerBound = 1 AND er.upperBound = 1 AND er.eOpposite.lowerBound = 1 AND er.eOpposite.upperBound = 1) THEN 
			SET exp.body = append("\\self = ", ozra.name, ".", er.eOpposite.name)
					
			ENDIF,
			
			// 1 to many relationship not ordered	
			IF (er.lowerBound = 1 AND er.upperBound = 1 AND NOT er.eOpposite.upperBound = 1)  
				AND er.eOpposite.ordered = false
			THEN	
			SET exp.body = append("\\self \\in ", ozra.name, ".", er.eOpposite.name)
			ENDIF,
			
			// 1 to many relationship ordered	
			IF (er.lowerBound = 1 AND er.upperBound = 1 AND NOT er.eOpposite.upperBound = 1) 
				AND er.eOpposite.ordered = true
							
			THEN 
			SET exp.body = append("\\self \\in \\ran(", ozra.name, ".", er.eOpposite.name, ")")
			ENDIF,
			
			// not ordered many to 1 relationship	
			IF er.ordered = false
				AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND er.eOpposite.lowerBound = 1 
				AND er.eOpposite.upperBound = 1 
			THEN 
			SET exp.body = append("\\forall o: ", ozra.name, " @ ", "\\self = o.", er.eOpposite.name)
			ENDIF,
			
			// ordered many to 1 relationship	
			IF er.ordered = true 
				AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND er.eOpposite.lowerBound = 1 
				AND er.eOpposite.upperBound = 1 
			THEN 
			SET exp.body = append("\\forall o: \\ran(", ozra.name, ") @ ", "\\self = o.", er.eOpposite.name)
			ENDIF,
			
			// not ordered many to not ordered many relationship
			IF er.ordered = false
				 AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND NOT (er.eOpposite.lowerBound = 1  AND er.eOpposite.upperBound = 1) 
				 AND er.eOpposite.ordered = false
			THEN 
			SET exp.body = append("\\forall o: ", ozra.name, " @ ", "\\self \\in o.", er.eOpposite.name)
			ENDIF,
			
			// ordered many to ordered many relationship
			IF er.ordered = true
				AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND NOT (er.eOpposite.lowerBound = 1  AND er.eOpposite.upperBound = 1) 
				AND er.eOpposite.ordered = true
				THEN 
			SET exp.body = append("\\forall o: \\ran(", ozra.name, ") @ ", "\\self \\in \\ran(o.", er.eOpposite.name, ")")
			ENDIF,
			
			// ordered many to not ordered many relationship
			IF er.ordered = true
				AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND NOT (er.eOpposite.lowerBound = 1  AND er.eOpposite.upperBound = 1) 
				AND  er.eOpposite.ordered = false
				THEN 
			SET exp.body = append("\\forall o: \\ran(", ozra.name, ") @ ", "\\self \\in o.", er.eOpposite.name)
			ENDIF,
			
			// not ordered many to ordered many relationship
			IF er.ordered = false
				AND NOT (er.lowerBound = 1 AND er.upperBound = 1) AND NOT (er.eOpposite.lowerBound = 1  AND er.eOpposite.upperBound = 1) 
				AND er.eOpposite.ordered = true
			THEN 
			SET exp.body = append("\\forall o:", ozra.name, " @ ", "\\self \\in \\ran(o.", er.eOpposite.name, ")")
				
			ENDIF,
			
			pre.specification = exp, ozra.constraint = pre
		
			ENDIF
						
			LINKING	EReferenceOZRelAttribute
			WITH	ozrel = ozra, eref = er, ozclass = ozc, eclass = ec
		;
	
	
	// Pattern to check the existence of Ecore annotation
	//
//	PATTERN isEAnnotation(ean)
//	    FORALL  EAnnotation ean;
	    
	
	// an example rule converting ecore class annotations to OZ class comment
//	RULE EClassEAnnotation2OZClassInvariant(ean, ozp, oze, ec, ozc)
//		FORALL 	EAnnotation ean, EClass ec 
//		WHERE	ean.eModelElement = ec
//		AND	ec.eAnnotations = ean
//		AND	lookupClass(ozc, ec)
//		MAKE	OZComment ozc
//		SET 	ozc.body = ean.source
//			ozc.comment = ozc
//		;