← All examples

example NewDemo

options
	require_consistency=false
	dont_validate_unsafe=true
	always_reload=true
	timeout = 60
#		prover=monoidal 
		

typeside Ty = literal {
	external_types
		Integer -> "java.lang.Integer"
		Float -> "java.math.BigDecimal"
		String -> "java.lang.String"
	external_parsers 
		Float -> "x => java.math.BigDecimal.valueOf(java.lang.Double.parseDouble(x))"
		Integer -> "x => java.lang.Integer.parseInt(x)"
		String -> "x => x"
	external_functions
		"+" : Float,Float->Float = "(x, y) => x.add(y)"	
		"*" : Float,Float->Float = "(x, y) => x.multiply(y)"	
		"-" : Float,Float->Float = "(x, y) => x.subtract(y)"	
		"/" : Float,Float->Float = "(x, y) => x.divide(y)"	
		"MAX" : Float,Float->Float = "(x, y) => x.max(y)"
		"MIN" : Float,Float->Float = "(x, y) => x.min(y)"		
	equations
		
}		

#schema S1 = importFromJDBC <url>
schema Olog1Schema = literal : Ty {
	entity Patient
	attributes ID first_name last_name birthdate create_date : String

	entity Visit
	attributes ID patient_id visit_date : String

	entity Observation
	attributes ID visit_id clinician_id obs_type observation : String
}
constraints Olog1Constraints = literal : Olog1Schema {
	forall x y : Observation where x.ID = y.ID -> where x = y
	forall x y : Visit where x.ID = y.ID -> where x = y
	forall x y : Patient where x.ID = y.ID -> where x = y
	forall x : Observation -> exists y : Visit where x.visit_id = y.ID
	forall x : Visit -> exists y : Patient where x.patient_id = y.ID
}
schema Olog2Schema = literal : Ty {
	entity Prescription
	attributes ID patient_id date details : String

	entity Patient 
	attributes ID fname lname dob : String

	entity Observation
	attributes ID patient_id clinician_id obs_type obs_date observation : String
}
constraints Olog2Constraints = literal : Olog2Schema {
	forall x y : Observation where x.ID = y.ID -> where x = y
	forall x y : Prescription where x.ID = y.ID -> where x = y
	forall x y : Patient where x.ID = y.ID -> where x = y
	forall x : Prescription -> exists y : Patient where x.patient_id = y.ID
	forall x : Observation -> exists y : Patient where x.patient_id = y.ID
}
#instance O1 = importJdbc <url>
instance Olog1Data = literal : Olog1Schema {
	generators
		p1 p2 p3 : Patient
		v1 v2 v3 : Visit
		o1 o2 o3 : Observation
	equations
		p1.ID = 937189 p1.first_name = john p1.last_name = doe 
		p1.birthdate = 340465020 p1.create_date = 1187438212 	
		p2.ID = 937190 p2.first_name = amrit p2.last_name = kumar 
		p2.birthdate = 246222505 p2.create_date = 1187444008
		p3.ID = 937191 p3.first_name = alexandra p3.last_name = grant 
		p3.birthdate = 121408849 p3.create_date = 1187445155 	

		v1.ID = 1237827 v1.patient_id = 937189 v1.visit_date = 1187438212
		v2.ID = 1237828 v2.patient_id = 937190 v2.visit_date = 1187444008
		v3.ID = 1237829 v3.patient_id = 937191 v3.visit_date = 1187445155

		o1.ID = 487298329 o1.visit_id = 1237827 o1.clinician_id = 562 
		o1.obs_type = HR o1.observation = 114
		o2.ID = 487298330 o2.visit_id = 1237827 o2.clinician_id = 562 
		o2.obs_type = WT o2.observation = 180
		o3.ID = 487298331 o3.visit_id = 1237827 o3.clinician_id = 562 
		o3.obs_type = BP o3.observation = "130/82"
}

instance Olog2Data = literal : Olog2Schema {
generators
		p1 p2 p3 : Patient
		v1 v2 v3 : Prescription
		o1 o2 o3 : Observation
	equations
		p1.ID = 25234 p1.fname = alexandra p1.lname = grant 
		p1.dob = 121408849
		p2.ID = 25235 p2.fname = vincent p2.lname = "von hoff" 
		p2.dob = 409235232
		p3.ID = 25236 p3.fname = brian p3.lname = tsai 
		p3.dob = 380665171 	

		v1.ID = 675345 v1.patient_id = 25234 v1.date = 1639676732
		v1.details = Enalapril
		v2.ID = 675346 v2.patient_id = 25234 v2.date = 1639696544
		v2.details = chlorothiazide
		v3.ID = 675347 v3.patient_id = 25235 v3.date = 1639704522
		v3.details = lisinopril

		o1.ID = 154298449 o1.patient_id = 25234 o1.clinician_id = 132 
		o1.obs_type = HR o1.obs_date = 1639676732 o1.observation=116
		o2.ID = 154298450 o2.patient_id = 25234 o2.clinician_id = 132 
		o2.obs_type = WT o2.obs_date = 1639676732 o2.observation=220
		o3.ID = 154298451 o3.patient_id = 25234 o3.clinician_id = 132 
		o3.obs_type = BP o3.obs_date = 1639676732 o3.observation="132/82"

}
command check1 = check Olog1Constraints Olog1Data
command check2 = check Olog2Constraints Olog2Data

schema_colimit C = quotient Olog1Schema + Olog2Schema : Ty {
	entity_equations
		Olog1Schema.Patient = Olog2Schema.Patient
		Olog1Schema.Observation = Olog2Schema.Observation
	observation_equations
		forall x.     x.first_name = x.fname #x.first_name = uppercase(x.fname)
		forall x.     x.last_name = x.lname 
		forall x.     x.birthdate = x.dob #x.bd = x.dob+1
		forall x.     x.Olog1Schema_Observation_observation = x.Olog2Schema_Observation_observation
		forall x.     x.Olog1Schema_Observation_ID = x.Olog2Schema_Observation_ID
		forall x.     x.Olog1Schema_Observation_clinician_id = x.Olog2Schema_Observation_clinician_id  
		forall x.     x.Olog1Schema_Observation_obs_type = x.Olog2Schema_Observation_obs_type
}

schema_colimit D = simplify C

instance Olog1DataFwd = sigma (getMapping D Olog1Schema) Olog1Data
instance Olog2DataFwd = sigma (getMapping D Olog2Schema) Olog2Data

constraints Olog1ConstraintsFwd = sigma (getMapping D Olog1Schema) Olog1Constraints
constraints Olog2ConstraintsFwd = sigma (getMapping D Olog2Schema) Olog2Constraints

instance CoProd = coproduct Olog1DataFwd + Olog2DataFwd  : getSchema D

constraints Rules = literal : getSchema D {
	imports Olog1ConstraintsFwd Olog2ConstraintsFwd	
	
	forall x y : Patient where x.first_name=y.first_name x.last_name=y.last_name 
	-> where x=y

	forall x y : Observation where x.obs_date = y.obs_date 
	 -> where x.visit_id = y.visit_id

	forall x y : Observation where x.visit_id = y.visit_id
	 -> where x.patient_id = y.patient_id

	
	forall x : Observation y : Visit z : Patient z2 : Patient 
		where x.visit_id = y.ID z.ID = y.patient_id  x.patient_id = z2.Olog2Schema_Patient_ID 
	 -> where z = z2

	forall x y : Observation where x.visit_id = y.visit_id 
	-> where x.obs_date = y.obs_date 

	forall x : Observation y : Visit where x.visit_id = y.ID 
	-> where y.visit_date = x.obs_date
}

instance Colim = chase Rules CoProd

instance Olog1DataBkwd = delta (getMapping D Olog1Schema) Colim
instance Olog2DataBkwd = delta (getMapping D Olog2Schema) Colim

instance CoProd

Observation
IDobs_dateclinician_idvisit_idobs_typeobservationIDpatient_id
0?05621237827HR114487298329?1
1?25621237827WT180487298330?3
2?45621237827BP130/82487298331?5
31639676732132?6HR11615429844925234
41639676732132?7WT22015429845025234
51639676732132?8BP132/8215429845125234
Patient
IDIDfirst_namebirthdatelast_nameOlog2Schema_Patient_IDcreate_date
6937189john340465020doe?91187438212
7937190amrit246222505kumar?101187444008
8937191alexandra121408849grant?111187445155
9?12alexandra121408849grant25234?13
10?14vincent409235232von hoff25235?15
11?16brian380665171tsai25236?17
Prescription
IDpatient_idIDdetailsdate
1225234675345Enalapril1639676732
1325234675346chlorothiazide1639696544
1425235675347lisinopril1639704522
Visit
IDvisit_datepatient_idID
1511874382129371891237827
1611874440089371901237828
1711874451559371911237829


instance Colim

Observation
IDobs_dateclinician_idvisit_idobs_typeobservationIDpatient_id
01639676732132?0BP132/8215429845125234
11639676732132?0WT22015429845025234
21639676732132?0HR11615429844925234
311874382125621237827HR114487298329?1
411874382125621237827WT180487298330?1
511874382125621237827BP130/82487298331?1
Patient
IDIDfirst_namebirthdatelast_nameOlog2Schema_Patient_IDcreate_date
6937191alexandra121408849grant252341187445155
7937189john340465020doe?11187438212
8?2vincent409235232von hoff25235?3
9?4brian380665171tsai25236?5
10937190amrit246222505kumar?61187444008
Prescription
IDpatient_idIDdetailsdate
1125234675345Enalapril1639676732
1225234675346chlorothiazide1639696544
1325235675347lisinopril1639704522
Visit
IDvisit_datepatient_idID
141639676732937191?0
1511874382129371891237827
1611874440089371901237828
1711874451559371911237829


instance Olog1Data

Observation
IDIDvisit_idclinician_idobs_typeobservation
04872983291237827562HR114
14872983301237827562WT180
24872983311237827562BP130/82
Patient
IDIDfirst_namelast_namebirthdatecreate_date
3937189johndoe3404650201187438212
4937190amritkumar2462225051187444008
5937191alexandragrant1214088491187445155
Visit
IDIDpatient_idvisit_date
612378279371891187438212
712378289371901187444008
812378299371911187445155


instance Olog1DataBkwd

Observation
IDIDvisit_idclinician_idobs_typeobservation
0154298451?0132BP132/82
1154298450?0132WT220
2154298449?0132HR116
34872983291237827562HR114
44872983301237827562WT180
54872983311237827562BP130/82
Patient
IDIDfirst_namelast_namebirthdatecreate_date
6937191alexandragrant1214088491187445155
7937189johndoe3404650201187438212
8?1vincentvon hoff409235232?2
9?3briantsai380665171?4
10937190amritkumar2462225051187444008
Visit
IDIDpatient_idvisit_date
11?09371911639676732
1212378279371891187438212
1312378289371901187444008
1412378299371911187445155


instance Olog1DataFwd

Observation
IDobs_dateclinician_idvisit_idobs_typeobservationIDpatient_id
0?05621237827HR114487298329?1
1?25621237827WT180487298330?3
2?45621237827BP130/82487298331?5
Patient
IDIDfirst_namebirthdatelast_nameOlog2Schema_Patient_IDcreate_date
3937189john340465020doe?61187438212
4937190amrit246222505kumar?71187444008
5937191alexandra121408849grant?81187445155
Prescription
IDpatient_idIDdetailsdate
Visit
IDvisit_datepatient_idID
611874382129371891237827
711874440089371901237828
811874451559371911237829


instance Olog2Data

Observation
IDIDpatient_idclinician_idobs_typeobs_dateobservation
015429844925234132HR1639676732116
115429845025234132WT1639676732220
215429845125234132BP1639676732132/82
Patient
IDIDfnamelnamedob
325234alexandragrant121408849
425235vincentvon hoff409235232
525236briantsai380665171
Prescription
IDIDpatient_iddatedetails
6675345252341639676732Enalapril
7675346252341639696544chlorothiazide
8675347252351639704522lisinopril


instance Olog2DataBkwd

Observation
IDIDpatient_idclinician_idobs_typeobs_dateobservation
015429845125234132BP1639676732132/82
115429845025234132WT1639676732220
215429844925234132HR1639676732116
3487298329?0562HR1187438212114
4487298330?0562WT1187438212180
5487298331?0562BP1187438212130/82
Patient
IDIDfnamelnamedob
625234alexandragrant121408849
7?0johndoe340465020
825235vincentvon hoff409235232
925236briantsai380665171
10?1amritkumar246222505
Prescription
IDIDpatient_iddatedetails
11675345252341639676732Enalapril
12675346252341639696544chlorothiazide
13675347252351639704522lisinopril


instance Olog2DataFwd

Observation
IDobs_dateclinician_idvisit_idobs_typeobservationIDpatient_id
01639676732132?0HR11615429844925234
11639676732132?1WT22015429845025234
21639676732132?2BP132/8215429845125234
Patient
IDIDfirst_namebirthdatelast_nameOlog2Schema_Patient_IDcreate_date
3?3alexandra121408849grant25234?4
4?5vincent409235232von hoff25235?6
5?7brian380665171tsai25236?8
Prescription
IDpatient_idIDdetailsdate
625234675345Enalapril1639676732
725234675346chlorothiazide1639696544
825235675347lisinopril1639704522
Visit
IDvisit_datepatient_idID


command check1

Satisfied

command check2

Satisfied