diff --git a/src/de/dhbwstuttgart/sat/asp/ASPStringConverter.java b/src/de/dhbwstuttgart/sat/asp/ASPStringConverter.java new file mode 100644 index 00000000..0497b09a --- /dev/null +++ b/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); + } +} diff --git a/src/de/dhbwstuttgart/sat/asp/Clingo.java b/src/de/dhbwstuttgart/sat/asp/Clingo.java index 85f6dc56..ed1e9f40 100644 --- a/src/de/dhbwstuttgart/sat/asp/Clingo.java +++ b/src/de/dhbwstuttgart/sat/asp/Clingo.java @@ -17,16 +17,20 @@ public class Clingo { private static final List 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/reduce2.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/unify.lp")); + programFiles.add(new File("/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/unifyWithoutWildcards/adapt.lp")); } public Clingo(List 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"; diff --git a/src/de/dhbwstuttgart/sat/asp/model/ASPRule.java b/src/de/dhbwstuttgart/sat/asp/model/ASPRule.java index 8d4d73f9..24ed9269 100644 --- a/src/de/dhbwstuttgart/sat/asp/model/ASPRule.java +++ b/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; diff --git a/src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java b/src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java index c7be7dbc..b3534f47 100644 --- a/src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java +++ b/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.typeinference.result.ResultSet; +import de.dhbwstuttgart.exceptions.DebugException; +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 java.util.Set; +import javax.json.Json; +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){ - Set ret = new HashSet<>(); - for(String pair : result.split(",")){ + private final Collection originalTPHs; + private ResultSet resultSet; + private Map types = new HashMap<>(); + private Set tphs = new HashSet<>(); + private Map parameterLists = new HashMap<>(); + /** + * Parst clingo output welcher als JSON (option --outf=2) ausgibt + * @param toParse + * @return + */ + public static ResultSet parse(String toParse, Collection oldPlaceholders){ + return new ASPParser(toParse, oldPlaceholders).resultSet; + } + + + private ASPParser(String toParse, Collection 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 ret = new HashSet<>(); + //Zuerst die params und typeVars: + for(int i = 0; i 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 params = this.getParams(rs); + this.types.put(ls,new ParsedType(ls, params)); + } + } + + private List getParams(String pointer) { + List 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 ret = parameterLists.stream().filter(aspParameterList -> aspParameterList.name.equals(rs)).findAny(); + //return ret.get(); } } \ No newline at end of file diff --git a/src/de/dhbwstuttgart/sat/asp/parser/model/ParsedASPStatement.java b/src/de/dhbwstuttgart/sat/asp/parser/model/ParsedASPStatement.java deleted file mode 100644 index 614bddb0..00000000 --- a/src/de/dhbwstuttgart/sat/asp/parser/model/ParsedASPStatement.java +++ /dev/null @@ -1,7 +0,0 @@ -package de.dhbwstuttgart.sat.asp.parser.model; - -public class ParsedASPStatement { - public ParsedASPStatement(String statement){ - - } -} diff --git a/src/de/dhbwstuttgart/sat/asp/parser/model/ParsedType.java b/src/de/dhbwstuttgart/sat/asp/parser/model/ParsedType.java new file mode 100644 index 00000000..c49ce831 --- /dev/null +++ b/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 params; + public ParsedType(String name, List params){ + this.name = name; + this.params = params; + } +} diff --git a/src/de/dhbwstuttgart/sat/asp/writer/ASPGenerator.java b/src/de/dhbwstuttgart/sat/asp/writer/ASPGenerator.java index 38652b43..b1483423 100644 --- a/src/de/dhbwstuttgart/sat/asp/writer/ASPGenerator.java +++ b/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> constraints1 = constraints.cartesianProduct().iterator().next(); List constraintPairs = new ArrayList<>(); for(Constraint 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 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); - } - - public static String toConstant(JavaClassName name){ - return toConstant(name.toString().replace(".", "_")); - } - - public static String toConstant(String name){ - return "c" + name.toString().replace(".", "_"); + return new ASPRefType(ASPStringConverter.toConstant(cl.getClassName()), params); } private class TypeConverter implements TypeVisitor{ @@ -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)); } } diff --git a/src/de/dhbwstuttgart/sat/asp/writer/model/ASPParameterList.java b/src/de/dhbwstuttgart/sat/asp/writer/model/ASPParameterList.java index 3c176e49..178bb8fa 100644 --- a/src/de/dhbwstuttgart/sat/asp/writer/model/ASPParameterList.java +++ b/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(){ diff --git a/src/de/dhbwstuttgart/sat/asp/writer/model/ASPTypeVar.java b/src/de/dhbwstuttgart/sat/asp/writer/model/ASPTypeVar.java index 8b3c1af6..24b33eaf 100644 --- a/src/de/dhbwstuttgart/sat/asp/writer/model/ASPTypeVar.java +++ b/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 diff --git a/src/de/dhbwstuttgart/typeinference/result/PairTPHEqualTPH.java b/src/de/dhbwstuttgart/typeinference/result/PairTPHEqualTPH.java index 64d0ce0b..c24fe211 100644 --- a/src/de/dhbwstuttgart/typeinference/result/PairTPHEqualTPH.java +++ b/src/de/dhbwstuttgart/typeinference/result/PairTPHEqualTPH.java @@ -9,7 +9,7 @@ public class PairTPHEqualTPH extends ResultPair getFC() { Set ret = new HashSet<>(); - ret.add(ASTFactory.createObjectClass()); - ret.add(ASTFactory.createClass(java.util.List.class)); return ret; } public ConstraintSet getPairs() { ConstraintSet 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; } } diff --git a/test/asp/UnifyWithoutWildcards.java b/test/asp/UnifyWithoutWildcards.java new file mode 100644 index 00000000..9e7c867d --- /dev/null +++ b/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 getFC() { + Set ret = new HashSet<>(); + ret.add(ASTFactory.createObjectClass()); + ret.add(ASTFactory.createClass(java.util.List.class)); + return ret; + } + + public ConstraintSet getPairs() { + ConstraintSet ret = new ConstraintSet<>(); + ret.addUndConstraint(new Pair(TypePlaceholder.fresh(new NullToken()), ASTFactory.createObjectType(), PairOperator.SMALLERDOT)); + return ret; + } +}