Funktionierender Clingo Test

src/de/dhbwstuttgart/sat/asp/ASPStringConverter.java

@@ -0,0 +1,17 @@
+package de.dhbwstuttgart.sat.asp;
+
+import de.dhbwstuttgart.parser.scope.JavaClassName;
+
+public class ASPStringConverter {
+    public static String toConstant(JavaClassName name){
+        return toConstant(name.toString().replace(".", "_"));
+    }
+
+    public static String toConstant(String name){
+        return "c" + name.toString().replace(".", "_");
+    }
+
+    public static String fromConstant(String s){
+        return s.replace("_", ".").substring(1);
+    }
+}

src/de/dhbwstuttgart/sat/asp/Clingo.java

@@ -17,16 +17,20 @@ public class Clingo {
     private static final List<File> programFiles = new ArrayList<>();
     static{
         programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/basis.lp"));
+        programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/finiteclosure.lp"));
         programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/subst.lp"));
-        programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/reduce1.lp"));
+        programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/reduce.lp"));
-        programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/reduce2.lp"));
         programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/unify.lp"));
+        programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/adapt.lp"));
     }
 
     public Clingo(List<File> inputFiles){
         this.input = inputFiles;
     }
 
+    /*
+    TODO: Clingo per Java Wrapper https://stackoverflow.com/questions/3356200/using-java-to-wrap-over-c
+     */
     public String runClingo() throws IOException, InterruptedException {
         String pathToClingo =
                 "/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/clingo-5.2.1-linux-x86_64/clingo";

src/de/dhbwstuttgart/sat/asp/model/ASPRule.java

@@ -9,8 +9,8 @@ public enum ASPRule {
     ASP_PARAMLISTNUMERATION_NAME("paramNum"),
     ASP_PARAMLIST_END_POINTER("null"),
     ASP_TYPE("type"),
-    ASP_FCTYPE("type")
+    ASP_FCTYPE("typeFC"),
-    ;
+    ASP_TYPE_VAR("typeVar");
 
     private final String text;
 

src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java

@@ -1,17 +1,187 @@
 package de.dhbwstuttgart.sat.asp.parser;
 
-import de.dhbwstuttgart.typeinference.result.ResultPair;
+import de.dhbwstuttgart.exceptions.DebugException;
-import de.dhbwstuttgart.typeinference.result.ResultSet;
+import de.dhbwstuttgart.parser.NullToken;
+import de.dhbwstuttgart.parser.scope.JavaClassName;
+import de.dhbwstuttgart.sat.asp.ASPStringConverter;
+import de.dhbwstuttgart.sat.asp.model.ASPRule;
+import de.dhbwstuttgart.sat.asp.parser.model.ParsedType;
+import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
+import de.dhbwstuttgart.sat.asp.writer.model.ASPParameterList;
+import de.dhbwstuttgart.sat.asp.writer.model.ASPRefType;
+import de.dhbwstuttgart.sat.asp.writer.model.ASPType;
+import de.dhbwstuttgart.syntaxtree.type.*;
+import de.dhbwstuttgart.typeinference.result.*;
 
-import java.util.HashSet;
+import javax.json.Json;
-import java.util.Set;
+import javax.json.JsonArray;
+import javax.json.JsonObject;
+import java.io.StringReader;
+import java.util.*;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
+/**
+ * Ablauf:
+ * - Erst werden alle benötigten Statements eingelesen. Die Pointer bleiben als Strings erhalten
+ * - Anschließend müssen diese wieder zu einem Unify Ergebnis zurückgewandelt werden
+ * - Hier nicht die Typen aus dem unify.model packages verwenden.
+ * TODO: Überlegen welche Informationen noch nach der Unifizierung gebraucht werden
+ *  -> Eigentlich nur die korrekten Namen der Typen und TPHs
+ */
 public class ASPParser {
-    ResultSet parse(String result){
+    private final Collection<TypePlaceholder> originalTPHs;
-        Set<ResultPair> ret = new HashSet<>();
+    private ResultSet resultSet;
-        for(String pair : result.split(",")){
+    private Map<String, ParsedType> types = new HashMap<>();
+    private Set<String> tphs = new HashSet<>();
+    private Map<String, ParameterListNode> parameterLists = new HashMap<>();
 
+    /**
+     * Parst clingo output welcher als JSON (option --outf=2) ausgibt
+     * @param toParse
+     * @return
+     */
+    public static ResultSet parse(String toParse, Collection<TypePlaceholder> oldPlaceholders){
+        return new ASPParser(toParse, oldPlaceholders).resultSet;
+    }
+
+
+    private ASPParser(String toParse, Collection<TypePlaceholder> oldPlaceholders){
+        this.originalTPHs = oldPlaceholders;
+        JsonObject jsonResult = Json.createReader(new StringReader(toParse)).readObject();
+        JsonArray results = jsonResult.getJsonArray("Call").getJsonObject(0).
+                getJsonArray("Witnesses").getJsonObject(0).
+                getJsonArray("Value");
+
+        /*
+        Diese Funktion läuft im folgenden mehrmals über das Result aus dem ASP Programm.
+        Dabei werden Schritt für Schritt die Felder dieser Klasse befüllt die am Schluss das ResultSet ergeben
+         */
+        Set<ResultPair> ret = new HashSet<>();
+        //Zuerst die params und typeVars:
+        for(int i = 0; i<results.size();i++){
+            String aspStatement = results.getString(i);
+            parseParameter(aspStatement);
+            parseTypeVar(aspStatement);
         }
-        return new ResultSet(ret);
+        //Dann die Typen, das ist wichtig, da die Typen auf die Parameter referenzieren:
+        for(int i = 0; i<results.size();i++){
+            String aspStatement = results.getString(i);
+            parseType(aspStatement);
+        }
+        //Dann die Equalsdot Statements
+        for(int i = 0; i<results.size();i++){
+            String aspStatement = results.getString(i);
+            ResultPair p = parseEqualsDot(aspStatement);
+            if(p != null)ret.add(p);
+            p = parseSmallerDot(aspStatement);
+            if(p != null)ret.add(p);
+        }
+
+        this.resultSet = new ResultSet(ret);
+    }
+
+    private ResultPair parseSmallerDot(String statement) {
+        //TODO
+        return null;
+    }
+
+    private ResultPair parseEqualsDot(String statement){
+        Pattern p = Pattern.compile(ASPRule.ASP_PAIR_EQUALS_NAME+"\\(([^,]+),([^,]+)\\)");
+        Matcher m = p.matcher(statement);
+        boolean b = m.matches();
+        if(b){
+            if(m.groupCount()<2)throw new DebugException("Fehler in Regex");
+            String ls = m.group(1);
+            String rs = m.group(2);
+            RefTypeOrTPHOrWildcardOrGeneric lsType = this.getType(ls);
+            RefTypeOrTPHOrWildcardOrGeneric rsType = this.getType(rs);
+            if(lsType instanceof TypePlaceholder && rsType instanceof RefType)
+                return new PairTPHequalRefTypeOrWildcardType((TypePlaceholder) lsType, rsType);
+        }
+        return null;
+    }
+
+    private RefTypeOrTPHOrWildcardOrGeneric getType(String name) {
+        if(tphs.contains(name)){
+            name = ASPStringConverter.fromConstant(name);
+            for(TypePlaceholder tph : originalTPHs){
+                if(tph.getName().equals(name))return tph;
+            }
+            return TypePlaceholder.fresh(new NullToken());
+        }else
+        if(types.containsKey(name)){
+            List<RefTypeOrTPHOrWildcardOrGeneric> params = new ArrayList<>();
+            ParsedType t = types.get(name);
+            for(String param : t.params){
+                params.add(this.getType(param));
+            }
+            return new RefType(new JavaClassName(ASPStringConverter.fromConstant(t.name)), params, new NullToken());
+        }else throw new DebugException("Der Typ " + name + " konnte nicht bestimmt werden");
+    }
+
+    private static class ParameterListNode{
+        final String type;
+        final String nextNode;
+
+        public ParameterListNode(String type, String next) {
+            this.type = type;
+            this.nextNode = next;
+        }
+    }
+    private void parseParameter(String statement){
+        Pattern p = Pattern.compile(ASPRule.ASP_PARAMLIST_NAME+"\\(([^,]+),([^,]+),([^,]+)\\)");
+        Matcher m = p.matcher(statement);
+        boolean b = m.matches();
+        if(b){
+            if(m.groupCount()<3)throw new DebugException("Fehler in Regex");
+            String pointer = m.group(1);
+            String type = m.group(2);
+            String next = m.group(2);
+            if(next.equals(ASPRule.ASP_PARAMLIST_END_POINTER.toString()))next = null;
+            if(this.parameterLists.containsKey(pointer)){
+                throw new DebugException("Fehler in Ergebnisparsen");
+            }
+            this.parameterLists.put(pointer,new ParameterListNode(type, next));
+        }
+    }
+
+    private void parseTypeVar(String statement){
+        Pattern p = Pattern.compile(ASPRule.ASP_TYPE_VAR+"\\(([^,]+)\\)");
+        Matcher m = p.matcher(statement);
+        boolean b = m.matches();
+        if(b){
+            if(m.groupCount()<1)throw new DebugException("Fehler in Regex");
+            String name = m.group(1);
+            this.tphs.add(name);
+        }
+    }
+
+    private void parseType(String statement){
+        Pattern p = Pattern.compile(ASPRule.ASP_TYPE+"\\(([^,]+),([^,]+)\\)");
+        Matcher m = p.matcher(statement);
+        boolean b = m.matches();
+        if(b){
+            if(m.groupCount()<2)throw new DebugException("Fehler in Regex");
+            String ls = m.group(1);
+            String rs = m.group(2);
+            List<String> params = this.getParams(rs);
+            this.types.put(ls,new ParsedType(ls, params));
+        }
+    }
+
+    private List<String> getParams(String pointer) {
+        List<String> params = new ArrayList<>();
+        if(pointer.equals(ASPRule.ASP_PARAMLIST_END_POINTER.toString()))return params;
+        while(pointer != null){
+            if(!parameterLists.containsKey(pointer))
+                throw new DebugException("Fehler in Ergebnisparsen");
+            ParameterListNode param = parameterLists.get(pointer);
+            pointer = param.nextNode;
+            params.add(param.type);
+        }
+        return params;
+        //Optional<ASPParameterList> ret = parameterLists.stream().filter(aspParameterList -> aspParameterList.name.equals(rs)).findAny();
+        //return ret.get();
     }
 }

src/de/dhbwstuttgart/sat/asp/parser/model/ParsedASPStatement.java

@@ -1,7 +0,0 @@
-package de.dhbwstuttgart.sat.asp.parser.model;
-
-public class ParsedASPStatement {
-    public ParsedASPStatement(String statement){
-
-    }
-}

src/de/dhbwstuttgart/sat/asp/parser/model/ParsedType.java

@@ -0,0 +1,12 @@
+package de.dhbwstuttgart.sat.asp.parser.model;
+
+import java.util.List;
+
+public class ParsedType {
+    public final String name;
+    public final List<String> params;
+    public ParsedType(String name, List<String> params){
+        this.name = name;
+        this.params = params;
+    }
+}

src/de/dhbwstuttgart/sat/asp/writer/ASPGenerator.java

@@ -3,6 +3,7 @@ package de.dhbwstuttgart.sat.asp.writer;
 import de.dhbwstuttgart.exceptions.NotImplementedException;
 import de.dhbwstuttgart.parser.SyntaxTreeGenerator.FCGenerator;
 import de.dhbwstuttgart.parser.scope.JavaClassName;
+import de.dhbwstuttgart.sat.asp.ASPStringConverter;
 import de.dhbwstuttgart.sat.asp.writer.model.*;
 import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
 import de.dhbwstuttgart.syntaxtree.GenericTypeVar;
@@ -24,7 +25,6 @@ public class ASPGenerator {
         List<Constraint<Pair>> constraints1 = constraints.cartesianProduct().iterator().next();
         List<Pair> constraintPairs = new ArrayList<>();
         for(Constraint<Pair> constraint : constraints1){
-            System.out.println(UnifyTypeFactory.convert(constraint));
             constraintPairs.addAll(constraint);
         }
         asp = toASP(constraintPairs, FCGenerator.toFC(fcClasses));
@@ -65,18 +65,10 @@ public class ASPGenerator {
     private ASPRefType convert(ClassOrInterface cl){
         List<ASPType> paramList = new ArrayList<>();
         for(GenericTypeVar gtv : cl.getGenerics()){
-            paramList.add(new ASPGenericType(toConstant(gtv.getName())));
+            paramList.add(new ASPGenericType(ASPStringConverter.toConstant(gtv.getName())));
         }
         ASPParameterList params = new ASPParameterList(paramList, writer);
-        return new ASPRefType(toConstant(cl.getClassName()), params);
+        return new ASPRefType(ASPStringConverter.toConstant(cl.getClassName()), params);
-    }
-
-    public static String toConstant(JavaClassName name){
-        return toConstant(name.toString().replace(".", "_"));
-    }
-
-    public static String toConstant(String name){
-        return "c" + name.toString().replace(".", "_");
     }
 
     private class TypeConverter implements TypeVisitor<ASPType>{
@@ -88,7 +80,7 @@ public class ASPGenerator {
                 paramList.add(gtv.acceptTV(this));
             }
             ASPParameterList params = new ASPParameterList(paramList, writer);
-            return new ASPRefType(toConstant(type.getName()), params);
+            return new ASPRefType(ASPStringConverter.toConstant(type.getName()), params);
         }
 
         @Override
@@ -98,7 +90,7 @@ public class ASPGenerator {
 
         @Override
         public ASPType visit(TypePlaceholder typePlaceholder) {
-            return new ASPTypeVar(toConstant(typePlaceholder.getName()));
+            return new ASPTypeVar(ASPStringConverter.toConstant(typePlaceholder.getName()));
         }
 
         @Override
@@ -108,7 +100,7 @@ public class ASPGenerator {
 
         @Override
         public ASPType visit(GenericRefType genericRefType) {
-            return new ASPRefType(toConstant(genericRefType.getName()),
+            return new ASPRefType(ASPStringConverter.toConstant(genericRefType.getName()),
                     new ASPParameterList(new ArrayList<>(), writer));
         }
     }

src/de/dhbwstuttgart/sat/asp/writer/model/ASPParameterList.java

@@ -1,5 +1,6 @@
 package de.dhbwstuttgart.sat.asp.writer.model;
 
+import de.dhbwstuttgart.sat.asp.ASPStringConverter;
 import de.dhbwstuttgart.sat.asp.model.ASPRule;
 import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
 import de.dhbwstuttgart.sat.asp.writer.ASPWriter;
@@ -30,13 +31,12 @@ public class ASPParameterList {
                 writer.add(new ASPStatement(ASPRule.ASP_PARAMLIST_NAME + "(" + param + ")"));
                 writer.add(new ASPStatement(ASPRule.ASP_PARAMLISTNUMERATION_NAME + "(" + name + "," +t + "," + paramNum + ")"));
                 paramNum++;
-                //paramDefinitions.add(new ASPStatement(ASP_PARAMLIST_NAME + "(" + param + ")"));
             }
         }
     }
 
     private String newName() {
-        return ASPGenerator.toConstant(NameGenerator.makeNewName());
+        return ASPStringConverter.toConstant(NameGenerator.makeNewName());
     }
 
     public String toString(){

src/de/dhbwstuttgart/sat/asp/writer/model/ASPTypeVar.java

@@ -1,5 +1,7 @@
 package de.dhbwstuttgart.sat.asp.writer.model;
 
+import de.dhbwstuttgart.sat.asp.model.ASPRule;
+
 public class ASPTypeVar implements ASPType{
     private final String name;
 
@@ -9,7 +11,7 @@ public class ASPTypeVar implements ASPType{
 
     @Override
     public String toString() {
-        return "typeVar("+ name +")";
+        return ASPRule.ASP_TYPE_VAR+"("+ name +")";
     }
 
     @Override

src/de/dhbwstuttgart/typeinference/result/PairTPHEqualTPH.java

@@ -9,7 +9,7 @@ public class PairTPHEqualTPH extends ResultPair<TypePlaceholder, TypePlaceholder
     }
 
     @Override
-    public void accept(ResultSetVisitor visitor) {
+    public void accept(ResultPairVisitor visitor) {
         visitor.visit(this);
     }
 }

src/de/dhbwstuttgart/typeinference/result/PairTPHequalRefTypeOrWildcardType.java

@@ -18,7 +18,7 @@ public class PairTPHequalRefTypeOrWildcardType extends ResultPair{
     }
 
     @Override
-    public void accept(ResultSetVisitor visitor) {
+    public void accept(ResultPairVisitor visitor) {
         visitor.visit(this);
     }
 }

src/de/dhbwstuttgart/typeinference/result/PairTPHsmallerTPH.java

@@ -17,7 +17,7 @@ public class PairTPHsmallerTPH extends ResultPair{
     }
 
     @Override
-    public void accept(ResultSetVisitor visitor) {
+    public void accept(ResultPairVisitor visitor) {
         visitor.visit(this);
     }
 }

src/de/dhbwstuttgart/typeinference/result/ResultPair.java

@@ -9,7 +9,7 @@ public abstract class ResultPair<A extends RefTypeOrTPHOrWildcardOrGeneric,B ext
     private final A left;
     private final B right;
 
-    public abstract void accept(ResultSetVisitor visitor);
+    public abstract void accept(ResultPairVisitor visitor);
 
     public ResultPair(A left, B right){
         this.left = left;

src/de/dhbwstuttgart/typeinference/result/ResultPairVisitor.java

@@ -0,0 +1,7 @@
+package de.dhbwstuttgart.typeinference.result;
+
+public interface ResultPairVisitor {
+    void visit(PairTPHsmallerTPH p);
+    void visit(PairTPHequalRefTypeOrWildcardType p);
+    void visit(PairTPHEqualTPH p);
+}

src/de/dhbwstuttgart/typeinference/result/ResultSetVisitor.java

@@ -2,10 +2,7 @@ package de.dhbwstuttgart.typeinference.result;
 
 import de.dhbwstuttgart.syntaxtree.type.*;
 
-public interface ResultSetVisitor {
+public interface ResultSetVisitor extends ResultPairVisitor{
-    void visit(PairTPHsmallerTPH p);
-    void visit(PairTPHequalRefTypeOrWildcardType p);
-    void visit(PairTPHEqualTPH p);
 
     void visit(RefType refType);
 

test/asp/ClingoTest.java

@@ -1,23 +1,28 @@
 package asp;
 
 import de.dhbwstuttgart.parser.NullToken;
+import de.dhbwstuttgart.sat.asp.parser.ASPParser;
 import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
 import de.dhbwstuttgart.sat.asp.Clingo;
 import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
 import de.dhbwstuttgart.syntaxtree.factory.ASTFactory;
+import de.dhbwstuttgart.syntaxtree.type.RefTypeOrTPHOrWildcardOrGeneric;
 import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
 import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
 import de.dhbwstuttgart.typeinference.constraints.Pair;
+import de.dhbwstuttgart.typeinference.result.ResultSet;
 import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
 import org.junit.Test;
 
+import javax.json.Json;
+import javax.json.JsonObject;
 import java.io.*;
 import java.util.*;
 
 public class ClingoTest {
     public static final String rootDirectory = "~/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards";
     public static final String tempDirectory = "/tmp/";
-
+    private final TypePlaceholder testType = TypePlaceholder.fresh(new NullToken());
     @Test
     public void test() throws IOException, InterruptedException, ClassNotFoundException {
         String content = "";
@@ -28,19 +33,21 @@ public class ClingoTest {
         writer.close();
 
         Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp")));
-        System.out.println(clingo.runClingo());
+        String result = clingo.runClingo();
+        System.out.println(result);
+        ResultSet resultSet = ASPParser.parse(result, Arrays.asList(testType));
+        RefTypeOrTPHOrWildcardOrGeneric resolvedType = resultSet.resolveType(testType).resolvedType;
+        assert resolvedType.toString().equals(ASTFactory.createObjectType().toString());
     }
 
     public Collection<ClassOrInterface> getFC() {
         Set<ClassOrInterface> ret = new HashSet<>();
-        ret.add(ASTFactory.createObjectClass());
-        ret.add(ASTFactory.createClass(java.util.List.class));
         return ret;
     }
 
     public ConstraintSet<Pair> getPairs() {
         ConstraintSet<Pair> ret = new ConstraintSet<>();
-        ret.addUndConstraint(new Pair(TypePlaceholder.fresh(new NullToken()), ASTFactory.createObjectType(), PairOperator.SMALLERDOT));
+        ret.addUndConstraint(new Pair(testType, ASTFactory.createObjectType(), PairOperator.EQUALSDOT));
         return ret;
     }
 }

test/asp/UnifyWithoutWildcards.java

@@ -0,0 +1,29 @@
+package asp;
+
+import de.dhbwstuttgart.parser.NullToken;
+import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
+import de.dhbwstuttgart.syntaxtree.factory.ASTFactory;
+import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
+import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
+import de.dhbwstuttgart.typeinference.constraints.Pair;
+import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
+
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Set;
+
+public class UnifyWithoutWildcards {
+
+    public Collection<ClassOrInterface> getFC() {
+        Set<ClassOrInterface> ret = new HashSet<>();
+        ret.add(ASTFactory.createObjectClass());
+        ret.add(ASTFactory.createClass(java.util.List.class));
+        return ret;
+    }
+
+    public ConstraintSet<Pair> getPairs() {
+        ConstraintSet<Pair> ret = new ConstraintSet<>();
+        ret.addUndConstraint(new Pair(TypePlaceholder.fresh(new NullToken()), ASTFactory.createObjectType(), PairOperator.SMALLERDOT));
+        return ret;
+    }
+}