tweaks

// 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

}

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