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 Olog2Data

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


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 Olog1DataFwd

Observation
IDvisit_idobs_dateclinician_idIDpatient_idobservationobs_type
01237827?0562487298329?1114HR
11237827?2562487298330?3180WT
21237827?4562487298331?5130/82BP
Patient
IDcreate_datebirthdatefirst_nameOlog2Schema_Patient_IDIDlast_name
31187438212340465020john?6937189doe
41187444008246222505amrit?7937190kumar
51187445155121408849alexandra?8937191grant
Prescription
IDdateIDpatient_iddetails
Visit
IDIDpatient_idvisit_date
612378279371891187438212
712378289371901187444008
812378299371911187445155


instance Olog2DataFwd

Observation
IDvisit_idobs_dateclinician_idIDpatient_idobservationobs_type
0?0163967673213215429844925234116HR
1?1163967673213215429845025234220WT
2?2163967673213215429845125234132/82BP
Patient
IDcreate_datebirthdatefirst_nameOlog2Schema_Patient_IDIDlast_name
3?3121408849alexandra25234?4grant
4?5409235232vincent25235?6von hoff
5?7380665171brian25236?8tsai
Prescription
IDdateIDpatient_iddetails
6163967673267534525234Enalapril
7163969654467534625234chlorothiazide
8163970452267534725235lisinopril
Visit
IDIDpatient_idvisit_date


instance CoProd

Observation
IDvisit_idobs_dateclinician_idIDpatient_idobservationobs_type
01237827?0562487298329?1114HR
11237827?2562487298330?3180WT
21237827?4562487298331?5130/82BP
3?6163967673213215429844925234116HR
4?7163967673213215429845025234220WT
5?8163967673213215429845125234132/82BP
Patient
IDcreate_datebirthdatefirst_nameOlog2Schema_Patient_IDIDlast_name
61187438212340465020john?9937189doe
71187444008246222505amrit?10937190kumar
81187445155121408849alexandra?11937191grant
9?12121408849alexandra25234?13grant
10?14409235232vincent25235?15von hoff
11?16380665171brian25236?17tsai
Prescription
IDdateIDpatient_iddetails
12163967673267534525234Enalapril
13163969654467534625234chlorothiazide
14163970452267534725235lisinopril
Visit
IDIDpatient_idvisit_date
1512378279371891187438212
1612378289371901187444008
1712378299371911187445155


instance Colim

Observation
IDvisit_idobs_dateclinician_idIDpatient_idobservationobs_type
0?0163967673213215429845125234132/82BP
1?0163967673213215429845025234220WT
2?0163967673213215429844925234116HR
312378271187438212562487298329?1114HR
412378271187438212562487298330?1180WT
512378271187438212562487298331?1130/82BP
Patient
IDcreate_datebirthdatefirst_nameOlog2Schema_Patient_IDIDlast_name
61187445155121408849alexandra25234937191grant
71187438212340465020john?1937189doe
8?2409235232vincent25235?3von hoff
9?4380665171brian25236?5tsai
101187444008246222505amrit?6937190kumar
Prescription
IDdateIDpatient_iddetails
11163967673267534525234Enalapril
12163969654467534625234chlorothiazide
13163970452267534725235lisinopril
Visit
IDIDpatient_idvisit_date
14?09371911639676732
1512378279371891187438212
1612378289371901187444008
1712378299371911187445155


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


command check1

Satisfied

command check2

Satisfied