From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../logic2viatra/queries/TypeAnalysis.vql | 223 +++++++++++++++++++++ 1 file changed, 223 insertions(+) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql new file mode 100644 index 00000000..ebab542c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql @@ -0,0 +1,223 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries + +import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" +import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" +import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" + +/** + * Direct supertypes of a type. + */ +private pattern supertypeDirect(subtype : Type, supertype : Type) { + Type.supertypes(subtype, supertype); +} + +/** + * All supertypes of a type. + */ + +private pattern supertypePlus(subtype: Type, supertype: Type) { + find supertypeDirect+(subtype,supertype); +} + +private pattern supertypeStar(subtype: Type, supertype: Type) { + subtype == supertype; +} or { + find supertypePlus(subtype,supertype); +} + +pattern hasDefinedSupertype(type:Type) { + find supertypeStar(type,superType); + TypeDefinition(superType); +} + +pattern dontHaveDefinedSupertype(type:TypeDeclaration) { + neg find hasDefinedSupertype(type); +} + +/////////////////////// +// New element types +/////////////////////// + +/** + * A new element can has 'type' as a dynamic type iff + * (1) 'type' is concrete and + * (2) 'type' does not have defined supertype + * (including the case when 'type' itself is defined). + */ +private pattern possibleNewElementDynamicType(type:TypeDeclaration) { + Type.isAbstract(type,false); + find dontHaveDefinedSupertype(type); +} +///** +// * The type of a new element can be refined from 'previous' to 'refined'. +// */ +//private pattern newElementTypeRefinementPath(previous:TypeDeclaration, refined:TypeDeclaration) { +// find possibleNewElementDynamicType(previous); +// find possibleNewElementDynamicType(refined); +// find supertypePlus(refined,previous); +//} + +/** + * New element can be created with type 'type' iff it can has 'type' as a dynamic type. + */ +pattern newElementTypeConstructor(type:TypeDeclaration) { + find possibleNewElementDynamicType(type); +} + +/** + * New element can be refined to type 'refined' iff + * (1) type is concrete + * (2) the new type cover each existing type of the previous state, i.e. + * (2') it does not have type that: + */ + +pattern newElementTypeRefinementTarget(refined: TypeDeclaration) { + find possibleNewElementDynamicType(refined); +} + +private pattern incompatibleType(type:TypeDeclaration, incompatible:TypeDeclaration) { + LogicProblem.types(problem,type); + LogicProblem.types(problem,incompatible); + neg find supertypeStar(type, incompatible); +} + +pattern incompatibleSuperType(type:TypeDeclaration, incompatibleType1:TypeDeclaration, incompatibleType2:TypeDeclaration) { + find incompatibleType(type, incompatibleType1); + find incompatibleType(type, incompatibleType2); + find supertypePlus(incompatibleType1, incompatibleType2); +} + +pattern incompatibleTopType(type:TypeDeclaration, incompatible:TypeDeclaration) { + find incompatibleType(type, incompatible); + neg find incompatibleSuperType(type, incompatible, _); +} + +pattern newElementTypeRefinementNegativeConstraint(refined:TypeDeclaration, inhibitor:TypeDeclaration) { + find incompatibleTopType(refined, inhibitor); +} or { + find possibleNewElementDynamicType(refined); + refined == inhibitor; +} + +pattern newElementMayTypeNegativeConstraint(mayType: TypeDeclaration, inhibitor: TypeDeclaration) { + find incompatibleTopType(mayType, inhibitor); +} + +/////////////////////// +// Old element types +/////////////////////// + +//TODO old element types + +//private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { +// find interpretation(problem,interpetation); +// LogicProblem.types(problem,type); +// PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); +// PartialTypeInterpratation.interpretationOf(typeInterpretation,type); +//} +// +//pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { +// find interpretation(problem,interpetation); +// find mustExist(problem,interpetation,element); +// LogicProblem.types(problem,type); +// TypeDefinition.elements(type,element); +//} or { +// find mustExist(problem,interpetation,element); +// find typeInterpretation(problem,interpetation,type,typeInterpretation); +// PartialTypeInterpratation.elements(typeInterpretation,element); +//} +// +// +// +///// Complex type reasoning patterns /// +//// +//// In a valid type system, for each element e there is exactly one type T where +//// 1: T(e) - but we dont know this for type declaration +//// 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. +//// 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: +//// D(e) && D-->T && !T(e) +//// 3: There is no T' that T'->T and T'(e) +//// 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: +//// D(e) && ![T--->D] && T(e) +//// 4: T is not abstract +//// Such type T is called Dynamic type of e, while other types are called static types. +//// +//// The following patterns checks the possible dynamic types for an element +// +//pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { +// // 1: T(e) +// find directInstanceOf(problem,interpretation,element,dynamic); +// // 2e is not true: D(e) && D-->T && !T(e) +// neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); +// // 3e is not true: D(e) && ![T--->D] && T(e) +// neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); +// // 4: T is not abstract +// Type.isAbstract(dynamic,false); +//} +// +//pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) +//// case 1: element is defined at least once +//{ +// LogicProblem.types(problem,dynamic); +// // select a random definition 'randomType' +// find directInstanceOf(problem,interpretation,element,randomType); +// // dynamic is a subtype of 'randomType' +// find supertypeStar(dynamic,randomType); +// // 2e is not true: D(e) && D-->T && !T(e) +// neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); +// // 3e is not true: D(e) && ![T--->D] && T(e) +// neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); +// // 4: T is not abstract +// Type.isAbstract(dynamic,false); +//} or +//// case 2: element is not defined anywhere +//{ +// find mayExist(problem,interpretation,element); +// // there is no definition +// neg find directInstanceOf(problem,interpretation,element,_); +// // 2e is not true: D(e) && D-->T && !T(e) +// // because non of the definition contains element, the type cannot have defined supertype +// LogicProblem.types(problem,dynamic); +// PartialInterpretation.problem(interpretation,problem); +// neg find typeWithDefinedSupertype(dynamic); +// // 3e is not true: D(e) && ![T--->D] && T(e) +// // because there is no definition, dynamic covers all definition +// // 4: T is not abstract +// Type.isAbstract(dynamic,false); +//} +// +///** +// * supertype -------> element <------- otherSupertype +// * A A +// * | | +// * wrongDynamic -----------------------------X +// */ +//private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { +// find directInstanceOf(problem,interpretation,element,supertype); +// find directInstanceOf(problem,interpretation,element,otherSupertype); +// find supertypeStar(wrongDynamic,supertype); +// neg find supertypeStar(wrongDynamic,otherSupertype); +//} +// +// +///** +// * supertype -------> element <---X--- otherSupertype +// * A A +// * | | +// * wrongDynamic -----------------------------+ +// */ +//private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { +// find directInstanceOf(problem,interpretation,element,supertype); +// neg find elementInTypeDefinition(element,otherSupertype); +// find supertypeStar(wrongDynamic, supertype); +// find supertypeStar(wrongDynamic, otherSupertype); +//} +// +//private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { +// TypeDefinition.elements(definition,element); +//} +// +//private pattern typeWithDefinedSupertype(type:TypeDeclaration) { +// find supertypeStar(type,definedSupertype); +// TypeDefinition(definedSupertype); +//} -- cgit v1.2.3-54-g00ecf