1 files changed, 150 insertions, 12 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index 1f071635..bc0b3e23 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -1,19 +1,157 @@
 package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder
 
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
+import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import java.util.ArrayList
 import java.util.Collection
 import java.util.List
-import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
 
-interface Logic2VampireLanguageMapper_TypeMapper {
-        def void transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace);
-        //samples below 2 lines
-        def List<VLSTerm> transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace)
-        def VLSTerm getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace)
-        
-        def int getUndefinedSupertypeScope(int undefinedScope,Logic2VampireLanguageMapperTrace trace)
-        def VLSTerm transformReference(DefinedElement referred,Logic2VampireLanguageMapperTrace trace)
-        
-        def VampireModelInterpretation_TypeInterpretation getTypeInterpreter()
-}
\ No newline at end of file
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
+
+class Logic2VampireLanguageMapper_TypeMapper  {
+        private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
+        private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support
+        val Logic2VampireLanguageMapper base
+
+        new(Logic2VampireLanguageMapper base) {
+                LogicproblemPackage.eINSTANCE.class
+                this.base = base
+        }
+
+        def protected transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) {
+                
+//              val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes
+//              trace.typeMapperTrace = typeTrace
+                val VLSVariable variable = createVLSVariable => [it.name = "A"]
+
+                // 1. Each type (class) is a predicate with a single variable as input
+                for (type : types) {
+                        val typePred = createVLSFunction => [
+                                it.constant = support.toIDMultiple("t", type.name.split(" ").get(0))
+                                it.terms += support.duplicate(variable)
+                        ]
+//                      typeTrace.type2Predicate.put(type, typePred)
+                        trace.type2Predicate.put(type, typePred)
+                }
+
+                // 2. Map each ENUM type definition to fof formula
+                for (type : types.filter(TypeDefinition)) {
+                        val List<VLSFunction> orElems = newArrayList
+                        for (e : type.elements) {
+                                val enumElemPred = createVLSFunction => [
+                                        it.constant = support.toIDMultiple("e", e.name.split(" ").get(0), e.name.split(" ").get(2))
+                                        it.terms += support.duplicate(variable)
+                                ]
+//                              typeTrace.element2Predicate.put(e, enumElemPred)
+                                trace.element2Predicate.put(e, enumElemPred)
+                                orElems.add(enumElemPred)
+                        }
+
+                        val res = createVLSFofFormula => [
+                                it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0))
+                                // below is temporary solution
+                                it.fofRole = "axiom"
+                                it.fofFormula = createVLSUniversalQuantifier => [
+                                        it.variables += support.duplicate(variable)
+                                        it.operand = createVLSEquivalent => [
+//                                              it.left = createVLSFunction => [
+//                                                      it.constant = type.lookup(typeTrace.type2Predicate).constant
+//                                                      it.terms += createVLSVariable => [it.name = "A"]
+//                                              ]
+//                                              it.left = type.lookup(typeTrace.type2Predicate)
+                                                it.left = type.lookup(trace.type2Predicate)
+
+                                                it.right = support.unfoldOr(orElems)
+
+                                        // TEMPPPPPPP
+//                                              it.right = support.unfoldOr(type.elements.map [e |
+//                                                      
+//                                                      createVLSEquality => [
+//                                                              it.left = support.duplicate(variable)
+//                                                              it.right = createVLSDoubleQuote => [
+//                                                                      it.value = "\"a" + e.name + "\""
+//                                                              ]
+//                                                      ]
+//                                              ])
+                                        // END TEMPPPPP
+                                        ]
+                                ]
+
+                        ]
+                        trace.specification.formulas += res
+                }
+                
+                //HIERARCHY HANDLER
+                
+                
+                // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates
+                // and store in a map
+                for (t1 : types.filter[!isIsAbstract]) {
+                        for (t2 : types) {
+                                // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes
+                                if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) {
+//                                      typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate)))
+                                        trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate)))
+                                } else {
+//                                      typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+                                        trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [
+                                                it.operand = support.duplicate(t2.lookup(trace.type2Predicate))
+                                        ])
+                                }
+                        }
+//                      typeTrace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(typeTrace.type2PossibleNot.values)))
+//                      typeTrace.type2PossibleNot.clear
+                        trace.type2And.put(t1, support.unfoldAnd(new ArrayList<VLSTerm>(trace.type2PossibleNot.values)))
+                        trace.type2PossibleNot.clear
+                }
+
+                // 5. create fof function that is an or with all the elements in map
+                val hierarch = createVLSFofFormula => [
+                        it.name = "hierarchyHandler"
+                        it.fofRole = "axiom"
+                        it.fofFormula = createVLSUniversalQuantifier => [
+                                it.variables += support.duplicate(variable)
+                                it.operand = createVLSEquivalent => [
+                                        it.left = support.topLevelTypeFunc
+//                                      it.right = support.unfoldOr(new ArrayList<VLSTerm>(typeTrace.type2And.values))
+                                        it.right = support.unfoldOr(new ArrayList<VLSTerm>(trace.type2And.values))
+                                ]
+                        ]
+                ]
+
+                trace.specification.formulas += hierarch
+
+        }
+
+        //below are from previous interface
+        def protected transformTypeReference(Type referred, Logic2VampireLanguageMapper mapper,
+                Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected getUndefinedSupertype(Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected getUndefinedSupertypeScope(int undefinedScope, Logic2VampireLanguageMapperTrace trace) {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+        def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) {
+                createVLSDoubleQuote => [
+                        it.value = "\"a" + referred.name + "\""
+                ]
+        }
+
+        def protected getTypeInterpreter() {
+                throw new UnsupportedOperationException("TODO: auto-generated method stub")
+        }
+
+}