stan/JavaTypeUnifyASP
1
0
Fork 0
forked from i21017/JavaTypeUnify
Code Pull Requests Activity

Implement Parser

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-06-07 10:51:42 +02:00
parent 313b021fdc
commit 2b7b17060a
6 changed files with 349 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/main/antlr4/de/dhbwstuttgart/input/parser/ConstraintSet.g4 Normal file
View File

@ -0,0 +1,22 @@
grammar ConstraintSet;
constraintSet : (constraints | orConstraint)+;
orConstraint : '{' constraints ('|' constraints)+ '}';
constraints : '{' constraint+ '}' | constraint+;
constraint: subtypeCons | equalsCons;
subtypeCons : type '<.' type;
equalsCons : type '=.' type;
type : tph | namedType;
tph : LOWERCASELETTER IDENTIFIER?;
namedType : IDENTIFIER params?;
params : '<' type (',' type)* '>';
LOWERCASELETTER : [a-z];
IDENTIFIER: (LOWERCASELETTER | [A-Z])+;
KOMMA : ',' -> skip;
NEWLINE : [\r\n]+ -> skip;
WS: [ \t] -> skip ;

18
src/main/asp/unify.pl
View File

@ -1,17 +1,13 @@
% TEST INPUT
%orCons(undCons(lessdot(type("ArrayList", params(tph(tphA))), type("List", params(type("Object", null)))), undCons(lessdot(type("List", params(tph(tphA))), tph(tphA)), null)),
%undCons(lessdot(type("Object", null), type("List", null)), null)
%).
%lessdot(type("List", params(tph(tphA))), tph(tphA)).
%undCons(lessdot(type("List",params(type("Integer", null))),tph("test")),null).
undCons(lessdot( type("List",params(type("Integer", null))),tph("test")),null).
undCons(lessdot(tph("test"),type("List",params(tph("name2")))), null).
orCons(undCons(equalsdot(tph("e"),type("bj",null)),undCons(lessdot(tph("e"),type("Integer",null)),undCons(lessdot(tph("p"),tph("l")),undCons(equalsdot(type("Boolean",null),tph("g")),undCons(equalsdot(tph("t"),type("bc",null)),undCons(lessdot(type("Vector",params(type("Integer",null))),tph("r")),undCons(lessdot(tph("f"),tph("e")), null))))))), null).
%%%%%
super(type("MyPair", params(X, Y)), type("Pair", params(Y, X))) :- super(type("MyPair", params(X, Y))).
super(type("ArrayList", params(X)), type("List", params(X))) :- super(type("ArrayList", params(X))).
super(type("List", params(X)), type("Object", null)) :- super(type("List", params(X))).
super(type("Integer", null), type("Object", null)) :- super(type("Integer", null)).
super(type("Matrix", null), type("Vector", params(type("Vector", params(type("Integer", null)))))) :- super(type("Matrix", null)).
super(type("Vector", params(X)), type("Object", null)) :- super(type("Vector", params(X))).
% Subtyping
super(A, A) :- super(A, B). % reflexive
@ -96,6 +92,8 @@ tphs(tph(A), params(type(C, P), X)) :- tphs( params(type(C, P), X)), tphs(tph(A)
% solve
sigma(tph(A), type(C,P)) :- equalsdot(tph(A), type(C,P)).
sigma2(tph(A), type(C,P)) :- lessdot(tph(A), type(C,P)), not sigma(tph(A), _).
% #show sigma/2.
#show subst/2.
#show sigma2/2.
#show sigma/2.
%#show subst/2.

55
src/main/java/de/dhbwstuttgart/input/ConstraintParser.java Normal file
View File

@ -0,0 +1,55 @@
package de.dhbwstuttgart.input;
import de.dhbwstuttgart.input.parser.ConstraintSetLexer;
import de.dhbwstuttgart.input.parser.ConstraintSetParser;
import de.dhbwstuttgart.sat.asp.*;
import org.antlr.v4.runtime.CharStream;
import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.CommonTokenStream;
import java.util.ArrayList;
import java.util.List;
import java.util.Set;
import java.util.stream.Collectors;
public class ConstraintParser {
public static List<List<Set<Pair>>> parse(String cons){
CharStream input = CharStreams.fromString(cons);
de.dhbwstuttgart.input.parser.ConstraintSetLexer lexer = new ConstraintSetLexer(input);
CommonTokenStream tokens = new CommonTokenStream(lexer);
ConstraintSetParser parser = new ConstraintSetParser(tokens);
ConstraintSetParser.ConstraintSetContext conSet = parser.constraintSet(); //Parsen
Set<Pair> undCons = conSet.constraints().stream().flatMap(c -> parseUndConstraint(c).stream()).collect(Collectors.toSet());
var ret = new ArrayList<List<Set<Pair>>>();
var orCons = conSet.orConstraint().stream().map(ConstraintParser::parseOrConstraint).toList();
ret.add(List.of(undCons));
ret.addAll(orCons);
return ret;
}
private static List<Set<Pair>> parseOrConstraint(ConstraintSetParser.OrConstraintContext ctx) {
return ctx.constraints().stream().map(ConstraintParser::parseUndConstraint).toList();
}
private static Set<Pair> parseUndConstraint(ConstraintSetParser.ConstraintsContext ctx){
return ctx.constraint().stream().map(ConstraintParser::parseConstraint).collect(Collectors.toSet());
}
private static Pair parseConstraint(ConstraintSetParser.ConstraintContext ctx){
if(ctx.equalsCons() != null){
return new EqualsDot(parseType(ctx.equalsCons().type().get(0)),
parseType(ctx.equalsCons().type().get(1)));
}else{
return new LessDot(parseType(ctx.subtypeCons().type().get(0)),
parseType(ctx.subtypeCons().type().get(1)));
}
}
private static Type parseType(ConstraintSetParser.TypeContext ctx) {
if(ctx.tph()!=null){
return new TypePlaceholder(ctx.tph().getText());
}else{
if(ctx.namedType().params() != null)
return new NamedType(ctx.namedType().IDENTIFIER().getText(), ctx.namedType().params().type().stream().map(ConstraintParser::parseType).toList());
else
return new NamedType(ctx.namedType().IDENTIFIER().getText(), List.of());
}
}
}

2
src/main/java/de/dhbwstuttgart/sat/asp/ASPGenerator.java
View File

@ -19,7 +19,7 @@ public class ASPGenerator {
}else {
// undCOns verschachteln
Set<Pair> first = undCon.get(0);
undCon.remove(0);
undCon = undCon.stream().filter(x->!first.equals(x)).collect(Collectors.toList());
return "orCons(" + generateUndCons(first) + ","+ generateOrCons(undCon) + ")";
}/*
String ret = "orCons(";

8
src/main/java/de/dhbwstuttgart/sat/asp/EqualsDot.java Normal file
View File

@ -0,0 +1,8 @@
package de.dhbwstuttgart.sat.asp;
public record EqualsDot(Type left, Type right) implements Pair {
@Override
public String toASP() {
return "equalsdot("+ left().toASP() + "," + right().toASP() + ")";
}
}

256
src/test/java/UnifyTest.java
View File

@ -1,3 +1,4 @@
import de.dhbwstuttgart.input.ConstraintParser;
import de.dhbwstuttgart.sat.asp.*;
import org.apache.commons.io.output.NullWriter;
import org.junit.Test;
@ -13,9 +14,262 @@ public class UnifyTest {
public static final String rootDirectory = System.getProperty("user.dir")+"/resources/javFiles/";
@Test
public void generateConstraintSet(){
System.out.println(ASPGenerator.generateUndCons(genOrConstraintWithOneSolution("test")));
System.out.println(ASPGenerator.generateOrCons(generateOrConstraintTwoSolutions("test")));
}
@Test
public void parserTest(){
String input = "Boolean =. g," +
"t =. bc," +
"f <. e," +
"e =. bj," +
"Vector<Integer> <. r," +
"p <. l," +
"e <. Number,";
System.out.println(ASPGenerator.generateASP(ConstraintParser.parse(input)));
}
@Test
public void matrix2k(){
//und-constraints
//T =. BC
//java.lang.Boolean =. G
//G =. java.lang.Boolean
//F <. E
//E =. BJ
//Vector<java.lang.Integer> <. R
//P <. L
//E <!=. java.lang.Number
//C =. A
//M =. Matrix
//AC <. AB
//Matrix <. C
//AB =. AV
//X <!=. java.lang.Number
//java.lang.Boolean =. AD
//AU <. Z
//AD =. java.lang.Boolean
//H =. Matrix
//AA <. Z
//AB <!=. java.lang.Number
//V =. java.lang.Boolean
//java.lang.Boolean =. V
//J <!=. java.lang.Number
//oder-constraints
//set #1
//Matrix <. Matrix
//set #2
//F =. java.lang.Float ;
// F =. java.lang.Integer
//set #3
//H =. Vector<ALB>
//java.lang.Integer =. J
//H =. Matrix
//java.lang.Integer =. J
//H =. ? extends Vector<ALB>
//java.lang.Integer =. J
//set #4
//ALC =. P
//M =. Vector<ALC>
//E <. java.lang.Integer
//Vector<java.lang.Integer> =. P
//M =. ? extends Matrix
//E <. java.lang.Integer
//Vector<java.lang.Integer> =. P
//M =. Matrix
//E <. java.lang.Integer
//ALC =. P
//M =. ? extends Vector<ALC>
//E <. java.lang.Integer
//set #5
//Vector<ALD> <. Vector<java.lang.Integer>
//set #6
//U =. java.lang.Float
//U =. java.lang.Integer
//set #7
//L =. ? extends Matrix
//java.lang.Integer =. X
//L =. ? extends Vector<AMH>
//java.lang.Integer =. X
//L =. Matrix
//java.lang.Integer =. X
//L =. Vector<AMH>
//java.lang.Integer =. X
//set #8
//AA =. java.lang.Float
//AA =. java.lang.Integer
//set #9
//AC =. java.lang.Integer
//AC =. java.lang.Float
//set #10
//L =. ? extends Matrix
//java.lang.Integer =. AF
//L =. ? extends Vector<ANL>
//java.lang.Integer =. AF
//L =. Matrix
//java.lang.Integer =. AF
//L =. Vector<ANL>
//java.lang.Integer =. AF
//set #11
//Vector<java.lang.Integer> =. AJ
//L =. Matrix
//AB <. java.lang.Integer
//ANM =. AJ
//L =. ? extends Vector<ANM>
//AB <. java.lang.Integer
//Vector<java.lang.Integer> =. AJ
//L =. ? extends Matrix
//AB <. java.lang.Integer
//ANM =. AJ
//L =. Vector<ANM>
//AB <. java.lang.Integer
//set #12
//AB <. java.lang.Integer
//Vector<java.lang.Integer> =. AN
//B =. Matrix
//ANN =. AN
//AB <. java.lang.Integer
//B =. ? extends Vector<ANN>
//B =. Vector<ANN>
//ANN =. AN
//AB <. java.lang.Integer
//B =. ? extends Matrix
//AB <. java.lang.Integer
//Vector<java.lang.Integer> =. AN
//set #13
//Vector<java.lang.Integer> =. AR
//AN =. ? extends Matrix
//T <. java.lang.Integer
//AN =. ? extends Vector<ANO>
//ANO =. AR
//T <. java.lang.Integer
//AN =. Vector<ANO>
//ANO =. AR
//T <. java.lang.Integer
//AN =. Matrix
//Vector<java.lang.Integer> =. AR
//T <. java.lang.Integer
//set #14
//java.lang.Integer =. AT
//AJ <. java.lang.Integer
//AR <. java.lang.Integer
//java.lang.Float =. AT
//AR <. java.lang.Float
//AJ <. java.lang.Float
//set #15
//java.lang.Float =. AU
//AT <. java.lang.Float
//Z <. java.lang.Float
//java.lang.Integer =. AU
//Z <. java.lang.Integer
//AT <. java.lang.Integer
//set #16
//Z <. ANP
//R =. ? extends Vector<ANP>
//java.lang.Boolean =. BA
//R =. ? extends Matrix
//Z <. Vector<java.lang.Integer>
//java.lang.Boolean =. BA
//Z <. ANP
//R =. Vector<ANP>
//java.lang.Boolean =. BA
//Z <. Vector<java.lang.Integer>
//java.lang.Boolean =. BA
//R =. Matrix
//set #17
//R <. Vector<java.lang.Integer>
//C =. ? extends Matrix
//java.lang.Boolean =. BH
//java.lang.Boolean =. BH
//R <. ANQ
//C =. Vector<ANQ>
//R <. Vector<java.lang.Integer>
//java.lang.Boolean =. BH
//C =. Matrix
//java.lang.Boolean =. BH
//C =. ? extends Vector<ANQ>
//R <. ANQ
}
@Test
public void matrixTestBasic(){
/*
//und-constraints
//Matrix <. ret
//Integer <. i
//Matrix <. Vector<x?>
//x? <. v1
//i <. Integer
//Vector<Integer> <. v2
//v1 <. Vector<y?>
//m <. Vector<z?>
//z? <. zr
//zr <. Vector<z2?>
//z2? <. z2r
//z2r <. Integer
//v1 <. Vector<y2?>
//y2? <. y2r
//y2r <. Integer
*/
HashSet<Pair> cons = new HashSet<>();
//v2 <. x2r
cons.add(new LessDot(new TypePlaceholder("v2"), new TypePlaceholder("x2r")));
//x2? <. x2r
cons.add(new LessDot(new TypePlaceholder("x2"), new TypePlaceholder("x2r")));
//ret <. Vector<x2?>
cons.add(new LessDot(new TypePlaceholder("ret"), new NamedType("Vector", List.of(new TypePlaceholder("x2")))));
//v2 <. Vector<x3?>
cons.add(new LessDot(new TypePlaceholder("v2"), new NamedType("Vector", List.of(new TypePlaceholder("x3")))));
//x3? <. x3r
cons.add(new LessDot(new TypePlaceholder("x3"), new TypePlaceholder("x3r")));
//Integer <. x3r
cons.add(new LessDot(new NamedType("Integer", List.of()), new TypePlaceholder("x3r")));
//Matrix <. ret
cons.add(new LessDot(new NamedType("Matrix", List.of()), new TypePlaceholder("ret")));
//Integer <. i
cons.add(new LessDot(new NamedType("Integer", List.of()), new TypePlaceholder("i")));
//Matrix <. Vector<x?>
cons.add(new LessDot(new NamedType("Matrix", List.of()), new NamedType("Vector", List.of(new TypePlaceholder("x")))));
//x? <. v1
cons.add(new LessDot(new TypePlaceholder("x"), new TypePlaceholder("v1")));
//i <. Integer
cons.add(new LessDot(new TypePlaceholder("i"), new NamedType("Integer", List.of())));
//Vector<Integer> <. v2
cons.add(new LessDot(new NamedType("Vector", List.of(new NamedType("Integer", List.of()))), new TypePlaceholder("v2")));
//v1 <. Vector<y?>
cons.add(new LessDot(new TypePlaceholder("v1"), new NamedType("Vector", List.of(new TypePlaceholder("y")))));
//m <. Vector<z?>
cons.add(new LessDot(new TypePlaceholder("m"), new NamedType("Vector", List.of(new TypePlaceholder("z")))));
//z? <. zr
cons.add(new LessDot(new TypePlaceholder("z"), new TypePlaceholder("zr")));
//zr <. Vector<z2?>
cons.add(new LessDot(new TypePlaceholder("z"), new TypePlaceholder("zr")));
//z2? <. z2r
//z2r <. Integer
//v1 <. Vector<y2?>
//y2? <. y2r
//y2r <. Integer
cons.add(new LessDot(new TypePlaceholder("z2"), new TypePlaceholder("z2r"))); // z2? <. z2r
cons.add(new LessDot(new TypePlaceholder("z2r"), new NamedType("Integer", List.of()))); // z2r <. Integer
cons.add(new LessDot(new TypePlaceholder("v1"), new NamedType("Vector", List.of(new TypePlaceholder("y2"))))); // v1 <. Vector<y2?>
cons.add(new LessDot(new TypePlaceholder("y2"), new TypePlaceholder("y2r"))); // y2? <. y2r
cons.add(new LessDot(new TypePlaceholder("y2r"), new NamedType("Integer", List.of()))); // y2r <. Integer
for(Pair p : cons){
System.out.println(p.toASP() + ".");
}
System.out.println(ASPGenerator.generateUndCons(cons));
}
private List<Set<Pair>> generateOrConstraintTwoSolutions(String name){
return List.of(genOrConstraintWithOneSolution(name+"1"), genOrConstraintWithOneSolution(name+"2"));
}
private Set<Pair> genOrConstraintWithOneSolution(String name){
Type type1 = new TypePlaceholder(name);
Type type2 = new NamedType("List", List.of(new NamedType("Integer", List.of())));