add find_semantic_subtype_matches() as potential alternative to is_semantic_subtype_of()

README.md

@@ -5,8 +5,6 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc)
 
 ## Ladder Types
 
-### Motivation
-
 In order to implement complex datastructures and algorithms, usually
 many layers of abstraction are built ontop of each other.
 Consequently higher-level data types are encoded into lower-level data
@@ -59,48 +57,6 @@ this:
 1696093021:1696093039:1528324679:1539892301:1638141920:1688010253
 ```
 
-### Syntax
-
-In their core form, type-terms can be one of the following:
-- (**Atomic Type**)        |   `SomeTypeName`
-- (**Literal Integer**)    |   `0` | `1` | `2` | ...
-- (**Literal Character**)  |   `'a'` | `'b'` | `'c'` | ...
-- (**Literal String**)     |   `"abc"`
-- (**Parameter Application**) | `<T1 T2>` given `T1` and `T2` are type-terms
-- (**Ladder**)                | `T1 ~ T2` given `T1` and `T2` are type-terms
-
-Ontop of that, the following syntax-sugar is defined:
-
-#### Complex Types
-- `[ T ]` <===> `<Seq T>`
-- `{ a:A b:B }` <===> `<Struct <"a" A> <"b" B>>`
-- `a:A | b:B` <===> `<Enum <"a" A> <"b" B>>`
-
-#### Function Types
-- `A -> B` <===> `<Fn A B>`
-
-#### Reference Types
-- `*A`  <===> `<Ptr A>`
-- `&A`  <===> `<ConstRef A>`
-- `&!A` <===> `<MutRef A>`
-
-
-### Equivalences
-
-#### Currying
-`<<A B> C>` <===> `<A B C>`
-
-#### Ladder-Normal-Form
-exhaustively apply `<A B~C>` ===> `<A B>~<A C>`
-
-e.g. `[<Digit 10>]~[Char]~[Ascii]` is in **LNF**
-
-#### Parameter-Normal-Form
-exhaustively apply `<A B>~<A C>` ===> `<A B~C>`
-
-e.g. `[<Digit 10>~Char~Ascii]` is in **PNF**
-
-
 ## How to use this crate
 
 ```rust
@@ -117,19 +73,6 @@ fn main() {
 }
 ```
 
-## Roadmap
-
-- [x] (Un-)Parsing
-- [x] (De-)Currying
-- [x] Unification
-- [x] Ladder-Normal-Form
-- [x] Parameter-Normal-Form
-- [ ] (De)-Sugaring
-  - [ ] Seq
-  - [ ] Enum
-  - [ ] Struct
-  - [ ] References
-  - [ ] Function
 
 ## License
 [GPLv3](COPYING)

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();