lib-laddertypes/src/lib.rs

99 lines
2.1 KiB
Rust

pub mod bimap;
pub mod dict;
pub mod term;
pub mod lexer;
pub mod parser;
pub mod unparser;
pub mod sugar;
pub mod curry;
pub mod lnf;
pub mod pnf;
pub mod subtype;
pub mod unification;
pub mod morphism;
pub mod morphism_base;
pub mod morphism_path;
pub mod steiner_tree;
#[cfg(test)]
mod test;
#[cfg(feature = "pretty")]
mod pretty;
pub use {
dict::*,
term::*,
sugar::*,
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
}
}
}
}