1 files changed, 194 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
new file mode 100644
index 00000000..fbbd9fb5
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
@@ -0,0 +1,194 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import org.eclipse.emf.ecore.EClass
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
+class GenericTypeIndexer implements TypeIndexer {
+        val PatternGenerator base;
+        
+        new(PatternGenerator base) {
+                this.base = base
+        }
+        override requiresTypeAnalysis() { false }
+        
+        public override getRequiredQueries() '''
+        private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) {
+                PartialInterpretation.newElements(interpretation,element);
+        }
+        
+        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);
+        }
+        
+        private 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);
+        }
+        
+        /**
+         * Direct supertypes of a type.
+         */
+        private pattern supertypeDirect(subtype : Type, supertype : Type) {
+                Type.supertypes(subtype, supertype);
+        }
+        
+        /**
+         * All supertypes of a type.
+         */
+        private pattern supertypeStar(subtype: Type, supertype: Type) {
+                subtype == supertype;
+        } or {
+                find supertypeDirect+(subtype,supertype);
+        }
+        
+        /// 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
+        
+        private 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);
+        }
+        
+        private 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);
+                TypeDefinition(otherSupertype);
+                find supertypeStar(wrongDynamic, supertype);
+                find supertypeStar(wrongDynamic, otherSupertype);
+        }
+        
+        private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) {
+                TypeDefinition.elements(definition,element);
+        }
+        
+        private pattern typeWithDefinedSupertype(type:Type) {
+                find supertypeStar(type,definedSupertype);
+                TypeDefinition(definedSupertype);
+        }
+        '''
+        
+        public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) {
+                '''
+                «FOR type:problem.types»
+                        «problem.generateMustInstenceOf(type)»
+                        «problem.generateMayInstanceOf(type)»
+                «ENDFOR»
+                '''
+        }
+        
+        private def patternName(Type type, Modality modality)
+                '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»'''
+        
+        private def generateMustInstenceOf(LogicProblem problem, Type type) {
+                '''
+                /**
+                 * An element must be an instance of type "«type.name»".
+                 */
+                private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+                        Type.name(type,"«type.name»");
+                        find directInstanceOf(problem,interpretation,element,type);
+                }
+                '''
+        }
+        
+        private def generateMayInstanceOf(LogicProblem problem, Type type) {
+                '''
+                /**
+                 * An element may be an instance of type "«type.name»".
+                 */
+                private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
+                        Type.name(type,"«type.name»");
+                        find possibleDynamicType(problem,interpretation,dynamic,element);
+                        find supertypeStar(dynamic,type);
+                }
+                '''
+        }
+        
+        public override referInstanceOf(Type type, Modality modality, String variableName) {
+                '''find «patternName(type,modality)»(problem,interpretation,«variableName»);'''
+        }
+        public override referInstanceOf(EClass type, Modality modality, String variableName) {
+                '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''class «type.name»''')»(problem,interpretation,«variableName»);'''
+        }
+}
+\ No newline at end of file

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend new file mode 100644 index 00000000..fbbd9fb5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend
@@ -0,0 +1,194 @@
	1	package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns
	2
	3	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	4	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
	5	import org.eclipse.emf.ecore.EClass
	6	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
	7	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	8	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult
	9
	10	class GenericTypeIndexer implements TypeIndexer {
	11	val PatternGenerator base;
	12
	13	new(PatternGenerator base) {
	14	this.base = base
	15	}
	16	override requiresTypeAnalysis() { false }
	17
	18	public override getRequiredQueries() '''
	19	private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) {
	20	PartialInterpretation.newElements(interpretation,element);
	21	}
	22
	23	private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) {
	24	find interpretation(problem,interpetation);
	25	LogicProblem.types(problem,type);
	26	PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation);
	27	PartialTypeInterpratation.interpretationOf(typeInterpretation,type);
	28	}
	29
	30	private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) {
	31	find interpretation(problem,interpetation);
	32	find mustExist(problem,interpetation,element);
	33	LogicProblem.types(problem,type);
	34	TypeDefinition.elements(type,element);
	35	} or {
	36	find mustExist(problem,interpetation,element);
	37	find typeInterpretation(problem,interpetation,type,typeInterpretation);
	38	PartialTypeInterpratation.elements(typeInterpretation,element);
	39	}
	40
	41	/**
	42	* Direct supertypes of a type.
	43	*/
	44	private pattern supertypeDirect(subtype : Type, supertype : Type) {
	45	Type.supertypes(subtype, supertype);
	46	}
	47
	48	/**
	49	* All supertypes of a type.
	50	*/
	51	private pattern supertypeStar(subtype: Type, supertype: Type) {
	52	subtype == supertype;
	53	} or {
	54	find supertypeDirect+(subtype,supertype);
	55	}
	56
	57	/// Complex type reasoning patterns ///
	58	//
	59	// In a valid type system, for each element e there is exactly one type T where
	60	// 1: T(e) - but we dont know this for type declaration
	61	// 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true.
	62	// 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e:
	63	// D(e) && D-->T && !T(e)
	64	// 3: There is no T' that T'->T and T'(e)
	65	// 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:
	66	// D(e) && ![T--->D] && T(e)
	67	// 4: T is not abstract
	68	// Such type T is called Dynamic type of e, while other types are called static types.
	69	//
	70	// The following patterns checks the possible dynamic types for an element
	71
	72	private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) {
	73	// 1: T(e)
	74	find directInstanceOf(problem,interpretation,element,dynamic);
	75	// 2e is not true: D(e) && D-->T && !T(e)
	76	neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic);
	77	// 3e is not true: D(e) && ![T--->D] && T(e)
	78	neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic);
	79	// 4: T is not abstract
	80	Type.isAbstract(dynamic,false);
	81	}
	82
	83	private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement)
	84	// case 1: element is defined at least once
	85	{
	86	LogicProblem.types(problem,dynamic);
	87	// select a random definition 'randomType'
	88	find directInstanceOf(problem,interpretation,element,randomType);
	89	// dynamic is a subtype of 'randomType'
	90	find supertypeStar(dynamic,randomType);
	91	// 2e is not true: D(e) && D-->T && !T(e)
	92	neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic);
	93	// 3e is not true: D(e) && ![T--->D] && T(e)
	94	neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic);
	95	// 4: T is not abstract
	96	Type.isAbstract(dynamic,false);
	97	} or
	98	// case 2: element is not defined anywhere
	99	{
	100	find mayExist(problem,interpretation,element);
	101	// there is no definition
	102	neg find directInstanceOf(problem,interpretation,element,_);
	103	// 2e is not true: D(e) && D-->T && !T(e)
	104	// because non of the definition contains element, the type cannot have defined supertype
	105	LogicProblem.types(problem,dynamic);
	106	PartialInterpretation.problem(interpretation,problem);
	107	neg find typeWithDefinedSupertype(dynamic);
	108	// 3e is not true: D(e) && ![T--->D] && T(e)
	109	// because there is no definition, dynamic covers all definition
	110	// 4: T is not abstract
	111	Type.isAbstract(dynamic,false);
	112	}
	113
	114	/**
	115	* supertype -------> element <------- otherSupertype
	116	* A A
	117	* \| \|
	118	* wrongDynamic -----------------------------X
	119	*/
	120	private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) {
	121	find directInstanceOf(problem,interpretation,element,supertype);
	122	find directInstanceOf(problem,interpretation,element,otherSupertype);
	123	find supertypeStar(wrongDynamic,supertype);
	124	neg find supertypeStar(wrongDynamic,otherSupertype);
	125	}
	126
	127	/**
	128	* supertype -------> element <---X--- otherSupertype
	129	* A A
	130	* \| \|
	131	* wrongDynamic -----------------------------+
	132	*/
	133	private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) {
	134	find directInstanceOf(problem,interpretation,element,supertype);
	135	neg find elementInTypeDefinition(element,otherSupertype);
	136	TypeDefinition(otherSupertype);
	137	find supertypeStar(wrongDynamic, supertype);
	138	find supertypeStar(wrongDynamic, otherSupertype);
	139	}
	140
	141	private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) {
	142	TypeDefinition.elements(definition,element);
	143	}
	144
	145	private pattern typeWithDefinedSupertype(type:Type) {
	146	find supertypeStar(type,definedSupertype);
	147	TypeDefinition(definedSupertype);
	148	}
	149	'''
	150
	151	public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) {
	152	'''
	153	«FOR type:problem.types»
	154	«problem.generateMustInstenceOf(type)»
	155	«problem.generateMayInstanceOf(type)»
	156	«ENDFOR»
	157	'''
	158	}
	159
	160	private def patternName(Type type, Modality modality)
	161	'''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»'''
	162
	163	private def generateMustInstenceOf(LogicProblem problem, Type type) {
	164	'''
	165	/**
	166	* An element must be an instance of type "«type.name»".
	167	*/
	168	private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
	169	Type.name(type,"«type.name»");
	170	find directInstanceOf(problem,interpretation,element,type);
	171	}
	172	'''
	173	}
	174
	175	private def generateMayInstanceOf(LogicProblem problem, Type type) {
	176	'''
	177	/**
	178	* An element may be an instance of type "«type.name»".
	179	*/
	180	private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) {
	181	Type.name(type,"«type.name»");
	182	find possibleDynamicType(problem,interpretation,dynamic,element);
	183	find supertypeStar(dynamic,type);
	184	}
	185	'''
	186	}
	187
	188	public override referInstanceOf(Type type, Modality modality, String variableName) {
	189	'''find «patternName(type,modality)»(problem,interpretation,«variableName»);'''
	190	}
	191	public override referInstanceOf(EClass type, Modality modality, String variableName) {
	192	'''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''class «type.name»''')»(problem,interpretation,«variableName»);'''
	193	}
	194	} \ No newline at end of file