diff --git a/src/lib.rs b/src/lib.rs index 11a001f..a06c3d1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -27,3 +27,70 @@ pub use { unification::*, morphism::* }; + + +pub fn common_halo( + a: &TypeTerm, + b: &TypeTerm +) -> Option< TypeTerm > { + match (a,b) { + (TypeTerm::Ladder(rs1), TypeTerm::Ladder(rs2)) => { + let mut halo_rungs = Vec::new(); + + for (r1, r2) in rs1.iter().zip(rs2.iter()) { + if let Some(h) = common_halo(r1, r2) { + halo_rungs.push(h); + } else { + return Some(TypeTerm::Ladder(halo_rungs).normalize()); + } + } + + if halo_rungs.len() == 0 { + None + } else { + Some(TypeTerm::Ladder(halo_rungs).normalize()) + } + } + + (TypeTerm::App(a1), TypeTerm::App(a2)) => { + let mut halo_args = Vec::new(); + + for (r1, r2) in a1.iter().zip(a2.iter()) { + if let Some(h) = common_halo(r1, r2) { + halo_args.push(h); + } else { + return Some(TypeTerm::Ladder(halo_args).normalize()); + } + } + + if halo_args.len() == 0 { + None + } else { + Some(TypeTerm::App(halo_args).normalize()) + } + } + + (TypeTerm::Ladder(rsl), r) => { + if rsl.first().unwrap() == r { + Some(r.clone()) + } else { + None + } + } + (l, TypeTerm::Ladder(rsr)) => { + if rsr.first().unwrap() == l { + Some(l.clone()) + } else { + None + } + } + + (a1, a2) => { + if a1 == a2 { + Some(a1.clone()) + } else { + None + } + } + } +} diff --git a/src/test/halo.rs b/src/test/halo.rs new file mode 100644 index 0000000..780b7fd --- /dev/null +++ b/src/test/halo.rs @@ -0,0 +1,39 @@ +use crate::{dict::BimapTypeDict, parser::*, unparser::*}; + +#[test] +fn test_common_halo() { + let mut dict = BimapTypeDict::new(); + + assert_eq!( + crate::common_halo( + &dict.parse("A~B~C").expect("parse error"), + &dict.parse("A~B~C").expect("parse error") + ), + Some(dict.parse("A~B~C").expect("parse error")) + ); + + assert_eq!( + crate::common_halo( + &dict.parse("A~B~X").expect("parse error"), + &dict.parse("A~B~Y").expect("parse error") + ), + Some(dict.parse("A~B").expect("parse error")) + ); + + assert_eq!( + crate::common_halo( + &dict.parse("A~<B C~D>").expect("parse error"), + &dict.parse("A~<B C~E>").expect("parse error") + ), + Some(dict.parse("A~<B C>").expect("parse error")) + ); + + + assert_eq!( + crate::common_halo( + &dict.parse("A").expect("parse error"), + &dict.parse("A~<B C~E>").expect("parse error") + ), + Some(dict.parse("A").expect("parse error")) + ); +} diff --git a/src/test/mod.rs b/src/test/mod.rs index 41f5e71..1cd4673 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -8,4 +8,4 @@ pub mod subtype; pub mod substitution; pub mod unification; pub mod morphism; - +pub mod halo;