import 'QVTimperative.ecore'

--package ocl
--context Element
--def: joinNames(names : Set(String)) : String = '{' + names->sortedBy(n | n)->iterate(n; s : String = '' | if s = '' then n else s + ';' + n endif) + '}'
--endpackage

package qvtimperative

context AddStatement
inv CompatibleTypeForValue: ownedExpression.type?.conformsTo(targetVariable.type)

context BufferStatement
inv CompatibleTypeForValue: ownedExpression <> null implies ownedExpression.type.oclAsType(ocl::CollectionType).elementType.conformsTo(type)

context CheckStatement
inv TypeIsBoolean: ownedExpression.type = Boolean

context DeclareStatement
--inv CompatibleTypeForCheckedValue: isCheck implies type.conformsTo(ownedExpression.type)
inv CompatibleTypeForUncheckedValue: not isCheck implies ownedExpression.type?.conformsTo(type)

--context GuardParameter
--FIXME completeType inv TypedModelContainsType: referredTypedModel.allUsedPackages->includes(type.oclContainer())

context ImperativeTransformation
inv AllRulesAreMappings: rule->forAll(oclIsKindOf(Mapping))
inv UniqueTargetNames: rule->selectByKind(EntryPoint)->select(targetName <> null)->isUnique(targetName)

--context ImperativeTypedModel
--def: allUsedPackages : Set(ocl::Package) = usedPackage
--inv NameIsNotNull : name <> null
--inv NotBothInputAndOutput: not (isInput and isOutput)

context Mapping
inv NameIsNotNull : name <> null
inv MappingParameterNamesAreUnique: ownedMappingParameters->isUnique(name)
inv LocalVariableNamesAreUnique: ownedMappingParameters->union(ownedStatements->selectByKind(VariableStatement))->isUnique(name)
-- FIXME statment ordering

context MappingCall
def: referredNames : OrderedSet(String) = referredMapping.ownedMappingParameters.name->asSet()->sortedBy(n | n)
def: bindingNames : OrderedSet(String) = ownedMappingParameterBindings.boundVariable.name->asSet()->sortedBy(n | n)
inv MatchingCallBindings('MappingCall::MatchingCallBindings: ' + referredMapping.name + ' ' + joinNames(bindingNames) + ' <> ' + joinNames(referredNames)): referredNames = bindingNames
inv NotBothInstallAndInvoke: not (isInstall and isInvoke)
inv UniqueCallBindings: ownedMappingParameterBindings->isUnique(boundVariable)

context MappingParameterBinding
inv ParameterIsMappingParameter: owningMappingCall.referredMapping.ownedMappingParameters->includes(boundVariable)

context NewStatement
inv CompatibleTypeForValue: ownedExpression <> null implies ownedExpression.type?.conformsTo(type)
inv NonDataTypeForType: not type.oclIsKindOf(ocl::DataType)
--FIXME completeType inv TypedModelContainsType: referredTypedModel.allUsedPackages->includes(type.oclContainer())

context SetStatement
def:resolvedProperty : ocl::Property[1] = if isOpposite then targetProperty.opposite else targetProperty endif

inv CompatibleClassForProperty:
	let requiredType = resolvedProperty.owningClass in
	let actualType = targetVariable.type in
	Tuple{
		status : Boolean = actualType?.conformsTo(requiredType),
		message : String = 'SetStatement::CompatibleClassForProperty: ' + actualType?.name + ' must conform to ' + requiredType?.name
	}.status

inv CompatibleTypeForPartialValue:
	isPartial implies
		let requiredType = resolvedProperty.type.oclAsType(ocl::CollectionType).elementType in
		let actualType = ownedExpression.type in
		Tuple{
			status : Boolean = actualType?.conformsTo(requiredType),
			message : String = 'SetStatement::CompatibleTypeForPartialValue: ' + actualType?.name + ' must conform to ' + requiredType.name
		}.status

inv CompatibleTypeForTotalValue:
	not isPartial implies
		let requiredType = resolvedProperty.type in
		let actualType = ownedExpression.type in
		Tuple{
			status : Boolean = actualType?.conformsTo(requiredType),
			message : String = 'SetStatement::CompatibleTypeForTotalValue: ' + actualType?.name + ' must conform to ' + requiredType?.name
		}.status

inv ValueDoesNotNavigateFromRealizedVariables:
ownedExpression->closure(e : ocl::OclElement | e.oclContents())->selectByKind(ocl::VariableExp)->select(referredVariable.oclIsKindOf(NewStatement))->select(s | s.oclContainer().oclIsKindOf(ocl::CallExp) and s.oclContainer().oclAsType(ocl::CallExp).ownedSource = s)->isEmpty()

inv TargetPropertyIsNotReadOnly:
not resolvedProperty.isReadOnly

context SimpleParameterBinding
inv CompatibleTypeForCheckedValue: isCheck implies boundVariable.type?.conformsTo(value.type)
inv CompatibleTypeForUncheckedValue: not isCheck implies value.type?.conformsTo(boundVariable.type)

context Statement
def: joinNames(names : OrderedSet(String)) : String = '{' + names/*->sortedBy(n | n)*/->iterate(n; s : String = '' | if s = '' then n else s + ';' + n endif) + '}'


endpackage