add common_halo

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
+            }
+        }
+    }
+}

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"))
+        );
+}

src/test/mod.rs

@@ -8,4 +8,4 @@ pub mod subtype;
 pub mod substitution;
 pub mod unification;
 pub mod morphism;
-
+pub mod halo;