Fix type compatibility where casting is needed

knowsys · Nov 1, 2023 · 69b253d · 69b253d
1 parent 2348953
commit 69b253d
Show file tree

Hide file tree

Showing 4 changed files with 106 additions and 16 deletions.
diff --git a/nemo/src/io/parser.rs b/nemo/src/io/parser.rs
@@ -705,7 +705,12 @@ impl<'a> RuleParser<'a> {
                             }),
                             map(
                                 separated_list1(self.parse_comma(), self.parse_type_name()),
-                                |type_names| type_names.into_iter().collect(),
+                                |type_names| {
+                                    type_names
+                                        .into_iter()
+                                        .map(TypeConstraint::AtLeast)
+                                        .collect()
+                                },
                             ),
                         ))),
                         cut(token("]")),
@@ -1377,17 +1382,22 @@ mod test {
             predicate.clone(),
             NativeDataSource::DsvFile(DsvFile::csv_file(
                 file,
-                [PrimitiveType::Any, PrimitiveType::Integer]
-                    .into_iter()
-                    .collect(),
+                [
+                    TypeConstraint::AtLeast(PrimitiveType::Any),
+                    TypeConstraint::AtLeast(PrimitiveType::Integer),
+                ]
+                .into_iter()
+                .collect(),
             )),
         );
 
         let single_string_source = DataSourceDeclaration::new(
             predicate,
             NativeDataSource::DsvFile(DsvFile::csv_file(
                 file,
-                [PrimitiveType::String].into_iter().collect(),
+                [TypeConstraint::AtLeast(PrimitiveType::String)]
+                    .into_iter()
+                    .collect(),
             )),
         );
 

diff --git a/nemo/src/model/types/primitive_types.rs b/nemo/src/model/types/primitive_types.rs
@@ -75,13 +75,11 @@ generate_logical_type_enum!(
 impl PartialOrd for PrimitiveType {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
         match self {
-            Self::Any => {
-                if matches!(other, Self::Any) {
-                    Some(std::cmp::Ordering::Equal)
-                } else {
-                    Some(std::cmp::Ordering::Greater)
-                }
-            }
+            Self::Any => match other {
+                Self::Any => Some(std::cmp::Ordering::Equal),
+                Self::String => Some(std::cmp::Ordering::Greater),
+                _ => None, // TODO: should be the following once reasoning supports casting: Some(std::cmp::Ordering::Greater),
+            },
             Self::String => match other {
                 Self::Any => Some(std::cmp::Ordering::Less),
                 Self::String => Some(std::cmp::Ordering::Equal),

diff --git a/nemo/src/program_analysis/type_inference.rs b/nemo/src/program_analysis/type_inference.rs
@@ -47,6 +47,8 @@ pub(super) fn infer_types(program: &ChaseProgram) -> TypeInferenceResult {
             .or_insert(vec![TypeRequirement::None; arity]);
     }
 
+    eprintln!("{type_requirements:?}");
+
     let position_graph = PositionGraph::from_rules(program.rules());
 
     let type_requirements = position_graph.propagate_type_requirements(type_requirements)?;
@@ -65,6 +67,8 @@ pub(super) fn infer_types(program: &ChaseProgram) -> TypeInferenceResult {
         })
         .collect();
 
+    eprintln!("{pred_types:?}");
+
     // we check that everything is consistent
     position_graph.check_type_requirement_compatibility(&pred_types)?;
 
@@ -232,7 +236,8 @@ mod test {
                 ChaseFact, ChaseProgram, ChaseRule, Constructor, PrimitiveAtom, VariableAtom,
             },
             Constant, Constraint, DataSourceDeclaration, DsvFile, Identifier, NativeDataSource,
-            NumericLiteral, PrimitiveTerm, PrimitiveType, Term, TupleConstraint, Variable,
+            NumericLiteral, PrimitiveTerm, PrimitiveType, Term, TupleConstraint, TypeConstraint,
+            Variable,
         },
         program_analysis::{analysis::get_fresh_rule_predicate, type_inference::infer_types},
     };
@@ -648,7 +653,9 @@ mod test {
                     c,
                     NativeDataSource::DsvFile(DsvFile::csv_file(
                         "",
-                        [PrimitiveType::Any].into_iter().collect(),
+                        [TypeConstraint::AtLeast(PrimitiveType::Any)]
+                            .into_iter()
+                            .collect(),
                     )),
                 )],
                 vec![basic_rule, exis_rule, rule_with_constant],
@@ -809,4 +816,71 @@ mod test {
         let inferred_types = infer_types(&b_and_c_conflict_decl_resolvable).unwrap().0;
         assert_eq!(inferred_types, expected_types);
     }
+
+    #[test]
+    fn infer_types_a_unresolvable_conflict_with_source_decls_of_b_and_c() {
+        let (
+            (basic_rule, exis_rule, rule_with_constant),
+            (fact1, fact2, fact3),
+            (a, b, c, _r, _s, _t, _q),
+        ) = get_test_rules_and_facts_and_predicates();
+
+        let a_unresolvable_conflict_with_source_decls_of_b_and_c = ChaseProgram::new(
+            None,
+            Default::default(),
+            vec![
+                DataSourceDeclaration::new(
+                    b,
+                    NativeDataSource::DsvFile(DsvFile::csv_file(
+                        "",
+                        [TypeConstraint::AtLeast(PrimitiveType::Integer)]
+                            .into_iter()
+                            .collect(),
+                    )),
+                ),
+                DataSourceDeclaration::new(
+                    c,
+                    NativeDataSource::DsvFile(DsvFile::csv_file(
+                        "",
+                        [TypeConstraint::AtLeast(PrimitiveType::Integer)]
+                            .into_iter()
+                            .collect(),
+                    )),
+                ),
+            ],
+            vec![basic_rule, exis_rule, rule_with_constant],
+            vec![fact1, fact2, fact3],
+            [(a, vec![PrimitiveType::Any])].into_iter().collect(),
+            Default::default(),
+        );
+
+        let inferred_types_res = infer_types(&a_unresolvable_conflict_with_source_decls_of_b_and_c);
+        eprintln!("{inferred_types_res:?}");
+        assert!(inferred_types_res.is_err());
+    }
+
+    #[test]
+    fn infer_types_s_decl_unresolvable_conflict_with_fact_values() {
+        let (
+            (basic_rule, exis_rule, rule_with_constant),
+            (fact1, fact2, fact3),
+            (_a, _b, _c, _r, s, _t, _q),
+        ) = get_test_rules_and_facts_and_predicates();
+
+        let s_decl_unresolvable_conflict_with_fact_values = ChaseProgram::new(
+            None,
+            Default::default(),
+            vec![],
+            vec![basic_rule, exis_rule, rule_with_constant],
+            vec![fact1, fact2, fact3],
+            [(s, vec![PrimitiveType::Any, PrimitiveType::Integer])]
+                .into_iter()
+                .collect(),
+            Default::default(),
+        );
+
+        let inferred_types_res = infer_types(&s_decl_unresolvable_conflict_with_fact_values);
+        eprintln!("{inferred_types_res:?}");
+        assert!(inferred_types_res.is_err());
+    }
 }
diff --git a/nemo/src/program_analysis/type_inference/type_requirement.rs b/nemo/src/program_analysis/type_inference/type_requirement.rs
@@ -37,11 +37,19 @@ impl TypeRequirement {
         match self {
             Self::Hard(t1) => match other {
                 Self::Hard(t2) => (t1 == t2).then_some(self),
-                Self::Soft(t2) => (t1 >= t1.max_type(&t2)).then_some(self),
+                Self::Soft(t2) => {
+                    let max = t1.max_type(&t2);
+                    // check if the max type is compatible with both types via partial ord
+                    (t1 >= max && max >= t2).then_some(self)
+                }
                 Self::None => Some(self),
             },
             Self::Soft(t1) => match other {
-                Self::Hard(t2) | Self::Soft(t2) => Some(Self::Soft(t1.max_type(&t2))),
+                Self::Hard(t2) | Self::Soft(t2) => {
+                    let max = t1.max_type(&t2);
+                    // check if the max type is compatible with both types via partial ord
+                    (max >= t1 && max >= t2).then_some(Self::Soft(max))
+                }
                 Self::None => Some(self),
             },
             Self::None => match other {