Commit a58d1cd1 authored by Ryan Wisnesky's avatar Ryan Wisnesky
Browse files

improve pivot

parent efaea921

src/main/java/catdata/aql/AqlPivot.java

+66 −9
Changes for src/main/java/catdata/aql/AqlPivot.java: 66 added lines, 9 removed lines.
Original line number Diff line number Diff line 
package catdata.aql;





import java.util.Collection;

import java.util.HashMap;

import java.util.HashSet;

import java.util.LinkedList;
@@ -14,11 +15,9 @@ import catdata.Pair; 
import catdata.Triple;

import catdata.Util;

import catdata.aql.AqlOptions.AqlOption;

import catdata.aql.It.ID;

import catdata.aql.exp.SchExpRaw.Att;

import catdata.aql.exp.SchExpRaw.En;

import catdata.aql.exp.SchExpRaw.Fk;

import catdata.aql.fdm.InitialAlgebra;

import catdata.aql.fdm.LiteralInstance;
@@ -30,7 +29,7 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
	

	public final Mapping<Ty, En, Sym, Fk, Att, En0, Fk0, Att0> F;

	

	public Instance<Ty, En, Sym, Fk, Att, X, Y, ID, Chc<Y, Pair<ID, Att>>> J;

	public Instance<Ty, En, Sym, Fk, Att, X, Y, X, Y> J;



	public AqlPivot(Instance<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> i, AqlOptions strat) {

		I = i;
@@ -48,12 +47,19 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
		Collage<Ty, En, Sym, Fk, Att, X, Y> col = new Collage<>();

		col.addAll(I.algebra().talg().convert());

		

		Ctx<En, Collection<X>> ensX = new Ctx<>();

		Ctx<Ty, Collection<Y>> tysX = new Ctx<>();

		Ctx<X, Ctx<Fk, X>> fksX = new Ctx<>();

		Set<Eq<Ty, Void, Sym, Void, Void, Void, Y>> eqsX = new HashSet<>();

		Ctx<X, Ctx<Att, Term<Ty, Void, Sym, Void, Void, Void, Y>>> attsX = new Ctx<>();

		

		for (En0 en : I.schema().ens) {

			for (X x0 : I.algebra().en(en)) {

				String x = x0.toString();

				ens.add(new En(x));

				ens0.put(new En(x), en);

				col.gens.put(x0, new En(x));

				ensX.put(new En(x), Util.singSet(x0));

				for (Att0 att : I.schema().attsFrom(en)) {

					Att xxx = new Att(new En(x),att.toString());

					atts.put(xxx, new Pair<>(new En(x),I.schema().atts.get(att).second));
@@ -64,6 +70,14 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
					r = I.algebra().att(att, x0).convert();

					col.eqs.add(new Eq<Ty, En, Sym, Fk, Att, X, Y>(new Ctx<>(), l, r));

					eqs0.add(new Pair<>(l,r));

					

					Ctx<Att, Term<Ty, Void, Sym, Void, Void, Void, Y>> 

					ctx0 = attsX.map.get(x0);

					if (ctx0 == null) {

						ctx0 = new Ctx<>();

					}

					ctx0.put(xxx, I.algebra().att(att, x0));

					attsX.map.put(x0, ctx0);

				}

				for (Fk0 fk : I.schema().fksFrom(en)) {

					Fk xxx = new Fk(new En(x),fk.toString());
@@ -75,19 +89,35 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
					r = Term.Gen(I.algebra().fk(fk, x0));

					col.eqs.add(new Eq<Ty, En, Sym, Fk, Att, X, Y>(new Ctx<>(), l, r));

					eqs0.add(new Pair<>(l,r));

					

					Ctx<Fk, X> ctx0 = fksX.map.get(x0);

					if (ctx0 == null) {

						ctx0 = new Ctx<>();

					}

					ctx0.put(xxx, I.algebra().fk(fk, x0));

					fksX.map.put(x0, ctx0);

				}

			}

		}

		

		for (Ty ty : I.schema().typeSide.tys) {

			tysX.map.put(ty, new HashSet<>());

		}

		for (Y y : I.algebra().talg().sks.map.keySet()) {

			Term<Ty, En, Sym, Fk, Att, X, Y> l = Term.Sk(y); 

			Term<Ty, En, Sym, Fk, Att, X, Y> r = foo(I.algebra().reprT(Term.Sk(y)));

			

			col.eqs.add(new Eq<Ty, En, Sym, Fk, Att, X, Y>(new Ctx<>(), l, r));

			eqs0.add(new Pair<>(l,r));

			Ty ty = I.algebra().talg().sks.get(y);

			Collection<Y> ctx0 = tysX.map.get(ty);

			ctx0.add(y);

			tysX.map.put(ty, ctx0);

		}

		eqsX.addAll(I.algebra().talg().eqs);

		

		DP<Ty, En, Sym, Fk, Att, Void, Void> dp = new DP<>() {

		

		DP<Ty, En, Sym, Fk, Att, Void, Void> dp1 = new DP<>() {



			@Override

			public String toStringProver() {
@@ -102,18 +132,44 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
			

		};

		

		intI = new Schema<>(I.schema().typeSide, ens , atts, fks, new HashSet<>(), dp, I.allowUnsafeJava());

		

		

		intI = new Schema<>(I.schema().typeSide, ens , atts, fks, new HashSet<>(), dp1, I.allowUnsafeJava());

				

		F = new Mapping<Ty, En, Sym, Fk, Att, En0, Fk0, Att0>(ens0, atts0, fks0, intI, I.schema(), false);

		

		col.addAll(intI.collage());

		

		

		InitialAlgebra<Ty, En, Sym, Fk, Att, X, Y, ID> initial = new InitialAlgebra<>(strat, intI, col, new It(),

				Object::toString, Object::toString);

		

		J = new LiteralInstance<Ty, En, Sym, Fk, Att, X, Y, ID, Chc<Y, Pair<ID, Att>>>

		(intI, col.gens.map, col.sks.map, eqs0, initial.dp(), initial,

		Algebra<Ty, En, Sym, Fk, Att, X, Y, X, Y> initial = 

				new ImportAlgebra<Ty, En, Sym, Fk, Att, X, Y>(intI, ensX, tysX, fksX, attsX, Object::toString, Object::toString, (Boolean) strat.getOrDefault(AqlOption.allow_java_eqs_unsafe), eqsX);

//		

		DP<Ty, En, Sym, Fk, Att, X, Y> dp2 = new DP<>() {



			@Override

			public String toStringProver() {

				return "Pivot prover";

			}



			@Override

			public boolean eq(Ctx<Var, Chc<Ty, En>> ctx, Term<Ty, En, Sym, Fk, Att, X, Y> lhs,

					Term<Ty, En, Sym, Fk, Att, X, Y> rhs) {

				if (!ctx.isEmpty()) {

					return Util.anomaly();

				} else if (lhs.hasTypeType()) {

					Term<Ty, Void, Sym, Void, Void, Void, Y> y1 = initial.intoY(lhs);

					Term<Ty, Void, Sym, Void, Void, Void, Y> y2 = initial.intoY(rhs);

					return I.dp().eq(new Ctx<>(), I.algebra().reprT(y1), I.algebra().reprT(y2)); 

				} else {

					return initial.intoX(lhs).equals(initial.intoX(rhs));

				}

			}

			

		};

		

		J = new LiteralInstance<Ty, En, Sym, Fk, Att, X, Y, X, Y>

		(intI, col.gens.map, col.sks.map, eqs0, dp2, initial,

				(Boolean) strat.getOrDefault(AqlOption.require_consistency),

				(Boolean) strat.getOrDefault(AqlOption.allow_java_eqs_unsafe));
@@ -149,4 +205,5 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> { 
		return Util.anomaly();

	}

	

	

}

src/main/java/catdata/aql/ImportAlgebra.java

+38 −22
Changes for src/main/java/catdata/aql/ImportAlgebra.java: 38 added lines, 22 removed lines.
Original line number Diff line number Diff line 
package catdata.aql;



import java.util.Collection;

import java.util.Set;

import java.util.function.Function;

import java.util.stream.Collectors;



import catdata.Chc;

import catdata.Ctx;

import catdata.Triple;

import catdata.Util;



public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,Att,X,Y,X,Y>  implements DP<Ty,En,Sym,Fk,Att,X,Y>  {

public class ImportAlgebra<Ty, En, Sym, Fk, Att, X, Y> extends Algebra<Ty, En, Sym, Fk, Att, X, Y, X, Y>

		implements DP<Ty, En, Sym, Fk, Att, X, Y> {



	private final Schema<Ty, En, Sym, Fk, Att> schema;

	private final Ctx<En, Collection<X>> ens;
@@ -24,7 +25,14 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 


//	private final Ctx<Y, Term<Ty, En, Sym, Fk, Att, X, Y>> reprT_extra;



	public ImportAlgebra(Schema<Ty, En, Sym, Fk, Att> schema, Ctx<En, Collection<X>> ens, Ctx<Ty, Collection<Y>> tys, Ctx<X, Ctx<Fk, X>> fks, Ctx<X, Ctx<Att, Term<Ty, Void, Sym, Void, Void, Void, Y>>> atts, Function<X, String> printX, Function<Y, String> printY, boolean dontCheckClosure) {

	public ImportAlgebra(Schema<Ty, En, Sym, Fk, Att> schema,

			Ctx<En, Collection<X>> ens, Ctx<Ty, Collection<Y>> tys,

			Ctx<X, Ctx<Fk, X>> fks, 

			Ctx<X, Ctx<Att, Term<Ty, Void, Sym, Void, Void, Void, Y>>> atts, 

			Function<X, String> printX, 

			Function<Y, String> printY, 

			boolean dontCheckClosure, 

			Set<Eq<Ty, Void, Sym, Void, Void, Void, Y>> eqs) { 

		this.schema = schema;

		this.ens = ens;

		this.tys = tys;
@@ -32,7 +40,8 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
		this.atts = atts;

		this.printX = printX;

		this.printY = printY; 

		initTalg(); 

		initTalg(eqs); 

		

		if (!dontCheckClosure) {

			checkClosure();

		}
@@ -44,26 +53,32 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
				for (Fk fk : schema.fksFrom(en)) {

					if (!fks.containsKey(x)) {

						// moved inside fk loop because don't have Ctx if no fks/atts out

						throw new RuntimeException("Incomplete import: no foreign key values specified for ID " + x + " in entity " + en);

						throw new RuntimeException(

								"Incomplete import: no foreign key values specified for ID " + x + " in entity " + en);

					}

					if (!fks.get(x).containsKey(fk)) {

						throw new RuntimeException("Incomplete import: no value for foreign key " + fk + " specified for  ID " + x+ " in entity " + en);

						throw new RuntimeException("Incomplete import: no value for foreign key " + fk

								+ " specified for  ID " + x + " in entity " + en);

					}

					X y = fk(fk, x);

					if (!ens.get(schema.fks.get(fk).second).contains(y)) {

						throw new RuntimeException("Incomplete import: value for " + x + "'s foreign key " + fk + " is " + y + " which is not an ID imported into " + schema.fks.get(fk).second) ;

						throw new RuntimeException("Incomplete import: value for " + x + "'s foreign key " + fk + " is "

								+ y + " which is not an ID imported into " + schema.fks.get(fk).second);

					}

				}

				for (Att att : schema.attsFrom(en)) {

					if (!atts.containsKey(x)) {

						throw new RuntimeException("Incomplete import: no attribute " + att + " specified for ID " + x + " in entity " + en);

						throw new RuntimeException("Incomplete import: no attribute " + att + " specified for ID " + x

								+ " in entity " + en);

					}

					if (!atts.get(x).containsKey(att)) {

						throw new RuntimeException("Incomplete import: no value for attribute " + att + " specified for  ID " + x + " in entity " + en);

						throw new RuntimeException("Incomplete import: no value for attribute " + att

								+ " specified for  ID " + x + " in entity " + en);

					}

					Term<Ty, Void, Sym, Void, Void, Void, Y> y = att(att, x);

					if (y.sk != null && !tys.get(schema.atts.get(att).second).contains(y.sk)) {

						throw new RuntimeException("Incomplete import: value for " + x + "'s attribute " + att + " is " + y.sk + " which is not an ID imported into " + schema.atts.get(att).second) ;

						throw new RuntimeException("Incomplete import: value for " + x + "'s attribute " + att + " is "

								+ y.sk + " which is not an ID imported into " + schema.atts.get(att).second);

					}

				}

			}
@@ -75,16 +90,13 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
		}



		/*

		 * for (Fk fk : schema.fksFrom(en)) {

					if (!fks.get(x).containsKey(fk)) {

						throw new RuntimeException("Incomplete import: no value for " + x + " along fk " + fk);

					}

					if (!ens.get)

				}

		 * for (Fk fk : schema.fksFrom(en)) { if (!fks.get(x).containsKey(fk)) { throw

		 * new RuntimeException("Incomplete import: no value for " + x + " along fk " +

		 * fk); } if (!ens.get) }

		 */

	}



	private void initTalg() {

	private void initTalg(Set<Eq<Ty, Void, Sym, Void, Void, Void, Y>> eqs0) {

		talg.syms.putAll(schema.typeSide.syms.map);

		talg.tys.addAll(schema.typeSide.tys);

		talg.java_fns.putAll(schema.typeSide.js.java_fns.map);
@@ -96,12 +108,15 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
			}

		}

		for (Triple<Ctx<Var, Ty>, Term<Ty, Void, Sym, Void, Void, Void, Void>, Term<Ty, Void, Sym, Void, Void, Void, Void>> x : schema.typeSide.eqs) {

			talg.eqs.add(new Eq<>(x.first.inLeft(), x.second.mapGenSk(Util.voidFn(), Util.voidFn()), x.third.mapGenSk(Util.voidFn(),Util.voidFn())));

			talg.eqs.add(new Eq<>(x.first.inLeft(), x.second.mapGenSk(Util.voidFn(), Util.voidFn()),

					x.third.mapGenSk(Util.voidFn(), Util.voidFn())));

		}

		talg.eqs.addAll(eqs0);

	}



	@Override

	public boolean eq(Ctx<Var, Chc<Ty, En>> ctx, Term<Ty, En, Sym, Fk, Att, X, Y> lhs, Term<Ty, En, Sym, Fk, Att, X, Y> rhs) {

	public boolean eq(Ctx<Var, Chc<Ty, En>> ctx, Term<Ty, En, Sym, Fk, Att, X, Y> lhs,

			Term<Ty, En, Sym, Fk, Att, X, Y> rhs) {

		if (!ctx.isEmpty()) {

			Util.anomaly();

		} else if (lhs.hasTypeType()) {
@@ -148,9 +163,11 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
	@Override

	public Term<Ty, En, Sym, Fk, Att, X, Y> reprT_protected(Term<Ty, Void, Sym, Void, Void, Void, Y> y) {

		if (schema.typeSide.js.java_tys.isEmpty()) {

			return y.map(Function.identity(), Function.identity(), Util.voidFn(), Util.voidFn(), Util.voidFn(), Function.identity());

			return y.map(Function.identity(), Function.identity(), Util.voidFn(), Util.voidFn(), Util.voidFn(),

					Function.identity());

		}

		return schema.typeSide.js.reduce(y.map(Function.identity(), Function.identity(), Util.voidFn(), Util.voidFn(), Util.voidFn(), Function.identity()));

		return schema.typeSide.js.reduce(y.map(Function.identity(), Function.identity(), Util.voidFn(), Util.voidFn(),

				Util.voidFn(), Function.identity()));

	}



	@Override
@@ -183,5 +200,4 @@ public class ImportAlgebra<Ty,En,Sym,Fk,Att,X,Y> extends Algebra<Ty,En,Sym,Fk,At 
		return talg.eqs.isEmpty(); // TODO aql guess

	}





}

src/main/java/catdata/aql/exp/InstExp.java

+3 −3
Changes for src/main/java/catdata/aql/exp/InstExp.java: 3 added lines, 3 removed lines.
Original line number Diff line number Diff line
@@ -65,7 +65,7 @@ public abstract class InstExp<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> 
	///////////////////////////////////////////////////////////////////////



	public static final class InstExpPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y>

	extends InstExp<Ty, SchExpRaw.En, Sym, SchExpRaw.Fk, SchExpRaw.Att, X, Y, ID, Chc<Y, Pair<ID, catdata.aql.exp.SchExpRaw.Att>>> {

	extends InstExp<Ty, catdata.aql.exp.SchExpRaw.En, Sym, catdata.aql.exp.SchExpRaw.Fk, catdata.aql.exp.SchExpRaw.Att, X, Y, X, Y> {

			

		public InstExpPivot(InstExp<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> i, List<Pair<String, String>> ops) {

			I = i;
@@ -85,10 +85,10 @@ public abstract class InstExp<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> 
			return ops;

		}

		@Override

		public Instance<Ty, catdata.aql.exp.SchExpRaw.En, Sym, catdata.aql.exp.SchExpRaw.Fk, catdata.aql.exp.SchExpRaw.Att, X, Y, ID, Chc<Y, Pair<ID, catdata.aql.exp.SchExpRaw.Att>>> eval(

		public Instance<Ty, catdata.aql.exp.SchExpRaw.En, Sym, catdata.aql.exp.SchExpRaw.Fk, catdata.aql.exp.SchExpRaw.Att, X, Y, X, Y> eval(

				AqlEnv env) {

			AqlOptions strat = new AqlOptions(ops, null, env.defaults);

			Instance<Ty, SchExpRaw.En, Sym, SchExpRaw.Fk, SchExpRaw.Att, X, Y, ID, Chc<Y, Pair<ID, SchExpRaw.Att>>> l = new AqlPivot<>(I.eval(env), strat).J;

			Instance<Ty, catdata.aql.exp.SchExpRaw.En, Sym, catdata.aql.exp.SchExpRaw.Fk, catdata.aql.exp.SchExpRaw.Att, X, Y, X, Y> l = new AqlPivot<>(I.eval(env), strat).J;

			return l;

		}

		@Override

src/main/java/catdata/aql/exp/InstExpImport.java

+2 −1
Changes for src/main/java/catdata/aql/exp/InstExpImport.java: 2 added lines, 1 removed line.
Original line number Diff line number Diff line 
package catdata.aql.exp;



import java.util.Collection;

import java.util.Collections;

import java.util.HashSet;

import java.util.LinkedList;

import java.util.List;
@@ -247,7 +248,7 @@ public abstract class InstExpImport<Handle, Q> 
		}



		ImportAlgebra<Ty, En, Sym, Fk, Att, Gen, Null<?>> alg = new ImportAlgebra<>(sch, ens0, tys0, fks0, atts0,

				Object::toString, Object::toString, dont_check_closure);

				Object::toString, Object::toString, dont_check_closure, Collections.emptySet());



		SaturatedInstance<catdata.aql.exp.TyExpRaw.Ty, catdata.aql.exp.SchExpRaw.En, catdata.aql.exp.TyExpRaw.Sym, catdata.aql.exp.SchExpRaw.Fk, catdata.aql.exp.SchExpRaw.Att, catdata.aql.exp.InstExpRaw.Gen, Null<?>, catdata.aql.exp.InstExpRaw.Gen, Null<?>> x = new SaturatedInstance<>(alg, alg, (Boolean) op.getOrDefault(AqlOption.require_consistency),

				(Boolean) op.getOrDefault(AqlOption.allow_java_eqs_unsafe), true, extraRepr);

src/main/java/catdata/aql/exp/InstExpJdbcAll.java

+2 −1
Changes for src/main/java/catdata/aql/exp/InstExpJdbcAll.java: 2 added lines, 1 removed line.
Original line number Diff line number Diff line
@@ -4,6 +4,7 @@ import java.sql.Connection; 
import java.sql.DriverManager;

import java.sql.SQLException;

import java.util.Collection;

import java.util.Collections;

import java.util.HashMap;

import java.util.HashSet;

import java.util.List;
@@ -151,7 +152,7 @@ public class InstExpJdbcAll extends InstExp<Ty, En, Sym, Fk, Att, Gen, Null<?>, 
			}

		}



		ImportAlgebra<Ty, En, Sym, Fk, Att, Gen, Null<?>> alg = new ImportAlgebra<Ty,En,Sym,Fk,Att,Gen,Null<?>>(sch, ens0, tys0, fks0, atts0, Object::toString, Object::toString, dontCheckClosure);

		ImportAlgebra<Ty, En, Sym, Fk, Att, Gen, Null<?>> alg = new ImportAlgebra<Ty,En,Sym,Fk,Att,Gen,Null<?>>(sch, ens0, tys0, fks0, atts0, Object::toString, Object::toString, dontCheckClosure, Collections.emptySet());



		return new SaturatedInstance<>(alg, alg, (Boolean) ops.getOrDefault(AqlOption.require_consistency), (Boolean) ops.getOrDefault(AqlOption.allow_java_eqs_unsafe), true, extraRepr);

	}