From 6c574d620f0a94574416cd09fe0621a5f04d1742 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 21 Jul 2024 17:45:43 +0200 Subject: [PATCH] add find_semantic_subtype_matches() as potential alternative to is_semantic_subtype_of() --- src/subtype.rs | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/src/subtype.rs b/src/subtype.rs index 8c46752..c068a0d 100644 --- a/src/subtype.rs +++ b/src/subtype.rs @@ -2,7 +2,49 @@ use crate::term::TypeTerm; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ -impl TypeTerm { +impl TypeTerm { + pub fn find_semantic_subtype_matches(&self, expected_type: &TypeTerm) + -> Option<(TypeTerm, TypeTerm, 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] { + // found first match. + // now find first mismatch. + for j in i..usize::min(provided_lnf.len(), i+expected_lnf.len()) { + if provided_lnf[j] != expected_lnf[ j-i ] { + + eprintln!("found match at {}, mismatch at {}", i, j); + let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. j ].into_iter().cloned().collect() ); + let provided_reprladder = TypeTerm::Ladder( provided_lnf[ j .. ].into_iter().cloned().collect() ); + let expected_reprladder = TypeTerm::Ladder( expected_lnf[ j-i .. ].into_iter().cloned().collect() ); + return Some((syntactic_subladder, provided_reprladder, expected_reprladder)); + } + } + + eprintln!("only syntactic subtype"); + + // syntactic subtype + let n = { + if provided_lnf.len() + i < expected_lnf.len() { + 1 + } else { + 2 + } + }; + + let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. provided_lnf.len()-1 ].into_iter().cloned().collect() ); + let provided_reprladder = TypeTerm::Ladder( provided_lnf[ provided_lnf.len()-n .. ].into_iter().cloned().collect() ); + let expected_reprladder = TypeTerm::Ladder( expected_lnf[ provided_lnf.len()-n-i .. ].into_iter().cloned().collect() ); + return Some((syntactic_subladder, provided_reprladder, expected_reprladder)); + } + } + + None + } + // 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();