-----------------------------------------------------------------------
-- EMOF
-----------------------------------------------------------------------
package EMOF

context Class
def: allOwnedAttributes : Set(Property) =
    superClass.allOwnedAttributes->asSet()->union(ownedAttribute)
def: allSuperClasses : Set(Class) =
    superClass.allSuperClasses->asSet()->union(superClass)
def: definesProperty(p : Property) : Boolean =
    allOwnedAttributes->includes(p)
    
context Element
def: ancestors : OrderedSet(Element) =
    if container() <> null
    then container().oclAsType(Element).ancestors->append(self)
    else self->asOrderedSet()
    endif
def: hasAncestor(e : Element) : Boolean =
    let parent : Element = container() in
    (parent = e)
    or ((parent <> null) and parent.hasAncestor(e))
def: children : Set(Element) =
    Element.allInstances()->select(e | e.ancestors->includes(self))   
def: allVariableExps : Set(EssentialOCL::VariableExp) =
    children->select(oclIsKindOf(EssentialOCL::VariableExp))
        .oclAsType(EssentialOCL::VariableExp)->asSet()
def: allReferencedVariables : Set(EssentialOCL::Variable) =
    allVariableExps.referredVariable->asSet()
def: allOclExpressions : Set(EssentialOCL::OclExpression) =
    children->select(oclIsKindOf(EssentialOCL::OclExpression))
        .oclAsType(EssentialOCL::OclExpression)->asSet()
def: allCollectionTypes : Set(EssentialOCL::CollectionType) =
    allOclExpressions.type->select(oclIsKindOf(EssentialOCL::CollectionType))
        .oclAsType(EssentialOCL::CollectionType)->asSet()
def: locallyDefined(v : EssentialOCL::Variable) : Boolean =
    if (oclIsKindOf(EssentialOCL::LetExp)
        and (oclAsType(EssentialOCL::LetExp).variable = v))
    or (oclIsKindOf(EssentialOCL::IterateExp)
        and ((oclAsType(EssentialOCL::IterateExp).result = v) 
             or oclAsType(EssentialOCL::IterateExp).iterator->includes(v)))
    or (oclIsKindOf(EssentialOCL::LoopExp)
        and oclAsType(EssentialOCL::IterateExp).iterator->includes(v))
    then true
    else let parent : EMOF::Element = container() in
        if parent.oclIsKindOf(EssentialOCL::OclExpression)
        or parent.oclIsKindOf(EssentialOCL::CollectionLiteralPart)
        or parent.oclIsKindOf(EssentialOCL::TupleLiteralPart)
        then parent.locallyDefined(v)
        else false
        endif
    endif
--def: properAncestors : OrderedSet(Element)
----    = ancestors->excluding(self)
--    = ancestors->excluding(self)->asOrderedSet()   
--def: properChildren : Set(Element)
--    = children->excluding(self)
    
context Type
def: transitiveElementType() : Type =
    if oclIsKindOf(EssentialOCL::CollectionType)
    then oclAsType(EssentialOCL::CollectionType).elementType.transitiveElementType()
    else self
    endif
def: isPredefinedType() : Boolean =
    (self = Boolean)
    or (self = Integer)
    or (self = Real)
    or (self = String)
    or (self = UnlimitedNatural)
def: assignableFrom(t : Type) : Boolean = -- FIXME Set assignments
    if oclIsKindOf(EssentialOCL::CollectionType) and t.oclIsKindOf(EssentialOCL::CollectionType)
    then let et : Type = oclAsType(EssentialOCL::CollectionType).elementType in
        et = OclVoid
        or et.assignableFrom(t.oclAsType(EssentialOCL::CollectionType).elementType)
    else t.getMetaClass().allSuperClasses->includes(getMetaClass())
    endif   
def: matches(t : Type) : Boolean =
    self = t                   -- FIXME   

context Property
def: propertyKind : EssentialOCL::CollectionKind =
    if upper <= 1
    then null
    else if isUnique
        then
            if isOrdered
            then EssentialOCL::CollectionKind::OrderedSet
            else EssentialOCL::CollectionKind::Set
            endif
        else
            if isOrdered
            then EssentialOCL::CollectionKind::Sequence
            else EssentialOCL::CollectionKind::Bag
            endif 
        endif
    endif

endpackage

-----------------------------------------------------------------------
-- EssentialOCL
-----------------------------------------------------------------------
package EssentialOCL
    
context Variable
def: isSpecialVariable() : Boolean =
    name = '_'

context OclExpression
--def: allReferencedTypes : Set(EMOF::Type)
--    = allOclExpressions.type->asSet()
--def: allReferencedCollectionTypes : Set(CollectionType)
--    = allOclExpressions.type->select(oclIsKindOf(CollectionType)).oclAsType(CollectionType)->asSet()
def: allReferencedElementTypes : Set(EMOF::Type) =
    allOclExpressions.type.transitiveElementType()->asSet()
--def: nonExpressionParent : EMOF::Element
--    = if container().oclIsKindOf(OclExpression)
--    then container().oclAsType(OclExpression).nonExpressionParent
--    else container()
--    endif
def: isSpecialVariableReference() : Boolean =
    oclIsKindOf(EssentialOCL::VariableExp)
    and let v : EssentialOCL::Variable
        = oclAsType(EssentialOCL::VariableExp).referredVariable in
    (v <> null) and v.isSpecialVariable()
    
context VariableExp
inv UnderscoreOnlyUsedAsCollectionTemplateExpMemberOrRest:
    name = '_'
    implies container().oclIsKindOf(QVTTemplate::CollectionTemplateExp)
    and let cte : QVTTemplate::CollectionTemplateExp
        = container().oclAsType(QVTTemplate::CollectionTemplateExp) in
        (cte.rest = self)
        or (cte.member->exists(referredVariable = self))
    
context CollectionType
def: kind() : CollectionKind =
    if oclIsKindOf(BagType) then CollectionKind::Bag
    else if oclIsKindOf(OrderedSetType) then CollectionKind::OrderedSet
    else if oclIsKindOf(SequenceType) then CollectionKind::Sequence
    else if oclIsKindOf(SetType) then CollectionKind::Set
    else CollectionKind::Collection
    endif endif endif endif

endpackage

-----------------------------------------------------------------------
-- QVTBase
-----------------------------------------------------------------------
package QVTBase

context TypedModel
def: allDependsOn : Set(TypedModel) =
    if dependsOn <> null
    then dependsOn.allDependsOn->asSet()->union(dependsOn)
    else Set{}
    endif
def: declaredPackages : Set(EMOF::Package) =
    dependsOn.declaredPackages->asSet()->union(usedPackage)
def: declaresType(t : EMOF::Type) : Boolean =
    t.isPredefinedType()
    or declaredPackages->includes(t._package)
def: equivalentTo(t : TypedModel) : Boolean =
    declaredPackages = t.declaredPackages
inv DependsOnIsAcyclic :
    allDependsOn->excludes(self)

context Transformation
def: allExtends : Set(Transformation) =
    if extends <> null
    then extends.allExtends->including(extends)
    else Set{}
    endif
def: declaredPackages : Set(EMOF::Package) =
    modelParameter.declaredPackages->asSet()
def: definesRule(r : Rule) : Boolean =
    rule->includes(r) or extends->exists(definesRule(r)) 
def: declaresType(t : EMOF::Type) : Boolean =
    t.isPredefinedType() or declaredPackages->includes(t._package)
def: definesModel(m : TypedModel) : Boolean =
    modelParameter->includes(m)
def: modelParameter(requiredName : String) : TypedModel =
    modelParameter->any(name = requiredName)
inv ExtendsIsAcyclic :
    allExtends->excludes(self)
inv ModelParameterNamesAreCompatibleWithExtension :
    extends <> null
    implies modelParameter.name = extends.modelParameter.name
inv EveryModelParameterUsedPackagesIsCompatibleWithExtension :
    extends <> null
    implies modelParameter->forAll(m |
        m.declaredPackages = extends.modelParameter(m.name).declaredPackages)
inv ModelParameterNamesAreUnique :
    modelParameter->isUnique(name)
inv RuleNamesAreUnique :
    rule->isUnique(name)
inv SynthesizedTypesAreOwned :
    ownedType->includesAll(allCollectionTypes)

context Domain
def: transformation : Transformation =
    rule.transformation
def: declaredPackages : Set(EMOF::Package) =
    typedModel.usedPackage
def: declaresType(t : EMOF::Type) : Boolean =
    t.isPredefinedType() or declaredPackages->includes(t._package)
inv TypedModelExistsWarning :
    typedModel <> null
inv TypedModelDefinedByTransformation :
    typedModel <> null
    implies transformation.definesModel(typedModel)
inv CheckableOrEnforceable :
    isCheckable or isEnforceable

context Rule
def: domain(requiredName : String) : Domain =
    domain->any(name = requiredName)
inv OverridesIsCompatible :
    overrides <> null
    implies domain->forAll(d |
        d.typedModel.equivalentTo(overrides.domain(d.name).typedModel)) 
inv OverridesDefinedByTransformation :
    overrides <> null implies transformation.definesRule(overrides)
inv DomainNamesAreUnique :
    domain->isUnique(name)
inv TypedModelsAreUnique :
    domain->isUnique(typedModel)

context Function
inv IsSideEffectFree :
    true -- FIXME no RelationCallExp, no ImperativeOCL
inv EveryFunctionParameterIsAFunctionParameter :
    ownedParameter->forAll(oclIsKindOf(FunctionParameter))

context Predicate
inv ConditionExpressionIsBoolean :
    conditionExpression.type.oclIsKindOf(Boolean)
--inv VariablesAreBoundByPattern :
--    pattern.bindsTo->includesAll(conditionExpression.allReferencedVariables)

context Pattern
inv NoVariableIsAFunctionParameter :
    not bindsTo->exists(oclIsKindOf(FunctionParameter))
        
endpackage

-----------------------------------------------------------------------
-- QVTCore
-----------------------------------------------------------------------
package QVTCore

context Mapping
def: allSpecifications : Set(Mapping)
    = specification.allSpecifications->asSet()->union(specification)
def: sideArea(domain : CoreDomain) : CoreDomain
    = domain->any(name = domain.name)
def: allMiddleAreas : Set(Mapping)
    = let childAreas : Bag(Mapping) = specification.allMiddleAreas->including(self)
    in if _context <> null
    then childAreas->union(_context.allMiddleAreas)->asSet()
    else childAreas->asSet() endif
def: allSideAreas(domain : CoreDomain) : Set(CoreDomain)
    = let childAreas : Bag(CoreDomain) = specification.allSideAreas(domain)->including(sideArea(domain))
    in if _context <> null
    then childAreas->union(_context.allSideAreas(domain))->asSet()
    else childAreas->asSet() endif
--def: declaresType(t : EMOF::Type) : Boolean
--    = true -- FIXME declaredPackages->includes(t._package)
inv ComposedMappingIsUnnamed :
    _context <> null implies name = null
inv NonComposedMappingIsNamed :
    _context = null implies name <> null
inv SpecificationIsAcyclic :
    allSpecifications->excludes(self)
inv RefinedMappingIsNotComposed :
    specification <> null implies _context = null
inv EveryRefinedMappingIsDefinedByTransformation :
    specification->forAll(s | transformation.definesRule(s))
inv EveryDomainIsACoreDomain :
    domain->forAll(oclIsKindOf(CoreDomain))

context Area
inv AreaIsCoreDomainOrMapping:
    oclIsKindOf(CoreDomain) or oclIsKindOf(Mapping)
def: bottomVariables : Set(EssentialOCL::Variable)
    = bottomPattern.variable->union(bottomPattern.realizedVariable)
def: guardVariables : Set(EssentialOCL::Variable)
    = guardPattern.variable
def: areaVariables : Set(EssentialOCL::Variable)
    = bottomVariables->union(guardVariables)
def: isMiddle : Boolean
    = oclIsKindOf(Mapping)
def: isEnforceable : Boolean
    = if (isMiddle)
    then oclAsType(Mapping).domain->exists(isEnforceable)
    else oclAsType(CoreDomain).isEnforceable endif

context CoreDomain
def: mapping : Mapping
    = rule.oclAsType(Mapping)
def: middleArea : Area
    = mapping
def: allDomains : Set(CoreDomain)
    = mapping.allSideAreas(self)
def: allBottomPatterns : Set(BottomPattern)
    = allDomains.bottomPattern->asSet()
def: allGuardPatterns : Set(GuardPattern)
    = allDomains.guardPattern->asSet()
def: allTypedModels : Set(QVTBase::TypedModel)
    = typedModel.allDependsOn
def: domainBottomVariables : Set(EssentialOCL::Variable)
    = bottomVariables->union(middleArea.bottomVariables)
def: domainGuardVariables : Set(EssentialOCL::Variable)
    = guardVariables->union(middleArea.guardVariables)
def: domainVariables : Set(EssentialOCL::Variable)
    = domainBottomVariables->union(domainGuardVariables)
def: declaresVariable(v : EssentialOCL::Variable) : Boolean
    = domainVariables->includes(v)
inv HasTypedModel :
    typedModel <> null
inv VariableNamesAreUnique :
    domainVariables->isUnique(name)

context CorePattern
def: area : CoreDomain
    = if oclIsKindOf(GuardPattern)
    then oclAsType(BottomPattern).area.oclAsType(CoreDomain)
    else oclAsType(GuardPattern).area.oclAsType(CoreDomain)
    endif
def: domain : CoreDomain
    = area
--def: mapping : Mapping
--    = domain.mapping
def: bottomPattern : BottomPattern
    = area.bottomPattern
def: guardPattern : GuardPattern
    = area.guardPattern
def: bottomPatternVariables : Set(EssentialOCL::Variable)
    = bottomPattern.variable->union(bottomPattern.realizedVariable)
def: guardPatternVariables : Set(EssentialOCL::Variable)
    = guardPattern.variable
def: patternVariables : Set(EssentialOCL::Variable)
    = bottomPatternVariables->union(guardPattern.guardPatternVariables)
inv VariableNamesAreUnique :
    patternVariables->isUnique(name)
inv EveryVariableTypeIsDeclaredByMapping :
    patternVariables->forAll(v | area.declaresType(v.type))
-- inv EnforcedDomainAssignsAllProperties

--context GuardPattern

context BottomPattern
def: declaresVariable(v : EssentialOCL::Variable) : Boolean
    = domain.declaresVariable(v)
   
context Assignment
def: area : Area
    = bottomPattern.area
def: domain : CoreDomain
    = bottomPattern.domain
inv DefaultIsInCoreDomain :
    isDefault implies area.isEnforceable   
inv EveryValueVariableIsDeclaredByBottomPattern :
    value.allReferencedVariables->asSet()->forAll(v | bottomPattern.declaresVariable(v))
   
context PropertyAssignment
inv SlotExpressionTypeIsClass:
    slotExpression.type.oclIsKindOf(EMOF::Class)
inv SlotExpressionIsVariableExp:
    slotExpression.oclIsKindOf(EssentialOCL::VariableExp)
inv SlotExpressionVariableIsDeclaredByDomain:
    domain.declaresVariable(slotExpression.oclAsType(EssentialOCL::VariableExp).referredVariable)
inv ReferredPropertyIsDefinedBySlot:
    slotExpression.type.oclAsType(EMOF::Class).definesProperty(targetProperty)
inv ValueTypeMatchesPropertyType:
    targetProperty.type.assignableFrom(value.type)
   
context VariableAssignment
inv TargetVariableIsDeclaredByBottomPattern:
    bottomPattern.declaresVariable(targetVariable)
inv ValueTypeMatchesVariableType:
    targetVariable.type.assignableFrom(value.type)
    
context RealizedVariable
inv ParentIsBottomPattern :
    container().oclIsKindOf(BottomPattern)
def: bottomPattern : BottomPattern
    = container().oclAsType(BottomPattern)
def: area : Area
    = bottomPattern.area
inv MappingIsNotEnforceableWarning :
    area.isEnforceable
    
context EnforcementOperation
def: argumentVariables : Set(EssentialOCL::Variable)
    = operationCallExp.argument->select(oclIsKindOf(EssentialOCL::VariableExp)).oclAsType(EssentialOCL::VariableExp).referredVariable->asSet()
inv ExpressionIncludesTheVariables :
    argumentVariables = bottomPattern.bottomPatternVariables
endpackage