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
ObservationID | 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 |
PatientID | ID | fname | lname | dob |
---|
3 | 25234 | alexandra | grant | 121408849 |
4 | 25235 | vincent | von hoff | 409235232 |
5 | 25236 | brian | tsai | 380665171 |
PrescriptionID | ID | patient_id | date | details |
---|
6 | 675345 | 25234 | 1639676732 | Enalapril |
7 | 675346 | 25234 | 1639696544 | chlorothiazide |
8 | 675347 | 25235 | 1639704522 | lisinopril |
instance Olog1Data
ObservationID | 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 |
PatientID | 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 |
VisitID | ID | patient_id | visit_date |
---|
6 | 1237827 | 937189 | 1187438212 |
7 | 1237828 | 937190 | 1187444008 |
8 | 1237829 | 937191 | 1187445155 |
instance Olog1DataFwd
ObservationID | visit_id | obs_date | clinician_id | ID | patient_id | observation | obs_type |
---|
0 | 1237827 | ?0 | 562 | 487298329 | ?1 | 114 | HR |
1 | 1237827 | ?2 | 562 | 487298330 | ?3 | 180 | WT |
2 | 1237827 | ?4 | 562 | 487298331 | ?5 | 130/82 | BP |
PatientID | create_date | birthdate | first_name | Olog2Schema_Patient_ID | ID | last_name |
---|
3 | 1187438212 | 340465020 | john | ?6 | 937189 | doe |
4 | 1187444008 | 246222505 | amrit | ?7 | 937190 | kumar |
5 | 1187445155 | 121408849 | alexandra | ?8 | 937191 | grant |
PrescriptionID | date | ID | patient_id | details |
---|
VisitID | ID | patient_id | visit_date |
---|
6 | 1237827 | 937189 | 1187438212 |
7 | 1237828 | 937190 | 1187444008 |
8 | 1237829 | 937191 | 1187445155 |
instance Olog2DataFwd
ObservationID | visit_id | obs_date | clinician_id | ID | patient_id | observation | obs_type |
---|
0 | ?0 | 1639676732 | 132 | 154298449 | 25234 | 116 | HR |
1 | ?1 | 1639676732 | 132 | 154298450 | 25234 | 220 | WT |
2 | ?2 | 1639676732 | 132 | 154298451 | 25234 | 132/82 | BP |
PatientID | create_date | birthdate | first_name | Olog2Schema_Patient_ID | ID | last_name |
---|
3 | ?3 | 121408849 | alexandra | 25234 | ?4 | grant |
4 | ?5 | 409235232 | vincent | 25235 | ?6 | von hoff |
5 | ?7 | 380665171 | brian | 25236 | ?8 | tsai |
PrescriptionID | date | ID | patient_id | details |
---|
6 | 1639676732 | 675345 | 25234 | Enalapril |
7 | 1639696544 | 675346 | 25234 | chlorothiazide |
8 | 1639704522 | 675347 | 25235 | lisinopril |
VisitID | ID | patient_id | visit_date |
---|
instance CoProd
ObservationID | visit_id | obs_date | clinician_id | ID | patient_id | observation | obs_type |
---|
0 | 1237827 | ?0 | 562 | 487298329 | ?1 | 114 | HR |
1 | 1237827 | ?2 | 562 | 487298330 | ?3 | 180 | WT |
2 | 1237827 | ?4 | 562 | 487298331 | ?5 | 130/82 | BP |
3 | ?6 | 1639676732 | 132 | 154298449 | 25234 | 116 | HR |
4 | ?7 | 1639676732 | 132 | 154298450 | 25234 | 220 | WT |
5 | ?8 | 1639676732 | 132 | 154298451 | 25234 | 132/82 | BP |
PatientID | create_date | birthdate | first_name | Olog2Schema_Patient_ID | ID | last_name |
---|
6 | 1187438212 | 340465020 | john | ?9 | 937189 | doe |
7 | 1187444008 | 246222505 | amrit | ?10 | 937190 | kumar |
8 | 1187445155 | 121408849 | alexandra | ?11 | 937191 | grant |
9 | ?12 | 121408849 | alexandra | 25234 | ?13 | grant |
10 | ?14 | 409235232 | vincent | 25235 | ?15 | von hoff |
11 | ?16 | 380665171 | brian | 25236 | ?17 | tsai |
PrescriptionID | date | ID | patient_id | details |
---|
12 | 1639676732 | 675345 | 25234 | Enalapril |
13 | 1639696544 | 675346 | 25234 | chlorothiazide |
14 | 1639704522 | 675347 | 25235 | lisinopril |
VisitID | ID | patient_id | visit_date |
---|
15 | 1237827 | 937189 | 1187438212 |
16 | 1237828 | 937190 | 1187444008 |
17 | 1237829 | 937191 | 1187445155 |
instance Colim
ObservationID | visit_id | obs_date | clinician_id | ID | patient_id | observation | obs_type |
---|
0 | ?0 | 1639676732 | 132 | 154298451 | 25234 | 132/82 | BP |
1 | ?0 | 1639676732 | 132 | 154298450 | 25234 | 220 | WT |
2 | ?0 | 1639676732 | 132 | 154298449 | 25234 | 116 | HR |
3 | 1237827 | 1187438212 | 562 | 487298329 | ?1 | 114 | HR |
4 | 1237827 | 1187438212 | 562 | 487298330 | ?1 | 180 | WT |
5 | 1237827 | 1187438212 | 562 | 487298331 | ?1 | 130/82 | BP |
PatientID | create_date | birthdate | first_name | Olog2Schema_Patient_ID | ID | last_name |
---|
6 | 1187445155 | 121408849 | alexandra | 25234 | 937191 | grant |
7 | 1187438212 | 340465020 | john | ?1 | 937189 | doe |
8 | ?2 | 409235232 | vincent | 25235 | ?3 | von hoff |
9 | ?4 | 380665171 | brian | 25236 | ?5 | tsai |
10 | 1187444008 | 246222505 | amrit | ?6 | 937190 | kumar |
PrescriptionID | date | ID | patient_id | details |
---|
11 | 1639676732 | 675345 | 25234 | Enalapril |
12 | 1639696544 | 675346 | 25234 | chlorothiazide |
13 | 1639704522 | 675347 | 25235 | lisinopril |
VisitID | ID | patient_id | visit_date |
---|
14 | ?0 | 937191 | 1639676732 |
15 | 1237827 | 937189 | 1187438212 |
16 | 1237828 | 937190 | 1187444008 |
17 | 1237829 | 937191 | 1187445155 |
instance Olog1DataBkwd
ObservationID | 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 |
PatientID | 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 |
VisitID | ID | patient_id | visit_date |
---|
11 | ?0 | 937191 | 1639676732 |
12 | 1237827 | 937189 | 1187438212 |
13 | 1237828 | 937190 | 1187444008 |
14 | 1237829 | 937191 | 1187445155 |
instance Olog2DataBkwd
ObservationID | 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 |
PatientID | 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 |
PrescriptionID | ID | patient_id | date | details |
---|
11 | 675345 | 25234 | 1639676732 | Enalapril |
12 | 675346 | 25234 | 1639696544 | chlorothiazide |
13 | 675347 | 25235 | 1639704522 | lisinopril |
command check1
Satisfied
command check2
Satisfied