add pivot

\subsection{{\tt options}}

Allowable options are {\tt timeout} and {\tt dont\_validate\_unsafe}, which disables checking that equations preserved.

\section{{\tt pivot <instance> <options>}}

Computes the schema mapping $pivot(I) \to I$.  

\chapter{Kind  {\tt query}}

A query $S \to T$ assigns to each entity $en$ in $S$ a (``frozen'') instance on $T$, which we will write as $[en]$, and to each foreign key $fk : e \to e'$ a transform $[fk] : [e'] \to [e]$ (note the reversal), and to each attribute $att : e \to \tau$ a term of type $\tau$ in context $[e]$.  

The expression ${\tt getMapping} \ C \ X$ gets the mapping $X \to C$ associated with schema $X$ in the colimit of schemas $C$.

\section{{\tt pivot <instance> <options>}}

Computes the 'schema of elements' for an instance $I$.  Each row in $I$ is an entity in $pivot(I)$.  

\chapter{Kind {\tt constraints}}

\section{{\tt literal : <schema>}}

Allowable options are the same as for an instance.

\section{{\tt pivot <instance> <options>}}

Computes the canonical instance $J$ associated with 'schema of elements' for an instance $I$.  Each row in $I$ is an entity in $pivot(I)$, and we have a mapping $pivot(I) : pivot(I) \to I$ as well.  This instance $J$ has the property that $\Sigma_{pivot(I)}(J)=I$.

\section{{\tt random : <schema>}}

Constructs a random instance with the specified number of generators per entity or type. Then for each generator $e:s$ and fk/att $f : s \to t$, it adds equation $f(e) = y$, where $y:t$ is a randomly selected generator (or no equation if t has no generators).

Interprets all equations $p = q$ as rewrite rules $p \to q$ regardless of termination behavior.  Can diverge.

\subsubsection{{\tt program\_allow\_nonconfluence\_unsafe}}

Interprets all equations $p = q$ as rewrite rules $p \to q$ regardless of confluence.  Can diverge.

\subsection{{\tt completion}}

Applies unfailing (ordered) Knuth-Bendix completion specialized to lexicographic path ordering.  If no completion precedence is given, attempts to infer a precedence using constraint-satisfaction techniques.

	public enum AqlOption {

		quotient_use_chase,

		chase_style,

		maedmax_allow_empty_sorts_unsafe,

		allow_empty_sorts_unsafe,

		maedmax_path,

		program_allow_nonconfluence_unsafe,

		gui_sample,

		gui_sample_size,

		import_dont_check_closure_unsafe,

	//@SuppressWarnings("static-method")

	private static Object getDefault(AqlOption option) {

		switch (option) {

		case program_allow_nonconfluence_unsafe:

			return false;

		case quotient_use_chase:

			return true;

		case jdbc_no_distinct_unsafe:

			return 16*1024;

		case maedmax_path:

			return "/home/ryan/maedmax/maedmax";

		case maedmax_allow_empty_sorts_unsafe:

		case allow_empty_sorts_unsafe:

			return false;

		case chase_style:

			return "parallel";

	private static Object getFromMap(Map<String, String> map, Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col, AqlOption op) {

		switch (op) {

		case program_allow_nonconfluence_unsafe:

			return op.getBoolean(map);

		case quotient_use_chase:

			return op.getBoolean(map);

		case jdbc_query_export_convert_type:

			return op.getInteger(map);

		case maedmax_path:

			return op.getString(map);

		case maedmax_allow_empty_sorts_unsafe:

		case allow_empty_sorts_unsafe:

			return op.getBoolean(map);

		case chase_style:

			return op.getString(map);

package catdata.aql;

import java.util.HashMap;

import java.util.HashSet;

import java.util.LinkedList;

import java.util.List;

import java.util.Map;

import java.util.Set;

import catdata.Chc;

import catdata.Ctx;

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;

public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> {

	public final Instance<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> I;

	public final Schema<Ty, En, Sym, Fk, Att> intI;

	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 AqlPivot(Instance<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> i, AqlOptions strat) {

		I = i;

		Set<En> ens = new HashSet<>();

		Map<Att, Pair<En, Ty>> atts = new HashMap<>();

		Map<Fk, Pair<En, En>> fks = new HashMap<>();

		Map<En, En0> ens0 = new HashMap<>();

		Map<Att, Triple<Var, En0, Term<Ty, En0, Sym, Fk0, Att0, Void, Void>>> atts0 = new HashMap<>();

		Map<Fk, Pair<En0, List<Fk0>>> fks0 = new HashMap<>();

		Set<Pair<Term<Ty, En, Sym, Fk, Att, X, Y>, Term<Ty, En, Sym, Fk, Att, X, Y>>> 

		eqs0 = new HashSet<>();

		Collage<Ty, En, Sym, Fk, Att, X, Y> col = new Collage<>();

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

		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));

				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));

					atts0.put(xxx, new Triple<>(new Var("x"), en, Term.Att(att, Term.Var(new Var("x")))));

					Term<Ty, En, Sym, Fk, Att, X, Y> 

					l = Term.Att(xxx, Term.Gen(x0));

					Term<Ty, En, Sym, Fk, Att, 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));

				}

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

					Fk xxx = new Fk(new En(x),fk.toString());

					fks.put(xxx, new Pair<>(new En(x), new En(I.algebra().fk(fk, x0).toString())));					

					fks0.put(xxx, new Pair<>(en,Util.singList(fk)));

					Term<Ty, En, Sym, Fk, Att, X, Y> 

					l = Term.Fk(xxx, Term.Gen(x0));

					Term<Ty, En, Sym, Fk, Att, 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));

				}

			}

		}

		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));

		}

		DP<Ty, En, Sym, Fk, Att, Void, Void> dp = 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, Void, Void> lhs,

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

				return lhs.equals(rhs);

			}

		};

		intI = new Schema<>(I.schema().typeSide, ens , atts, fks, new HashSet<>(), dp, 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,

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

				(Boolean) strat.getOrDefault(AqlOption.allow_java_eqs_unsafe));

		J.validate();

	}

	private X bar(Term<Void, En0, Void, Fk0, Void, Gen, Void> t) {

		if (t.gen != null) {

			return I.algebra().gen(t.gen);

		} else if (t.fk != null) {

			X x = bar(t.arg);

			return I.algebra().fk(t.fk, x);

		} 

		return Util.anomaly();

	}

	private Term<Ty, En, Sym, Fk, Att, X, Y> foo(Term<Ty, En0, Sym, Fk0, Att0, Gen, Sk> t) {

		if (t.obj != null) {

			return Term.Obj(t.obj, t.ty);

		} else if (t.sym != null) {

			List<Term<Ty, En, Sym, Fk, Att, X, Y>> l = new LinkedList<>();

			for (Term<Ty, En0, Sym, Fk0, Att0, Gen, Sk> s : t.args) {

				l.add(foo(s));

			}

			return Term.Sym(t.sym, l);

		} else if (t.sk != null) {

			return I.algebra().sk(t.sk).convert();

		} else if (t.att != null) {

			X x = bar(t.arg.convert());

			return Term.Att(new Att(new En(x.toString()),t.att.toString()), Term.Gen(x));

		} 

		return Util.anomaly();

	}

}

				return new KBtoDP<>(js, col1.simplify().second, new CongruenceProver<>(col1.simplify().first.toKB()));

			case program:

				boolean check   = !(Boolean) ops.getOrDefault(AqlOption.dont_verify_is_appropriate_for_prover_unsafe);

				boolean check2  = !(Boolean) ops.getOrDefault(AqlOption.program_allow_nonconfluence_unsafe);

				check = check && check2;

				boolean allowNonTerm = (Boolean) ops.getOrDefault(AqlOption.program_allow_nontermination_unsafe);

				try {

					if (!allowNonTerm) {

					throw new RuntimeException(ex.getMessage() + "\n\nPossible solution: add options program_allow_nontermination_unsafe=true, or prover=completion");

				}

				return new KBtoDP<>(js, col1.simplify().second, new ProgramProver<>(check, Var.it, col1.simplify().first.toKB())); // use																																																		

				//return new KBtoDP<>(js, col1.simplify().second, new ProgramProver<>(check, Var.it, col1.simplify().first.toKB())); // use																																																		

			case completion:

				return new KBtoDP<>(js, col1.simplify().second, new CompletionProver<>(col1.toKB().syms.keySet(), ops, col1.simplify().first));

			case monoidal:

				return new MonoidalFreeDP<>(js, col1.simplify().second, col1.simplify().first); // use																																					// simplified

			case maedmax:

				String exePath = (String) ops.getOrDefault(AqlOption.maedmax_path);

				Boolean b = (Boolean) ops.getOrDefault(AqlOption.maedmax_allow_empty_sorts_unsafe);

				Boolean b = (Boolean) ops.getOrDefault(AqlOption.allow_empty_sorts_unsafe);

				return new KBtoDP<>(js, col1.simplify().second, new MaedmaxProver<>(exePath, col1.simplify().first.toKB(), b, timeout)); // use																																																		

			default:

	//TODO aql validate instances against algebras

}