Commit 3db29760 authored by Ryan Wisnesky's avatar Ryan Wisnesky
Browse files

add record linkage finder

parent bff8c851
......@@ -280,8 +280,6 @@ All schemas are ``on'' a typeside, and contain entities, foreign keys, attribute
\section{{\tt empty : <typeside>}}
The empty {\tt schema} with no entities, foreign keys, or attributes, on a particular {\tt typeside}.
\section{{\tt id <schema>}}
The identity mapping on a schema.
\section{{\tt schemaOf <instance>}}
The {\tt schema} of an {\tt instance}.
......@@ -327,7 +325,7 @@ Gets the schema associated with a colimit of schemas.
A schema mapping $F : S \to T$ takes entities in $S$ to entities in $T$, foreign keys in $S$ to paths in $T$, and attributes in $S$ to terms in $T$, in a way that is functorial: if $f : s \to s'$ is a symbol in $S$, then it must be that $F(f) : F(s) \to F(s')$. In addition, if $\forall \Gamma . e = e'$ is provable in $S$, then $\forall F(\Gamma). F(e) = F(e')$ must be provable in $T$.
\section{{\tt id <schema>}}
\section{{\tt identity <schema>}}
The identity schema mapping on a particular schema.
\section{{\tt [<mapping> ; <mapping>]}}
......@@ -351,7 +349,7 @@ Allowable options are {\tt timeout} and {\tt dont\_validate\_unsafe}, which disa
\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]$.
\section{{\tt id <schema>}}
\section{{\tt identity <schema>}}
The identity query on a schema.
\section{{\tt toQuery <mapping>}}
......@@ -453,7 +451,7 @@ If $F : S \to T$ is a mapping and $I$ is an $S$-instance, then $\Sigma_F I$ is a
If $F : S \to T$ is a mapping and $I$ is an $S$-instance, then $\Pi_F I$ is a $T$-instance.
\section{{\tt sigma\_chase <mapping> <instance>}}
Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm. See {\tt chase\_style} option.
Like {\tt sigma}, but uses an alternative chase/left-kan extension based algorithm. See {\tt chase\_style} option. Require the input instance to have a free type algebra. Option {\tt timeout} is also supported.
\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$.
......@@ -498,6 +496,20 @@ Expects a list of (single) SQL commands inside a section. Each SQL query should
\section{{\tt quotient\_csv <instance>}}
Expects a list of filenames inside a section. Each file should have 2 columns, where each column has a generator from the input instance. The union of these files defines an equivalence relation and this expression quotients the input instance by this relation.
\section{{\tt quotient\_query <instance>}}
Expects a list of queries, on per entity, e.g.,
\begin{verbatim}
entity E -> {from x:X y:Y where x.a = y.b}
entity F -> {from x:X y:Y}
\end{verbatim}
each query should have no attributes and no foreign keys. The resulting matched pairs $(x,y)$ are treated
as equations for performing the quotient.
\subsection{{\tt options}}
Allowed are {\tt timeout}, {\tt prover} and related options, {\tt always\_reload}, and {\tt require\_consistency}.
\section{{\tt import\_jdbc\_all [jdbcclass] [jdbcuri]}}
Imports a SQL database onto an autogenerated AQL schema. The AQL schema will have one attribute per column in the input DB, and one foreign key per foreign key in the input DB, and equations capturing the input DB's foreign key constraints. The type side will have a single type, ``dom''. When the [jdbcclass] and [jdbcuri] are the empty string, their values will be determined by the {\tt jdbc\_default\_class} and {\tt jdbc\_default\_string} options. See also option {\tt import\_col\_seperator}.
......@@ -550,9 +562,9 @@ Allowable options are {\tt timeout}, {\tt prover} and related options, {\tt requ
\subsection{{\tt equations}}
A list of ground (non quantified) equations to quotient by. Allowable options are {\tt timeout}, {\tt prover} and related options, and {\tt require\_consistency}.
\section{{\tt chase <constraints> <instance> [number]}}
\section{{\tt chase <constraints> <instance>}}
Chases the input instance with the input constraints up to the given maximum number of iterations. If the chase succeeds, the result instance will satisfy the constraints. The options will be used for the construction of the intermediate instances during the chase process.
If the chase succeeds, the result instance will satisfy the constraints. The options will be used for the construction of the intermediate instances during the chase process.
\subsection{{\tt options}}
Allowable options are the same as for an instance.
......@@ -569,7 +581,7 @@ A {\tt ctx(<generator> | <labelled null> -> integer)}.
Allowable options are the same for literal instances, and {\tt random\_seed}.
\chapter{Kind {\tt transform}}
\section{{\tt id <instance>}}
\section{{\tt identity <instance>}}
%todo
The identity transform on an instance.
\section{{\tt [<transform> ; <transform>]}}
......@@ -681,7 +693,7 @@ Conservatively checks that an instance is consistent (e.g., does not prove $1=2$
\section{{\tt export\_csv\_instance <instance> [directory]}}
Exports an instance as CSV. The directory name will contain one file named $en.csv$ per entity $en$. The file for $en$ will be a CSV file with a header; the fields of the header will be an ID column name (specified using options), as well as any attributes and foreign keys whose domain is $en$. AQL rows that are not constants will be exported as nulls.
Exports an instance as CSV. The directory name will contain one file named $en.csv$ per entity $en$. The file for $en$ will be a CSV file with a header; the fields of the header will be an ID column name (specified using options), as well as any attributes and foreign keys whose domain is $en$. AQL values that are not constants will be exported as nulls.
\subsection{{\tt options}}
Allowed are {\tt timeout}, {\tt always\_reload}, {\tt csv} related options, and {\tt id\_column\_name}, and {\it start\_ids\_at}.
......@@ -790,7 +802,7 @@ Used with {\tt import\_jdbc\_all} to import no data (only schema).
When disabled, relaxes AQL's nominal typing discipline for colimit instances.
\section{{\tt allow\_java\_eqs\_unsafe = boolean}}
When enabled, allows arbitrary equations involving java typeside symbols.
When enabled, allows arbitrary equations involving java typeside symbols. Induces undefined behavior.
\section{{\tt dont\_validate\_unsafe = boolean}}
When enabled, mappings and transforms and queries are not checked to be equality-preserving. For a query, when true it also disables decision procedure construction for sub-queries.
......
......@@ -165,6 +165,7 @@ instance i17 = pi (identity s2) (empty : s2) { options prover = completion }
//quotient_jdbc -- see JDBC example
//quotient_csv -- see JDBC example (yes, JDBC example)
//import_csv -- See FinanceColim1 example
//quotient_query - see Link example
instance i13 = literal : s3 {
generators
......
//Record Linkage
schema S = literal : sql {
entities
Element
attributes
name1 name2 : Element -> String
num1 num2 : Element -> String
}
instance I = literal : S {
generators
e1 e2 e3 x y z d : Element
equations
e1.name1 = "H" e1.num1 = "1"
e2.name1 = "He" e2.num1 = "2"
e3.name1 = "Li" e3.num1 = "3"
x.name2 = "Hydrogen" x.num2 = "1"
y.name2 = "Helium" y.num2 = "2"
z.name2 = "Lithium" z.num2 = "3"
d.name2 = "Beryllium" d.num2 = "4"
}
instance J = quotient_query I {
entity Element -> {from a:Element b:Element where a.num1 = b.num2}
}
......@@ -76,7 +76,7 @@ public final class AqlOptions {
query_compose_use_incomplete,
import_as_theory,
import_null_on_err_unsafe,
import_joined,
//import_joined,
map_nulls_arbitrarily_unsafe,
jdbc_default_class,
jdbc_default_string,
......@@ -234,8 +234,8 @@ public final class AqlOptions {
return false;
case map_nulls_arbitrarily_unsafe:
return false;
case import_joined:
return true;
//case import_joined:
// return true;
case coproduct_allow_type_collisions_unsafe:
return false;
case coproduct_allow_entity_collisions_unsafe:
......@@ -412,8 +412,8 @@ public final class AqlOptions {
return op.getBoolean(map);
case map_nulls_arbitrarily_unsafe:
return op.getBoolean(map);
case import_joined:
return op.getBoolean(map);
//case import_joined:
//return op.getBoolean(map);
case coproduct_allow_type_collisions_unsafe:
return op.getBoolean(map);
case coproduct_allow_entity_collisions_unsafe:
......
......@@ -21,6 +21,11 @@ import catdata.graph.DAG;
public final class Schema<Ty, En, Sym, Fk, Att> implements Semantics {
public Schema<Ty, En, Sym, Void, Void> discretize() {
Schema<Ty, En, Sym, Fk, Att> x = new Schema<Ty, En, Sym, Fk, Att>(typeSide, ens, new HashMap<>(), new HashMap<>(), new HashSet<>(), dp, false);
return (Schema<Ty, En, Sym, Void, Void>) x;
}
@Override
public int size() {
return ens.size() + atts.size() + fks.size() + eqs.size();
......
......@@ -14,14 +14,15 @@ public abstract class AqlParser {
protected AqlParser() { }
public static AqlParser getParser() {
//todo: use fred's parser here?
return new CombinatorParser();
}
public static final String[] ops = new String[] { ",", ".", ";", ":", "{", "}", "(", ")", "=", "->", "@", "(*",
"*)", "+", "[", "]", "<-" };
public static final String[] res = new String[] { "sigma_chase", "entity", "md", "quotient_jdbc", "random", "sql",
public static final String[] res = new String[] {
"quotient_query",
"sigma_chase", "entity", "md", "quotient_jdbc", "random", "sql",
"chase", "check", "import_csv", "quotient_csv", "coproduct", "simple", "assert_consistent",
"coproduct_sigma", "coequalize", "html", "quotient", "entity_equations", "schema_colimit", "exists",
"constraints", "getMapping", "getSchema", "typeside", "schema", "mapping", "instance", "transform", "query",
......
......@@ -104,9 +104,6 @@ import catdata.aql.exp.TyExpRaw.Ty;
@SuppressWarnings("deprecation")
public class CombinatorParser extends AqlParser {
private static final Terminals RESERVED = Terminals.caseSensitive(ops, Util.union(res, opts));
private static final Parser<Void> IGNORED = Parsers
......@@ -132,6 +129,8 @@ public class CombinatorParser extends AqlParser {
// }
private static Parser<RawTerm> term() {
Reference<RawTerm> ref = Parser.newReference();
Parser<RawTerm> ann = Parsers.tuple(ident, token("@"), ident).map(x -> new RawTerm(x.a, x.c));
......@@ -305,7 +304,7 @@ public class CombinatorParser extends AqlParser {
options.between(token("{"), token("}")).optional())
.map(x -> new InstExpCoEval(x.b, x.c, x.d == null ? new LinkedList<>() : x.d));
Parser ret = Parsers.or(sigma_chase, l2, pi, frozen, instExpCsvQuot(), instExpJdbcQuot(), instExpCoProd(), instExpRand(),
Parser ret = Parsers.or(queryQuotientExpRaw(), sigma_chase, l2, pi, frozen, instExpCsvQuot(), instExpJdbcQuot(), instExpCoProd(), instExpRand(),
instExpCoEq(), instExpJdbcAll(), chase, instExpJdbc(), empty, instExpRaw(), var, sigma, delta, distinct,
eval, colimInstExp(), dom, anon, cod, instExpCsv(), coeval, parens(inst_ref), instExpQuotient());
......@@ -1029,6 +1028,24 @@ public class CombinatorParser extends AqlParser {
return ret;
}
private static Parser<InstExpQueryQuotient> queryQuotientExpRaw() {
Parser<Pair<List<catdata.Pair<LocStr, PreBlock>>, List<catdata.Pair<String, String>>>>
pa = Parsers.tuple( preblock(false).many(), options);
Parser<Tuple3<Token, InstExp<?, ?, ?, ?, ?, ?, ?, ?, ?>, Token>>
l = Parsers.tuple(token("quotient_query"), inst_ref.lazy(), token("{"));
/*
* List<Pair<LocStr, String>> params, SchExp<?, ?, ?, ?, ?> c, SchExp<?, ?, ?, ?, ?> d, List<LocStr> imports,
List<Pair<LocStr, PreBlock>> list, List<Pair<String, String>> options
*/
Parser<InstExpQueryQuotient> ret = Parsers.tuple(l, pa, token("}"))
.map(x -> new InstExpQueryQuotient(
x.a.b, x.b.a, x.b.b));
return ret;
}
private static Parser<QueryExpRaw> queryExpRaw() {
Parser<Pair<List<catdata.Pair<LocStr, String>>, List<catdata.Pair<LocStr, RawTerm>>>> q = Parsers.tuple(Parsers.tuple(token("params"), env(ident, ":")).map(x->x.b).optional(), Parsers.tuple(token("bindings"), env(term(), "=")).map(x->x.b).optional()) ;
......
......@@ -167,7 +167,7 @@ public abstract class InstExpImport<Handle, Q>
op = new AqlOptions(options, null, env.defaults);
import_as_theory = (boolean) op.getOrDefault(AqlOption.import_as_theory);
isJoined = (boolean) op.getOrDefault(AqlOption.import_joined);
isJoined =true; // (boolean) op.getOrDefault(AqlOption.import_joined);
idCol = (String) op.getOrDefault(AqlOption.id_column_name);
nullOnErr = (Boolean) op.getOrDefault(AqlOption.import_null_on_err_unsafe);
prepend_entity_on_ids = (Boolean) op.getOrDefault(AqlOption.prepend_entity_on_ids);
......@@ -248,9 +248,11 @@ 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);
return new SaturatedInstance<>(alg, alg, (Boolean) op.getOrDefault(AqlOption.require_consistency),
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);
//x.validate(); so don't trigger eqs
x.checkSatisfaction();
return x;
}
protected abstract String getHelpStr();
......
package catdata.aql.exp;
import java.util.Collection;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.stream.Collectors;
import java.util.Set;
import catdata.Chc;
import catdata.Ctx;
import catdata.Pair;
import catdata.Triple;
import catdata.Util;
import catdata.aql.AqlOptions;
import catdata.aql.AqlOptions.AqlOption;
import catdata.aql.Collage;
import catdata.aql.Eq;
import catdata.aql.Instance;
import catdata.aql.It;
import catdata.aql.It.ID;
import catdata.aql.Kind;
import catdata.aql.Query;
import catdata.aql.RawTerm;
import catdata.aql.Schema;
import catdata.aql.Term;
import catdata.aql.Var;
import catdata.aql.exp.AqlEnv;
import catdata.aql.exp.AqlTyping;
import catdata.aql.exp.InstExp;
import catdata.aql.exp.InstExpRaw.Gen;
import catdata.aql.exp.InstExpRaw.Sk;
import catdata.aql.exp.InteriorLabel;
import catdata.aql.exp.LocStr;
import catdata.aql.exp.QueryExpRaw;
import catdata.aql.exp.QueryExpRaw.Block;
import catdata.aql.exp.QueryExpRaw.PreBlock;
import catdata.aql.exp.QueryExpRaw.Trans;
import catdata.aql.exp.Raw;
import catdata.aql.exp.SchExp;
import catdata.aql.exp.SchExpRaw.Att;
import catdata.aql.exp.SchExpRaw.En;
import catdata.aql.exp.SchExpRaw.Fk;
import catdata.aql.exp.TyExpRaw.Sym;
import catdata.aql.exp.TyExpRaw.Ty;
import catdata.aql.fdm.EvalAlgebra.Row;
import catdata.aql.fdm.EvalInstance;
import catdata.aql.fdm.InitialAlgebra;
import catdata.aql.fdm.LiteralInstance;
public class InstExpQueryQuotient<X, Y>
extends InstExp<Ty,En,Sym,Fk,Att,Gen,Sk,ID,Chc<Sk, Pair<ID, Att>>> implements Raw {
public final InstExp<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> I;
public final Map<String, String> options;
public final Set<Block> queries;
public InstExpQueryQuotient(InstExp<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> i,
List<Pair<LocStr, PreBlock>> list,
List<Pair<String, String>> options) {
I = i;
this.options = Util.toMapSafely(options);
this.queries = Util.toSetSafely(list).stream().map(x -> new Block(x.second, x.first))
.collect(Collectors.toSet());
for (Pair<LocStr, PreBlock> p : list) {
List<InteriorLabel<Object>> f = new LinkedList<>();
f.add(new InteriorLabel<>("entities", p.second, p.first.loc, x -> p.first.str).conv());
raw.put(p.first.str, f);
}
for (Block b : queries) {
if (!b.atts.isEmpty()) {
throw new RuntimeException("Matcher should not have attributes");
}
if (!b.fks.isEmpty()) {
throw new RuntimeException("Matcher should not have attributes");
}
if (b.gens.size() != 2) {
throw new RuntimeException("Matcher should have two variables in from clause");
}
for (Pair<Var, En> s : b.gens) {
if (!s.second.equals(b.en)) {
throw new RuntimeException("Matchers from clause should have entity " + b.en.str);
}
}
}
}
private Ctx<String, List<InteriorLabel<Object>>> raw = new Ctx<>();
@Override
public Ctx<String, List<InteriorLabel<Object>>> raw() {
return raw;
}
@Override
public Map<String, String> options() {
return options;
}
@Override
public SchExp<Ty, En, Sym, Fk, Att> type(AqlTyping G) {
return I.type(G);
}
@Override
public Instance<Ty, En, Sym, Fk, Att, Gen, Sk, ID, Chc<Sk, Pair<ID, Att>>> eval(AqlEnv env) {
Instance<Ty, En, Sym, Fk, Att, Gen, Sk, X, Y> I0 = I.eval(env);
Schema<Ty, En, Sym, Void, Void> dst = I0.schema().discretize();
Ctx<En, Triple<Ctx<Var, En>, Collection<Eq<Ty, En, Sym, Fk, Att, Var, Var>>, AqlOptions>> ens = new Ctx<>();
Ctx<En, Collage<Ty, En, Sym, Fk, Att, Var, Var>> cols = new Ctx<>();
for (Block b : queries) {
QueryExpRaw.processBlock(b.options, env, I0.schema(), ens, cols, b, new Ctx<>());
}
Query<Ty, En, Sym, Fk, Att, En, Void, Void> q = Query
.makeQuery(ens, new Ctx<>(), new Ctx<>(), I0.schema(), dst, true, false);
EvalInstance<Ty, En, Sym, Fk, Att, Gen, Sk, En, Void, Void, X, Y> J = new EvalInstance<>(q, I.eval(env), new AqlOptions(options, null, env.defaults));
Collage<Ty, En, Sym, Fk, Att, Gen, Sk> col = new Collage<>(I0.collage());
Set<Pair<Term<Ty, En, Sym, Fk, Att, Gen, Sk>, Term<Ty, En, Sym, Fk, Att, Gen, Sk>>>
eqs0 = new HashSet<>(I0.eqs());
AqlOptions strat = new AqlOptions(options, col, env.defaults);
for (Row<En, X> p : J.gens().keySet()) {
Map<Var, X> m = p.asMap();
List<Var> vs = new LinkedList<>(m.keySet());
Var v1 = vs.get(0);
Var v2 = vs.get(1);
X x1 = p.get(v1);
X x2 = p.get(v2);
Term<Void, En, Void, Fk, Void, Gen, Void> t1 = I0.algebra().repr(x1);
Term<Void, En, Void, Fk, Void, Gen, Void> t2 = I0.algebra().repr(x2);
eqs0.add(new Pair<>(t1.convert(), t2.convert()));
col.eqs.add(new Eq<>(new Ctx<>(), t1.convert(), t2.convert()));
}
InitialAlgebra<Ty, En, Sym, Fk, Att, Gen, Sk, ID> initial0 = new InitialAlgebra<>(strat, I0.schema(), col, new It(), Object::toString, Object::toString);
return new LiteralInstance<>(I0.schema(), col.gens.map, col.sks.map, eqs0, initial0.dp(), initial0, (Boolean) strat.getOrDefault(AqlOption.require_consistency), (Boolean) strat.getOrDefault(AqlOption.allow_java_eqs_unsafe));
}
private String toString;
@Override
public String toString() {
if (toString != null) {
return toString;
}
toString = "";
List<String> temp = new LinkedList<>();
if (!queries.isEmpty()) {
for (Block x : queries) {
temp.add(x.toString());
}
toString += "\n\t\t" + Util.sep(temp, "\n\n\t\t") + "\n";
}
if (!options.isEmpty()) {
toString += "\toptions";
temp = new LinkedList<>();
for (Entry<String, String> sym : options.entrySet()) {
temp.add(sym.getKey() + " = " + sym.getValue());
}
toString += "\n\t\t" + Util.sep(temp, "\n\t\t") + "\n";
}
toString = "quotient_query {\n" + toString + "}";
return toString;
}
@Override
public int hashCode() {
final int prime = 31;
int result = 1;
result = prime * result + ((I == null) ? 0 : I.hashCode());
result = prime * result + ((options == null) ? 0 : options.hashCode());
result = prime * result + ((queries == null) ? 0 : queries.hashCode());
return result;
}
@Override
public boolean equals(Object obj) {
if (this == obj)
return true;
if (obj == null)
return false;
if (getClass() != obj.getClass())
return false;
InstExpQueryQuotient other = (InstExpQueryQuotient) obj;
if (I == null) {
if (other.I != null)
return false;
} else if (!I.equals(other.I))
return false;
if (options == null) {
if (other.options != null)
return false;
} else if (!options.equals(other.options))
return false;
if (queries == null) {
if (other.queries != null)
return false;
} else if (!queries.equals(other.queries))
return false;
return true;
}
@Override
public Collection<Pair<String, Kind>> deps() {
return I.deps();
}
}
......@@ -178,9 +178,13 @@ extends InstExp<Ty,En,Sym,Fk,Att,Pair<Integer,En>, Pair<Integer, Att>,Pair<Integ
};
return new SaturatedInstance
SaturatedInstance<Ty, En, Sym, Fk, Att, Pair<Integer, En>, Pair<Integer, Att>, Pair<Integer, En>, Pair<Integer, Att>> x = new SaturatedInstance
<Ty, En, Sym, Fk, Att, Pair<Integer,En>, Pair<Integer, Att>, Pair<Integer,En>, Pair<Integer, Att>>
(alg, dp, false, true, false, new Ctx<>());
//x.validate();
x.checkSatisfaction();
return x;
}
......
......@@ -30,7 +30,9 @@ extends Instance<Ty, En1, Sym, Fk1, Att1, Pair<En1, X>, Y, Pair<En1, X>, Y>
I = i;
alg = new DeltaAlgebra<>(F, I.algebra());
J = new SaturatedInstance<>(alg, dp(), I.requireConsistency(), I.allowUnsafeJava(), false, null);
validate();
if (J.size() < 16 * 1024) {
validate();
}
}
@Override
......
......@@ -68,7 +68,7 @@ public class EvalAlgebra<Ty, En1, Sym, Fk1, Att1, Gen, Sk, En2, Fk2, Att2, X, Y>
if (r.en2 != null) {
return map;
}
map.put(v, x);
map.put(r.v, r.x);
r = r.tail;
}
}
......
......@@ -292,7 +292,7 @@ extends Instance<Ty, En, Sym, Fk, Att, X, Y, X, Y> {
}
}
private void checkSatisfaction() {
public void checkSatisfaction() {
for (Triple<Pair<Var, En>, Term<Ty, En, Sym, Fk, Att, Void, Void>, Term<Ty, En, Sym, Fk, Att, Void, Void>> eq : schema().eqs) {
for (X x : algebra().en(eq.first.second)) {
Term<Ty, En, Sym, Fk, Att, X, Y> lhs = eq.second.mapGenSk(Util.<X>voidFn(), Util.<Y>voidFn()).subst(Util.singMap0(eq.first.first, Term.Gen(x)));
......
......@@ -123,7 +123,7 @@ class LeftKan {
if (s.second.equals(y)) {
it.remove();
l.add(new Pair<>(s.first, x));
}
}
}
a.addAll(l);
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment