Commit 36e15531 authored by Ryan Wisnesky's avatar Ryan Wisnesky
Browse files

add accessor for frozen instances

parent abcabeee

doc/aqlmanual/aqlmanual.tex

+10 −3
Changes for doc/aqlmanual/aqlmanual.tex: 10 added lines, 3 removed lines.
Original line number Diff line number Diff line
@@ -358,7 +358,7 @@ The identity query on a schema. 
Constructs the query $Q^F$ such that $eval(Q^F) \cong \Delta_F$ and $coeval(Q_F) \cong \Sigma_F$ for the mapping F.



\section{{\tt toCoQuery <mapping>}}

Constructs the query $Q_F$ such that $coeval(Q_F) \cong \Delta_F$ and $eval(Q_F) \cong \Pi_F$ for the mapping F.  The option {\tt toCoQuery\_max\_term\_size} controls the maximum size of the terms to be searched.

Constructs the query $Q_F$ such that $coeval(Q_F) \cong \Delta_F$ and $eval(Q_F) \cong \Pi_F$ for the mapping F.  The option {\tt toCoQuery\_max\_term\_size} controls the maximum size of the terms to be searched.  Note that $F$ must be surjective on attributes to succeed.



\section{{\tt [ <query> ; <query> ]}}

Composes two queries: if {\tt f : A -> B} and {\tt g : B -> C}, then {\tt [ f ; g ] : A -> C} using the complete ``view unfolding'' algorithm.   The incomplete co-evaluation based method can be used instead with the {\tt query\_compose\_use\_incomplete} option.
@@ -449,8 +449,11 @@ If $F : S \to T$ is a mapping and $J$ is an $T$-instance, then $\Delta_F J$ is a 
\section{{\tt sigma <mapping> <instance>}}

If $F : S \to T$ is a mapping and $I$ is an $S$-instance, then $\Sigma_F I$ is a $T$-instance. 



\section{{\tt sigma\_chase <mapping> <instance> number}}

Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm.

\section{{\tt sigma\_chase <mapping> <instance>}}

Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm.  See {\tt chase\_style} option.



\section{{\tt frozen <query> <target entity>}}

If $Q : S \to T$ is a query and $t$ is a $T$-entity, then $frozen \ Q \ t$ is the ``frozen'' or ``canonical'' $S$-instance for $t$ in $Q$. 



\section{{\tt coproduct\_sigma (<mapping> <instance>)+ : <schema>}}

The expression {\tt coproduct\_sigma}  $F \ I \ G \ J \ : S$ means $\Sigma_F(I) + \Sigma_G(J)$, where $+$ is $S$-instance co-product.  Arbitrarily many mapping-instance pairs can be used.  This operation is provided to help minimize the number of intermediate materializations required to execute an AQL program.
@@ -1064,6 +1067,10 @@ Defines the name of the AQL environment being constructed for use with the {\tt 


Defines the SQL quasi-type to be used with CONVERT statements when emitting SQL for AQL queries.  A good initial guess is VARCHAR for H2 and CHAR for MySQL.



\subsection{{\tt chase\_style}}



Either {\tt parallel} (faster, but uses more space) or {\tt leftkan} (slower, but uses less space).



\end{document}

resources/examples/aql/All_Syntax.aql

+1 −0
Changes for resources/examples/aql/All_Syntax.aql: 1 added line, 0 removed lines.
Original line number Diff line number Diff line
@@ -154,6 +154,7 @@ instance i20 = coproduct_unrestricted i1 + i2 : s3 { options prover = completion 
instance i11 = coequalize (identity i1) (identity i1) { options prover = completion }

instance i12 = chase literal : s3 { } i3 

instance i15 = anonymize i12

instance i16 = frozen q3 Q

//random -- see Employees example

//import_jdbc -- see JDBC example

//import_jdbc_all -- see JDBC example

src/catdata/aql/Chase.java

+157 −14
Changes for src/catdata/aql/Chase.java: 157 added lines, 14 removed lines.
Original line number Diff line number Diff line
@@ -6,6 +6,7 @@ import java.util.Iterator; 
import java.util.LinkedList;

import java.util.List;

import java.util.Set;

import java.util.function.BiFunction;



import catdata.BinRelMap;

import catdata.Chc;
@@ -27,10 +28,10 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 


		public final Ctx<En1, Ctx<X, Lineage<Void, En2, Void, Fk2, Void, Gen, Void>>> us;



		public final Ctx<Ty, BinRelMap<Lineage<Ty, Void, Sym, Void, Void, Void, Y>, Lineage<Ty, Void, Sym, Void, Void, Void, Y>>> tys;

		public final Ctx<Att2, BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Ty, Void, Sym, Void, Void, Void, Y>>> atts;

		public final Ctx<Ty, BinRelMap<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> tys;

		public final Ctx<Att2, BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> atts;



		public final Ctx<Ty, Ctx<Y, Lineage<Ty, Void, Sym, Void, Void, Void, Y>>> vs;

		public final Ctx<Ty, Ctx<Y, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> vs;



		public Content() {

			ens = new Ctx<>();
@@ -76,12 +77,12 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
			}



			for (Ty ty : F.src.typeSide.tys) {

				BinRelMap<Lineage<Ty, Void, Sym, Void, Void, Void, Y>, Lineage<Ty, Void, Sym, Void, Void, Void, Y>> x = c.tys

				BinRelMap<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> x = c.tys

						.get(ty);

				tys.get(ty).addAll(x);

			}

			for (Att2 att : atts.keySet()) {

				BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Ty, Void, Sym, Void, Void, Void, Y>> x = c.atts

				BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> x = c.atts

						.get(att);

				atts.get(att).addAll(x);

			}
@@ -124,16 +125,17 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
			this.vs = new Ctx<>();



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

				Ctx<Y, Lineage<Ty, Void, Sym, Void, Void, Void, Y>> ctx = new Ctx<>();

				Ctx<Y, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> ctx = new Ctx<>();

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

					ctx.put(y, new Lineage<>(fresh.next(), Term.Sk(y)));

					ctx.put(y, Chc.inRight(I.algebra().reprT(Term.Sk(y))));

				}

				vs.put(ty, ctx);

			}

		}



		// TODO aql update

		public Content merge(Ctx<En2, UnionFind<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>>> ufs) {

		public Content merge(Ctx<En2, UnionFind<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>>> ufs,

				Ctx<Ty, UnionFind<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> ufs2) {

			Content ret = new Content();

			for (En2 en : F.dst.ens) {

				for (Pair<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Void, En2, Void, Fk2, Void, Gen, Void>> x : ens
@@ -164,6 +166,67 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
					ret.us.get(en).put(x, ufs.get(F.ens.get(en)).find(n));

				}

			}



			// partitions to their constants, if any

			Ctx<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> pars = new Ctx<>();

			for (Ty ty : F.dst.typeSide.tys) {

				for (Pair<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> x : tys

						.get(ty)) {

					if (x.first.left) {

						continue;

					}



					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> par = ufs2.get(ty).find(x.first);

					if (pars.containsKey(par)) {

						Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk> parConst = pars.get(par);

						if (!I.dp().eq(new Ctx<>(), x.first.r, parConst)) {

							throw new RuntimeException("Collision: " + x.first.r + " not provably equal to " + parConst

									+ " in input instance.");

						}

					} else {

						pars.put(par, x.first.r);

					}

				}

			}



			BiFunction<Ty, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> nf = (

					t, zz) -> {

						Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> y = ufs2.get(t).find(zz);

						if (pars.containsKey(y)) {

							return Chc.inRight(pars.get(y));

						}

						return y;

			};



			for (Ty ty : F.dst.typeSide.tys) {

				for (Pair<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> x : tys

						.get(ty)) {

					if (!x.first.equals(x.second)) {

						Util.anomaly();

					}

					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> n = nf.apply(ty, x.first);

					ret.tys.get(ty).add(n, n);

				}

			}

			// System.out.println("yyy " + ret);

			for (Att2 att : F.dst.atts.keySet()) {

				En2 a = F.dst.atts.get(att).first;

				Ty b = F.dst.atts.get(att).second;

				for (Pair<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> x : atts

						.get(att)) {

					Lineage<Void, En2, Void, Fk2, Void, Gen, Void> n1 = ufs.get(a).find(x.first);

					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> n2 = nf.apply(b, x.second);

					ret.atts.get(att).add(n1, n2);

					// System.out.println("on " + fk + " doing " + x + " is " + n1 + "," + n2);

				}

			}

			// System.out.println("xxx " + ret);

			for (Ty ty : vs.keySet()) {

				for (Y x : vs.get(ty).keySet()) {

					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> n = vs.get(ty).get(x);

					ret.vs.get(ty).put(x, nf.apply(ty, n));

				}

			}

			// System.out.println("merged " + ret);

			// ret.iso = iso.map((k,x)->new Pair<>(k,x.map(y->ufs.get(k).find(y))));

			return ret;
@@ -227,6 +290,10 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
		for (En2 en : F.dst.ens) {

			ufs.put(en, new UnionFind<>(new HashSet<>()));

		}

		Ctx<Ty, UnionFind<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> ufs2 = new Ctx<>();

		for (Ty ty : F.dst.typeSide.tys) {

			ufs2.put(ty, new UnionFind<>(new HashSet<>()));

		}

		Boolean[] changed = new Boolean[] { false };



		makeArrowsTotal(toAdd, changed);
@@ -235,25 +302,26 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 


		moveObjects(toAdd, changed);



		//todo

		doEqs(toAdd, ufs, changed);



		T.addAll(toAdd);



		makeFunctional(ufs, changed);

		makeFunctional(ufs, changed, ufs2);



		if (!changed[0]) {

			return false;

		}



		T = T.merge(ufs);



		T = T.merge(ufs, ufs2);



		return true;

	}



	static int x = 0;



	public void makeFunctional(Ctx<En2, UnionFind<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>>> ufs,

			Boolean[] changed) {

			Boolean[] changed, Ctx<Ty, UnionFind<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>> ufs2) {

		for (En2 v : F.dst.ens) {

			for (Fk2 a : F.dst.fksFrom(v)) {
@@ -271,6 +339,27 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
							ufs.get(w).union(y1, y2);

							// System.out.println("equating " + y1 + " = " + y2 + " at " + w);



							changed[0] = true;

						}

					}

				}

			}

			for (Att2 a : F.dst.attsFrom(v)) {



				// T_a(x,y1) /\ T_b(x,y2) -> y2=y1;

				Ty w = F.dst.atts.get(a).second;

				BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>

				T_a = T.atts.get(a);



				for (Lineage<Void, En2, Void, Fk2, Void, Gen, Void> x : T_a.keySet()) {

					Collection<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> ys = T_a.get(x);

					// System.out.println("collection is " + ys);

					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> y1 = Util.get0X(ys);

					for (Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> y2 : ys) {

						if (!y1.equals(y2)) {

							ufs2.get(w).union(y1, y2);

							// System.out.println("equating " + y1 + " = " + y2 + " at " + w);



							changed[0] = true;

						}

					}
@@ -411,6 +500,23 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
				}

			}

		}

		

		for (Ty a : F.src.typeSide.tys) {

			// T_v(x) -> Ey. T_a(x,y)

			// this is the 'loading' step in the Content constructor



			// T_a(x,y) -> T_v(x) /\ T_w(y)

			Ty w = a;

			Ctx<Y, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> T_a = T.vs.get(a);

			BinRelMap<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> 

			T_w = T.tys.get(w);

			for (Y xy : T_a.keySet()) {

				Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> x = T_a.get(xy);

				if (!T_w.containsKey(x)) {

					changed[0] = changed[0] | toAdd.tys.get(w).add(x, x);

				}

			}

		}

	}



	public void makeObjectsTotal(Content toAdd, Boolean[] changed) {
@@ -438,14 +544,33 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
				}

			}

			

			for (Att2 a : F.dst.attsFrom(v)) {

				BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> 

				T_a = T.atts.get(a);



				// T_a(x,y) -> T_v(x) /\ T_w(y)

				Ty w = F.dst.atts.get(a).second;

				BinRelMap<Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>

				T_w = T.tys.get(w);

				for (Pair<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>> xy : T_a) {

					Lineage<Void, En2, Void, Fk2, Void, Gen, Void> x = xy.first;

					Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>> y = xy.second;

					if (!T_v.containsKey(x)) {

						changed[0] = changed[0] | toAdd.ens.get(v).add(x, x);

					}

					if (!T_w.containsKey(y)) {

						changed[0] = changed[0] | toAdd.tys.get(w).add(y, y);

					}

				}

			}

		}

	}



	public void makeArrowsTotal(Content toAdd, Boolean[] changed) {

		// a : v -> w

		for (En2 v : F.dst.ens) {

			BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Void, En2, Void, Fk2, Void, Gen, Void>> T_v = T.ens

					.get(v);

			BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Void, En2, Void, Fk2, Void, Gen, Void>> 

			T_v = T.ens.get(v);

			for (Fk2 a : F.dst.fksFrom(v)) {



				// T_v(x) -> Ey. T_a(x,y)
@@ -458,8 +583,26 @@ public class Chase<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk, X, Y> { 
					}

				}

			}

		}

		

		for (En2 v : F.dst.ens) {

			BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Lineage<Void, En2, Void, Fk2, Void, Gen, Void>> 

			T_v = T.ens.get(v);

			for (Att2 a : F.dst.attsFrom(v)) {



				// T_v(x) -> Ey. T_a(x,y)

				BinRelMap<Lineage<Void, En2, Void, Fk2, Void, Gen, Void>, Chc<Integer, Term<Ty, En1, Sym, Fk1, Att1, Gen, Sk>>>

				T_a = T.atts.get(a);

				for (Lineage<Void, En2, Void, Fk2, Void, Gen, Void> x : T_v.keySet()) {

					if (T_a.get(x) == null || T_a.get(x).isEmpty()) { // latter should be impossible

						toAdd.atts.get(a).add(x, Chc.inLeft(fresh.next()));

						changed[0] = true;

					}

				}

			}

		}

		

		

	}



}

src/catdata/aql/Query.java

+7 −3
Changes for src/catdata/aql/Query.java: 7 added lines, 3 removed lines.
Original line number Diff line number Diff line
@@ -541,7 +541,7 @@ public final class Query<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2> implements Sem 
		public final Ctx<Var, En1> gens;

		public final Collection<Eq<Ty, En1, Sym, Fk1, Att1, Var, Void>> eqs;

		public final Schema<Ty, En1, Sym, Fk1, Att1> schema;

		private final DP<Ty, En1, Sym, Fk1, Att1, Var, Void> dp;

		private  DP<Ty, En1, Sym, Fk1, Att1, Var, Void> dp;

		public final AqlOptions options;



		public Frozen(Ctx<Var, En1> gens, Collection<Eq<Ty, En1, Sym, Fk1, Att1, Var, Void>> eqs,
@@ -580,7 +580,11 @@ public final class Query<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2> implements Sem 
		}



		@Override

		public DP<Ty, En1, Sym, Fk1, Att1, Var, Void> dp() {

		public synchronized DP<Ty, En1, Sym, Fk1, Att1, Var, Void> dp() {

			if (dp == null) {

				dp = AqlProver.create(options, collage(), schema.typeSide.js);

				return dp;

			}

			return dp;

		}
@@ -591,7 +595,7 @@ public final class Query<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2> implements Sem 
			if (hidden != null) {

				return hidden;

			}

			hidden = new InitialAlgebra<>(dp, schema, collage(), new It(), x -> x.toString(), x -> x.toString());

			hidden = new InitialAlgebra<>(dp(), schema, collage(), new It(), x -> x.toString(), x -> x.toString());

			return hidden;

		}

src/catdata/aql/exp/AqlParser.java

+1 −1
Changes for src/catdata/aql/exp/AqlParser.java: 1 added line, 1 removed line.
Original line number Diff line number Diff line
@@ -28,7 +28,7 @@ public abstract class AqlParser { 
			"command", "graph", "exec_jdbc", "exec_js", "exec_cmdline", "literal", "add_to_classpath", 

			"identity", "match", "attributes", "empty", "imports", "types", "constants", "functions", "equations",

			"forall", "java_types", "multi_equations",

			"toQuery", "toCoQuery", "anonymize",

			"toQuery", "toCoQuery", "anonymize", "frozen", 

			"java_constants", "java_functions", "options", "entities", "src", "unique", "dst", "path_equations",

			"observation_equations", "generators", "rename", "remove", "modify",

			"foreign_keys", "lambda", "sigma", "delta", "pi", "unit", "counit", "eval", "coeval", "ed", "chase", "from",