Commit c20364f9 authored by Fred Eisele's avatar Fred Eisele
Browse files

Merge branch 'master' of https://github.com/CategoricalData/fql

parents 031f8b20 a4355c78
// Universal Warehousing Demo
// user defined functions, in Java
typeside Type = literal {
java_types
String = "java.lang.String"
java_constants
String = "return input[0]"
java_functions
toUpper : String -> String = "return input[0].toUpperCase()"
}
///////////////////////////////////////////////////////////////////////////
// input schemas
schema AmphibianSchema = literal : Type {
entities
Amphibian Animal
foreign_keys
toAnimal : Amphibian -> Animal
attributes
species : Animal -> String
}
// formalizes text from http://catinf.com/demo/WaterDB/schema.txt
schema LandSchema = literal : Type {
imports
AmphibianSchema
entities
LandAnimal
foreign_keys
isA : Amphibian -> LandAnimal
isA : LandAnimal -> Animal
path_equations
isA.isA = toAnimal
}
// formalizes text from http://catinf.com/demo/WaterDB/schema.txt
schema WaterSchema = literal : Type {
imports
AmphibianSchema
entities
WaterAnimal
foreign_keys
isA : Amphibian -> WaterAnimal
isA : WaterAnimal -> Animal
path_equations
isA.isA = toAnimal
}
///////////////////////////////////////////////////////////////////////////
//input instances
instance LandInstance = import_csv "http://catinf.com/demo/LandDB" : LandSchema
instance WaterInstance = import_csv "http://catinf.com/demo/WaterDB" : WaterSchema
///////////////////////////////////////////////////////////////////////////.....
//compute the canonical schema colimit, then enhances its semantics
schema_colimit UniversalWarehouseSchema = quotient LandSchema + WaterSchema : Type {
entity_equations
LandSchema.Animal = WaterSchema.Animal
LandSchema.Amphibian = WaterSchema.Amphibian
path_equations
LandSchema_Amphibian_toAnimal = WaterSchema_Amphibian_toAnimal
}
schema_colimit ModifiedWarehouseSchema = modify UniversalWarehouseSchema {
rename entities
LandSchema_Amphibian__WaterSchema_Amphibian -> Amphibian
LandSchema_Animal__WaterSchema_Animal -> Animal
LandSchema_LandAnimal -> Land
WaterSchema_WaterAnimal -> Water
rename foreign_keys
Amphibian.LandSchema_Amphibian_isA -> land_is
Amphibian.WaterSchema_Amphibian_isA -> water_is
Amphibian.WaterSchema_Amphibian_toAnimal -> redundantW
Amphibian.LandSchema_Amphibian_toAnimal -> redundantL
Water.WaterSchema_WaterAnimal_isA -> isA
Land.LandSchema_LandAnimal_isA -> isA
rename attributes
Animal.LandSchema_Animal_species -> land_species
Animal.WaterSchema_Animal_species -> water_species
remove foreign_keys
Amphibian.redundantL -> land_is . isA
Amphibian.redundantW -> water_is. isA
}
////////////////////////////////////////////////////////////////////////////////////////////////
// migrate the data onto the warehouse schema
schema WarehouseSchema = getSchema ModifiedWarehouseSchema
mapping LandToWarehouse = getMapping ModifiedWarehouseSchema LandSchema
mapping WaterToWarehouse = getMapping ModifiedWarehouseSchema WaterSchema
instance LandInstanceForward = sigma LandToWarehouse LandInstance
instance WaterInstanceForward = sigma WaterToWarehouse WaterInstance
instance UnmergedWarehouse = coproduct LandInstanceForward + WaterInstanceForward : WarehouseSchema
////////////////////////////////////////////////////////////////////////////////////////////////
// merge duplicates
instance Warehouse = quotient_query UnmergedWarehouse {
entity Amphibian -> {from a:Amphibian b:Amphibian where toUpper(a.land_is.isA.land_species) = toUpper(b.water_is.isA.water_species)}
}
////////////////////////////////////////////////////////////////////////////////////////////////
// export the warehouse to SQL
command storeWH = export_jdbc_instance Warehouse "" "" ""
//view exported SQL instance
command view1 = exec_jdbc "" "" {
"SELECT * FROM Animal"
"SELECT * FROM Amphibian"
"SELECT * FROM Land"
"SELECT * FROM Water"
"DROP TABLE Animal" //drop tables in case we want to run the demo again
"DROP TABLE Amphibian"
"DROP TABLE Land"
"DROP TABLE Water"
}
////////////////////////////////////////////////////////////////////////////////////////////////
// Application 0 : View warehouse as graph
schema WarehouseAsGraph = pivot Warehouse
////////////////////////////////////////////////////////////////////////////////////////////////
// Application 1 : Project (round-trip) the warehouse back onto the land schema
instance RoundTripLand = delta LandToWarehouse Warehouse
transform RoundTripLandFn = unit LandToWarehouse LandInstance
////////////////////////////////////////////////////////////////////////////////////////////////
// Application 2 : Project further onto the Amphibians schema with a query
query LandToAmphibians = literal : LandSchema -> AmphibianSchema {
entity Amphibian -> {from amp:Amphibian
//where amp.toAnimal.species = "frog"
foreign_keys toAnimal -> {anim -> amp.toAnimal}}
entity Animal -> {from anim:Animal
//where anim.species = "frog"
attributes species -> anim.species}
}
instance RoundTripAmphibians = eval LandToAmphibians RoundTripLand
////////////////////////////////////////////////////////////////////////////////////////////////
// Application 3 : Check and/or repair additional rules
constraints AllFksInjective = literal : WarehouseSchema {
forall a1 a2 : Amphibian where a1.land_is = a2.land_is -> where a1 = a2
forall a1 a2 : Amphibian where a1.water_is = a2.water_is -> where a1 = a2
forall l1 l2 : Land where l1.isA = l2.isA -> where l1 = l2
forall w1 w2 : Water where w1.isA = w2.isA -> where w1 = w2
}
command cmd = check AllFksInjective Warehouse
instance ANonInjectiveWarehouse = literal : WarehouseSchema {
generators
frog1 frog2 : Amphibian
frog : Land
equations
frog1.land_is = frog
frog2.land_is = frog
}
instance RepairedInjectiveWarehouse = chase AllFksInjective ANonInjectiveWarehouse
schema C = literal : sql {
entities
a1 a2 a3 b1 b2 c1 c2 c3 c4
foreign_keys
g1 : a1 -> b1
g2 : a2 -> b2
g3 : a3 -> b2
h1 : a1 -> c1
h2 : a2 -> c2
h3 : a3 -> c4
attributes
a1_str : a1 -> Varchar
a2_str : a2 -> Varchar
a3_str : a3 -> Varchar
b1_str : b1 -> Varchar
b2_str : b2 -> Varchar
c1_str : c1 -> Varchar
c2_str : c2 -> Varchar
c3_str : c3 -> Varchar
c4_str : c4 -> Varchar
}
schema D = literal : sql {
entities
A B C
foreign_keys
G : A -> B
H : A -> C
attributes
A_str : A -> Varchar
B_str : B -> Varchar
C_str : C -> Varchar
}
mapping F = literal : C -> D {
entity
a1 -> A
foreign_keys
h1 -> A.H
g1 -> A.G
attributes
a1_str -> A_str
entity
a2 -> A
foreign_keys
h2 -> A.H
g2 -> A.G
attributes
a2_str -> A_str
entity
a3 -> A
foreign_keys
g3 -> A.G
h3 -> A.H
attributes
a3_str -> A_str
entity
b1 -> B
attributes
b1_str -> B_str
entity
b2 -> B
attributes
b2_str -> B_str
entity
c1 -> C
attributes
c1_str -> C_str
entity
c2 -> C
attributes
c2_str -> C_str
entity
c3 -> C
attributes
c3_str -> C_str
entity
c4 -> C
attributes
c4_str -> C_str
}
instance I = random : C {
generators
a1 -> 10
a2 -> 10
a3 -> 10
b1 -> 10
b2 -> 10
c1 -> 10
c2 -> 10
c3 -> 10
c4 -> 10
//options
// random_seed = 2
}
instance J = sigma_chase F I
instance J2 = sigma F I
schema cat = literal : empty {
entities
Ob Mor Pair
foreign_keys
id: Ob -> Mor
dom: Mor -> Ob
cod: Mor -> Ob
fst: Pair -> Mor
snd: Pair -> Mor
comp: Pair -> Mor
path_equations
id.dom = Ob
id.cod = Ob
fst.dom = comp.dom
fst.cod = snd.dom
snd.cod = comp.cod
options
}
constraints theEDs = literal : cat {
//every composable pair gives a Pair
forall f g:Mor
where f.cod=g.dom ->
exists unique fg:Pair
where fg.fst=f fg.snd=g
//left unitality
forall fid:Pair
where fid.fst.cod.id = fid.snd
->
where fid.comp = fid.fst
//right unitality
forall idf:Pair
where idf.snd.dom.id = idf.fst
->
where idf.comp = idf.snd
//associativity
forall fg gh fgThenh fThengh: Pair
where
fg.snd = gh.fst
fgThenh.fst = fg.comp
fgThenh.snd = gh.snd
fThengh.fst = fg.fst
fThengh.snd = gh.comp
->
where fgThenh.comp = fThengh.comp
}
// You can make similar constraints on AQLschema.
schema AQLschema = literal : empty {
imports
cat
entities
StringAtt IntAtt
foreign_keys
on: StringAtt -> Ob
on: IntAtt -> Ob
}
instance mysch = literal : AQLschema {
generators
c d: Ob
f : Mor
name: StringAtt
equations
f.dom=c f.cod=d
name.on=c
}
typeside Ty = literal {
java_types
String = "java.lang.String"
Integer = "java.lang.Integer"
java_constants
String = "return input[0]"
Integer = "return java.lang.Integer.parseInt(input[0])"
java_functions
plus : Integer,Integer -> Integer = "return (input[0] + input[1]).intValue()"
}
schema AQLinstance = literal : Ty {
imports AQLschema
entities
recordID
StringCell
IntCell
fkCell
foreign_keys
col: IntCell -> IntAtt col: StringCell -> StringAtt
row: IntCell -> recordID row: StringCell -> recordID
inTable: recordID -> Ob
col: fkCell -> Mor
row : fkCell -> recordID
pointsTo: fkCell -> recordID
path_equations
//col.on = row.inTable // StringCell
//col.on = row.inTable // IntCell
col.dom = row.inTable // fkCell
//col.cod = row.pointsTo // fkCell
attributes
value : StringCell -> String
value : IntCell -> Integer
}
//add all constraints for categories + ...
constraints moreEDs = literal : AQLinstance {
imports theEDs
//string fields are nonempty and atomic (you can get rid of one or the other if you choose)
forall r:recordID sa:StringAtt
where r.inTable=sa.on ->
exists unique value:StringCell
where value.col=sa value.row=r
//int fields are nonempty and atomic
forall r:recordID sa:IntAtt
where r.inTable=sa.on ->
exists unique value:IntCell
where value.col=sa value.row=r
// fk fields are nonempty and atomic
forall r:recordID m:Mor
where r.inTable=m.dom ->
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
schema Net = literal : empty {
entities
Input Place Trans Output
foreign_keys
place : Input -> Place
trans : Input -> Trans
place : Output -> Place
trans : Output -> Trans
}
/*
* p1 ->t1-> p2 ->t2-> p3
*/
instance N = literal : Net {
generators
p1 p2 p3 : Place
t1 t2 : Trans
i1 i2 : Input
o1 o2 : Output
equations
i1.place = p1
i1.trans = t1
o1.trans = t1
o1.place = p2
i2.place = p2
i2.trans = t2
o2.trans = t2
o2.place = p3
options
interpret_as_algebra = true
}
/*
entities
i1 i2 o1 o2 p1 p2 p3 t1 t2
foreign_keys
trans : o2 -> t2
place : o2 -> p3
place : o1 -> p2
trans : o1 -> t1
trans : i2 -> t2
place : i2 -> p2
place : i1 -> p1
trans : i1 -> t1
*/
schema intN = pivot N
mapping proj = pivot N // intN -> Net
constraints injectivity = literal : Net {
forall x y : Input
where x.place = y.place -> where x = y
forall x y : Output
where x.trans = y.trans -> where x = y
}
///////////////////////////////////////////////////////////////
//example:
//this is an instance on intN and passes the injectivity check
instance I = literal : intN {
generators
token1time1 : p1
token1time2 : p2
token1time3 : p3
fire12 : t1
fire23 : t2
equations
options
interpret_as_algebra = true
}
instance J = sigma proj I // have J = N
command validate1 = check injectivity J
......@@ -31,7 +31,7 @@ command createCsvData = exec_js {
"Java.type(\"catdata.Util\").writeFile(\"eId,is\\n10,0\\n11,1\\n12,2\", \"/Users/ryan/Desktop/Employee.csv\")"
}
instance I0 = import_csv "/Users/ryan/Desktop/" : S0 {
instance I0 = import_csv "file:///Users/ryan/Desktop/" : S0 {
Employee -> {Employee -> eId eAsP -> is eSsn -> is}
//eId -> eId can be ommitted
......@@ -85,7 +85,7 @@ command createCsvData2 = exec_js {
"Java.type(\"catdata.Util\").writeFile(\"ssn,nameOf,Likes\\n0,a,a\\n1,b,\\\"a,b,d\\\"\\n2,c,\\\"\\\"\\n\", \"/Users/ryan/Desktop/Person.csv\")"
}
instance I = import_csv "/Users/ryan/Desktop/" : S {
instance I = import_csv "file:////Users/ryan/Desktop/" : S {
Person -> {
Person -> ssn
name -> nameOf
......
......@@ -12,7 +12,7 @@ public class Null<X> {
@Override
public String toString() {
return "lbl" + x ;
return x.toString() ;
}
@Override
......
......@@ -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
......
......@@ -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) {