add shift_variables() and in Morphism trait add ctx()

src/context/mod.rs

@@ -48,6 +48,7 @@ impl Context {
     }
 }
 
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 impl TypeDict for Arc<RwLock<Context>> {
     fn add_typename(&mut self, tn: &str) -> u64 {
@@ -114,6 +115,8 @@ impl TypeDict for Arc<RwLock<Context>> {
     }
 }
 
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
 impl Substitution for Arc<RwLock<Context>> {
     fn saturate(&mut self) {
         let mut locked_self = self.read().unwrap();
@@ -137,13 +140,38 @@ impl Substitution for Arc<RwLock<Context>> {
     }
 }
 
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
 pub trait LayeredContext {
     fn add_variable(&self, symbol: &str, kind: TypeKind ) -> u64;
     fn bind(&self, var: u64, val: TypeTerm) -> Result<(), SubstError>;
     fn scope(&self) -> Self;
+
+    fn shift_variables(&self, other: &Arc<RwLock<Context>>, t: TypeTerm) -> TypeTerm;
 }
 
 impl LayeredContext for Arc<RwLock<Context>> {
+    fn shift_variables(&self, other: &Arc<RwLock<Context>>, mut t: TypeTerm) -> TypeTerm {
+        let mut σ = HashMapSubst::new();
+        let l = self.read().unwrap().γ.len() as u64;
+
+        for (i,entry) in other.read().unwrap().γ.iter().enumerate() {
+            let i = i as u64;
+
+            // make variable name unique
+            let mut s = entry.symbol.clone();
+            while self.get_typeid(&s).is_some() {
+                s.push_str("'");
+            }
+
+            self.add_variable(&s, entry.kind.clone());
+            σ.insert(i, TypeTerm::Var(i + l));
+        }
+
+        t.apply_subst(&σ);
+        t
+    }
+
     fn add_variable(&self, symbol: &str, kind: TypeKind ) -> u64 {
         //self.write().unwrap().dict.add_varname(symbol.into());
         let mut locked_self = self.write().unwrap();
@@ -159,7 +187,8 @@ impl LayeredContext for Arc<RwLock<Context>> {
 
     fn bind(&self, var: u64, val: TypeTerm) -> Result<(), SubstError> {
         let mut locked_self = self.write().unwrap();
-        if (var as usize) < locked_self.γ.len() {
+        let l = locked_self.γ.len() as u64;
+        if var < l {
             if locked_self.γ[var as usize].value.is_none() {
                 locked_self.γ[var as usize].value = Some(val);
                 Ok(())
@@ -167,10 +196,10 @@ impl LayeredContext for Arc<RwLock<Context>> {
                 Err(SubstError::AlreadyAssigned)
             }
         } else {
-            let l = locked_self.γ.len() as u64;
             if let Some(parent) = locked_self.parent.as_mut() {
                 parent.bind(var - l, val)
             } else {
+                eprintln!("ERROR: assign invalid variable");
                 Err(SubstError::InvalidVariable)
             }
         }

src/morphism/instance.rs

@@ -243,5 +243,3 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
         }
     }
 }
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism/mod.rs

@@ -22,6 +22,7 @@ use {
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 pub trait Morphism : Sized {
+    fn ctx(&self) -> Arc<RwLock<Context>>;
     fn get_type(&self) -> MorphismType;
     fn weight(&self) -> u64 {
         1

src/test/morphism_graph.rs

@@ -1,8 +1,7 @@
 use {
-    crate::{dict::*, morphism::*, parser::*,
-        HashMapSubst, TypeTerm
+    crate::{dict::*, morphism::*, parser::*, ConstraintError, ConstraintPair, ConstraintSystem, Context, HashMapSubst, LayeredContext, TypeKind, TypeTerm
     },
-    std::collections::HashMap
+    std::{collections::HashMap, sync::{Arc, RwLock}}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -10,6 +9,10 @@ use {
 #[derive(Clone, Debug, PartialEq, Eq)]
 struct DummyMorphism(MorphismType);
 impl Morphism for DummyMorphism {
+    fn ctx(&self) -> Arc<RwLock<Context>> {
+        Context::new()
+    }
+
     fn get_type(&self) -> MorphismType {
         self.0.clone()
     }
@@ -79,6 +82,54 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
 }
 
 
+#[test]
+fn test_morphism_compat() {
+    let ctx = Context::new();
+
+    let mut c1 = ctx.scope();
+    c1.add_variable("T1", TypeKind::Type);
+    c1.add_variable("T2", TypeKind::Type);
+    let t1 = MorphismType {
+        bounds: Vec::new(),
+        src_type: c1.parse("<Seq T1>~<A T1 T2>").unwrap(),
+        dst_type: c1.parse("<Seq T1>~<B T2 T2>").unwrap()
+    };
+
+    let mut c2 = ctx.scope();
+    c2.add_variable("S1", TypeKind::Type);
+    c2.add_variable("T1", TypeKind::Type); //< this variable name is scoped thus a *different* variable than T1 from t1
+    let t2 = MorphismType {
+        bounds: Vec::new(),
+        src_type: c2.parse("<Seq NotT>~<B S1 T1>").unwrap(),
+        dst_type: c2.parse("<Seq NotT>~<C T1>").unwrap()
+    };
+
+    // pull t1 & t2 into root ctx
+    let t1 = ctx.shift_variables(&c1, t1.dst_type.clone());
+    let t2 = ctx.shift_variables(&c2, t2.src_type.clone());
+
+    let csp = ConstraintSystem::new_sub(vec![
+        ConstraintPair {
+            lhs: t1.clone(),
+            rhs: t2.clone(),
+            addr: vec![]
+        }
+    ]);
+
+    eprintln!("t1 = {:?} = {}", t1, t1.pretty(&mut ctx.clone(), 0));
+    eprintln!("t2 = {:?} = {}", t2, t2.pretty(&mut ctx.clone(), 0));
+
+    match csp.solve() {
+        Ok((Ψ,σ)) => {
+            eprintln!("σ = {:?}", σ);
+            assert!(true);
+        }
+        Err(err) => {
+            assert!(false);
+        }
+    }
+}
+
 #[test]
 fn test_morphgraph_id() {
     let (mut dict, mut base) = morphism_test_setup();