From 74177d1d30b99e2b436105a46e03008f8cecdf1b Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 30 Oct 2023 17:22:00 +0100 Subject: [PATCH] substitutions --- src/term.rs | 30 ++++++++++++++++++++++++++++++ src/test/mod.rs | 1 + src/test/substitution.rs | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 63 insertions(+) create mode 100644 src/test/substitution.rs diff --git a/src/term.rs b/src/term.rs index 25fee14..f5e8f5f 100644 --- a/src/term.rs +++ b/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 + ) -> &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 + } } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ diff --git a/src/test/mod.rs b/src/test/mod.rs index 9d13c07..4cde4e3 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -4,4 +4,5 @@ pub mod parser; pub mod curry; pub mod lnf; pub mod subtype; +pub mod substitution; diff --git a/src/test/substitution.rs b/src/test/substitution.rs new file mode 100644 index 0000000..7959b08 --- /dev/null +++ b/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 --> + σ.insert + (dict.add_varname(String::from("U")), + dict.parse("").unwrap()); + + + assert_eq!( + dict.parse("").unwrap() + .apply_substitution(&|typid|{ σ.get(typid).cloned() }).clone(), + dict.parse(">").unwrap() + ); +} +