small fixes and tweaks

resources/examples/aql/Meta.aql

+
+
 schema cat = literal : empty {
 	entities
 		Ob Mor Pair
@@ -122,3 +124,13 @@ constraints moreEDs = literal : AQLinstance {
  	exists unique value:fkCell
  	where value.col=m value.row=r
 }
+
+/*
+For given AQL schemas X and Y, there may be no AQL schema MapXY such that MapXY-Inst ~ AQL mappings X -> Y.  Rather, the mappings X -> Y are isomorphic to the transforms X* => Y*, where X* and Y* are the Schema instances associated to X and Y. 
+
+But, there is an AQL schema Mapping := AQLSchema * Arrow such that Mapping-Inst ~ all AQL mappings of any type.
+
+Question: are the set of AQL transforms I => J given by the transforms I* => J*, where I* and J* are the Instance instances associated to I and J?
+
+Question: Is there an AQL schema Transform := AQLInstance * Arrow such that TransformInst ~ all AQL transforms of any type.  Or should be an instance?  Or nothing at all?
+*/
\ No newline at end of file

src/main/java/catdata/aql/Algebra.java

@@ -40,9 +40,14 @@ public abstract class Algebra<Ty,En,Sym,Fk,Att,Gen,Sk,X,Y> /* implements DP<Ty,E
 		return talg().eqs.isEmpty();
 	} */
 	
-	public abstract boolean hasFreeTypeAlgebraOnJava(); /* {
-		return talg().eqs.stream().filter(x -> talg().java_tys.containsKey(talg().type(x.ctx, x.lhs).l)).collect(Collectors.toList()).isEmpty();
-	} */
+	public boolean hasFreeTypeAlgebraOnJava() {
+		for (Eq<Ty, Void, Sym, Void, Void, Void, Y> eq : talg().eqs) {
+			if (schema().typeSide.js.java_tys.containsKey(talg().type(eq.ctx, eq.lhs).l)) {
+				return false;
+			}
+		}
+		return true;
+	}
 	
 	/**
 	 * The Xs need be to be unique across ens, so that repr can invert.  Is it worth checking this? TODO aql

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

@@ -8,6 +8,7 @@ import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.Function;
 
 import catdata.Chc;
 import catdata.Ctx;
@@ -121,35 +122,34 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> {
 
 			@Override
 			public String toStringProver() {
-				return "Pivot prover";
+				return "Pivot prover (sch)";
 			}
 
 			@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);
+				Var v = Util.get0(ctx.keySet());
+				En en = ctx.get(v).r;
+
+				return I.dp().eq(new Ctx<>(), trans(en, lhs), trans(en, rhs));
 			}
 			
 		};
 		
-		
-		
 		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());
 		
-		
-		
 		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";
+				return "Pivot prover (inst)";
 			}
 
 			@Override
@@ -174,7 +174,36 @@ public class AqlPivot<Ty, En0, Sym, Fk0, Att0, Gen, Sk, X, Y> {
 				(Boolean) strat.getOrDefault(AqlOption.allow_java_eqs_unsafe));
 		
 		J.validate();
+	}
 
+	private Term<Void, En0, Void, Fk0, Void, Gen, Void> trans1(En en, Term<Void, En, Void, Fk, Void, Void, Void> t) {
+		if (t.gen != null) {
+			return Util.abort(t.gen);
+		} else if (t.var != null) {
+			return I.algebra().repr((X)en.str);
+		} else if (t.fk != null) {
+			Term<Void, En0, Void, Fk0, Void, Gen, Void> x = trans1(en, t.arg);
+			return Term.Fk((Fk0) new Fk(t.fk.en, t.fk.str), x); //TODO check
+		} 
+		return Util.anomaly();
+	}
+	
+	private Term<Ty, En0, Sym, Fk0, Att0, Gen, Sk> trans(En en, Term<Ty, En, Sym, Fk, Att, Void, Void> t) {
+		if (t.obj != null) {
+			return Term.Obj(t.obj, t.ty);
+		} else if (t.sym != null) {
+			List<Term<Ty, En0, Sym, Fk0, Att0, Gen, Sk>> l = new LinkedList<>();
+			for (Term<Ty, En, Sym, Fk, Att, Void, Void> s : t.args) {
+				l.add(trans(en, s));
+			}
+			return Term.Sym(t.sym, l);
+		} else if (t.sk != null) {
+			return Util.abort(t.sk);
+		} else if (t.att != null) {
+			Term<Void, En0, Void, Fk0, Void, Gen, Void> x = trans1(en, t.arg.asArgForAtt());
+			return Term.Att((Att0)new Att(t.att.en,t.att.str), x.map(Util::abort, Util::abort, Function.identity(), Util::abort, Function.identity(), Util::abort));
+		} 
+		return Util.anomaly();
 	}
 
 	private X bar(Term<Void, En0, Void, Fk0, Void, Gen, Void> t) {

src/main/java/catdata/aql/AqlProver.java

@@ -110,7 +110,7 @@ public class AqlProver {
 		for (Eq<Ty, En, Sym, 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)) {
+			} else if (size(eq.lhs) > size(eq.rhs) && numOccs(eq.lhs, eq.rhs) ) {
 				ret.eqs.add(eq);
 			} else {
 				throw new RuntimeException("Cannot orient " + eq + " in a size reducing manner.");
@@ -120,6 +120,16 @@ public class AqlProver {
 		return ret;
 	}
 
+	private static <Ty, En, Sym, Fk, Att, Gen, Sk> boolean numOccs(Term<Ty, En, Sym, Fk, Att, Gen, Sk> lhs, Term<Ty, En, Sym, Fk, Att, Gen, Sk> rhs) {
+		for (Var v : lhs.vars()) {
+			if (!(lhs.vars().stream().filter((x)->x.equals(v)).count() >=
+			    rhs.vars().stream().filter((x)->x.equals(v)).count())) {
+				return false;
+			}
+		}
+		return true;
+	}
+
 	private static <Ty, En, Sym, Fk, Att, Gen, Sk> int size(Term<Ty, En, Sym, Fk, Att, Gen, Sk> e) {
 		if (e.obj != null || e.gen != null || e.sk != null || e.var != null) {
 			return 1;

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

@@ -195,9 +195,5 @@ public class ImportAlgebra<Ty, En, Sym, Fk, Att, X, Y> extends Algebra<Ty, En, S
 		return talg.eqs.isEmpty();
 	}
 
-	@Override
-	public boolean hasFreeTypeAlgebraOnJava() {
-		return talg.eqs.isEmpty(); // TODO aql guess
-	}
 
 }

src/main/java/catdata/aql/Instance.java

@@ -108,6 +108,10 @@ public abstract class Instance<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> implements S
 		if (!allowUnsafeJava() && !algebra().hasFreeTypeAlgebraOnJava()) {
 			throw new RuntimeException("Unsafe use of java - AQL's behavior is undefined.  Possible solution: add allow_java_eqs_unsafe=true, change the equations, or contact support at info@catinf.com.  Type algebra is\n\n" + algebra().talg());
 		}
+		//reasoning will be incomplete, but if enabled we can't e.g., import into a java typeside with fns
+		//if (schema().typeSide.hasImplicitJavaEqs()) {
+		//	return false;
+		//}
 		
 		
 	}

src/main/java/catdata/aql/Term.java

@@ -859,7 +859,7 @@ public final class Term<Ty, En, Sym, Fk, Att, Gen, Sk> {
 	}
 
 
-	public Set<Var> vars() {
+	public List<Var> vars() {
 		return toKB().vars();
 	} 
 	

src/main/java/catdata/aql/TypeSide.java

@@ -18,8 +18,6 @@ import catdata.aql.AqlOptions.AqlOption;
 
 public class TypeSide<Ty, Sym> implements Semantics {
 	
-	
-	
 	@Override
 	public int size() {
 		return tys.size() + syms.size() + eqs.size();

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

@@ -272,7 +272,7 @@ public class InstExpCsv
 				String zz = mediate.apply(att.convert());
 				if (!m.containsKey(zz)) {
 					throw new RuntimeException("No column " + att + " in file for " + en + " nor explicit mapping for "
-							+ att + " given. Tried " + zz + " and options are " + m.keySet());
+							+ att + " given. Tried " + zz + " and options are " + Util.alphabetical(m.keySet()));
 				}
 				int z = m.get(zz);
 				if (z >= row.length) {

src/main/java/catdata/aql/fdm/SigmaChaseAlgebra.java

@@ -47,9 +47,10 @@ public class SigmaChaseAlgebra<Ty, En1, Sym, Fk1, Att1, En2, Fk2, Att2, Gen, Sk,
 		if (!X.algebra().talg().eqs.isEmpty()) {
 			throw new RuntimeException("Chase cannot be used: type algebra of input instance is not necessarily free");
 		}
-		if (X.schema().typeSide.hasImplicitJavaEqs()) {
+		//if (X.schema().typeSide.hasImplicitJavaEqs()) {
+		// reasoning will be incomplete
 		//	throw new RuntimeException("Chase cannot be used: type algebra of input instance uses java functions");		
-		}
+		//}
 
 	
 		

src/main/java/catdata/provers/KBExp.java

@@ -67,11 +67,11 @@ public abstract class KBExp<C, V> {
 
 	public abstract KBApp<C, V> getApp();
 
-	private Set<V> vars = null;
+	private List<V> vars = null;
 
-	public Set<V> vars() {
+	public List<V> vars() {
 		if (vars == null) {
-			vars = new HashSet<>();
+			vars = new LinkedList<>();
 			vars(vars);
 		}
 		return vars;