substitutions

src/term.rs

@@ -78,6 +78,36 @@ impl TypeTerm {
     pub fn char_arg(&mut self, c: char) -> &mut Self {
         self.arg(TypeTerm::Char(c))
     }
+
+    /// recursively apply substitution to all subterms,
+    /// which will replace all occurences of variables which map
+    /// some type-term in `subst`
+    pub fn apply_substitution(
+        &mut self,
+        subst: &impl Fn(&TypeID) -> Option<TypeTerm>
+    ) -> &mut Self {
+        match self {
+            TypeTerm::TypeID(typid) => {
+                if let Some(t) = subst(typid) {
+                    *self = t;
+                }
+            }
+
+            TypeTerm::Ladder(rungs) => {
+                for r in rungs.iter_mut() {
+                    r.apply_substitution(subst);
+                }
+            }
+            TypeTerm::App(args) => {
+                for r in args.iter_mut() {
+                    r.apply_substitution(subst);
+                }
+            }
+            _ => {}
+        }
+
+        self
+    }
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/test/mod.rs

@@ -4,4 +4,5 @@ pub mod parser;
 pub mod curry;
 pub mod lnf;
 pub mod subtype;
+pub mod substitution;
 

src/test/substitution.rs

@@ -0,0 +1,32 @@
+
+use {
+    crate::{dict::*, term::*},
+    std::iter::FromIterator
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[test]
+fn test_subst() {
+    let mut dict = TypeDict::new();
+
+    let mut σ = std::collections::HashMap::new();
+
+    // T  -->  ℕ
+    σ.insert
+        (dict.add_varname(String::from("T")),
+         dict.parse("ℕ").unwrap());
+
+    // U  -->  <Seq Char>
+    σ.insert
+        (dict.add_varname(String::from("U")),
+         dict.parse("<Seq Char>").unwrap());
+
+
+    assert_eq!(
+        dict.parse("<Seq T~U>").unwrap()
+            .apply_substitution(&|typid|{ σ.get(typid).cloned() }).clone(),
+        dict.parse("<Seq ℕ~<Seq Char>>").unwrap()
+    );
+}
+