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
Keywords:

typeside_literal
chase
constraints_literal
sigma
delta
schema_literal
instance_literal
check
simplify
quotient
coproduct
sigma

Options:




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 Olog2Data

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


instance Olog2DataFwd

Observation
IDpatient_idobs_dateobs_typeclinician_idIDvisit_idobservation
0252341639676732HR132154298449?0116
1252341639676732WT132154298450?1220
2252341639676732BP132154298451?2132/82
Patient
IDcreate_dateOlog2Schema_Patient_IDbirthdatelast_namefirst_nameID
3?325234121408849grantalexandra?4
4?525235409235232von hoffvincent?6
5?725236380665171tsaibrian?8
Prescription
IDIDdetailsdatepatient_id
6675345Enalapril163967673225234
7675346chlorothiazide163969654425234
8675347lisinopril163970452225235
Visit
IDIDpatient_idvisit_date


instance Olog1DataFwd

Observation
IDpatient_idobs_dateobs_typeclinician_idIDvisit_idobservation
0?0?1HR5624872983291237827114
1?2?3WT5624872983301237827180
2?4?5BP5624872983311237827130/82
Patient
IDcreate_dateOlog2Schema_Patient_IDbirthdatelast_namefirst_nameID
31187438212?6340465020doejohn937189
41187444008?7246222505kumaramrit937190
51187445155?8121408849grantalexandra937191
Prescription
IDIDdetailsdatepatient_id
Visit
IDIDpatient_idvisit_date
612378279371891187438212
712378289371901187444008
812378299371911187445155


instance CoProd

Observation
IDpatient_idobs_dateobs_typeclinician_idIDvisit_idobservation
0?0?1HR5624872983291237827114
1?2?3WT5624872983301237827180
2?4?5BP5624872983311237827130/82
3252341639676732HR132154298449?6116
4252341639676732WT132154298450?7220
5252341639676732BP132154298451?8132/82
Patient
IDcreate_dateOlog2Schema_Patient_IDbirthdatelast_namefirst_nameID
61187438212?9340465020doejohn937189
71187444008?10246222505kumaramrit937190
81187445155?11121408849grantalexandra937191
9?1225234121408849grantalexandra?13
10?1425235409235232von hoffvincent?15
11?1625236380665171tsaibrian?17
Prescription
IDIDdetailsdatepatient_id
12675345Enalapril163967673225234
13675346chlorothiazide163969654425234
14675347lisinopril163970452225235
Visit
IDIDpatient_idvisit_date
1512378279371891187438212
1612378289371901187444008
1712378299371911187445155


instance Colim

Observation
IDpatient_idobs_dateobs_typeclinician_idIDvisit_idobservation
0252341639676732BP132154298451?0132/82
1252341639676732WT132154298450?0220
2252341639676732HR132154298449?0116
3?11187438212HR5624872983291237827114
4?11187438212WT5624872983301237827180
5?11187438212BP5624872983311237827130/82
Patient
IDcreate_dateOlog2Schema_Patient_IDbirthdatelast_namefirst_nameID
6118744515525234121408849grantalexandra937191
71187438212?1340465020doejohn937189
8?225235409235232von hoffvincent?3
9?425236380665171tsaibrian?5
101187444008?6246222505kumaramrit937190
Prescription
IDIDdetailsdatepatient_id
11675345Enalapril163967673225234
12675346chlorothiazide163969654425234
13675347lisinopril163970452225235
Visit
IDIDpatient_idvisit_date
14?09371911639676732
1512378279371891187438212
1612378289371901187444008
1712378299371911187445155


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


command check1

Satisfied

command check2

Satisfied