From ccd60fc7bfd50cc03a21a4ceeea930c25a6ce262 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Mon, 2 Oct 2023 18:58:39 +0200
Subject: [PATCH] implement subtype checks

---
 src/lib.rs          |  1 +
 src/subtype.rs      | 51 +++++++++++++++++++++++++++++++
 src/test/subtype.rs | 74 +++++++++++++++++++++++++++++++++++++++++++--
 3 files changed, 124 insertions(+), 2 deletions(-)
 create mode 100644 src/subtype.rs

diff --git a/src/lib.rs b/src/lib.rs
index d46d35b..3f725bc 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -6,6 +6,7 @@ pub mod lexer;
 pub mod parser;
 pub mod curry;
 pub mod lnf;
+pub mod subtype;
 
 #[cfg(test)]
 mod test;
diff --git a/src/subtype.rs b/src/subtype.rs
new file mode 100644
index 0000000..8f398b1
--- /dev/null
+++ b/src/subtype.rs
@@ -0,0 +1,51 @@
+use crate::term::TypeTerm;
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl TypeTerm {    
+    // returns ladder-step of first match and provided representation-type
+    pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
+        let provided_lnf = self.clone().get_lnf_vec();
+        let expected_lnf = expected_type.clone().get_lnf_vec();
+
+        for i in 0..provided_lnf.len() {
+            if provided_lnf[i] == expected_lnf[0] {
+                return Some((i, TypeTerm::Ladder(
+                    provided_lnf[i..].into_iter().cloned().collect()
+                )))
+            }
+        }
+
+        None
+    }
+
+    pub fn is_syntactic_subtype_of(&self, expected_type: &TypeTerm) -> Result<usize, Option<(usize, usize)>> {
+        if let Some((first_match, provided_type)) = self.is_semantic_subtype_of( expected_type ) {
+            let provided_lnf = provided_type.get_lnf_vec();
+            let expected_lnf = expected_type.clone().get_lnf_vec();
+
+            for i in 0 .. usize::min( provided_lnf.len(), expected_lnf.len() ) {
+                if provided_lnf[i] != expected_lnf[i] {
+                    return Err(Some((first_match, first_match+i)))
+                }
+            }
+
+            Ok(first_match)
+        } else {
+            Err(None)
+        }
+    }
+
+
+    // supertype analogs
+
+    pub fn is_semantic_supertype_of(&self, t: &TypeTerm) -> Option<(usize, TypeTerm)> {
+        t.is_semantic_subtype_of(self)
+    }
+
+    pub fn is_syntactic_supertype_of(&self, t: &TypeTerm) -> Result<usize, Option<(usize, usize)>> {
+        t.is_syntactic_subtype_of(self)
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/test/subtype.rs b/src/test/subtype.rs
index 77f6d1e..836b492 100644
--- a/src/test/subtype.rs
+++ b/src/test/subtype.rs
@@ -1,6 +1,76 @@
+use crate::dict::TypeDict;
 
 #[test]
-fn test_subtype() {
-    // todo
+fn test_semantic_subtype() {
+    let mut dict = TypeDict::new();
+
+    assert_eq!(
+        dict.parse("A~B~C").expect("parse error")
+            .is_semantic_subtype_of(
+                &dict.parse("A~B~C").expect("parse errror")
+            ),
+        Some((0, dict.parse("A~B~C").expect("parse errror")))
+    );
+
+    assert_eq!(
+        dict.parse("A~B1~C1").expect("parse error")
+            .is_semantic_subtype_of(
+                &dict.parse("A~B2~C2").expect("parse errror")
+            ),
+        Some((0, dict.parse("A~B1~C1").expect("parse errror")))
+    );
+    
+    assert_eq!(
+        dict.parse("A~B~C1").expect("parse error")
+            .is_semantic_subtype_of(
+                &dict.parse("B~C2").expect("parse errror")  
+            ),
+        Some((1, dict.parse("B~C1").expect("parse errror")))
+    );
+}
+
+#[test]
+fn test_syntactic_subtype() {
+    let mut dict = TypeDict::new();
+
+    assert_eq!(
+        dict.parse("A~B~C").expect("parse error")
+            .is_syntactic_subtype_of(
+                &dict.parse("A~B~C").expect("parse errror")  
+            ),
+        Ok(0)
+    );
+
+    assert_eq!(
+        dict.parse("A~B~C").expect("parse error")
+            .is_syntactic_subtype_of(
+                &dict.parse("B~C").expect("parse errror")  
+            ),
+        Ok(1)
+    );
+
+    assert_eq!(
+        dict.parse("A~B~C~D~E").expect("parse error")
+            .is_syntactic_subtype_of(
+                &dict.parse("C~D").expect("parse errror")  
+            ),
+        Ok(2)
+    );
+
+    assert_eq!(
+        dict.parse("A~B~C~D~E").expect("parse error")
+            .is_syntactic_subtype_of(
+                &dict.parse("C~G").expect("parse errror")  
+            ),
+        Err(Some((2,3)))
+    );
+
+    assert_eq!(
+        dict.parse("A~B~C~D~E").expect("parse error")
+            .is_syntactic_subtype_of(
+                &dict.parse("G~F~K").expect("parse errror")  
+            ),
+        Err(None)
+    );
 }