Erste lauffähige aber unvollständige Version des UnifyWithoutWildcards
This commit is contained in:
parent
3c732346d9
commit
19a1ef4024
46
src/de/dhbwstuttgart/sat/asp/Clingo.java
Normal file
46
src/de/dhbwstuttgart/sat/asp/Clingo.java
Normal file
@ -0,0 +1,46 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
|
||||
|
||||
import org.apache.commons.io.IOUtils;
|
||||
|
||||
import java.io.File;
|
||||
import java.io.IOException;
|
||||
import java.io.InputStream;
|
||||
import java.io.OutputStream;
|
||||
import java.nio.charset.StandardCharsets;
|
||||
import java.util.ArrayList;
|
||||
import java.util.List;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class Clingo {
|
||||
private final List<File> input;
|
||||
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/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/unify.lp"));
|
||||
}
|
||||
|
||||
public Clingo(List<File> inputFiles){
|
||||
this.input = inputFiles;
|
||||
}
|
||||
|
||||
public String runClingo() throws IOException, InterruptedException {
|
||||
String pathToClingo =
|
||||
"/home/janulrich/Sync/HiwiJob/ResearchPapers/MasterarbeitStadelmeier/asp/clingo-5.2.1-linux-x86_64/clingo";
|
||||
List<String> commands = new ArrayList<>();
|
||||
commands.add(pathToClingo);
|
||||
commands.add("--outf=2"); //use JSON-Output
|
||||
for(File file : input){
|
||||
commands.add(file.getPath());
|
||||
}
|
||||
commands.addAll(programFiles.stream().map(f->f.getPath()).collect(Collectors.toList()));
|
||||
Process clingo = new ProcessBuilder( commands.toArray(new String[0])).start();
|
||||
InputStream output = clingo.getInputStream();
|
||||
clingo.waitFor();
|
||||
String result = IOUtils.toString(output, StandardCharsets.UTF_8);
|
||||
return result;
|
||||
}
|
||||
}
|
24
src/de/dhbwstuttgart/sat/asp/model/ASPRule.java
Normal file
24
src/de/dhbwstuttgart/sat/asp/model/ASPRule.java
Normal file
@ -0,0 +1,24 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
|
||||
public enum ASPRule {
|
||||
ASP_GENERIC_TYPE_NAME("genericType"),
|
||||
ASP_PAIR_EQUALS_NAME("equals"),
|
||||
ASP_PAIR_SMALLER_NAME("smaller"),
|
||||
ASP_PAIR_SMALLER_DOT_NAME("smallerDot"),
|
||||
ASP_PARAMLIST_NAME("param"),
|
||||
ASP_PARAMLISTNUMERATION_NAME("paramNum"),
|
||||
ASP_PARAMLIST_END_POINTER("null"),
|
||||
ASP_TYPE("type")
|
||||
;
|
||||
|
||||
private final String text;
|
||||
|
||||
private ASPRule(final String text) {
|
||||
this.text = text;
|
||||
}
|
||||
|
||||
@Override
|
||||
public String toString() {
|
||||
return text;
|
||||
}
|
||||
}
|
@ -1,4 +0,0 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
|
||||
public interface ASPType {
|
||||
}
|
17
src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java
Normal file
17
src/de/dhbwstuttgart/sat/asp/parser/ASPParser.java
Normal file
@ -0,0 +1,17 @@
|
||||
package de.dhbwstuttgart.sat.asp.parser;
|
||||
|
||||
import de.dhbwstuttgart.typeinference.result.ResultPair;
|
||||
import de.dhbwstuttgart.typeinference.result.ResultSet;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Set;
|
||||
|
||||
public class ASPParser {
|
||||
ResultSet parse(String result){
|
||||
Set<ResultPair> ret = new HashSet<>();
|
||||
for(String pair : result.split(",")){
|
||||
|
||||
}
|
||||
return new ResultSet(ret);
|
||||
}
|
||||
}
|
@ -0,0 +1,7 @@
|
||||
package de.dhbwstuttgart.sat.asp.parser.model;
|
||||
|
||||
public class ParsedASPStatement {
|
||||
public ParsedASPStatement(String statement){
|
||||
|
||||
}
|
||||
}
|
@ -1,9 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
package de.dhbwstuttgart.sat.asp.writer;
|
||||
|
||||
import de.dhbwstuttgart.exceptions.DebugException;
|
||||
import de.dhbwstuttgart.exceptions.NotImplementedException;
|
||||
import de.dhbwstuttgart.parser.scope.JavaClassName;
|
||||
import de.dhbwstuttgart.sat.asp.model.*;
|
||||
import de.dhbwstuttgart.sat.asp.writer.model.*;
|
||||
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
|
||||
import de.dhbwstuttgart.syntaxtree.GenericTypeVar;
|
||||
import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory;
|
||||
@ -11,13 +10,10 @@ import de.dhbwstuttgart.syntaxtree.type.*;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
|
||||
|
||||
import java.sql.Ref;
|
||||
import java.util.ArrayList;
|
||||
import java.util.Collection;
|
||||
import java.util.List;
|
||||
import java.util.Optional;
|
||||
|
||||
public class ASPGenerator {
|
||||
ASPWriter writer = new ASPWriter();
|
@ -1,8 +1,6 @@
|
||||
package de.dhbwstuttgart.sat.asp;
|
||||
package de.dhbwstuttgart.sat.asp.writer;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRefType;
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPStatement;
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPType;
|
||||
import de.dhbwstuttgart.sat.asp.writer.model.ASPStatement;
|
||||
|
||||
import java.util.HashSet;
|
||||
|
@ -1,7 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
|
||||
public class ASPGenericType implements ASPType{
|
||||
public static final String ASP_GENERIC_TYPE_NAME = "genericType";
|
||||
private final String name;
|
||||
|
||||
public ASPGenericType(String name){
|
||||
@ -9,6 +10,6 @@ public class ASPGenericType implements ASPType{
|
||||
}
|
||||
|
||||
public String toString(){
|
||||
return ASP_GENERIC_TYPE_NAME + "(" + name + ")";
|
||||
return ASPRule.ASP_GENERIC_TYPE_NAME + "(" + name + ")";
|
||||
}
|
||||
}
|
@ -1,4 +1,4 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
public abstract class ASPPair {
|
||||
public final ASPType leftSide;
|
@ -1,13 +1,14 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
|
||||
public class ASPPairEquals extends ASPPair{
|
||||
private final static String ASP_PAIR_EQUALS_NAME = "equals";
|
||||
public ASPPairEquals(ASPType ls, ASPType rs){
|
||||
super(ls, rs);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected String getRuleName() {
|
||||
return ASP_PAIR_EQUALS_NAME;
|
||||
return ASPRule.ASP_PAIR_EQUALS_NAME.toString();
|
||||
}
|
||||
}
|
@ -1,13 +1,16 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
|
||||
import java.util.Map;
|
||||
|
||||
public class ASPPairSmaller extends ASPPair{
|
||||
private final static String ASP_PAIR_SMALLER_NAME = "smaller";
|
||||
public ASPPairSmaller(ASPType ls, ASPType rs){
|
||||
super(ls, rs);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected String getRuleName() {
|
||||
return ASP_PAIR_SMALLER_NAME;
|
||||
return ASPRule.ASP_PAIR_SMALLER_NAME.toString();
|
||||
}
|
||||
}
|
||||
}
|
@ -1,13 +1,14 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
|
||||
public class ASPPairSmallerDot extends ASPPair{
|
||||
private final static String ASP_PAIR_SMALLER_NAME = "smallerDot";
|
||||
public ASPPairSmallerDot(ASPType ls, ASPType rs){
|
||||
super(ls, rs);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected String getRuleName() {
|
||||
return ASP_PAIR_SMALLER_NAME;
|
||||
return ASPRule.ASP_PAIR_SMALLER_DOT_NAME.toString();
|
||||
}
|
||||
}
|
@ -1,18 +1,14 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.ASPGenerator;
|
||||
import de.dhbwstuttgart.sat.asp.ASPWriter;
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
|
||||
import de.dhbwstuttgart.sat.asp.writer.ASPWriter;
|
||||
import de.dhbwstuttgart.syntaxtree.factory.NameGenerator;
|
||||
|
||||
import java.util.HashSet;
|
||||
import java.util.Iterator;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
|
||||
public class ASPParameterList {
|
||||
private final static String ASP_PARAMLIST_NAME = "param";
|
||||
private final static String ASP_PARAMLISTNUMERATION_NAME = "paramNum";
|
||||
private final static String ASP_PARAMLIST_END_POINTER = "null";
|
||||
public final String name;
|
||||
private final List<ASPType> types;
|
||||
|
||||
@ -20,7 +16,7 @@ public class ASPParameterList {
|
||||
int paramNum = 0;
|
||||
this.types = types;
|
||||
if(types.size() == 0){
|
||||
name = ASP_PARAMLIST_END_POINTER;
|
||||
name = ASPRule.ASP_PARAMLIST_END_POINTER.toString();
|
||||
}else{
|
||||
name = newName();
|
||||
String nextPointer = name;
|
||||
@ -29,10 +25,10 @@ public class ASPParameterList {
|
||||
ASPType t = it.next();
|
||||
String param = nextPointer + "," + t.toString() + ",";
|
||||
nextPointer = newName();
|
||||
if(! it.hasNext())nextPointer = ASP_PARAMLIST_END_POINTER;
|
||||
if(! it.hasNext())nextPointer = ASPRule.ASP_PARAMLIST_END_POINTER.toString();
|
||||
param += nextPointer;
|
||||
writer.add(new ASPStatement(ASP_PARAMLIST_NAME + "(" + param + ")"));
|
||||
writer.add(new ASPStatement(ASP_PARAMLISTNUMERATION_NAME + "(" + name + "," +t + "," + paramNum + ")"));
|
||||
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 + ")"));
|
||||
}
|
@ -1,7 +1,8 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
import de.dhbwstuttgart.sat.asp.model.ASPRule;
|
||||
|
||||
public class ASPRefType implements ASPType {
|
||||
public static final String ASP_TYPE = "type";
|
||||
private final ASPParameterList params;
|
||||
private final String name;
|
||||
|
||||
@ -15,6 +16,6 @@ public class ASPRefType implements ASPType {
|
||||
}
|
||||
|
||||
public String toString(){
|
||||
return ASP_TYPE + "(" + name +"," + params.name + ")";
|
||||
return ASPRule.ASP_TYPE + "(" + name +"," + params.name + ")";
|
||||
}
|
||||
}
|
@ -1,4 +1,4 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
public class ASPStatement {
|
||||
private final String stmt;
|
4
src/de/dhbwstuttgart/sat/asp/writer/model/ASPType.java
Normal file
4
src/de/dhbwstuttgart/sat/asp/writer/model/ASPType.java
Normal file
@ -0,0 +1,4 @@
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
public interface ASPType {
|
||||
}
|
@ -1,4 +1,4 @@
|
||||
package de.dhbwstuttgart.sat.asp.model;
|
||||
package de.dhbwstuttgart.sat.asp.writer.model;
|
||||
|
||||
public class ASPTypeVar implements ASPType{
|
||||
private final String name;
|
46
test/asp/ClingoTest.java
Normal file
46
test/asp/ClingoTest.java
Normal file
@ -0,0 +1,46 @@
|
||||
package asp;
|
||||
|
||||
import de.dhbwstuttgart.parser.NullToken;
|
||||
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.TypePlaceholder;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.PairOperator;
|
||||
import org.junit.Test;
|
||||
|
||||
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/";
|
||||
|
||||
@Test
|
||||
public void test() throws IOException, InterruptedException {
|
||||
String content = "";
|
||||
content = new ASPGenerator(this.getPairs(), this.getFC()).getASP();
|
||||
|
||||
PrintWriter writer = new PrintWriter(tempDirectory + "test.lp", "UTF-8");
|
||||
writer.println(content);
|
||||
writer.close();
|
||||
|
||||
Clingo clingo = new Clingo(Arrays.asList(new File(tempDirectory + "test.lp")));
|
||||
System.out.println(clingo.runClingo());
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
}
|
@ -1,7 +1,7 @@
|
||||
package asp.typeinference;
|
||||
|
||||
import de.dhbwstuttgart.core.JavaTXCompiler;
|
||||
import de.dhbwstuttgart.sat.asp.ASPGenerator;
|
||||
import de.dhbwstuttgart.sat.asp.writer.ASPGenerator;
|
||||
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
|
||||
import de.dhbwstuttgart.syntaxtree.SourceFile;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
|
10
test/asp/unifywithoutwildcards/ASPTests.java
Normal file
10
test/asp/unifywithoutwildcards/ASPTests.java
Normal file
@ -0,0 +1,10 @@
|
||||
package asp.unifywithoutwildcards;
|
||||
|
||||
import org.junit.Test;
|
||||
|
||||
public class ASPTests {
|
||||
@Test
|
||||
public void test(){
|
||||
|
||||
}
|
||||
}
|
@ -1,29 +1,15 @@
|
||||
package typeinference;
|
||||
|
||||
import de.dhbwstuttgart.core.JavaTXCompiler;
|
||||
import de.dhbwstuttgart.parser.scope.JavaClassName;
|
||||
import de.dhbwstuttgart.sat.asp.ASPGenerator;
|
||||
import de.dhbwstuttgart.syntaxtree.ClassOrInterface;
|
||||
import de.dhbwstuttgart.syntaxtree.SourceFile;
|
||||
import de.dhbwstuttgart.syntaxtree.factory.ASTFactory;
|
||||
import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory;
|
||||
import de.dhbwstuttgart.syntaxtree.visual.ASTTypePrinter;
|
||||
import de.dhbwstuttgart.typedeployment.TypeInsert;
|
||||
import de.dhbwstuttgart.typedeployment.TypeInsertFactory;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Constraint;
|
||||
import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
|
||||
import de.dhbwstuttgart.typeinference.constraints.Pair;
|
||||
import de.dhbwstuttgart.typeinference.result.ResultSet;
|
||||
import de.dhbwstuttgart.typeinference.typeAlgo.TYPE;
|
||||
import de.dhbwstuttgart.typeinference.unify.TypeUnify;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
|
||||
import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
|
||||
import org.junit.Test;
|
||||
|
||||
import java.io.File;
|
||||
import java.io.IOException;
|
||||
import java.net.URL;
|
||||
import java.net.URLClassLoader;
|
||||
import java.nio.charset.Charset;
|
||||
import java.nio.charset.StandardCharsets;
|
||||
import java.nio.file.Files;
|
||||
@ -32,7 +18,6 @@ import java.util.ArrayList;
|
||||
import java.util.HashSet;
|
||||
import java.util.List;
|
||||
import java.util.Set;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
public class JavaTXCompilerTest {
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user