Commit 4a95a29f authored by Fred Eisele's avatar Fred Eisele
Browse files

regularized generic template Ty,Sym,En,Fk,Att,...

parent 91cc599d
......@@ -23,14 +23,14 @@ import catdata.Triple;
import catdata.Util;
public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,En,Sym,Fk,Att,Gen,Sk> */ {
public abstract class Algebra<Ty,Sym,En,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty, Sym, En,Fk,Att,Gen,Sk> */ {
//TODO aql generic map method like printX
//TODO aql add final eq method here
public abstract Schema<Ty,En,Sym,Fk,Att> schema();
public abstract Schema<Ty,Sym,En,Fk,Att> schema();
//TODO aql cant validate algebras bc are not dps
......@@ -125,11 +125,11 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
public abstract X fk(Fk fk, X x);
public abstract Term<Ty, Void, Sym, Void, Void, Void, Y> att(Att att, X x);
public abstract Term<Ty, Sym, Void, Void, Void, Void, Y> att(Att att, X x);
public abstract Term<Ty, Void, Sym, Void, Void, Void, Y> sk(Sk sk);
public abstract Term<Ty, Sym, Void, Void, Void, Void, Y> sk(Sk sk);
public final X nf(Term<Void, En, Void, Fk, Void, Gen, Void> term) {
public final X nf(Term<Void, Void, En, Fk, Void, Gen, Void> term) {
if (term.gen != null) {
return gen(term.gen);
} else if (term.fk != null) {
......@@ -138,7 +138,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
throw new RuntimeException("Anomaly: please report");
}
public abstract Term<Void, En, Void, Fk, Void, Gen, Void> repr(X x);
public abstract Term<Void, Void, En, Fk, Void, Gen, Void> repr(X x);
//rows
public int size() {
......@@ -167,14 +167,14 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
/**
* @return only equations for instance part (no typeside, no schema)
*/
public abstract Collage<Ty, Void, Sym, Void, Void, Void, Y> talg();
public abstract Collage<Ty, Sym, Void, Void, Void, Void, Y> talg();
/**
* @param y the T of Y must be obtained from a call to att or sk only!
* @return not a true normal form, but a 'simplified' term for e.g., display purposes
*/
public synchronized final Term<Ty,En,Sym,Fk,Att,Gen,Sk> reprT(Term<Ty, Void, Sym, Void, Void, Void, Y> y) {
Term<Ty,En,Sym,Fk,Att,Gen,Sk> ret = reprT_cache.get(y);
public synchronized final Term<Ty, Sym, En,Fk,Att,Gen,Sk> reprT(Term<Ty, Sym, Void, Void, Void, Void, Y> y) {
Term<Ty, Sym, En,Fk,Att,Gen,Sk> ret = reprT_cache.get(y);
if (ret != null) {
return ret;
}
......@@ -183,17 +183,17 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
return ret;
}
private final Map<Term<Ty, Void, Sym, Void, Void, Void, Y>, Term<Ty,En,Sym,Fk,Att,Gen,Sk>> reprT_cache = Collections.synchronizedMap(new HashMap<>());
public abstract Term<Ty,En,Sym,Fk,Att,Gen,Sk> reprT_protected(Term<Ty, Void, Sym, Void, Void, Void, Y> y);
private final Map<Term<Ty, Sym, Void, Void, Void, Void, Y>, Term<Ty, Sym, En,Fk,Att,Gen,Sk>> reprT_cache = Collections.synchronizedMap(new HashMap<>());
public abstract Term<Ty, Sym, En,Fk,Att,Gen,Sk> reprT_protected(Term<Ty, Sym, Void, Void, Void, Void, Y> y);
private final Map<Term<Ty, En, Sym, Fk, Att, Gen, Sk>, Term<Ty, Void, Sym, Void, Void, Void, Y>>
private final Map<Term<Ty, Sym, En, Fk, Att, Gen, Sk>, Term<Ty, Sym, Void, Void, Void, Void, Y>>
intoY_cache = Collections.synchronizedMap(new HashMap<>());
/**
* @param term of type sort
*/
public synchronized Term<Ty, Void, Sym, Void, Void, Void, Y> intoY(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
Term<Ty, Void, Sym, Void, Void, Void, Y> ret = intoY_cache.get(term);
public synchronized Term<Ty, Sym, Void, Void, Void, Void, Y> intoY(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
Term<Ty, Sym, Void, Void, Void, Void, Y> ret = intoY_cache.get(term);
if (ret != null) {
return ret;
}
......@@ -202,7 +202,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
return ret;
}
private Term<Ty, Void, Sym, Void, Void, Void, Y> intoY0(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
private Term<Ty, Sym, Void, Void, Void, Void, Y> intoY0(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
if (term.obj != null) {
return Term.Obj(term.obj, term.ty);
} else if (term.sym != null) {
......@@ -218,7 +218,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
/**
* @param term term of type entity
*/
public synchronized X intoX(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
public synchronized X intoX(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
if (term.gen != null) {
return nf(term.asGen());
} else if (term.fk != null) {
......@@ -227,7 +227,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
throw new RuntimeException("Anomaly: please report");
}
/*
public X eval(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term, Var var, X x) {
public X eval(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term, Var var, X x) {
if (term.var.equals(var)) {
return x;
} else if (term.gen != null) {
......@@ -267,7 +267,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
// --Commented out by Inspection START (12/24/16, 10:43 PM):
// //TODO aql visitor cleanup
// private Term<Ty, En, Sym, Fk, Att, X, Y> trans(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
// private Term<Ty, Sym, En, Fk, Att, X, Y> trans(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
// if (term.var != null) {
// return Term.Var(term.var);
// } else if (term.obj != null) {
......@@ -336,7 +336,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
}
/*
public Term<Ty, Void, Sym, Void, Void, Void, Y> trans(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
public Term<Ty, Sym, Void, Void, Void, Void, Y> trans(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
if (term.obj != null) {
return Term.Obj(term.obj, term.ty);
} else if (term.sym != null) {
......@@ -349,7 +349,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
throw new RuntimeException("Anomaly: please report");
}
private X trans1(Term<Void, En, Void, Fk, Void, Gen, Void> term) {
private X trans1(Term<Void, Void, En, Fk, Void, Gen, Void> term) {
if (term.gen != null) {
return nf(term);
} else if (term.fk != null) {
......@@ -376,12 +376,12 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
return set;
}
private final Map<Att, Set<Pair<X, Term<Ty, Void, Sym, Void, Void, Void, Y>>>> attsAsSet0 = new HashMap<>();
public synchronized Set<Pair<X, Term<Ty, Void, Sym, Void, Void, Void, Y>>> attAsSet(Att att) {
private final Map<Att, Set<Pair<X, Term<Ty, Sym, Void, Void, Void, Void, Y>>>> attsAsSet0 = new HashMap<>();
public synchronized Set<Pair<X, Term<Ty, Sym, Void, Void, Void, Void, Y>>> attAsSet(Att att) {
if (attsAsSet0.containsKey(att)) {
return attsAsSet0.get(att);
}
Set<Pair<X,Term<Ty, Void, Sym, Void, Void, Void, Y>>> set = new HashSet<>();
Set<Pair<X,Term<Ty, Sym, Void, Void, Void, Void, Y>>> set = new HashSet<>();
for (X x : en(schema().atts.get(att).first)) {
set.add(new Pair<>(x,att(att, x)));
}
......@@ -497,7 +497,7 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
}
private Object fromTerm(Term<Ty, Void, Sym, Void, Void, Void, Y> term) {
private Object fromTerm(Term<Ty, Sym, Void, Void, Void, Void, Y> term) {
if (term.obj != null) {
return term.obj;
}
......
......@@ -8,19 +8,19 @@ import catdata.Chc;
import catdata.Ctx;
import catdata.Pair;
public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> {
public class Anonymized<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> {
private final Instance<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> I;
private final Instance<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> I;
int fresh = 0;
private final Ctx<String, String> iso_string_1 = new Ctx<>(), iso_string_2 = new Ctx<>();
private final Ctx<Integer, Integer> iso_int_1 = new Ctx<>(), iso_int_2 = new Ctx<>();
private Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y>.InnerAlgebra algebra;
private Anonymized<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y>.InnerAlgebra algebra;
private DP<Ty, En, Sym, Fk, Att, Gen, Sk> dp;
private DP<Ty, Sym, En, Fk, Att, Gen, Sk> dp;
private class InnerDP implements DP<Ty, En, Sym, Fk, Att, Gen, Sk> {
private class InnerDP implements DP<Ty, Sym, En, Fk, Att, Gen, Sk> {
@Override
public String toStringProver() {
......@@ -28,17 +28,17 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@Override
public boolean eq(Ctx<Var, Chc<Ty, En>> ctx, Term<Ty, En, Sym, Fk, Att, Gen, Sk> lhs,
Term<Ty, En, Sym, Fk, Att, Gen, Sk> rhs) {
public boolean eq(Ctx<Var, Chc<Ty, En>> ctx, Term<Ty, Sym, En, Fk, Att, Gen, Sk> lhs,
Term<Ty, Sym, En, Fk, Att, Gen, Sk> rhs) {
return I.dp().eq(ctx, iso2(lhs), iso2(rhs));
}
}
private class InnerAlgebra extends Algebra<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> {
private class InnerAlgebra extends Algebra<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> {
@Override
public Schema<Ty, En, Sym, Fk, Att> schema() {
public Schema<Ty, Sym, En, Fk, Att> schema() {
return I.schema();
}
......@@ -58,25 +58,25 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@Override
public Term<Ty, Void, Sym, Void, Void, Void, Y> att(Att att, X x) {
public Term<Ty, Sym, Void, Void, Void, Void, Y> att(Att att, X x) {
return iso1(I.algebra().att(att, x)).convert();
}
@Override
public Term<Ty, Void, Sym, Void, Void, Void, Y> sk(Sk sk) {
public Term<Ty, Sym, Void, Void, Void, Void, Y> sk(Sk sk) {
return iso1(I.algebra().sk(sk)).convert();
}
@Override
public Term<Void, En, Void, Fk, Void, Gen, Void> repr(X x) {
public Term<Void, Void, En, Fk, Void, Gen, Void> repr(X x) {
return I.algebra().repr(x);
}
@Override
public Collage<Ty, Void, Sym, Void, Void, Void, Y> talg() {
Collage<Ty, Void, Sym, Void, Void, Void, Y> col = new Collage<>(I.algebra().talg());
public Collage<Ty, Sym, Void, Void, Void, Void, Y> talg() {
Collage<Ty, Sym, Void, Void, Void, Void, Y> col = new Collage<>(I.algebra().talg());
col.eqs.clear();
for (Eq<Ty, Void, Sym, Void, Void, Void, Y> eq : I.algebra().talg().eqs) {
for (Eq<Ty, Sym, Void, Void, Void, Void, Y> eq : I.algebra().talg().eqs) {
col.eqs.add(new Eq<>(eq.ctx, iso1(eq.lhs), iso1(eq.rhs)));
}
return col;
......@@ -91,7 +91,7 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@Override
public Term<Ty, En, Sym, Fk, Att, Gen, Sk> reprT_protected(Term<Ty, Void, Sym, Void, Void, Void, Y> y) {
public Term<Ty, Sym, En, Fk, Att, Gen, Sk> reprT_protected(Term<Ty, Sym, Void, Void, Void, Void, Y> y) {
return iso1(I.algebra().reprT_protected(iso2(y.convert()).convert())).convert();
}
......@@ -147,19 +147,19 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@SuppressWarnings("hiding")
private <En, Sym, Fk, Att, Gen, Sk> Term<Ty, En, Sym, Fk, Att, Gen, Sk> iso1(Term<Ty, En, Sym, Fk, Att, Gen, Sk> t) {
private <En, Sym, Fk, Att, Gen, Sk> Term<Ty, Sym, En, Fk, Att, Gen, Sk> iso1(Term<Ty, Sym, En, Fk, Att, Gen, Sk> t) {
return t.visit(x->Term.Var(x),(obj,ty)->Term.Obj(iso1(obj,ty),ty), (sym,x)->Term.Sym(sym, x), (fk,x)->Term.Fk(fk,x), (att,x)->Term.Att(att,x), x->Term.Gen(x), x->Term.Sk(x));
}
private Term<Ty, En, Sym, Fk, Att, Gen, Sk> iso2(Term<Ty, En, Sym, Fk, Att, Gen, Sk> t) {
private Term<Ty, Sym, En, Fk, Att, Gen, Sk> iso2(Term<Ty, Sym, En, Fk, Att, Gen, Sk> t) {
return t.visit(x->Term.Var(x),(obj,ty)->Term.Obj(iso2(obj,ty),ty), (sym,x)->Term.Sym(sym, x), (fk,x)->Term.Fk(fk,x), (att,x)->Term.Att(att,x), x->Term.Gen(x), x->Term.Sk(x));
}
//TODO aql note this can fail at runtime
public Anonymized(Instance<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> i) {
public Anonymized(Instance<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> i) {
I = i;
for (Att att : i.schema().atts.keySet()) {
for (Pair<X, Term<Ty, Void, Sym, Void, Void, Void, Y>> p : i.algebra().attAsSet(att)) {
for (Pair<X, Term<Ty, Sym, Void, Void, Void, Void, Y>> p : i.algebra().attAsSet(att)) {
iso1(p.second);
}
}
......@@ -169,7 +169,7 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@Override
public Schema<Ty, En, Sym, Fk, Att> schema() {
public Schema<Ty, Sym, En, Fk, Att> schema() {
return I.schema();
}
......@@ -184,17 +184,17 @@ public class Anonymized<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> extends Instance<Ty
}
@Override
public Set<Pair<Term<Ty, En, Sym, Fk, Att, Gen, Sk>, Term<Ty, En, Sym, Fk, Att, Gen, Sk>>> eqs() {
public Set<Pair<Term<Ty, Sym, En, Fk, Att, Gen, Sk>, Term<Ty, Sym, En, Fk, Att, Gen, Sk>>> eqs() {
return I.eqs().stream().map(x->new Pair<>(iso1(x.first),iso1(x.second))).collect(Collectors.toSet());
}
@Override
public DP<Ty, En, Sym, Fk, Att, Gen, Sk> dp() {
public DP<Ty, Sym, En, Fk, Att, Gen, Sk> dp() {
return dp;
}
@Override
public Algebra<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> algebra() {
public Algebra<Ty, Sym, En, Fk, Att, Gen, Sk, X, Y> algebra() {
return algebra;
}
......
......@@ -18,7 +18,7 @@ import catdata.aql.exp.Exp;
*/
public class AqlCmdLine {
public static <Ty, En, Sym, Fk, Att> String schemaToSql(Schema<Ty, En, Sym, Fk, Att> S) {
public static <Ty, Sym, En, Fk, Att> String schemaToSql(Schema<Ty, Sym, En, Fk, Att> S) {
//prefix, type of ID, ID col name , truncater, printer, varchar length
Map<En, Triple<List<Chc<Fk, Att>>, List<String>, List<String>>> sch_sql = S.toSQL("", "Integer", "ID", Integer.MAX_VALUE, Object::toString, 255);
......@@ -40,8 +40,8 @@ public class AqlCmdLine {
return sch.trim();
}
public static <Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2>
String queryToSql(Query<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2> q) {
public static <Ty, Sym, En1, Fk1, Att1, En2, Fk2, Att2>
String queryToSql(Query<Ty, Sym, En1, Fk1, Att1, En2, Fk2, Att2> q) {
//use "char" for mysql, "varchar" for H2
Map<En2, String> Q = q.unnest().toSQLViews("", "", "ID", "char").second; //must unnest
String ret = "";
......
......@@ -104,12 +104,12 @@ public class AqlJs<Ty, Sym> {
}
public <En, Fk, Att, Gen, Sk> Term<Ty, En, Sym, Fk, Att, Gen, Sk> reduce(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
public <En, Fk, Att, Gen, Sk> Term<Ty, Sym, En, Fk, Att, Gen, Sk> reduce(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
if (java_tys.isEmpty()) {
return term;
}
while (true) {
Term<Ty, En, Sym, Fk, Att, Gen, Sk> next = reduce1(term);
Term<Ty, Sym, En, Fk, Att, Gen, Sk> next = reduce1(term);
if (next.equals(term)) {
return next;
}
......@@ -117,12 +117,12 @@ public class AqlJs<Ty, Sym> {
}
}
private <En, Fk, Att, Gen, Sk> Term<Ty, En, Sym, Fk, Att, Gen, Sk> reduce1(Term<Ty, En, Sym, Fk, Att, Gen, Sk> term) {
private <En, Fk, Att, Gen, Sk> Term<Ty, Sym, En, Fk, Att, Gen, Sk> reduce1(Term<Ty, Sym, En, Fk, Att, Gen, Sk> term) {
if (term.var != null || term.gen != null || term.sk != null || term.obj != null) {
return term;
}
Term<Ty, En, Sym, Fk, Att, Gen, Sk> arg = null;
Term<Ty, Sym, En, Fk, Att, Gen, Sk> arg = null;
if (term.arg != null) {
arg = reduce1(term.arg);
}
......@@ -132,15 +132,15 @@ public class AqlJs<Ty, Sym> {
} else if (term.att != null) {
return Term.Att(term.att, arg);
} else if (term.args != null) {
List<Term<Ty, En, Sym, Fk, Att, Gen, Sk>> args = new LinkedList<>();
for (Term<Ty, En, Sym, Fk, Att, Gen, Sk> x : term.args) {
List<Term<Ty, Sym, En, Fk, Att, Gen, Sk>> args = new LinkedList<>();
for (Term<Ty, Sym, En, Fk, Att, Gen, Sk> x : term.args) {
args.add(reduce1(x));
}
if (!java_fns.containsKey(term.sym)) {
return Term.Sym(term.sym, args);
}
List<Object> unwrapped_args = new LinkedList<>();
for (Term<Ty, En, Sym, Fk, Att, Gen, Sk> t : args) {
for (Term<Ty, Sym, En, Fk, Att, Gen, Sk> t : args) {
if (t.obj != null) {
unwrapped_args.add(t.obj);
}
......
......@@ -159,7 +159,7 @@ public final class AqlOptions {
return ret;
}
public static List<Head<Ty, En, Sym, Fk, Att, Gen, Sk>> getPrec(String str, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col) {
public static List<Head<Ty, Sym, En, Fk, Att, Gen, Sk>> getPrec(String str, Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col) {
Util.assertNotNull(str);
return Arrays.asList(str.split("\\s+")).stream().map(x -> RawTerm.toHeadNoPrim(x, col)).collect(Collectors.toList());
......@@ -356,7 +356,7 @@ public final class AqlOptions {
* @param col possibly null
*/
@SuppressWarnings("hiding")
public <Ty, En, Sym, Fk, Att, Gen, Sk> AqlOptions(Map<String, String> map, @SuppressWarnings("rawtypes") Collage col, AqlOptions defaults) {
public <Ty, Sym, En, Fk, Att, Gen, Sk> AqlOptions(Map<String, String> map, @SuppressWarnings("rawtypes") Collage col, AqlOptions defaults) {
options = new HashMap<>(defaults.options);
for (String key : map.keySet()) {
AqlOption op = AqlOption.valueOf(key);
......@@ -371,7 +371,7 @@ public final class AqlOptions {
* @param map
* @param col possibly null
*/
/*public <Ty, En, Sym, Fk, Att, Gen, Sk> AqlOptions(Map<String, String> map, Collage<Ty,En,Sym,Fk,Att,Gen,Sk> col) {
/*public <Ty, Sym, En, Fk, Att, Gen, Sk> AqlOptions(Map<String, String> map, Collage<Ty, Sym, En,Fk,Att,Gen,Sk> col) {
options = new HashMap<>();
for (String key : map.keySet()) {
AqlOption op = AqlOption.valueOf(key);
......@@ -380,7 +380,7 @@ public final class AqlOptions {
}
} */
private static Object getFromMap(Map<String, String> map, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col, AqlOption op) {
private static Object getFromMap(Map<String, String> map, Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col, AqlOption op) {
switch (op) {
case jdbc_query_export_convert_type:
return op.getString(map);
......
......@@ -27,7 +27,7 @@ public class AqlProver {
//decide, for example, that e = 2 -> e + 1 = 3. So the DP is not necessarily a decision
//procedure for the input theory + java - or even any theory at all, because you may not have
//x = y and y = z -> x = z when java is involved.
public static <Ty, En, Sym, Fk, Att, Gen, Sk> DP<Ty, En, Sym, Fk, Att, Gen, Sk> create(AqlOptions ops, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col1, AqlJs<Ty, Sym> js) {
public static <Ty, Sym, En, Fk, Att, Gen, Sk> DP<Ty, Sym, En, Fk, Att, Gen, Sk> create(AqlOptions ops, Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col1, AqlJs<Ty, Sym> js) {
ProverName name = (ProverName) ops.getOrDefault(AqlOption.prover);
long timeout = (Long) ops.getOrDefault(AqlOption.timeout);
......@@ -78,7 +78,7 @@ public class AqlProver {
}
}
private static <Sk, En, Fk, Ty, Att, Sym, Gen> ProverName auto(AqlOptions ops, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col) {
private static <Sk, En, Fk, Ty, Att, Sym, Gen> ProverName auto(AqlOptions ops, Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col) {
if (col.eqs.isEmpty()) {
return ProverName.free;
} else if (col.isGround()) {
......@@ -91,7 +91,7 @@ public class AqlProver {
throw new RuntimeException("Cannot automatically chose prover: theory is not free, ground, monoidal, or program. Possible solutions include: \n\n1) use the completion prover, possibly with an explicit precedence (see KB example) \n\n2) Reorient equations from left to right to obtain a size-reducing orthogonal rewrite system \n\n3) Remove all equations involving function symbols of arity > 1 \n\n4) Remove all type side and schema equations \n\n5) disable checking of equations in queries using dont_validate_unsafe=true as an option \n\n6) adding options program_allow_nontermination_unsafe=true \n\n7) emailing support, info@catinf.com ");
}
private static <Ty, En, Sym, Fk, Att, Gen, Sk> boolean reorientable(Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col) {
private static <Ty, Sym, En, Fk, Att, Gen, Sk> boolean reorientable(Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col) {
try {
reorient(col);
} catch (Exception ex) {
......@@ -100,10 +100,10 @@ public class AqlProver {
return true;
}
private static <Ty, En, Sym, Fk, Att, Gen, Sk> Collage<Ty, En, Sym, Fk, Att, Gen, Sk> reorient(Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col) {
Collage<Ty, En, Sym, Fk, Att, Gen, Sk> ret = new Collage<>(col);
private static <Ty, Sym, En, Fk, Att, Gen, Sk> Collage<Ty, Sym, En, Fk, Att, Gen, Sk> reorient(Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col) {
Collage<Ty, Sym, En, Fk, Att, Gen, Sk> ret = new Collage<>(col);
ret.eqs.clear();
for (Eq<Ty, En, Sym, Fk, Att, Gen, Sk> eq : col.eqs) {
for (Eq<Ty, Sym, En, Fk, Att, Gen, Sk> eq : col.eqs) {
if (size(eq.lhs) < size(eq.rhs)) {
ret.eqs.add(new Eq<>(eq.ctx, eq.rhs, eq.lhs));
} else if (size(eq.lhs) > size(eq.rhs)) {
......@@ -116,14 +116,14 @@ public class AqlProver {
return ret;
}
private static <Ty, En, Sym, Fk, Att, Gen, Sk> int size(Term<Ty, En, Sym, Fk, Att, Gen, Sk> e) {
private static <Ty, Sym, En, Fk, Att, Gen, Sk> int size(Term<Ty, Sym, En, Fk, Att, Gen, Sk> e) {
if (e.obj != null || e.gen != null || e.sk != null || e.var != null) {
return 1;
} else if (e.att != null || e.fk != null) {
return 1 + size(e.arg);
}
int ret = 1;
for (Term<Ty, En, Sym, Fk, Att, Gen, Sk> arg : e.args) {
for (Term<Ty, Sym, En, Fk, Att, Gen, Sk> arg : e.args) {
ret += size(arg);
}
return ret;
......@@ -133,12 +133,12 @@ public class AqlProver {
// these Lists will never have dups
/* private static <Ty, En, Sym, Fk, Att, Gen, Sk> List<List<Head<Ty, En, Sym, Fk, Att, Gen, Sk>>> allArgs(Sym sym, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col) {
List<List<Head<Ty, En, Sym, Fk, Att, Gen, Sk>>> ret = new LinkedList<>();
/* private static <Ty, Sym, En, Fk, Att, Gen, Sk> List<List<Head<Ty, Sym, En, Fk, Att, Gen, Sk>>> allArgs(Sym sym, Collage<Ty, Sym, En, Fk, Att, Gen, Sk> col) {
List<List<Head<Ty, Sym, En, Fk, Att, Gen, Sk>>> ret = new LinkedList<>();
ret.add(new LinkedList<>());
for (Ty ty : col.syms.get(sym).first) {
List<Head<Ty, En, Sym, Fk, Att, Gen, Sk>> l = new LinkedList<>();
List<Head<Ty, Sym, En, Fk, Att, Gen, Sk>> l = new LinkedList<>();
for (Sym sym2 : col.syms.keySet()) {
if (col.syms.get(sym2).first.isEmpty() && col.syms.get(sym2).second.equals(ty)) {
l.add(Head.Sym(sym2));
......
This diff is collapsed.
This diff is collapsed.
......@@ -23,11 +23,11 @@ import catdata.provers.KBExp;
import catdata.provers.KBTheory;
//TODO: aql validate collage
public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
public class Collage<Ty, Sym, En, Fk, Att, Gen, Sk> {
@SuppressWarnings({ "hiding", "unchecked" })
public <Ty, En, Sym, Fk, Att, Gen, Sk> Collage<Ty, En, Sym, Fk, Att, Gen, Sk> convert() {
return (Collage<Ty, En, Sym, Fk, Att, Gen, Sk>) this;
public <Ty, Sym, En, Fk, Att, Gen, Sk> Collage<Ty, Sym, En, Fk, Att, Gen, Sk> convert() {
return (Collage<Ty, Sym, En, Fk, Att, Gen, Sk>) this;
}
// TODO: aql eep equations segregated?
......@@ -39,8 +39,8 @@ public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
/**
* only works on closed terms
*/
public Set<Term<Ty, En, Sym, Fk, Att, Gen, Void>> applyAllSymbolsNotSk(Set<Term<Ty, En, Sym, Fk, Att, Gen, Void>> set) {
Set<Term<Ty, En, Sym, Fk, Att, Gen, Void>> ret = new HashSet<>();
public Set<Term<Ty, Sym, En, Fk, Att, Gen, Void>> applyAllSymbolsNotSk(Set<Term<Ty, Sym, En, Fk, Att, Gen, Void>> set) {
Set<Term<Ty, Sym, En, Fk, Att, Gen, Void>> ret = new HashSet<>();
for (Gen gen : gens.keySet()) {
ret.add(Term.Gen(gen));
......@@ -49,7 +49,7 @@ public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
// ret.add(Term.Sk(sk));
// }
for (Fk fk : fks.keySet()) {
for (Term<Ty, En, Sym, Fk, Att, Gen, Void> arg : set) {
for (Term<Ty, Sym, En, Fk, Att, Gen, Void> arg : set) {
Chc<Ty, En> x = type(new Ctx<>(), arg.mapGenSk(Function.identity(), Util.voidFn()));
if (x.equals(Chc.inRight(fks.get(fk).first))) {
ret.add(Term.Fk(fk, arg));
......@@ -57,7 +57,7 @@ public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
}
}
for (Att att : atts.keySet()) {
for (Term<Ty, En, Sym, Fk, Att, Gen, Void> arg : set) {
for (Term<Ty, Sym, En, Fk, Att, Gen, Void> arg : set) {
Chc<Ty, En> x = type(new Ctx<>(), arg.mapGenSk(Function.identity(), Util.voidFn()));
if (x.equals(Chc.inRight(atts.get(att).first))) {
ret.add(Term.Att(att, arg));
......@@ -65,7 +65,7 @@ public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
}
}
for (Sym sym : syms.keySet()) {
for (List<Term<Ty, En, Sym, Fk, Att, Gen, Void>> args : helper(syms.get(sym), set)) {
for (List<Term<Ty, Sym, En, Fk, Att, Gen, Void>> args : helper(syms.get(sym), set)) {
ret.add(Term.Sym(sym, args));
}
}
......@@ -73,19 +73,19 @@ public class Collage<Ty, En, Sym, Fk, Att, Gen, Sk> {
return ret;
}
private List<Term<Ty, En, Sym, Fk, Att, Gen, Void>> getForTy(Chc<Ty,En> t, Collection<Term<Ty, En, Sym, Fk, Att, Gen, Void>> set) {
private List<Term<Ty, Sym, En, Fk, Att, Gen, Void>> getForTy(Chc<Ty,En> t, Collection<Term<Ty, Sym, En, Fk, Att, Gen, Void>> set) {
return set.stream().filter(x -> type(new Ctx<>(), x.mapGenSk(Function.identity(), Util.voidFn())).equals(t)).collect(Collectors.toList());
}
private List<List<Term<Ty, En, Sym, Fk, Att, Gen, Void>>> helper(Pair<List<Ty>, Ty> ty, Collection<Term<Ty, En, Sym, Fk, Att, Gen, Void>> set) {
List<List<Term<Ty, En, Sym, Fk, Att, Gen, Void>>> ret = new LinkedList<>();
private List<List<Term<Ty, Sym, En, Fk, Att, Gen, Void>>> helper(Pair<List<Ty>, Ty> ty, Collection<Term<Ty, Sym, En, Fk, Att, Gen, Void>> set) {