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**
ID	ID	patient_id	clinician_id	obs_type	obs_date	observation
0	154298449	25234	132	HR	1639676732	116
1	154298450	25234	132	WT	1639676732	220
2	154298451	25234	132	BP	1639676732	132/82

**Patient**
ID	ID	fname	lname	dob
3	25234	alexandra	grant	121408849
4	25235	vincent	von hoff	409235232
5	25236	brian	tsai	380665171

**Prescription**
ID	ID	patient_id	date	details
6	675345	25234	1639676732	Enalapril
7	675346	25234	1639696544	chlorothiazide
8	675347	25235	1639704522	lisinopril

instance Olog1Data

**Observation**
ID	ID	visit_id	clinician_id	obs_type	observation
0	487298329	1237827	562	HR	114
1	487298330	1237827	562	WT	180
2	487298331	1237827	562	BP	130/82

**Patient**
ID	ID	first_name	last_name	birthdate	create_date
3	937189	john	doe	340465020	1187438212
4	937190	amrit	kumar	246222505	1187444008
5	937191	alexandra	grant	121408849	1187445155

**Visit**
ID	ID	patient_id	visit_date
6	1237827	937189	1187438212
7	1237828	937190	1187444008
8	1237829	937191	1187445155

instance Olog1DataFwd

**Observation**
ID	observation	clinician_id	obs_date	ID	patient_id	obs_type	visit_id
0	114	562	?0	487298329	?1	HR	1237827
1	180	562	?2	487298330	?3	WT	1237827
2	130/82	562	?4	487298331	?5	BP	1237827

**Patient**
ID	create_date	last_name	ID	Olog2Schema_Patient_ID	birthdate	first_name
3	1187438212	doe	937189	?6	340465020	john
4	1187444008	kumar	937190	?7	246222505	amrit
5	1187445155	grant	937191	?8	121408849	alexandra

**Prescription**
ID	ID	patient_id	date	details

**Visit**
ID	visit_date	patient_id	ID
6	1187438212	937189	1237827
7	1187444008	937190	1237828
8	1187445155	937191	1237829

instance Olog2DataFwd

**Observation**
ID	observation	clinician_id	obs_date	ID	patient_id	obs_type	visit_id
0	116	132	1639676732	154298449	25234	HR	?0
1	220	132	1639676732	154298450	25234	WT	?1
2	132/82	132	1639676732	154298451	25234	BP	?2

**Patient**
ID	create_date	last_name	ID	Olog2Schema_Patient_ID	birthdate	first_name
3	?3	grant	?4	25234	121408849	alexandra
4	?5	von hoff	?6	25235	409235232	vincent
5	?7	tsai	?8	25236	380665171	brian

**Prescription**
ID	ID	patient_id	date	details
6	675345	25234	1639676732	Enalapril
7	675346	25234	1639696544	chlorothiazide
8	675347	25235	1639704522	lisinopril

**Visit**
ID	visit_date	patient_id	ID

instance CoProd

**Observation**
ID	observation	clinician_id	obs_date	ID	patient_id	obs_type	visit_id
0	114	562	?0	487298329	?1	HR	1237827
1	180	562	?2	487298330	?3	WT	1237827
2	130/82	562	?4	487298331	?5	BP	1237827
3	116	132	1639676732	154298449	25234	HR	?6
4	220	132	1639676732	154298450	25234	WT	?7
5	132/82	132	1639676732	154298451	25234	BP	?8

**Patient**
ID	create_date	last_name	ID	Olog2Schema_Patient_ID	birthdate	first_name
6	1187438212	doe	937189	?9	340465020	john
7	1187444008	kumar	937190	?10	246222505	amrit
8	1187445155	grant	937191	?11	121408849	alexandra
9	?12	grant	?13	25234	121408849	alexandra
10	?14	von hoff	?15	25235	409235232	vincent
11	?16	tsai	?17	25236	380665171	brian

**Prescription**
ID	ID	patient_id	date	details
12	675345	25234	1639676732	Enalapril
13	675346	25234	1639696544	chlorothiazide
14	675347	25235	1639704522	lisinopril

**Visit**
ID	visit_date	patient_id	ID
15	1187438212	937189	1237827
16	1187444008	937190	1237828
17	1187445155	937191	1237829

instance Colim

**Observation**
ID	observation	clinician_id	obs_date	ID	patient_id	obs_type	visit_id
0	132/82	132	1639676732	154298451	25234	BP	?0
1	220	132	1639676732	154298450	25234	WT	?0
2	116	132	1639676732	154298449	25234	HR	?0
3	114	562	1187438212	487298329	?1	HR	1237827
4	180	562	1187438212	487298330	?1	WT	1237827
5	130/82	562	1187438212	487298331	?1	BP	1237827

**Patient**
ID	create_date	last_name	ID	Olog2Schema_Patient_ID	birthdate	first_name
6	1187445155	grant	937191	25234	121408849	alexandra
7	1187438212	doe	937189	?1	340465020	john
8	?2	von hoff	?3	25235	409235232	vincent
9	?4	tsai	?5	25236	380665171	brian
10	1187444008	kumar	937190	?6	246222505	amrit

**Prescription**
ID	ID	patient_id	date	details
11	675345	25234	1639676732	Enalapril
12	675346	25234	1639696544	chlorothiazide
13	675347	25235	1639704522	lisinopril

**Visit**
ID	visit_date	patient_id	ID
14	1639676732	937191	?0
15	1187438212	937189	1237827
16	1187444008	937190	1237828
17	1187445155	937191	1237829

instance Olog2DataBkwd

**Observation**
ID	ID	patient_id	clinician_id	obs_type	obs_date	observation
0	154298451	25234	132	BP	1639676732	132/82
1	154298450	25234	132	WT	1639676732	220
2	154298449	25234	132	HR	1639676732	116
3	487298329	?0	562	HR	1187438212	114
4	487298330	?0	562	WT	1187438212	180
5	487298331	?0	562	BP	1187438212	130/82

**Patient**
ID	ID	fname	lname	dob
6	25234	alexandra	grant	121408849
7	?0	john	doe	340465020
8	25235	vincent	von hoff	409235232
9	25236	brian	tsai	380665171
10	?1	amrit	kumar	246222505

**Prescription**
ID	ID	patient_id	date	details
11	675345	25234	1639676732	Enalapril
12	675346	25234	1639696544	chlorothiazide
13	675347	25235	1639704522	lisinopril

instance Olog1DataBkwd

**Observation**
ID	ID	visit_id	clinician_id	obs_type	observation
0	154298451	?0	132	BP	132/82
1	154298450	?0	132	WT	220
2	154298449	?0	132	HR	116
3	487298329	1237827	562	HR	114
4	487298330	1237827	562	WT	180
5	487298331	1237827	562	BP	130/82

**Patient**
ID	ID	first_name	last_name	birthdate	create_date
6	937191	alexandra	grant	121408849	1187445155
7	937189	john	doe	340465020	1187438212
8	?1	vincent	von hoff	409235232	?2
9	?3	brian	tsai	380665171	?4
10	937190	amrit	kumar	246222505	1187444008

**Visit**
ID	ID	patient_id	visit_date
11	?0	937191	1639676732
12	1237827	937189	1187438212
13	1237828	937190	1187444008
14	1237829	937191	1187445155

command check1

Satisfies

command check2

Satisfies