wip: renamings, try to fix tests

- add more tests
- add struct & enum cases

README.md

@@ -1,6 +1,6 @@
 # lib-laddertypes
 
-Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc) 
+Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc)
 <hr/>
 
 ## Ladder Types
@@ -121,16 +121,15 @@ fn main() {
 
 - [x] (Un-)Parsing
 - [x] (De-)Currying
-- [x] Unification
-- [x] Ladder-Normal-Form
-- [x] Parameter-Normal-Form
-- [ ] (De)-Sugaring
-  - [ ] Seq
-  - [ ] Enum
-  - [ ] Struct
-  - [ ] References
-  - [ ] Function
+- [x] Normal-Form
+- [x] Pretty Debug
+- [ ] Sugared Parser
+- [ ] Universal Types, Function Types
+- [x] Constraint Solving (Unification, Subtype Satisfaction)
+- [x] Morphism Graph
+  - [x] Complex Morphisms
+  - [x] Find Shortest Path
+  - [x] Approximate Steiner Tree
 
 ## License
 [GPLv3](COPYING)
-

src/bimap.rs

@@ -2,6 +2,7 @@ use std::{collections::HashMap, hash::Hash};
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
+#[derive(Debug)]
 pub struct Bimap<V: Eq + Hash, Λ: Eq + Hash> {
     pub mλ: HashMap<V, Λ>,
     pub my: HashMap<Λ, V>,

src/constraint_system.rs

@@ -0,0 +1,809 @@
+use {
+    crate::{dict::*, term::TypeTerm, desugared_term::*, EnumVariant, StructMember, Substitution}, std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct ConstraintError {
+    pub addr: Vec<usize>,
+    pub t1: TypeTerm,
+    pub t2: TypeTerm
+}
+
+#[derive(Clone)]
+pub struct ConstraintPair {
+    pub addr: Vec<usize>,
+    pub lhs: TypeTerm,
+    pub rhs: TypeTerm,
+}
+
+impl ConstraintPair {
+    pub fn new(lhs: TypeTerm, rhs: TypeTerm) -> Self {
+        ConstraintPair {
+            lhs,rhs, addr:vec![]
+        }
+    }
+}
+
+pub struct ConstraintSystem {
+    σ: HashMap<TypeID, TypeTerm>,
+    upper_bounds: HashMap< u64, TypeTerm >,
+    lower_bounds: HashMap< u64, TypeTerm >,
+
+    equal_pairs: Vec<ConstraintPair>,
+    subtype_pairs: Vec<ConstraintPair>,
+    trait_pairs: Vec<ConstraintPair>,
+    parallel_pairs: Vec<ConstraintPair>
+}
+
+impl ConstraintSystem {
+    pub fn new(
+        equal_pairs: Vec<ConstraintPair>,
+        subtype_pairs: Vec<ConstraintPair>,
+        trait_pairs: Vec<ConstraintPair>,
+        parallel_pairs: Vec<ConstraintPair>
+    ) -> Self {
+        ConstraintSystem {
+            σ: HashMap::new(),
+
+            equal_pairs,
+            subtype_pairs,
+            trait_pairs,
+            parallel_pairs,
+
+            upper_bounds: HashMap::new(),
+            lower_bounds: HashMap::new(),
+        }
+    }
+
+    pub fn new_eq(eqs: Vec<ConstraintPair>) -> Self {
+        ConstraintSystem::new(  eqs, Vec::new(), Vec::new(), Vec::new() )
+    }
+
+    pub fn new_sub( subs: Vec<ConstraintPair>) -> Self {
+        ConstraintSystem::new( Vec::new(), subs, Vec::new(), Vec::new() )
+    }
+
+    pub fn new_trait(traits: Vec<ConstraintPair>) -> Self {
+        ConstraintSystem::new( Vec::new(), Vec::new(), traits, Vec::new() )
+    }
+
+    pub fn new_parallel( parallels: Vec<ConstraintPair>) -> Self {
+        ConstraintSystem::new(Vec::new(), Vec::new(), Vec::new(), parallels )
+    }
+
+
+    /// update all values in substitution
+    pub fn reapply_subst(&mut self) {
+        let mut new_σ = HashMap::new();
+        for (v, tt) in self.σ.iter() {
+            let mut tt = tt.clone();
+            tt.apply_subst(&self.σ);
+            //eprintln!("update σ : {:?} --> {:?}", v, tt);
+            new_σ.insert(v.clone(), tt.normalize());
+        }
+        self.σ = new_σ;
+    }
+
+
+    pub fn eval_equation(&mut self, unification_pair: ConstraintPair) -> Result<(), ConstraintError> {
+        match (&unification_pair.lhs, &unification_pair.rhs) {
+            (TypeTerm::TypeID(TypeID::Var(varid)), t) |
+            (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
+                if ! t.contains_var( *varid ) {
+                    self.σ.insert(TypeID::Var(*varid), t.clone());
+                    self.reapply_subst();
+                    Ok(())
+                } else if t == &TypeTerm::TypeID(TypeID::Var(*varid)) {
+                    Ok(())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
+                }
+            }
+
+            (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
+                if a1 == a2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
+                if n1 == n2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
+                if c1 == c2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+
+            (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
+            (TypeTerm::Spec(a1), TypeTerm::Spec(a2)) => {
+                if a1.len() == a2.len() {
+                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push(
+                            ConstraintPair {
+                                lhs: x,
+                                rhs: y,
+                                addr: new_addr
+                            });
+                    }
+                    Ok(())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            (TypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+                TypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+            => {
+                let mut new_addr = unification_pair.addr.clone();
+                new_addr.push(0);
+
+                if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
+                    if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
+                        let _seq_repr_ψ = self.eval_equation(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
+                    } else {
+                        return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+
+                if lhs_items.len() == rhs_items.len() {
+                    for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (TypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+                TypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+            => {
+                let new_addr = unification_pair.addr.clone();
+                if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
+                    if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
+                        let _struct_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
+                    } else {
+                        return Err(ConstraintError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+                if lhs_members.len() == rhs_members.len() {
+                    for (i,
+                            (StructMember{ symbol: lhs_symbol, ty: lhs_ty},
+                                StructMember{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (TypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+                TypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+            => {
+                let mut new_addr = unification_pair.addr.clone();
+                if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
+                    if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
+                        let _enum_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
+                    } else {
+                        return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+
+                if lhs_variants.len() == rhs_variants.len() {
+                    for (i,
+                            (EnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+                                EnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            _ => Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+        }
+    }
+
+
+    pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> {
+
+        if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) {
+            return Ok(());
+        }
+
+        if new_lower_bound.contains_var(v) {
+            // loop
+            return Err(());
+        }
+
+        if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
+                        eprintln!("var already exists. check max. type");
+            if let Ok(halo) = self.eval_subtype(
+                ConstraintPair {
+                    lhs: lower_bound.clone(),
+                    rhs: new_lower_bound.clone(),
+                    addr: vec![]
+                }
+            ) {
+                            eprintln!("found more general lower bound");
+                            eprintln!("set var {}'s lowerbound to {:?}", v, new_lower_bound.clone());
+                // generalize variable type to supertype
+                self.lower_bounds.insert(v, new_lower_bound);
+                Ok(())
+            } else if let Ok(halo) = self.eval_subtype(
+                ConstraintPair{
+                    lhs: new_lower_bound,
+                    rhs: lower_bound,
+                    addr: vec![]
+                }
+            ) {
+                            eprintln!("OK, is already larger type");
+                 Ok(())
+            } else {
+                            eprintln!("violated subtype restriction");
+                Err(())
+            }
+        } else {
+                        eprintln!("set var {}'s lowerbound to {:?}", v, new_lower_bound.clone());
+            self.lower_bounds.insert(v, new_lower_bound);
+            Ok(())
+        }
+    }
+
+
+    pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> {
+        if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) {
+            return Ok(());
+        }
+
+        if new_upper_bound.contains_var(v) {
+            // loop
+            return Err(());
+        }
+
+        if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
+            if let Ok(_halo) = self.eval_subtype(
+                ConstraintPair {
+                    lhs: new_upper_bound.clone(),
+                    rhs: upper_bound,
+                    addr: vec![]
+                }
+            ) {
+                eprintln!("found a lower upper bound: {} <= {:?}", v, new_upper_bound);
+                // found a lower upper bound
+                self.upper_bounds.insert(v, new_upper_bound);
+                Ok(())
+            } else {
+                eprintln!("new upper bound violates subtype restriction");
+                Err(())
+            }
+        } else {
+            eprintln!("set upper bound: {} <= {:?}", v, new_upper_bound);
+            self.upper_bounds.insert(v, new_upper_bound);
+            Ok(())
+        }
+    }
+
+    pub fn eval_subtype(&mut self, unification_pair: ConstraintPair) -> Result<
+        // ok: halo type
+        TypeTerm,
+        // error
+        ConstraintError
+    > {
+        eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
+        match (unification_pair.lhs.clone().strip(), unification_pair.rhs.clone().strip()) {
+
+            /*
+             Variables
+            */
+
+            (t, TypeTerm::TypeID(TypeID::Var(v))) => {
+                //eprintln!("t <= variable");
+                if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
+                    Ok(TypeTerm::unit())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
+                }
+            }
+
+            (TypeTerm::TypeID(TypeID::Var(v)), t) => {
+                //eprintln!("variable <= t");
+                if self.add_upper_subtype_bound(v, t.clone()).is_ok() {
+                    Ok(TypeTerm::unit())
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
+                }
+            }
+
+
+            /*
+             Atoms
+            */
+            (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
+                if a1 == a2 { Ok(TypeTerm::unit()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs}) }
+            }
+            (TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
+                if n1 == n2 { Ok(TypeTerm::unit()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
+                if c1 == c2 { Ok(TypeTerm::unit()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+
+            /*
+             Complex Types
+            */
+
+            (TypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+                TypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+            => {
+                let mut new_addr = unification_pair.addr.clone();
+                new_addr.push(0);
+
+                if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
+                    //eprintln!("subtype unify: rhs has seq-repr: {:?}", rhs_seq_repr);
+                    if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
+                        //eprintln!("check if it maches lhs seq-repr: {:?}", lhs_seq_repr);
+                        let _seq_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
+                        //eprintln!("..yes!");
+                    } else {
+                        //eprintln!("...but lhs has none.");
+                        return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+                let mut new_addr = unification_pair.addr.clone();
+                new_addr.push(1);
+                if lhs_items.len() == rhs_items.len() && lhs_items.len() > 0 {
+                    match self.eval_subtype( ConstraintPair { addr: new_addr.clone(), lhs: lhs_items[0].clone(), rhs: rhs_items[0].clone() } ) {
+                        Ok(ψ) => Ok(TypeTerm::Seq {
+                                seq_repr: None, // <<- todo
+                                items: vec![ψ]
+                            }.strip()),
+                        Err(e) => Err(ConstraintError{
+                                addr: new_addr,
+                                t1: e.t1,
+                                t2: e.t2,
+                            })
+                    }
+                } else {
+                    Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (TypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+                TypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+            => {
+                let new_addr = unification_pair.addr.clone();
+                if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
+                    if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
+                        let _struct_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
+                    } else {
+                        return Err(ConstraintError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+                if lhs_members.len() == rhs_members.len() {
+                    let mut halo_members = Vec::new();
+                    for (i,
+                            (StructMember{ symbol: lhs_symbol, ty: lhs_ty},
+                                StructMember{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+
+                        let ψ = self.eval_subtype( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+                        halo_members.push(StructMember { symbol: lhs_symbol, ty: ψ });
+                    }
+                    Ok(TypeTerm::Struct {
+                        struct_repr: None,
+                        members: halo_members
+                    })
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (TypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+                TypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+            => {
+                let mut new_addr = unification_pair.addr.clone();
+                if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
+                    if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
+                        let _enum_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
+                    } else {
+                        return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+                    }
+                }
+
+                if lhs_variants.len() == rhs_variants.len() {
+                    let mut halo_variants = Vec::new();
+                    for (i,
+                            (EnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+                                EnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        let ψ = self.eval_subtype( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+                        halo_variants.push(EnumVariant { symbol: lhs_symbol, ty: ψ });
+                    }
+                    Ok(TypeTerm::Enum {
+                        enum_repr: None,
+                        variants: halo_variants
+                    })
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+
+
+            /*
+             Ladders
+            */
+
+            (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
+
+                let mut l1_iter = a1.into_iter().enumerate().rev();
+                let mut l2_iter = a2.into_iter().rev();
+
+                let mut halo_ladder = Vec::new();
+
+                while let Some(rhs) = l2_iter.next() {
+                    //eprintln!("take rhs = {:?}", rhs);
+                    if let Some((i, lhs)) = l1_iter.next() {
+                        //eprintln!("take lhs ({}) = {:?}", i, lhs);
+                        let mut addr = unification_pair.addr.clone();
+                        addr.push(i);
+                        //eprintln!("addr = {:?}", addr);
+
+                        match (lhs.clone(), rhs.clone()) {
+                            (t, TypeTerm::TypeID(TypeID::Var(v))) => {
+
+                                if self.add_upper_subtype_bound(v,t.clone()).is_ok() {
+                                    let mut new_upper_bound_ladder = vec![ t ];
+
+                                    if let Some(next_rhs) = l2_iter.next() {
+
+                                    } else {
+                                        // ladder of rhs is empty
+                                        // take everything
+
+                                        while let Some((i,t)) = l1_iter.next() {
+                                            new_upper_bound_ladder.push(t);
+                                        }
+                                    }
+
+                                    new_upper_bound_ladder.reverse();
+                                    if self.add_upper_subtype_bound(v, TypeTerm::Ladder(new_upper_bound_ladder)).is_ok() {
+                                        // ok
+                                    } else {
+                                        return Err(ConstraintError {
+                                            addr,
+                                            t1: lhs,
+                                            t2: rhs
+                                        });
+                                    }
+                                } else {
+                                    return Err(ConstraintError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
+                                }
+                            }
+                            (lhs, rhs) => {
+                                if let Ok(ψ) = self.eval_subtype(
+                                    ConstraintPair {
+                                        lhs: lhs.clone(),
+                                        rhs: rhs.clone(),
+                                        addr:addr.clone(),
+                                    }
+                                ) {
+                                    // ok.
+                                    //eprintln!("rungs are subtypes. continue");
+                                    halo_ladder.push(ψ);
+                                } else {
+                                    return Err(ConstraintError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
+                                }
+                            }
+                        }
+                    } else {
+                        // not a subtype,
+                        return Err(ConstraintError {
+                            addr: vec![],
+                            t1: unification_pair.lhs,
+                            t2: unification_pair.rhs
+                        });
+                    }
+                }
+
+                //eprintln!("left ladder fully consumed");
+
+                for (i,t) in l1_iter {
+                    //!("push {} to halo ladder", t.pretty(self.dict,0));
+                    halo_ladder.push(t);
+                }
+                halo_ladder.reverse();
+                Ok(TypeTerm::Ladder(halo_ladder).strip())//.param_normalize())
+            },
+
+            (TypeTerm::Seq { seq_repr, items }, TypeTerm::Spec(mut args)) => {
+                let mut new_addr = unification_pair.addr.clone();
+                let mut n_halos_required = 0;
+                if args.len() > 1 {
+                    if let Some(seq_repr) = seq_repr {
+                        let rhs = args.remove(0);
+                        let reprψinterface = rhs.get_interface_type();
+                        let mut reprψ = self.eval_subtype(ConstraintPair{
+                            addr: new_addr.clone(),
+                            lhs: seq_repr.as_ref().clone(),
+                            rhs
+                        })?;
+
+                        let mut itemsψ = Vec::new();
+                        for (i,(item, arg)) in items.iter().zip(args.iter()).enumerate() {
+                            let mut new_addr = new_addr.clone();
+                            new_addr.push(i);
+                            let ψ = self.eval_subtype(ConstraintPair {
+                                addr: new_addr,
+                                lhs: item.clone(),
+                                rhs: arg.clone()
+                            })?;
+
+                            if ψ.is_empty() {
+                                itemsψ.push(item.get_interface_type());
+                            } else {
+                                if n_halos_required == 0 {
+                                    // first argument that requires halo,
+                                    // add highest-common-rung to sequence repr
+                                    reprψ = TypeTerm::Ladder(vec![
+                                        reprψ,
+                                        reprψinterface.clone()
+                                    ]).normalize();
+                                } else {
+                                    /* todo
+                                    if let Some(mut t) = itemsψ.last_mut() {
+                                        t = TypeTerm::Ladder(vec![
+                                            t.clone(),
+                                            args[i]
+                                        ]).normalize();
+                                    } else {
+                                        t =
+                                    }
+                                    */
+                                }
+
+                                n_halos_required += 1;
+
+                                itemsψ.push(ψ);
+                            }
+                        }
+                        eprintln!("itemsψ = {:?}", itemsψ);
+                        Ok(
+                            TypeTerm::Seq {
+                                seq_repr: if reprψ.is_empty() { None }
+                                          else { Some(Box::new(reprψ)) },
+                                items: itemsψ
+                            }
+                        )
+                    } else {
+                        Err(ConstraintError {
+                            addr: new_addr,
+                            t1: unification_pair.lhs,
+                            t2: unification_pair.rhs
+                        })
+                    }
+                } else {
+                    Err(ConstraintError {
+                        addr: unification_pair.addr,
+                        t1: unification_pair.lhs,
+                        t2: unification_pair.rhs
+                    })
+                }
+            }
+
+            (t, TypeTerm::Ladder(a1)) => {
+                Err(ConstraintError{ addr: unification_pair.addr, t1: t, t2: TypeTerm::Ladder(a1) })
+            }
+
+            (TypeTerm::Ladder(mut a1), t) => {
+                if a1.len() > 0 {
+                    let mut new_addr = unification_pair.addr.clone();
+                    new_addr.push( a1.len() - 1 );
+                    if let Ok(halo) = self.eval_subtype(
+                        ConstraintPair {
+                            lhs: a1.pop().unwrap(),
+                            rhs: t.clone(),
+                            addr: new_addr
+                        }
+                    ) {
+                        a1.push(halo);
+                        if a1.len() == 1 {
+                            Ok(a1.pop().unwrap())
+                        } else {
+                            Ok(TypeTerm::Ladder(a1).normalize())
+                        }
+                    } else {
+                        Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::Ladder(a1), t2: t })
+                    }
+                } else if t == TypeTerm::unit() {
+                    Ok(TypeTerm::unit())
+                } else {
+                    Err(ConstraintError { addr: unification_pair.addr, t1: TypeTerm::unit(), t2: t })
+                }
+            }
+
+
+            /*
+             Application
+            */
+
+            (TypeTerm::Spec(a1), TypeTerm::Spec(a2)) => {
+                if a1.len() == a2.len() {
+                    let mut halo_args = Vec::new();
+                    let mut n_halos_required = 0;
+
+                    for (i, (mut x, mut y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+
+                        x = x.strip();
+
+//                        eprintln!("before strip: {:?}", y);
+                        y = y.strip();
+//                        eprintln!("after strip: {:?}", y);
+//                        eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
+
+                        match self.eval_subtype(
+                            ConstraintPair {
+                                lhs: x.clone(),
+                                rhs: y.clone(),
+                                addr: new_addr,
+                            }
+                        ) {
+                            Ok(halo) => {
+                                if halo == TypeTerm::unit() {
+                                    let mut y = y.clone();
+                                    y.apply_subst(&self.σ);
+                                    y = y.strip();
+
+                                    let top = y.get_interface_type();
+                                    // eprintln!("add top {}", top.pretty(self.dict, 0));
+                                    halo_args.push(top);
+                                } else {
+                                    //println!("add halo {}", halo.pretty(self.dict, 0));
+                                    if n_halos_required > 0 {
+                                        let x = &mut halo_args[n_halos_required-1];
+                                        if let TypeTerm::Ladder(arg_rungs) = x {
+                                            let mut a = a2[n_halos_required-1].clone();
+                                            a.apply_subst(&self.σ);
+                                            arg_rungs.push(a.get_interface_type());
+                                        } else {
+                                            *x = TypeTerm::Ladder(vec![
+                                                x.clone(),
+                                                a2[n_halos_required-1].get_interface_type()
+                                            ]);
+
+                                            x.apply_subst(&self.σ);
+                                        }
+                                    }
+
+                                    halo_args.push(halo);
+                                    n_halos_required += 1;
+                                }
+                            },
+                            Err(err) => { return Err(err); }
+                        }
+                    }
+
+                    if n_halos_required > 0 {
+                        //eprintln!("halo args : {:?}", halo_args);
+                        Ok(TypeTerm::Spec(halo_args))
+                    } else {
+                        Ok(TypeTerm::unit())
+                    }
+                } else {
+                    Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            _ => Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+        }
+    }
+
+    pub fn solve(mut self) -> Result<(Vec<TypeTerm>, HashMap<TypeID, TypeTerm>), ConstraintError> {
+        // solve equations
+        while let Some( mut equal_pair ) = self.equal_pairs.pop() {
+            equal_pair.lhs.apply_subst(&self.σ);
+            equal_pair.rhs.apply_subst(&self.σ);
+
+            self.eval_equation(equal_pair)?;
+        }
+
+        // solve subtypes
+        eprintln!("------ SOLVE SUBTYPES ---- ");
+        for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+            subtype_pair.lhs.apply_subst(&self.σ);
+            subtype_pair.rhs.apply_subst(&self.σ);
+            let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+        }
+
+        // add variables from subtype bounds
+        for (var_id, t) in self.upper_bounds.iter() {
+//            eprintln!("VAR {} upper bound {:?}", var_id, t);
+            self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+        }
+
+        for (var_id, t) in self.lower_bounds.iter() {
+//            eprintln!("VAR {} lower bound {:?}", var_id, t);
+            self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+        }
+
+        self.reapply_subst();
+
+        eprintln!("------ MAKE HALOS -----");
+        let mut halo_types = Vec::new();
+        for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+            subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone();
+            subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone();
+
+            let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+            halo_types.push(halo);
+        }
+
+        // solve traits
+        while let Some( trait_pair ) = self.trait_pairs.pop() {
+            unimplemented!();
+        }
+
+        Ok((halo_types, self.σ))
+    }
+}
+
+pub fn unify(
+    t1: &TypeTerm,
+    t2: &TypeTerm
+) -> Result<HashMap<TypeID, TypeTerm>, ConstraintError> {
+    let unification = ConstraintSystem::new_eq(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    Ok(unification.solve()?.1)
+}
+
+pub fn subtype_unify(
+    t1: &TypeTerm,
+    t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
+    let unification = ConstraintSystem::new_sub(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
+}
+
+pub fn parallel_unify(
+    t1: &TypeTerm,
+    t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
+    let unification = ConstraintSystem::new_parallel(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/curry.rs

@@ -1,12 +1,12 @@
-use crate::term::*;
+use crate::desugared_term::*;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeTerm {
+impl DesugaredTypeTerm {
     /// transform term to have at max 2 entries in Application list
-    pub fn curry(self) -> TypeTerm {
+    pub fn curry(self) -> DesugaredTypeTerm {
         match self {
-            TypeTerm::App(args) => {
+            DesugaredTypeTerm::App(args) => {
                 if args.len() >= 2 {
                     let mut old_args = args.into_iter();
                     let mut new_args = vec![
@@ -16,19 +16,19 @@ impl TypeTerm {
 
                     for x in old_args {
                         new_args = vec![
-                            TypeTerm::App(new_args),
+                            DesugaredTypeTerm::App(new_args),
                             x
                         ];
                     }
 
-                    TypeTerm::App(new_args)
+                    DesugaredTypeTerm::App(new_args)
                 } else {
-                    TypeTerm::App(args)
+                    DesugaredTypeTerm::App(args)
                 }
             }
 
-            TypeTerm::Ladder(rungs) => {
-                TypeTerm::Ladder(rungs.into_iter().map(|r| r.curry()).collect())
+            DesugaredTypeTerm::Ladder(rungs) => {
+                DesugaredTypeTerm::Ladder(rungs.into_iter().map(|r| r.curry()).collect())
             }
 
             _ => self
@@ -38,11 +38,11 @@ impl TypeTerm {
     /// summarize all curried applications into one vec
     pub fn decurry(self) -> Self {
         match self {
-            TypeTerm::App(mut args) => {
+            DesugaredTypeTerm::App(mut args) => {
                 if args.len() > 0 {
                     let a0 = args.remove(0).decurry();
                     match a0 {
-                        TypeTerm::App(sub_args) => {
+                        DesugaredTypeTerm::App(sub_args) => {
                             for (i,x) in sub_args.into_iter().enumerate() {
                                 args.insert(i, x);
                             }
@@ -50,10 +50,10 @@ impl TypeTerm {
                         other => { args.insert(0, other); }
                     }
                 }
-                TypeTerm::App(args)
+                DesugaredTypeTerm::App(args)
             }
-            TypeTerm::Ladder(args) => {
-                TypeTerm::Ladder(args.into_iter().map(|a| a.decurry()).collect())
+            DesugaredTypeTerm::Ladder(args) => {
+                DesugaredTypeTerm::Ladder(args.into_iter().map(|a| a.decurry()).collect())
             }
             _ => self
         }

src/desugared_term.rs

@@ -0,0 +1,155 @@
+use crate::TypeID;
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, PartialEq, Eq, Hash, Debug)]
+pub enum DesugaredTypeTerm {
+
+    /* Atomic Terms */
+
+    // Base types from dictionary
+    TypeID(TypeID),
+
+    // Literals
+    Num(i64),
+    Char(char),
+
+    /* Complex Terms */
+
+    // Type Parameters
+    // avoid currying to save space & indirection
+    App(Vec< DesugaredTypeTerm >),
+
+    // Type Ladders
+    Ladder(Vec< DesugaredTypeTerm >),
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl DesugaredTypeTerm {
+    pub fn unit() -> Self {
+        DesugaredTypeTerm::Ladder(vec![])
+    }
+
+    pub fn new(id: TypeID) -> Self {
+        DesugaredTypeTerm::TypeID(id)
+    }
+
+    pub fn arg(&mut self, t: impl Into<DesugaredTypeTerm>) -> &mut Self {
+        match self {
+            DesugaredTypeTerm::App(args) => {
+                args.push(t.into());
+            }
+
+            _ => {
+                *self = DesugaredTypeTerm::App(vec![
+                    self.clone(),
+                    t.into()
+                ])
+            }
+        }
+        self
+    }
+
+    pub fn repr_as(&mut self, t: impl Into<DesugaredTypeTerm>) -> &mut Self {
+        match self {
+            DesugaredTypeTerm::Ladder(rungs) => {
+                rungs.push(t.into());
+            }
+
+            _ => {
+                *self = DesugaredTypeTerm::Ladder(vec![
+                    self.clone(),
+                    t.into()
+                ])
+            }
+        }
+
+        self
+    }
+
+    pub fn num_arg(&mut self, v: i64) -> &mut Self {
+        self.arg(DesugaredTypeTerm::Num(v))
+    }
+
+    pub fn char_arg(&mut self, c: char) -> &mut Self {
+        self.arg(DesugaredTypeTerm::Char(c))
+    }
+
+    pub fn contains_var(&self, var_id: u64) -> bool {
+        match self {
+            DesugaredTypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+            DesugaredTypeTerm::App(args) |
+            DesugaredTypeTerm::Ladder(args) => {
+                for a in args.iter() {
+                    if a.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            _ => false
+        }
+    }
+
+
+    /* strip away empty ladders
+     * & unwrap singletons
+     */
+    pub fn strip(self) -> Self {
+        match self {
+            DesugaredTypeTerm::Ladder(rungs) => {
+                let mut rungs :Vec<_> = rungs.into_iter()
+                    .filter_map(|mut r| {
+                        r = r.strip();
+                        if r != DesugaredTypeTerm::unit() {
+                            Some(match r {
+                                DesugaredTypeTerm::Ladder(r) => r,
+                                a => vec![ a ]
+                            })
+                        }
+                        else { None }
+                    })
+                .flatten()
+                .collect();
+
+                if rungs.len() == 1 {
+                    rungs.pop().unwrap()
+                } else {
+                    DesugaredTypeTerm::Ladder(rungs)
+                }
+            },
+            DesugaredTypeTerm::App(args) => {
+                let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
+                if args.len() == 0 {
+                    DesugaredTypeTerm::unit()
+                } else if args.len() == 1 {
+                    args.pop().unwrap()
+                } else {
+                    DesugaredTypeTerm::App(args)
+                }
+            }
+            atom => atom
+        }
+    }
+
+
+
+    pub fn get_interface_type(&self) -> DesugaredTypeTerm {
+        match self {
+            DesugaredTypeTerm::Ladder(rungs) => {
+                if let Some(top) = rungs.first() {
+                    top.get_interface_type()
+                } else {
+                    DesugaredTypeTerm::unit()
+                }
+            }
+            DesugaredTypeTerm::App(args) => {
+                DesugaredTypeTerm::App(args.iter().map(|a| a.get_interface_type()).collect())
+            }
+            atom => atom.clone()
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/dict.rs

@@ -8,9 +8,36 @@ pub enum TypeID {
     Var(u64)
 }
 
+pub trait TypeDict : Send + Sync {
+    fn insert(&mut self, name: String, id: TypeID);
+    fn add_varname(&mut self, vn: String) -> TypeID;
+    fn add_typename(&mut self, tn: String) -> TypeID;
+    fn get_typeid(&self, tn: &String) -> Option<TypeID>;
+    fn get_typename(&self, tid: &TypeID) -> Option<String>;
+
+    fn get_varname(&self, var_id: u64) -> Option<String> {
+        self.get_typename(&TypeID::Var(var_id))
+    }
+
+    fn add_synonym(&mut self, new: String, old: String) {
+        if let Some(tyid) = self.get_typeid(&old) {
+            self.insert(new, tyid);
+        }
+    }
+
+    fn get_typeid_creat(&mut self, tn: &str) -> TypeID {
+        if let Some(id) = self.get_typeid(&tn.to_string()) {
+            id
+        } else {
+            self.add_typename(tn.to_string())
+        }
+    }
+}
+
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-pub struct TypeDict {
+#[derive(Debug)]
+pub struct BimapTypeDict {
     typenames: Bimap<String, TypeID>,
     type_lit_counter: u64,
     type_var_counter: u64,
@@ -18,46 +45,66 @@ pub struct TypeDict {
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeDict {
+impl BimapTypeDict {
     pub fn new() -> Self {
-        TypeDict {
+        BimapTypeDict {
             typenames: Bimap::new(),
             type_lit_counter: 0,
             type_var_counter: 0,
         }
     }
+}
 
-    pub fn add_varname(&mut self, tn: String) -> TypeID {
+impl TypeDict for BimapTypeDict {
+    fn insert(&mut self, name: String, id: TypeID) {
+        self.typenames.insert(name, id);
+    }
+
+    fn add_varname(&mut self, tn: String) -> TypeID {
         let tyid = TypeID::Var(self.type_var_counter);
         self.type_var_counter += 1;
-        self.typenames.insert(tn, tyid.clone());
+        self.insert(tn, tyid.clone());
         tyid
     }
 
-    pub fn add_typename(&mut self, tn: String) -> TypeID {
+    fn add_typename(&mut self, tn: String) -> TypeID {
         let tyid = TypeID::Fun(self.type_lit_counter);
         self.type_lit_counter += 1;
-        self.typenames.insert(tn, tyid.clone());
+        self.insert(tn, tyid.clone());
         tyid
     }
 
-    pub fn add_synonym(&mut self, new: String, old: String) {
-        if let Some(tyid) = self.get_typeid(&old) {
-            self.typenames.insert(new, tyid);
-        }
-    }
-
-    pub fn get_typename(&self, tid: &TypeID) -> Option<String> {
+    fn get_typename(&self, tid: &TypeID) -> Option<String> {
         self.typenames.my.get(tid).cloned()
     }
 
-    pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+    fn get_typeid(&self, tn: &String) -> Option<TypeID> {
         self.typenames.mλ.get(tn).cloned()
     }
-
-    pub fn get_varname(&self, var_id: u64) -> Option<String> {
-        self.typenames.my.get(&TypeID::Var(var_id)).cloned()
-    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
+
+use std::sync::Arc;
+use std::ops::{Deref, DerefMut};
+use std::sync::RwLock;
+
+impl<T: TypeDict> TypeDict for Arc<RwLock<T>> {
+    fn insert(&mut self, name: String, id: TypeID) {
+        self.write().unwrap().insert(name, id);
+    }
+    fn add_varname(&mut self, vn: String) -> TypeID {
+        self.write().unwrap().add_varname(vn)
+    }
+    fn add_typename(&mut self, tn: String) -> TypeID {
+        self.write().unwrap().add_typename(tn)
+    }
+    fn get_typename(&self, tid: &TypeID)-> Option<String> {
+        self.read().unwrap().get_typename(tid)
+    }
+    fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+        self.read().unwrap().get_typeid(tn)
+    }
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>

src/lib.rs

@@ -1,16 +1,23 @@
+#![allow(mixed_script_confusables)]
 
 pub mod bimap;
 pub mod dict;
-pub mod term;
+
 pub mod lexer;
-pub mod parser;
+pub mod parser; // todo sugared variant
+pub mod curry; // todo: sugared variant
+//pub mod subtype; // deprecated
 pub mod unparser;
-pub mod sugar;
-pub mod curry;
-pub mod lnf;
+pub mod desugared_term; // deprecated
+pub mod term;
 pub mod pnf;
-pub mod subtype;
-pub mod unification;
+pub mod substitution;
+pub mod constraint_system;
+pub mod morphism;
+pub mod morphism_base;
+pub mod morphism_path;
+
+pub mod steiner_tree;
 
 #[cfg(test)]
 mod test;
@@ -20,7 +27,80 @@ mod pretty;
 
 pub use {
     dict::*,
+    desugared_term::*,
+    substitution::*,
     term::*,
-    sugar::*,
-    unification::*,
+    constraint_system::*,
+    morphism::*,
+    morphism_base::*,
+    morphism_path::*,
 };
+
+/*
+pub fn common_halo(
+    a: &DesugaredTypeTerm,
+    b: &DesugaredTypeTerm
+) -> Option< DesugaredTypeTerm > {
+    match (a,b) {
+        (DesugaredTypeTerm::Ladder(rs1), DesugaredTypeTerm::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(DesugaredTypeTerm::Ladder(halo_rungs).normalize());
+                }
+            }
+
+            if halo_rungs.len() == 0 {
+
+                None
+            } else {
+                Some(DesugaredTypeTerm::Ladder(halo_rungs).normalize())
+            }
+        }
+
+        (DesugaredTypeTerm::App(a1), DesugaredTypeTerm::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(DesugaredTypeTerm::Ladder(halo_args).normalize());
+                }
+            }
+
+            if halo_args.len() == 0 {
+                None
+            } else {
+                Some(DesugaredTypeTerm::App(halo_args).normalize())
+            }
+        }
+
+        (DesugaredTypeTerm::Ladder(rsl), r) => {
+            if rsl.first().unwrap() == r {
+                Some(r.clone())
+            } else {
+                None
+            }
+        }
+        (l, DesugaredTypeTerm::Ladder(rsr)) => {
+            if rsr.first().unwrap() == l {
+                Some(l.clone())
+            } else {
+                None
+            }
+        }
+
+        (a1, a2) => {
+            if a1 == a2 {
+                Some(a1.clone())
+            } else {
+                None
+            }
+        }
+    }
+}
+*/

src/lnf.rs

@@ -1,119 +0,0 @@
-use crate::term::TypeTerm;
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl TypeTerm {
-    /// does the type contain ladders (false) or is it 'flat' (true) ?
-    ///
-    /// Example:
-    /// ```<Seq <Digit 10>>``` is flat, but
-    /// ```<Digit 10>~Char``` is not
-    pub fn is_flat(&self) -> bool {
-        match self {
-            TypeTerm::TypeID(_) => true,
-            TypeTerm::Num(_) => true,
-            TypeTerm::Char(_) => true,
-            TypeTerm::App(args) => args.iter().fold(true, |s,x| s && x.is_flat()),
-            TypeTerm::Ladder(_) => false
-        }
-    }
-
-    /// transmute type into Ladder-Normal-Form (LNF)
-    ///
-    /// Example:
-    /// ```ignore
-    /// <Seq <Digit 10>~Char>
-    /// ⇒ <Seq <Digit 10>>~<Seq Char>
-    /// ```
-    pub fn normalize(self) -> Self {
-        let mut new_ladder = Vec::<TypeTerm>::new();
-
-        match self {
-            TypeTerm::Ladder(args) => {
-                for x in args.into_iter() {
-                    match x.normalize() {
-                        TypeTerm::Ladder(gs) => {
-                            for g in gs {
-                                new_ladder.push(g);
-                            }
-                        }
-                        g => {
-                            new_ladder.push(g);
-                        }
-                    }
-                }
-            }
-
-            TypeTerm::App(args) => {
-                let args_iter = args.into_iter();
-
-                new_ladder.push( TypeTerm::App(vec![]) );
-
-                for arg in args_iter {
-                    match arg.normalize() {
-                        TypeTerm::Ladder(rungs) => {
-                            // duplicate last element for each rung
-                            let l = new_ladder.len();
-                            for _ in 1..rungs.len() {
-                                new_ladder.push( new_ladder.last().unwrap().clone() );
-                            }
-
-                            for (i,r) in new_ladder.iter_mut().enumerate() {
-                                match r {
-                                    TypeTerm::App(al) => {
-                                        if i < l {
-                                            al.push(rungs[0].clone());
-                                        } else {
-                                            al.push(rungs[i-l+1].clone());
-                                        }
-                                    }
-                                    _ => unreachable!()
-                                }
-                            }
-                        }
-                        mut other => {
-                            other = other.normalize();
-                            for rung in new_ladder.iter_mut() {
-                                match rung {
-                                    TypeTerm::App(al) => {
-                                        al.push(other.clone());
-                                    }
-                                    _ => unreachable!()
-                                }
-                            }
-                        }
-                    }
-                }
-            }
-
-            atom => {
-                new_ladder.push(atom);
-            }
-        }
-
-        match new_ladder.len() {
-            0 => TypeTerm::unit(),
-            1 => new_ladder.into_iter().next().unwrap(),
-            _ => TypeTerm::Ladder( new_ladder )
-        }
-    }
-    
-    /// transmute type into a `Vec` containing
-    /// all rungs of the type in LNF
-    ///
-    /// Example:
-    /// ```<Seq <Digit 10>~Char>``` gives
-    /// ```ignore
-    /// vec![ <Seq <Digit 10>>,  <Seq Char> ]
-    /// ```
-    pub fn get_lnf_vec(self) -> Vec<TypeTerm> {
-        match self.normalize() {
-            TypeTerm::Ladder( v ) => {
-                v
-            },
-            flat => vec![ flat ]
-        }
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism.rs

@@ -0,0 +1,381 @@
+use {
+    crate::{
+        substitution::Substitution, term::{StructMember, TypeTerm},
+        constraint_system::ConstraintSystem, unparser::*, EnumVariant, TypeDict, TypeID
+    },
+    std::{collections::HashMap, u64}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct MorphismType {
+    pub src_type: TypeTerm,
+    pub dst_type: TypeTerm
+}
+
+impl MorphismType {
+    pub fn strip_halo(&self) -> MorphismType {
+        match (&self.src_type.clone().strip(), &self.dst_type.clone().strip()) {
+            (TypeTerm::Ladder(rungs_lhs), TypeTerm::Ladder(rungs_rhs)) => {
+
+                let mut lhs_iter = rungs_lhs.iter();
+                let mut rhs_iter = rungs_rhs.iter();
+                let mut last = MorphismType { src_type: TypeTerm::unit(), dst_type: TypeTerm::unit() };
+
+                while let (Some(lhs_top), Some(rhs_top)) = (lhs_iter.next(), rhs_iter.next()) {
+                    last = MorphismType{
+                        src_type: lhs_top.clone(),
+                        dst_type: rhs_top.clone()
+                    };
+
+                    if lhs_top != rhs_top {
+                        let x = MorphismType{ src_type: lhs_top.clone(), dst_type: rhs_top.clone() }.strip_halo();
+
+                        let mut rl : Vec<_> = lhs_iter.cloned().collect();
+                        rl.insert(0, x.src_type);
+                        let mut rr : Vec<_> = rhs_iter.cloned().collect();
+                        rr.insert(0, x.dst_type);
+
+                        return MorphismType {
+                            src_type: TypeTerm::Ladder(rl),
+                            dst_type: TypeTerm::Ladder(rr)
+                        };
+                    }
+                }
+
+                last
+            }
+
+            (TypeTerm::Spec(args_lhs), TypeTerm::Spec(args_rhs)) => {
+
+                let (rl, rr) = args_lhs.iter().zip(args_rhs.iter()).map(
+                    |(al,ar)| MorphismType{ src_type: al.clone(), dst_type: ar.clone() }.strip_halo()
+                )
+                .fold((vec![], vec![]), |(mut rl, mut rr), x| {
+                    rl.push(x.src_type);
+                    rr.push(x.dst_type);
+                    (rl,rr)
+                });
+
+                MorphismType {
+                    src_type: TypeTerm::Spec(rl),
+                    dst_type: TypeTerm::Spec(rr)
+                }
+            }
+
+            (TypeTerm::Seq { seq_repr:seq_repr_lhs, items:items_lhs },
+                TypeTerm::Seq { seq_repr: seq_repr_rhs, items:items_rhs })
+            => {
+                let (rl, rr) = items_lhs.iter().zip(items_rhs.iter()).map(
+                    |(al,ar)| MorphismType{ src_type: al.clone(), dst_type: ar.clone() }.strip_halo()
+                )
+                .fold((vec![], vec![]), |(mut rl, mut rr), x| {
+                    rl.push(x.src_type);
+                    rr.push(x.dst_type);
+                    (rl,rr)
+                });
+                MorphismType  {
+                    src_type: TypeTerm::Seq{ seq_repr: seq_repr_lhs.clone(), items: rl },
+                    dst_type: TypeTerm::Seq { seq_repr: seq_repr_rhs.clone(), items: rr }
+                }
+            }
+
+            (TypeTerm::Struct { struct_repr:struct_repr_lhs, members:members_lhs },
+                TypeTerm::Struct { struct_repr: struct_repr_rhs, members:members_rhs })
+            => {
+                let mut rl = Vec::new();
+                let mut rr = Vec::new();
+
+                for ar in members_rhs.iter() {
+                    let mut found = false;
+                    for al in members_lhs.iter() {
+                        if al.symbol == ar.symbol {
+                            let x = MorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
+                            rl.push( StructMember{
+                                symbol: al.symbol.clone(),
+                                ty: x.src_type
+                            });
+                            rr.push( StructMember{
+                                symbol: ar.symbol.clone(),
+                                ty: x.dst_type
+                            });
+                            found = true;
+                            break;
+                        }
+                    }
+
+                    if !found {
+                        return MorphismType {
+                            src_type: TypeTerm::Struct { struct_repr: struct_repr_lhs.clone(), members:members_lhs.clone() },
+                            dst_type: TypeTerm::Struct { struct_repr: struct_repr_rhs.clone(), members:members_rhs.clone() }
+                        };
+                    }
+                }
+
+                MorphismType  {
+                    src_type: TypeTerm::Struct{ struct_repr: struct_repr_lhs.clone(), members: rl },
+                    dst_type: TypeTerm::Struct{ struct_repr: struct_repr_rhs.clone(), members: rr }
+                }
+            }
+
+            (TypeTerm::Enum { enum_repr:enum_repr_lhs, variants:variants_lhs },
+                TypeTerm::Enum { enum_repr: enum_repr_rhs, variants:variants_rhs })
+            => {
+                let mut rl = Vec::new();
+                let mut rr = Vec::new();
+
+                for ar in variants_rhs.iter() {
+                    let mut found = false;
+                    for al in variants_lhs.iter() {
+                        if al.symbol == ar.symbol {
+                            let x = MorphismType{ src_type: al.ty.clone(), dst_type: ar.ty.clone() }.strip_halo();
+                            rl.push( EnumVariant{
+                                symbol: al.symbol.clone(),
+                                ty: x.src_type
+                            });
+                            rr.push( EnumVariant{
+                                symbol: ar.symbol.clone(),
+                                ty: x.dst_type
+                            });
+                            found = true;
+                            break;
+                        }
+                    }
+
+                    if !found {
+                        return MorphismType {
+                            src_type: TypeTerm::Enum { enum_repr: enum_repr_lhs.clone(), variants:variants_lhs.clone() },
+                            dst_type: TypeTerm::Enum { enum_repr: enum_repr_rhs.clone(), variants:variants_rhs.clone() }
+                        };
+                    }
+                }
+
+                MorphismType  {
+                    src_type: TypeTerm::Enum{ enum_repr: enum_repr_lhs.clone(), variants: rl },
+                    dst_type: TypeTerm::Enum { enum_repr: enum_repr_rhs.clone(), variants: rr }
+                }
+            }
+
+            (x,y) => MorphismType { src_type: x.clone(), dst_type: y.clone() }
+        }
+    }
+
+    pub fn apply_subst(&self, σ: &impl Substitution) -> MorphismType {
+        MorphismType {
+            src_type: self.src_type.clone().apply_subst(σ).clone(),
+            dst_type: self.dst_type.clone().apply_subst(σ).clone()
+        }
+    }
+
+
+    pub fn normalize(&self) -> MorphismType {
+        MorphismType {
+            src_type: self.src_type.clone().normalize(),
+            dst_type: self.dst_type.clone().normalize(),
+        }
+    }
+}
+
+pub trait Morphism : Sized {
+    fn get_type(&self) -> MorphismType;
+    fn weight(&self) -> u64 {
+        1
+    }
+}
+
+#[derive(Clone, PartialEq, Debug)]
+pub enum MorphismInstance<M: Morphism + Clone> {
+    Primitive{
+        ψ: TypeTerm,
+        σ: HashMap<TypeID, TypeTerm>,
+        morph: M,
+    },
+    Chain{
+        path: Vec<MorphismInstance<M>>
+    },
+    MapSeq{
+        ψ: TypeTerm,
+        seq_repr: Option<Box<TypeTerm>>,
+        item_morph: Box<MorphismInstance<M>>,
+    },
+    MapStruct{
+        ψ: TypeTerm,
+        src_struct_repr: Option<Box<TypeTerm>>,
+        dst_struct_repr: Option<Box<TypeTerm>>,
+        member_morph: Vec< (String, MorphismInstance<M>) >
+    },
+    MapEnum{
+        ψ: TypeTerm,
+        enum_repr: Option<Box<TypeTerm>>,
+        variant_morph: Vec< (String, MorphismInstance<M>) >
+    }
+}
+
+
+impl<M: Morphism + Clone> MorphismInstance<M> {
+    pub fn get_haloless_type(&self) -> MorphismType {
+        self.get_type().strip_halo()
+    }
+
+    pub fn get_type(&self) -> MorphismType {
+        match self {
+            MorphismInstance::Primitive { ψ, σ, morph } => {
+                MorphismType {
+                    src_type:
+                        TypeTerm::Ladder(vec![
+                            ψ.clone(),
+                            morph.get_type().src_type
+                                .apply_subst(σ).clone()
+                        ]).strip(),
+
+                    dst_type: TypeTerm::Ladder(vec![
+                            ψ.clone(),
+                            morph.get_type().dst_type
+                                .apply_subst(σ).clone()
+                        ]).strip(),
+                }
+            }
+            MorphismInstance::Chain { path } => {
+                if path.len() > 0 {
+                    let s = self.get_subst();
+                    MorphismType {
+                        src_type: path.first().unwrap().get_type().src_type.clone(),
+                        dst_type: path.last().unwrap().get_type().dst_type.clone()
+                    }.apply_subst(&s)
+                } else {
+                    MorphismType {
+                        src_type: TypeTerm::TypeID(TypeID::Fun(45454)),
+                        dst_type: TypeTerm::TypeID(TypeID::Fun(45454))
+                    }
+                }
+            }
+            MorphismInstance::MapSeq { ψ, seq_repr, item_morph } => {
+                MorphismType {
+                    src_type: TypeTerm::Ladder(vec![
+                        ψ.clone(),
+                        TypeTerm::Seq{ seq_repr: seq_repr.clone(),
+                            items: vec![ item_morph.get_type().src_type ]}
+                    ]),
+                    dst_type: TypeTerm::Ladder(vec![
+                        ψ.clone(),
+                        TypeTerm::Seq{ seq_repr: seq_repr.clone(),
+                            items: vec![ item_morph.get_type().dst_type ]}
+                    ])
+                }
+            }
+            MorphismInstance::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
+                MorphismType {
+                    src_type: TypeTerm::Ladder(vec![ ψ.clone(),
+                            TypeTerm::Struct{
+                                struct_repr: src_struct_repr.clone(),
+                                members:
+                                    member_morph.iter().map(|(symbol, morph)| {
+                                       StructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+                                    }).collect()
+                            }
+                        ]),
+                    dst_type: TypeTerm::Ladder(vec![ ψ.clone(),
+                            TypeTerm::Struct{
+                                struct_repr: dst_struct_repr.clone(),
+                                members: member_morph.iter().map(|(symbol, morph)| {
+                                    StructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+                                }).collect()
+                            }
+                        ])
+                }
+            }
+            MorphismInstance::MapEnum { ψ, enum_repr, variant_morph } => {
+                MorphismType {
+                    src_type: TypeTerm::Ladder(vec![ ψ.clone(),
+                            TypeTerm::Struct{
+                                struct_repr: enum_repr.clone(),
+                                members:
+                                    variant_morph.iter().map(|(symbol, morph)| {
+                                       StructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+                                    }).collect()
+                            }
+                        ]),
+                    dst_type: TypeTerm::Ladder(vec![ ψ.clone(),
+                            TypeTerm::Struct{
+                                struct_repr: enum_repr.clone(),
+                                members: variant_morph.iter().map(|(symbol, morph)| {
+                                    StructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+                                }).collect()
+                            }
+                        ])
+                }
+            }
+        }.normalize()
+    }
+
+    pub fn get_subst(&self) -> std::collections::HashMap< TypeID, TypeTerm > {
+        match self {
+            MorphismInstance::Primitive { ψ, σ, morph } => σ.clone(),
+            MorphismInstance::Chain { path } => {
+                path.iter().fold(
+                    std::collections::HashMap::new(),
+                    |mut σ, m| {
+                        σ = σ.append(&m.get_subst());
+                        σ
+                    }
+                )
+            },
+            MorphismInstance::MapSeq { ψ, seq_repr, item_morph } => {
+                item_morph.get_subst()
+            },
+            MorphismInstance::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
+                let mut σ = HashMap::new();
+                for (symbol, m) in member_morph.iter() {
+                    σ = σ.append(&mut m.get_subst());
+                }
+                σ
+            },
+            MorphismInstance::MapEnum { ψ, enum_repr, variant_morph } => {
+                todo!();
+                HashMap::new()
+            },
+        }
+    }
+
+    pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, TypeTerm >) {
+        let ty = self.get_type();
+        match self {
+            MorphismInstance::Primitive { ψ, σ, morph } => {
+                ψ.apply_subst(γ);
+                for (n,t) in σ.iter_mut() {
+                    t.apply_subst(γ);
+                }
+                for (n,t) in γ.iter() {
+                    if let TypeID::Var(varid) = n {
+                        if morph.get_type().src_type.apply_subst(σ).contains_var(*varid)
+                        || morph.get_type().dst_type.apply_subst(σ).contains_var(*varid) {
+                            σ.insert(n.clone(), t.clone());
+                        }
+                    }
+                }
+            },
+            MorphismInstance::Chain { path } => {
+                for n in path.iter_mut() {
+                    n.apply_subst(γ);
+                }
+            }
+            MorphismInstance::MapSeq { ψ, seq_repr, item_morph } => {
+                ψ.apply_subst(γ);
+                item_morph.apply_subst(γ);
+            }
+            MorphismInstance::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
+                for (_,ty) in member_morph {
+                    ty.apply_subst(γ);
+                }
+            },
+            MorphismInstance::MapEnum { ψ, enum_repr, variant_morph } => {
+                for (_,ty) in variant_morph {
+                    ty.apply_subst(γ);
+                }
+            }
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_base.rs

@@ -0,0 +1,190 @@
+use {
+    crate::{
+        morphism_path::{MorphismPath, ShortestPathProblem},
+        morphism::{MorphismInstance, Morphism, MorphismType},
+        TypeTerm, StructMember, TypeDict, TypeID
+    }, std::io::{Read, Write}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismBase<M: Morphism + Clone> {
+    morphisms: Vec< M >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<M: Morphism + Clone> MorphismBase<M> {
+    pub fn new() -> Self {
+        MorphismBase {
+            morphisms: Vec::new()
+        }
+    }
+
+    pub fn add_morphism(&mut self, m: M) {
+        self.morphisms.push( m );
+    }
+
+    pub fn get_morphism_instance(&self, ty: &MorphismType) -> Option<MorphismInstance<M>> {
+        if let Some(path) = ShortestPathProblem::new(self, ty.clone()).solve() {
+            if path.len() == 1 {
+                Some(path[0].clone())
+            } else {
+                Some(MorphismInstance::Chain { path })
+            }
+        } else {
+            None
+        }
+    }
+
+    pub fn complex_morphism_decomposition(&self, src_type: &TypeTerm, dst_type: &TypeTerm) -> Option< MorphismInstance<M> > {
+        let (src_ψ, src_floor) = src_type.get_floor_type();
+        let (dst_ψ, dst_floor) = dst_type.get_floor_type();
+
+        if !dst_ψ.is_empty() {
+            if !crate::constraint_system::subtype_unify(&src_ψ, &dst_ψ).is_ok() {
+                return None;
+            }
+        }
+
+        match (src_floor, dst_floor) {
+            (TypeTerm::Struct{ struct_repr: struct_repr_lhs, members: members_lhs},
+                TypeTerm::Struct { struct_repr: struct_repr_rhs, members: members_rhs })
+            => {
+                // todo: optimization: check if struct repr match
+
+                let mut member_morph = Vec::new();
+                let mut failed = false;
+                let mut necessary = false;
+
+                for StructMember{ symbol: symbol_rhs, ty: ty_rhs } in members_rhs.iter() {
+                    let mut found_src_member = false;
+                    for StructMember{ symbol: symbol_lhs, ty: ty_lhs } in members_lhs.iter() {
+                        if symbol_rhs == symbol_lhs {
+                            found_src_member = true;
+
+                            if let Some(mm) = self.get_morphism_instance(&MorphismType { src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+                                if ty_lhs != ty_rhs {
+                                    necessary = true;
+                                }
+                                member_morph.push((symbol_lhs.clone(), mm))
+                            } else {
+                                failed = true;
+                            }
+                            break;
+                        }
+                    }
+
+                    // member of rhs not found in lhs
+                    if ! found_src_member {
+                        failed = true;
+                        break;
+                    }
+                }
+
+                if ! failed && necessary {
+                    Some(MorphismInstance::MapStruct {
+                        ψ: src_ψ,
+                        src_struct_repr: struct_repr_lhs.clone(),
+                        dst_struct_repr: struct_repr_rhs.clone(),
+                        member_morph
+                    })
+                } else {
+                    None
+                }
+            }
+
+
+            (TypeTerm::Seq{ seq_repr: seq_repr_lhs, items: items_lhs },
+                TypeTerm::Seq{ seq_repr: _seq_rerpr_rhs, items: items_rhs })
+            => {
+                //let mut item_morphs = Vec::new();
+
+                for (ty_lhs, ty_rhs) in items_lhs.iter().zip(items_rhs.iter()) {
+                    if let Some(item_morph) = self.get_morphism_instance(&MorphismType{ src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+                        return Some(MorphismInstance::MapSeq { ψ: src_ψ, seq_repr: seq_repr_lhs.clone(), item_morph: Box::new(item_morph) });
+                    }
+                    break;
+                }
+                None
+            }
+
+            _ => {
+                None
+            }
+        }
+    }
+
+    pub fn enum_morphisms_from(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
+        let mut morphs = Vec::new();
+
+        //eprintln!("enum morphisms from {:?}", src_type);
+        for m in self.morphisms.iter() {
+            let m_src_type = m.get_type().src_type;
+            let m_dst_type = m.get_type().dst_type;
+
+            /* 1. primitive morphisms */
+
+            // check if the given start type is compatible with the
+            // morphisms source type,
+            // i.e. check if `src_type` is a subtype of `m_src_type`
+            if let Ok((ψ, σ)) = crate::constraint_system::subtype_unify(src_type, &m_src_type) {
+                let morph_inst = MorphismInstance::Primitive { ψ, σ, morph: m.clone() };
+                //eprintln!("..found direct morph to {:?}", morph_inst.get_type().dst_type);
+                morphs.push(morph_inst);
+            }
+
+            /* 2. check complex types */
+            else if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
+                //eprintln!("found complex morph to {:?}", complex_morph.get_type().dst_type);
+                morphs.push(complex_morph);
+            }
+        }
+
+        morphs
+    }
+
+
+    pub fn to_dot(&self, dict: &mut impl TypeDict) -> String {
+        let mut dot_source = String::new();
+
+        dot_source.push_str("digraph MorphismGraph {");
+
+        pub fn ty_to_dot_label(dict: &mut impl TypeDict, ty: &TypeTerm) -> String {
+            let pretty_str = ty.pretty(dict, 0);
+            let mut child = std::process::Command::new("aha").arg("--no-header")
+                .stdin( std::process::Stdio::piped() )
+                .stdout(std::process::Stdio::piped())
+                .spawn().expect("spawn child");
+            let mut stdin = child.stdin.take().expect("cant get stdin");
+            std::thread::spawn(move ||{ stdin.write_all(pretty_str.as_bytes()).expect("failed to write")});
+            let out = child.wait_with_output().expect("");
+            let html_str = String::from_utf8_lossy(&out.stdout).replace("\n", "<BR/>").replace("span", "B");
+            html_str
+        }
+
+        // add vertices
+        for (i,m) in self.morphisms.iter().enumerate() {
+            dot_source.push_str(&format!("
+                SRC{} [label=<{}>]
+                DST{} [label=<{}>]
+
+                SRC{} -> DST{} [label=\"{}\"]
+            ", i, ty_to_dot_label(dict, &m.get_type().src_type),
+                i, ty_to_dot_label(dict, &m.get_type().dst_type),
+                i,i,i
+            ));
+        }
+
+        // add edges
+
+
+        dot_source.push_str("}");
+
+        dot_source
+    }
+
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_path.rs

@@ -0,0 +1,105 @@
+use {
+    crate::{
+        dict::*,
+        morphism::{Morphism, MorphismType, MorphismInstance},
+        morphism_base::MorphismBase,
+        substitution::Substitution,
+        term::*, desugared_term::*,
+    }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismPath<M: Morphism + Clone> {
+    pub weight: u64,
+    pub cur_type: TypeTerm,
+    pub morphisms: Vec< MorphismInstance<M> >
+}
+
+
+impl<M: Morphism+Clone> MorphismPath<M> {
+    fn apply_subst(&mut self, σ: &std::collections::HashMap<TypeID, TypeTerm>) {
+        for m in self.morphisms.iter_mut() {
+            m.apply_subst(σ);
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub struct ShortestPathProblem<'a, M: Morphism + Clone> {
+    pub morphism_base: &'a MorphismBase<M>,
+    pub goal: TypeTerm,
+    queue: Vec< MorphismPath<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
+    pub fn new(morphism_base: &'a MorphismBase<M>, ty: MorphismType) -> Self {
+        ShortestPathProblem {
+            morphism_base,
+            queue: vec![
+                MorphismPath::<M> { weight: 0, cur_type: ty.src_type, morphisms: vec![] }
+            ],
+            goal: ty.dst_type
+        }
+    }
+
+    pub fn advance(&mut self, prev_path: &MorphismPath<M>, morph_inst: MorphismInstance<M>) {
+        let dst_type = morph_inst.get_type().dst_type;
+        //eprintln!("try morph to {:?}", dst_type.clone());//.sugar(type_dict).pretty(type_dict, 0));
+
+        let mut creates_loop = false;
+
+        let mut new_path = prev_path.clone();
+        new_path.apply_subst(&morph_inst.get_subst());
+        for m in new_path.morphisms.iter() {
+            if m.get_type().src_type == dst_type {
+                creates_loop = true;
+                break;
+            }
+        }
+
+        if ! creates_loop {
+            new_path.weight += 1;//next_morph_inst.get_weight();
+            new_path.cur_type = dst_type;
+
+            new_path.morphisms.push(morph_inst);
+            self.queue.push(new_path);
+        }
+    }
+
+    pub fn solve(&mut self) -> Option< Vec<MorphismInstance<M>> > {
+        while ! self.queue.is_empty() {
+            /* take the shortest partial path and try to advance it by one step */
+            self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
+            if let Some(mut cur_path) = self.queue.pop() {
+
+                /* 1. Check if goal is already reached by the current path */
+                if let Ok((_ψ, σ)) = crate::constraint_system::subtype_unify( &cur_path.cur_type, &self.goal ) {
+                    /* found path,
+                     * now apply substitution and trim to variables in terms of each step
+                     */
+                    cur_path.apply_subst(&σ);
+                    return Some(cur_path.morphisms);
+                }
+
+                /* 2. Try to advance current path */
+                else if let Some(complex_morph) =
+                    self.morphism_base.complex_morphism_decomposition( &cur_path.cur_type, &self.goal )
+                {
+                    self.advance(&cur_path, complex_morph);
+                }
+
+                for next_morph_inst in self.morphism_base.enum_morphisms_from(&cur_path.cur_type) {
+                    self.advance(&cur_path, next_morph_inst);
+                }
+            }
+        }
+        None
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/parser.rs

@@ -1,10 +1,8 @@
 use {
-    std::iter::Peekable,
     crate::{
-        dict::*,
-        term::*,
-        lexer::*
-    }
+        dict::*, lexer::*, desugared_term::*, TypeTerm, term::*
+
+    }, std::iter::Peekable
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -18,10 +16,29 @@ pub enum ParseError {
     UnexpectedToken
 }
 
+pub trait ParseLadderType {
+    fn parse(&mut self, s:&str) -> Result<TypeTerm, ParseError>;
+
+    fn parse_desugared(&mut self, s: &str) -> Result<DesugaredTypeTerm, ParseError>;
+
+    fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
+    where It: Iterator<Item = char>;
+
+    fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
+    where It: Iterator<Item = char>;
+
+    fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
+    where It: Iterator<Item = char>;
+}
+
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeDict {
-    pub fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
+impl<T: TypeDict> ParseLadderType for T {
+    fn parse(&mut self, s:&str) -> Result<TypeTerm, ParseError> {
+        Ok(self.parse_desugared(s)?.sugar(self))
+    }
+
+    fn parse_desugared(&mut self, s: &str) -> Result<DesugaredTypeTerm, ParseError> {
         let mut tokens = LadderTypeLexer::from(s.chars()).peekable();
 
         match self.parse_ladder(&mut tokens) {
@@ -36,7 +53,7 @@ impl TypeDict {
         }
     }
 
-    fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+    fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
     where It: Iterator<Item = char>
     {
         let mut args = Vec::new();
@@ -44,7 +61,7 @@ impl TypeDict {
             match tok {
                 Ok(LadderTypeToken::Close) => {
                     tokens.next();
-                    return Ok(TypeTerm::App(args));
+                    return Ok(DesugaredTypeTerm::App(args));
                 }
                 _ => {
                     match self.parse_ladder(tokens) {
@@ -57,7 +74,7 @@ impl TypeDict {
         Err(ParseError::UnexpectedEnd)
     }
 
-    fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+    fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
     where It: Iterator<Item = char>
     {
         match tokens.next() {
@@ -65,21 +82,21 @@ impl TypeDict {
             Some(Ok(LadderTypeToken::Close)) => Err(ParseError::UnexpectedClose),
             Some(Ok(LadderTypeToken::Ladder)) => Err(ParseError::UnexpectedLadder),
             Some(Ok(LadderTypeToken::Symbol(s))) =>
-                Ok(TypeTerm::TypeID(
+                Ok(DesugaredTypeTerm::TypeID(
                     if let Some(tyid) = self.get_typeid(&s) {
                         tyid
                     } else {
                         self.add_typename(s)
                     }
                 )),
-            Some(Ok(LadderTypeToken::Char(c))) => Ok(TypeTerm::Char(c)),
-            Some(Ok(LadderTypeToken::Num(n))) => Ok(TypeTerm::Num(n)),
+            Some(Ok(LadderTypeToken::Char(c))) => Ok(DesugaredTypeTerm::Char(c)),
+            Some(Ok(LadderTypeToken::Num(n))) => Ok(DesugaredTypeTerm::Num(n)),
             Some(Err(err)) => Err(ParseError::LexError(err)),
             None => Err(ParseError::UnexpectedEnd)
         }
     }
 
-    fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
+    fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<DesugaredTypeTerm, ParseError>
     where It: Iterator<Item = char>
     {
         let mut rungs = Vec::new();
@@ -88,7 +105,7 @@ impl TypeDict {
             Ok(t) => { rungs.push(t); }
             Err(err) => { return Err(err); }
         }
-        
+
         while let Some(tok) = tokens.peek() {
             match tok {
                 Ok(LadderTypeToken::Ladder) => {
@@ -100,7 +117,7 @@ impl TypeDict {
                             Err(err) => { return Err(err); }
                         }
                     } else {
-                        return Err(ParseError::UnexpectedLadder);    
+                        return Err(ParseError::UnexpectedLadder);
                     }
                 }
                 Err(lexerr) => {
@@ -115,7 +132,7 @@ impl TypeDict {
         match rungs.len() {
             0 => Err(ParseError::UnexpectedEnd),
             1 => Ok(rungs[0].clone()),
-            _ => Ok(TypeTerm::Ladder(rungs)),
+            _ => Ok(DesugaredTypeTerm::Ladder(rungs)),
         }
     }
 }

src/pnf.rs

@@ -1,8 +1,10 @@
-use crate::term::TypeTerm;
+use crate::{term::TypeTerm, constraint_system, EnumVariant, StructMember};
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm >  ) -> Vec< TypeTerm > {
+    eprintln!("splice ladders {:?} <<<====>>>  {:?} ", upper, lower);
+    // check for overlap
     for i in 0 .. upper.len() {
         if upper[i] == lower[0] {
             let mut result_ladder = Vec::<TypeTerm>::new();
@@ -12,6 +14,7 @@ pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm >  )
         }
     }
 
+    // no overlap found, just concatenate ladders
     upper.append(&mut lower);
     upper
 }
@@ -24,112 +27,305 @@ impl TypeTerm {
     /// <Seq <Digit 10>>~<Seq Char>
     /// ⇒ <Seq <Digit 10>~Char>
     /// ```
-    pub fn param_normalize(mut self) -> Self {
+    pub fn normalize(mut self) -> Self {
         match self {
             TypeTerm::Ladder(mut rungs) => {
-                if rungs.len() > 0 {
-                    let mut new_rungs = Vec::new();
-                    while let Some(bottom) = rungs.pop() {
-                        if let Some(last_but) = rungs.last_mut() {
-                            match (bottom, last_but) {
-                                (TypeTerm::App(bot_args), TypeTerm::App(last_args)) => {
-                                    if bot_args.len() == last_args.len() {
-                                        let mut new_rung_params = Vec::new();
-                                        let mut require_break = false;
+                if rungs.len() == 0 {
+                    return TypeTerm::unit();
+                } else if rungs.len() == 1 {
+                    return rungs.pop().unwrap().normalize();
+                }
 
-                                        if bot_args.len() > 0 {
-                                            if let Ok(_idx) =  last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
-                                                for i in 0 .. bot_args.len() {
+                let mut new_rungs = Vec::new();
+                let mut r2 = rungs.pop().unwrap().strip();
+                while let Some(r1) = rungs.pop() {
+                    let r1 = r1.strip();
+                    match (r1.clone(), r2.clone()) {
+                        (TypeTerm::Seq { seq_repr: seq_repr1, items: items1 },
+                         TypeTerm::Seq { seq_repr: seq_repr2, items: items2 })
+                        => {
+                            r2 = TypeTerm::Seq {
+                                    seq_repr:
+                                        if seq_repr1.is_some() || seq_repr2.is_some() {
+                                            let sr1 = if let Some(seq_repr1) = seq_repr1 { *seq_repr1.clone() }
+                                                        else { TypeTerm::unit() };
+                                            let sr2 = if let Some(seq_repr2) = seq_repr2 { *seq_repr2 }
+                                                        else { TypeTerm::unit() };
 
-                                                    let spliced_type_ladder = splice_ladders(
-                                                        last_args[i].clone().get_lnf_vec(),
-                                                        bot_args[i].clone().get_lnf_vec()
-                                                    );
-                                                    let spliced_type =
-                                                        if spliced_type_ladder.len() == 1 {
-                                                            spliced_type_ladder[0].clone()
-                                                        } else if spliced_type_ladder.len() > 1 {
-                                                            TypeTerm::Ladder(spliced_type_ladder)
-                                                        } else {
-                                                            TypeTerm::unit()
-                                                        };
-
-                                                    new_rung_params.push( spliced_type.param_normalize() );
-                                                }
-
-                                            } else {
-                                                new_rung_params.push(
-                                                    TypeTerm::Ladder(vec![
-                                                        last_args[0].clone(),
-                                                        bot_args[0].clone()
-                                                    ]).normalize()
-                                                );
-
-                                                for i in 1 .. bot_args.len() {
-                                                    if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
-                                                        let spliced_type_ladder = splice_ladders(
-                                                            last_args[i].clone().get_lnf_vec(),
-                                                            bot_args[i].clone().get_lnf_vec()
-                                                        );
-                                                        let spliced_type =
-                                                            if spliced_type_ladder.len() == 1 {
-                                                                spliced_type_ladder[0].clone()
-                                                            } else if spliced_type_ladder.len() > 1 {
-                                                                TypeTerm::Ladder(spliced_type_ladder)
-                                                            } else {
-                                                                TypeTerm::unit()
-                                                            };
-
-                                                        new_rung_params.push( spliced_type.param_normalize() );
-                                                    } else {
-                                                        new_rung_params.push( bot_args[i].clone() );
-                                                        require_break = true;
-                                                    }
-                                                }
-                                            }
-                                        }
-
-                                        if require_break {
-                                            new_rungs.push( TypeTerm::App(new_rung_params) );
+                                            Some(Box::new(
+                                                if sr1 == sr2 {
+                                                    sr1
+                                                } else if sr1 == TypeTerm::unit() {
+                                                    sr2
+                                                } else {
+                                                    TypeTerm::Ladder(vec![ sr1, sr2 ]).normalize()
+                                                }))
                                         } else {
-                                            rungs.pop();
-                                            rungs.push(TypeTerm::App(new_rung_params));
-                                        }
+                                            None
+                                        },
+                                    items:
+                                        items1.into_iter()
+                                            .zip(items2.into_iter())
+                                            .map(|(item1, item2)| {
+                                                if item1 == item2 {
+                                                    item1
+                                                } else {
+                                                    TypeTerm::Ladder(vec![ item1.clone(), item2 ])
+                                                }
+                                            })
+                                            .collect()
+                                };
+                        }
 
-                                    } else {
-                                        new_rungs.push( TypeTerm::App(bot_args) );
+                        (TypeTerm::Seq { seq_repr, items },
+                         TypeTerm::Spec( mut args )
+                        ) => {
+                            if args.len() == items.len()+1 {
+                                r2 = TypeTerm::Seq {
+                                    seq_repr: Some(Box::new(TypeTerm::Ladder(vec![
+                                        if let Some(seq_repr) = seq_repr {
+                                            *seq_repr.clone()
+                                        } else {
+                                            TypeTerm::unit()
+                                        },
+                                        args.remove(0)
+                                    ]).normalize())),
+
+                                    items: items.into_iter()
+                                        .zip(args.into_iter())
+                                        .map(|(i1, i2)| {
+                                            if i1 == i2 {
+                                                i1
+                                            } else {
+                                                TypeTerm::Ladder(vec![ i1, i2 ]).normalize()
+                                            }
+                                        })
+                                        .collect()
+                                };
+                            } else {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            }
+                        }
+
+                        (TypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
+                         TypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
+
+                            let mut condensed_struct_repr = None;
+                            let mut condensed_members = Vec::new();
+                            let mut require_break = false;
+
+
+                            if let Some(struct_repr1) = struct_repr1 {
+                                if let Some(struct_repr2) = struct_repr2 {
+                                    condensed_struct_repr = Some(Box::new(TypeTerm::Ladder(
+                                        vec![
+                                            struct_repr1.as_ref().clone(),
+                                            struct_repr2.as_ref().clone()
+                                        ]
+                                    ).normalize()))
+                                } else {
+                                    condensed_struct_repr = Some(Box::new(struct_repr1.as_ref().clone()));
+                                }
+                            } else {
+                                condensed_struct_repr = struct_repr2.clone();
+                            }
+
+                            for StructMember{ symbol: symbol2, ty: ty2 } in members2.iter() {
+                                let mut found = false;
+                                for StructMember{ symbol: symbol1, ty: ty1 } in members1.iter() {
+                                    if symbol2 == symbol1 {
+                                        condensed_members.push(StructMember {
+                                            symbol: symbol1.clone(),
+                                            ty: TypeTerm::Ladder(vec![
+                                                ty1.clone(),
+                                                ty2.clone()
+                                            ]).normalize()
+                                        });
+
+                                        found = true;
+                                        break;
                                     }
                                 }
-                                (bottom, last_buf) => {
-                                    new_rungs.push( bottom );
+
+                                if ! found {
+                                    require_break = true;
                                 }
                             }
-                        } else {
-                            new_rungs.push( bottom );
+
+                            if require_break {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            } else {
+                                r2 = TypeTerm::Struct {
+                                    struct_repr: condensed_struct_repr,
+                                    members: condensed_members
+                                };
+                            }
+                        }
+
+                        (TypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
+                         TypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
+                            let mut condensed_enum_repr = None;
+                            let mut condensed_variants = Vec::new();
+                            let mut require_break = false;
+
+                            if let Some(enum_repr1) = enum_repr1 {
+                                if let Some(enum_repr2) = enum_repr2 {
+                                    condensed_enum_repr = Some(Box::new(TypeTerm::Ladder(
+                                        vec![
+                                            enum_repr1.as_ref().clone(),
+                                            enum_repr2.as_ref().clone()
+                                        ]
+                                    ).normalize()))
+                                } else {
+                                    condensed_enum_repr = Some(Box::new(enum_repr1.as_ref().clone()));
+                                }
+                            } else {
+                                condensed_enum_repr = enum_repr2.clone();
+                            }
+
+                            for EnumVariant{ symbol: symbol2, ty: ty2 } in variants2.iter() {
+                                let mut found = false;
+                                for EnumVariant{ symbol: symbol1, ty: ty1 } in variants1.iter() {
+                                    if symbol2 == symbol1 {
+                                        condensed_variants.push(EnumVariant {
+                                            symbol: symbol1.clone(),
+                                            ty: TypeTerm::Ladder(vec![
+                                                ty1.clone(),
+                                                ty2.clone()
+                                            ]).normalize()
+                                        });
+
+                                        found = true;
+                                        break;
+                                    }
+                                }
+
+                                if ! found {
+                                    require_break = true;
+                                }
+                            }
+
+                            if require_break {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            } else {
+                                r2 = TypeTerm::Enum {
+                                    enum_repr: condensed_enum_repr,
+                                    variants: condensed_variants
+                                };
+                            }
+                        }
+
+                        (TypeTerm::Spec(args1), TypeTerm::Spec(args2)) => {
+                            if args1.len() == args2.len() {
+                                if let Ok((ψ,σ)) = constraint_system::subtype_unify(&args1[0], &args2[0]) {
+                                    let mut new_args = Vec::new();
+
+                                    for (a1, a2) in args1.into_iter().zip(args2.into_iter()) {
+                                        new_args.push(TypeTerm::Ladder(vec![ a1, a2 ]).normalize());
+                                    }
+
+                                    r2 = TypeTerm::Spec(new_args);
+                                    //new_rungs.push(r2.clone());
+                                } else {
+                                    new_rungs.push(r2);
+                                    r2 = r1;
+                                }
+                            } else {
+                                new_rungs.push(r2);
+                                r2 = r1;
+                            }
+                        }
+
+                        (TypeTerm::Univ(args1), TypeTerm::Univ(args2)) => {
+                            todo!();
+                        }
+
+                        (TypeTerm::Func(args1), TypeTerm::Func(args2)) => {
+                            todo!();
+                        }
+
+                        (TypeTerm::Morph(args1), TypeTerm::Morph(args2)) => {
+                            todo!();
+                        }
+
+                        (TypeTerm::Ladder(rr1), TypeTerm::Ladder(rr2)) => {
+                            if rr1.len() > 0 {
+                                let l = splice_ladders(rr1, rr2);
+                                r2 = TypeTerm::Ladder(l).normalize();
+                            }
+                        }
+
+                        (atomic1, TypeTerm::Ladder(mut rr2)) => {
+                            if !atomic1.is_empty() {
+                                if rr2.first() != Some(&atomic1) {
+                                    rr2.insert(0, atomic1);
+                                }
+                            }
+                            r2 = TypeTerm::Ladder(rr2).normalize();
+                        }
+
+
+                        (TypeTerm::Ladder(mut rr1), atomic2) => {
+                            if !atomic2.is_empty() {
+                                if rr1.last() != Some(&atomic2) {
+                                    rr1.push(atomic2);
+                                }
+                            }
+                            r2 = TypeTerm::Ladder(rr1).normalize();
+                        }
+
+
+                        (atomic1, atomic2) => {
+                            if atomic1.is_empty() {
+                            } else if atomic1 == atomic2 {
+                            } else if atomic2.is_empty() {
+                                r2 = atomic1;
+                            } else {
+                                new_rungs.push(atomic2);
+                                r2 = atomic1;
+                            }
                         }
                     }
+                }
 
+                if new_rungs.len() > 0 {
+                    new_rungs.push(r2);
                     new_rungs.reverse();
-
-                    if new_rungs.len() > 1 {
-                        TypeTerm::Ladder(new_rungs)
-                    } else if new_rungs.len() == 1 {
-                        new_rungs[0].clone()
-                    } else {
-                        TypeTerm::unit()
-                    }
+                    return TypeTerm::Ladder(new_rungs);
                 } else {
-                    TypeTerm::unit()
+                    return r2;
                 }
             }
 
-            TypeTerm::App(params) => {
-                TypeTerm::App(
+            TypeTerm::Spec(params) => {
+                TypeTerm::Spec(
                     params.into_iter()
-                        .map(|p| p.param_normalize())
+                        .map(|p| p.normalize())
                         .collect())
             }
 
+            TypeTerm::Seq { seq_repr, items } => TypeTerm::Seq {
+                seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.normalize())) } else { None },
+                items: items.into_iter().map(|p| p.normalize()).collect()
+            },
+            TypeTerm::Struct { struct_repr, members } => TypeTerm::Struct {
+                struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.normalize())) } else { None },
+                members: members.into_iter()
+                    .map(|StructMember{symbol, ty}|
+                        StructMember{ symbol, ty: ty.normalize() })
+                    .collect()
+            },
+            TypeTerm::Enum { enum_repr, variants } => TypeTerm::Enum {
+                enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.normalize())) } else { None },
+                variants: variants.into_iter()
+                    .map(|EnumVariant{symbol, ty}|
+                        EnumVariant{ symbol, ty: ty.normalize() })
+                    .collect()
+            },
+
             atomic => atomic
         }
     }

src/pretty.rs

@@ -1,26 +1,48 @@
 use {
-    crate::TypeDict,
-    crate::sugar::SugaredTypeTerm,
+    crate::{dict::TypeID, term::TypeTerm, StructMember, EnumVariant, TypeDict},
     tiny_ansi::TinyAnsi
 };
 
-impl SugaredTypeTerm {
-    pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+
+impl StructMember {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
+        format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
+    }
+}
+impl EnumVariant {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
+        format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
+    }
+}
+
+impl TypeTerm {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
         let indent_width = 4;
         match self {
-            SugaredTypeTerm::TypeID(id) => {
-                format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue()
+            TypeTerm::TypeID(id) => {
+                match id {
+                    TypeID::Var(varid) => {
+                        format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_magenta()
+                    },
+                    TypeID::Fun(funid) => {
+                        format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).blue().bold()
+                    }
+                }
             },
 
-            SugaredTypeTerm::Num(n) => {
-                format!("{}", n).bright_cyan()
+            TypeTerm::Num(n) => {
+                format!("{}", n).green().bold()
             }
 
-            SugaredTypeTerm::Char(c) => {
-                format!("'{}'", c)
+            TypeTerm::Char(c) => {
+                match c {
+                    '\0' => format!("'\\0'"),
+                    '\n' => format!("'\\n'"),
+                    _ => format!("'{}'", c)
+                }
             }
 
-            SugaredTypeTerm::Univ(t) => {
+            TypeTerm::Univ(t) => {
                 format!("{} {} . {}",
                     "∀".yellow().bold(),
                     dict.get_varname(0).unwrap_or("??".into()).bright_blue(),
@@ -28,9 +50,9 @@ impl SugaredTypeTerm {
                 )
             }
 
-            SugaredTypeTerm::Spec(args) => {
+            TypeTerm::Spec(args) => {
                 let mut s = String::new();
-                s.push_str(&"<".yellow().bold());
+                s.push_str(&"<".yellow());
                 for i in 0..args.len() {
                     let arg = &args[i];
                     if i > 0 {
@@ -38,19 +60,24 @@ impl SugaredTypeTerm {
                     }
                     s.push_str( &arg.pretty(dict,indent+1) );
                 }
-                s.push_str(&">".yellow().bold());
+                s.push_str(&">".yellow());
                 s
             }
 
-            SugaredTypeTerm::Struct(args) => {
+            TypeTerm::Struct{ struct_repr, members } => {
                 let mut s = String::new();
                 s.push_str(&"{".yellow().bold());
-                for arg in args {
+
+                if let Some(struct_repr) = struct_repr {
+                    s.push_str(&format!("{}{} ", "~".yellow(), struct_repr.pretty(dict, indent+1)));
+                }
+
+                for member in members {
                     s.push('\n');
                     for x in 0..(indent+1)*indent_width {
                         s.push(' ');
                     }
-                    s.push_str(&arg.pretty(dict, indent + 1));
+                    s.push_str(&member.pretty(dict, indent + 1));
                     s.push_str(&";\n".bright_yellow());
                 }
 
@@ -62,11 +89,16 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Enum(args) => {
+            TypeTerm::Enum{ enum_repr, variants } => {
                 let mut s = String::new();
                 s.push_str(&"(".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
+
+                if let Some(enum_repr) = enum_repr {
+                    s.push_str(&format!("{}{} ", "~".yellow(), enum_repr.pretty(dict, indent+1)));
+                }
+
+
+                for (i,variant) in variants.iter().enumerate() {
                     s.push('\n');
                     for x in 0..(indent+1)*indent_width {
                         s.push(' ');
@@ -74,7 +106,7 @@ impl SugaredTypeTerm {
                     if i > 0 {
                         s.push_str(&"| ".yellow().bold());
                     }
-                    s.push_str(&arg.pretty(dict, indent + 1));
+                    s.push_str(&variant.pretty(dict, indent + 1));
                 }
 
                 s.push('\n');
@@ -85,21 +117,26 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Seq(args) => {
+            TypeTerm::Seq{ seq_repr, items } => {
                 let mut s = String::new();
-                s.push_str(&"[ ".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
+                s.push_str(&"[".yellow().bold());
+
+                if let Some(seq_repr) = seq_repr {
+                    s.push_str(&format!("{}{}", "~".yellow(), seq_repr.pretty(dict, indent+1)));
+                }
+                s.push(' ');
+
+                for (i, item) in items.iter().enumerate() {
                     if i > 0 {
                         s.push(' ');
                     }
-                    s.push_str(&arg.pretty(dict, indent+1));
+                    s.push_str(&item.pretty(dict, indent+1));
                 }
                 s.push_str(&" ]".yellow().bold());
                 s
             }
 
-            SugaredTypeTerm::Morph(args) => {
+            TypeTerm::Morph(args) => {
                 let mut s = String::new();
                 for arg in args {
                     s.push_str(&"  ~~morph~~>  ".bright_yellow());
@@ -108,7 +145,7 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Func(args) => {
+            TypeTerm::Func(args) => {
                 let mut s = String::new();
                 for i in 0..args.len() {
                     let arg = &args[i];
@@ -116,7 +153,7 @@ impl SugaredTypeTerm {
                         s.push('\n');
                         for x in 0..(indent*indent_width) {
                             s.push(' ');
-                        }                
+                        }
                         s.push_str(&"-->  ".bright_yellow());
                     } else {
 //                        s.push_str("   ");
@@ -126,7 +163,7 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Ladder(rungs) => {
+            TypeTerm::Ladder(rungs) => {
                 let mut s = String::new();
                 for i in 0..rungs.len() {
                     let rung = &rungs[i];
@@ -144,5 +181,3 @@ impl SugaredTypeTerm {
         }
     }
 }
-
-

src/steiner_tree.rs

@@ -0,0 +1,250 @@
+use {
+    crate::{
+        Morphism, MorphismType, MorphismBase,
+        TypeTerm, MorphismInstance, TypeID, DesugaredTypeTerm
+    }, std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SteinerTree {
+    weight: u64,
+    goals: Vec< TypeTerm >,
+    pub edges: Vec< MorphismType >,
+}
+
+impl SteinerTree {
+    pub fn into_edges(self) -> Vec< MorphismType > {
+        self.edges
+    }
+
+    fn add_edge(&mut self, ty: MorphismType) {
+        self.weight += 1;
+
+        let ty = ty.normalize();
+
+        // check if by adding this new edge, we reach a goal
+        let mut new_goals = Vec::new();
+        let mut added = false;
+
+        for g in self.goals.clone() {
+            if let Ok(σ) = crate::unify(&ty.dst_type, &g) {
+                if !added {
+                    self.edges.push(ty.clone());
+
+                    // goal reached.
+                    for e in self.edges.iter_mut() {
+                        e.src_type = e.src_type.apply_subst(&σ).clone();
+                        e.dst_type = e.dst_type.apply_subst(&σ).clone();
+                    }
+                    added = true;
+                } else {
+                    new_goals.push(g);
+                }
+            } else {
+                new_goals.push(g);
+            }
+        }
+
+        if !added {
+            self.edges.push(ty.clone());
+        }
+
+        self.goals = new_goals;
+    }
+
+    fn is_solved(&self) -> bool {
+        self.goals.len() == 0
+    }
+
+    fn contains(&self, t: &TypeTerm) -> Option< HashMap<TypeID, TypeTerm> > {
+        for e in self.edges.iter() {
+            if let Ok(σ) = crate::constraint_system::unify(&e.dst_type, t) {
+                return Some(σ)
+            }
+        }
+
+        None
+    }
+}
+
+
+pub struct PathApproxSteinerTreeSolver {
+    root: TypeTerm,
+    leaves: Vec< TypeTerm >
+}
+
+impl PathApproxSteinerTreeSolver {
+    pub fn new(
+        root: TypeTerm,
+        leaves: Vec<TypeTerm>
+    ) -> Self {
+        PathApproxSteinerTreeSolver {
+            root, leaves
+        }
+    }
+
+    pub fn solve<M: Morphism + Clone + PartialEq>(self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+        let mut edges = Vec::<MorphismType>::new();
+
+        for goal in self.leaves {
+            eprintln!("solve steiner tree: find path to goal {:?}", goal);
+            // try to find shortest path from root to current leaf
+            if let Some(new_path) = crate::morphism_path::ShortestPathProblem::new(
+                morphisms,
+                MorphismType {
+                    src_type: self.root.clone(),
+                    dst_type: goal.clone()
+                }
+            ).solve() {
+                eprintln!("path to {:?} has len {}", goal.clone(), new_path.len());
+                for morph_inst in new_path {
+                    let t = morph_inst.get_type();
+                    if ! edges.contains(&t) {
+                        eprintln!("add edge {:?}", t);
+                        edges.push(t);
+                    }
+                }
+/*
+                // reduce new path so that it does not collide with any existing path
+                let mut src_type = self.root.clone();
+                let mut new_path_iter = new_path.into_iter().peekable();
+
+                // check all existing nodes..
+
+                if new_path_iter.peek().unwrap().get_type().src_type == src_type {
+                    eprintln!("skip initial node..");
+                    new_path_iter.next();
+                }
+
+                for mt in tree.iter() {
+                    //assert!( mt.src_type == &src_type );
+                    if let Some(t) = new_path_iter.peek() {
+                        eprintln!("");
+                        if &mt.dst_type == &t.get_type().src_type {
+                            // eliminate this node from new path
+                            src_type = new_path_iter.next().unwrap().get_type().src_type;
+                        }
+                    } else {
+                        break;
+                    }
+                }
+
+                for m in new_path_iter {
+                    tree.push(m.get_type());
+                }
+*/
+            } else {
+                eprintln!("could not find path\nfrom {:?}\nto {:?}", &self.root, &goal);
+                return None;
+            }
+        }
+
+        Some(SteinerTree {
+            weight: 0,
+            goals: vec![],
+            edges
+        })
+    }
+}
+
+
+/* given a representation tree with the available
+ * represenatations `src_types`, try to find
+ * a sequence of morphisms that span up all
+ * representations in `dst_types`.
+ */
+pub struct SteinerTreeProblem {
+    src_types: Vec< TypeTerm >,
+    queue: Vec< SteinerTree >
+}
+
+impl SteinerTreeProblem {
+    pub fn new(
+        src_types: Vec< TypeTerm >,
+        dst_types: Vec< TypeTerm >
+    ) -> Self {
+        SteinerTreeProblem {
+            src_types: src_types.into_iter().map(|t| t.normalize()).collect(),
+            queue: vec![
+                SteinerTree {
+                    weight: 0,
+                    goals: dst_types.into_iter().map(|t| t.normalize()).collect(),
+                    edges: Vec::new()
+                }
+            ]
+        }
+    }
+
+    pub fn next(&mut self) -> Option< SteinerTree > {
+        eprintln!("queue size = {}", self.queue.len());
+
+        /* FIXME: by giving the highest priority to
+         * candidate tree with the least remaining goals,
+         * the optimality of the search algorithm
+         * is probably destroyed, but it dramatically helps
+         * to tame the combinatorical explosion in this algorithm.
+         */
+        self.queue.sort_by(|t1, t2|
+            if t1.goals.len() < t2.goals.len() {
+                std::cmp::Ordering::Greater
+            } else if t1.goals.len() == t2.goals.len() {
+                if t1.weight < t2.weight {
+                    std::cmp::Ordering::Greater
+                } else {
+                    std::cmp::Ordering::Less
+                }
+            } else {
+                std::cmp::Ordering::Less
+            }
+        );
+        self.queue.pop()
+    }
+/*
+    pub fn solve_approx_path<M: Morphism + Clone>(&mut self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+        if let Some(master) = self.src_types.first() {
+
+
+        }
+    }
+*/
+    pub fn solve_bfs<M: Morphism + Clone>(&mut self, morphisms: &MorphismBase<M>) -> Option< SteinerTree > {
+
+        // take the currently smallest tree and extend it by one step
+        while let Some( mut current_tree ) = self.next() {
+
+            // check if current tree is a solution
+            if current_tree.goals.len() == 0 {
+                return Some(current_tree);
+            }
+
+            // get all vertices spanned by this tree
+            let mut current_nodes = self.src_types.clone();
+            for e in current_tree.edges.iter() {
+                current_nodes.push( e.dst_type.clone() );
+            }
+
+            // extend the tree by one edge and add it to the queue
+            for src_type in current_nodes {
+                for next_morph_inst in morphisms.enum_morphisms_from(&src_type) {
+                    //let dst_type = TypeTerm::Ladder(vec![dst_halo, dst_ty]).normalize();
+                    let dst_type = next_morph_inst.get_type().dst_type;
+
+                    if current_tree.contains( &dst_type ).is_none() {
+                        let mut new_tree = current_tree.clone();
+                        {
+                            let src_type = src_type.clone();
+                            let dst_type = dst_type.clone();
+                            new_tree.add_edge(MorphismType { src_type, dst_type }.normalize());
+                        }
+
+                        self.queue.push( new_tree );
+                    }
+                }
+            }
+        }
+
+        None
+    }
+}

src/substitution.rs

@@ -0,0 +1,114 @@
+
+use std::ops::DerefMut;
+use crate::{
+    TypeID,
+    DesugaredTypeTerm
+};
+use crate::term::*;
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub trait Substitution {
+    fn get(&self, t: &TypeID) -> Option< TypeTerm >;
+    fn add(&mut self, tyid: TypeID, val: TypeTerm);
+    fn append(self, rhs: &Self) -> Self;
+}
+
+impl Substitution for std::collections::HashMap< TypeID, TypeTerm > {
+    fn get(&self, t: &TypeID) -> Option< TypeTerm > {
+        (self as &std::collections::HashMap< TypeID, TypeTerm >).get(t).cloned()
+    }
+
+    fn add(&mut self, tyid: TypeID, val: TypeTerm) {
+        if let TypeID::Var(id) = tyid {
+            if !val.contains_var(id) {
+                self.insert(tyid, val.normalize());
+            } else {
+                eprintln!("substitution cannot contain loop");
+            }
+        }
+    }
+
+    fn append(self, rhs: &Self) -> Self {
+        let mut new_σ = std::collections::HashMap::new();
+        for (v, tt) in self.iter() {
+            let mut tt = tt.clone().normalize();
+            tt.apply_subst(rhs);
+            tt.apply_subst(&self);
+            new_σ.add(v.clone(), tt);
+        }
+        for (v, tt) in rhs.iter() {
+            new_σ.add(v.clone(), tt.clone().normalize());
+        }
+
+        new_σ
+    }
+}
+
+impl TypeTerm {
+    /// 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,
+        σ: &impl Substitution
+    ) -> &mut Self {
+        self.apply_subst(σ)
+    }
+
+    pub fn apply_subst(
+        &mut self,
+        σ: &impl Substitution
+    ) -> &mut Self {
+        match self {
+            TypeTerm::Num(_) => {},
+            TypeTerm::Char(_) => {},
+
+            TypeTerm::TypeID(typid) => {
+                if let Some(t) = σ.get(typid) {
+                    *self = t;
+                }
+            }
+            TypeTerm::Ladder(args) |
+            TypeTerm::Spec(args) |
+            TypeTerm::Func(args) |
+            TypeTerm::Morph(args)
+            => {
+                for r in args.iter_mut() {
+                    r.apply_subst(σ);
+                }
+            }
+
+            TypeTerm::Univ(t) => { t.apply_subst(σ); }
+
+            TypeTerm::Struct { struct_repr, members } => {
+                if let Some(struct_repr) = struct_repr.as_mut() {
+                    struct_repr.apply_subst(σ);
+                }
+                for StructMember{ symbol:_, ty } in members.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            },
+            TypeTerm::Enum { enum_repr, variants } => {
+                if let Some(enum_repr) = enum_repr.as_mut() {
+                    enum_repr.apply_subst(σ);
+                }
+                for EnumVariant{ symbol:_, ty } in variants.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            }
+            TypeTerm::Seq { seq_repr, items } => {
+                if let Some(seq_repr) = seq_repr {
+                    seq_repr.apply_subst(σ);
+                }
+                for ty in items.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            },
+        }
+
+        self
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/subtype.rs

@@ -1,16 +1,16 @@
-use crate::term::TypeTerm;
+use crate::term::DesugaredTypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeTerm {    
+impl DesugaredTypeTerm {
     // returns ladder-step of first match and provided representation-type
-    pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
+    pub fn is_semantic_subtype_of(&self, expected_type: &DesugaredTypeTerm) -> Option<(usize, DesugaredTypeTerm)> {
         let provided_lnf = self.clone().get_lnf_vec();
         let expected_lnf = expected_type.clone().get_lnf_vec();
 
         for i in 0..provided_lnf.len() {
             if provided_lnf[i] == expected_lnf[0] {
-                return Some((i, TypeTerm::Ladder(
+                return Some((i, DesugaredTypeTerm::Ladder(
                     provided_lnf[i..].into_iter().cloned().collect()
                 )))
             }
@@ -19,7 +19,7 @@ impl TypeTerm {
         None
     }
 
-    pub fn is_syntactic_subtype_of(&self, expected_type: &TypeTerm) -> Result<usize, (usize, usize)> {
+    pub fn is_syntactic_subtype_of(&self, expected_type: &DesugaredTypeTerm) -> Result<usize, (usize, usize)> {
         if let Some((first_match, provided_type)) = self.is_semantic_subtype_of( expected_type ) {
             let provided_lnf = provided_type.get_lnf_vec();
             let expected_lnf = expected_type.clone().get_lnf_vec();
@@ -39,13 +39,38 @@ impl TypeTerm {
 
     // supertype analogs
 
-    pub fn is_semantic_supertype_of(&self, t: &TypeTerm) -> Option<(usize, TypeTerm)> {
+    pub fn is_semantic_supertype_of(&self, t: &DesugaredTypeTerm) -> Option<(usize, DesugaredTypeTerm)> {
         t.is_semantic_subtype_of(self)
     }
 
-    pub fn is_syntactic_supertype_of(&self, t: &TypeTerm) -> Result<usize, (usize, usize)> {
+    pub fn is_syntactic_supertype_of(&self, t: &DesugaredTypeTerm) -> Result<usize, (usize, usize)> {
         t.is_syntactic_subtype_of(self)
     }
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+use crate::sugar::*;
+
+impl TypeTerm {
+    pub fn is_compatible(&self, supertype: TypeTerm) -> bool {
+        match (self, supertype) {
+            (TypeTerm::TypeID(idl), TypeTerm::TypeID(idr)) => {
+                if *idl == idr {
+                    true
+                } else {
+                    false
+                }
+            }
+
+
+            (TypeTerm::Ladder(l_rungs), TypeTerm::Ladder(r_rungs)) => {
+                false
+            }
+
+            _ => {
+                false
+            }
+        }
+    }
+}

src/sugar.rs

@@ -1,95 +0,0 @@
-use {
-    crate::{TypeTerm, TypeID}
-};
-
-pub enum SugaredTypeTerm {
-    TypeID(TypeID),
-    Num(i64),
-    Char(char),
-    Univ(Box< SugaredTypeTerm >),
-    Spec(Vec< SugaredTypeTerm >),
-    Func(Vec< SugaredTypeTerm >),
-    Morph(Vec< SugaredTypeTerm >),
-    Ladder(Vec< SugaredTypeTerm >),
-    Struct(Vec< SugaredTypeTerm >),
-    Enum(Vec< SugaredTypeTerm >),
-    Seq(Vec< SugaredTypeTerm >)
-}
-
-impl TypeTerm {
-    pub fn sugar(self: TypeTerm, dict: &mut crate::TypeDict) -> SugaredTypeTerm {
-        match self {
-            TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
-            TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
-            TypeTerm::Char(c) => SugaredTypeTerm::Char(c),
-            TypeTerm::App(args) => if let Some(first) = args.first() {
-                if first == &dict.parse("Func").unwrap() {
-                    SugaredTypeTerm::Func( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Morph").unwrap() {
-                    SugaredTypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Struct").unwrap() {
-                    SugaredTypeTerm::Struct( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Enum").unwrap() {
-                    SugaredTypeTerm::Enum( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Seq").unwrap() {
-                    SugaredTypeTerm::Seq( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Spec").unwrap() {
-                    SugaredTypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
-                }
-                else if first == &dict.parse("Univ").unwrap() {
-                    SugaredTypeTerm::Univ(Box::new(
-                        SugaredTypeTerm::Spec(
-                            args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect()
-                        )
-                    ))
-                }
-                else {
-                    SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
-                }
-            } else {
-                SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
-            },
-            TypeTerm::Ladder(rungs) =>            
-               SugaredTypeTerm::Ladder(rungs.into_iter().map(|t| t.sugar(dict)).collect())
-        }
-    }
-}
-
-impl SugaredTypeTerm {
-    pub fn desugar(self, dict: &mut crate::TypeDict) -> TypeTerm {
-        match self {
-            SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
-            SugaredTypeTerm::Num(n) => TypeTerm::Num(n),
-            SugaredTypeTerm::Char(c) => TypeTerm::Char(c),
-            SugaredTypeTerm::Univ(t) => t.desugar(dict),
-            SugaredTypeTerm::Spec(ts) => TypeTerm::App(ts.into_iter().map(|t| t.desugar(dict)).collect()),
-            SugaredTypeTerm::Ladder(ts) => TypeTerm::Ladder(ts.into_iter().map(|t|t.desugar(dict)).collect()),
-            SugaredTypeTerm::Func(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Func").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
-                ).collect()),
-            SugaredTypeTerm::Morph(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Morph").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
-                ).collect()),
-            SugaredTypeTerm::Struct(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Struct").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
-                ).collect()),
-            SugaredTypeTerm::Enum(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Enum").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
-                ).collect()),
-            SugaredTypeTerm::Seq(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Seq").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
-                ).collect()),
-        }
-    }
-}
-

src/term.rs

@@ -1,113 +1,585 @@
-use crate::TypeID;
+use {
+    crate::{parser::ParseLadderType, subtype_unify, DesugaredTypeTerm, TypeDict, TypeID}
+};
 
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone, PartialEq, Eq, Hash, Debug)]
-pub enum TypeTerm {
-
-    /* Atomic Terms */
-
-    // Base types from dictionary
-    TypeID(TypeID),
-
-    // Literals
-    Num(i64),
-    Char(char),
-
-    
-
-    /* Complex Terms */
-
-    // Type Parameters
-    // avoid currying to save space & indirection
-    App(Vec< TypeTerm >),
-
-    // Type Ladders
-    Ladder(Vec< TypeTerm >),
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct StructMember {
+    pub symbol: String,
+    pub ty: TypeTerm
 }
 
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct EnumVariant {
+    pub symbol: String,
+    pub ty: TypeTerm
+}
+
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub enum TypeTerm {
+    TypeID(TypeID),
+    Num(i64),
+    Char(char),
+    Univ(Box< TypeTerm >),
+    Spec(Vec< TypeTerm >),
+    Func(Vec< TypeTerm >),
+    Morph(Vec< TypeTerm >),
+    Ladder(Vec< TypeTerm >),
+    Struct{
+        struct_repr: Option< Box<TypeTerm> >,
+        members: Vec< StructMember >
+    },
+    Enum{
+        enum_repr: Option<Box< TypeTerm >>,
+        variants: Vec< EnumVariant >
+    },
+    Seq{
+        seq_repr: Option<Box< TypeTerm >>,
+        items: Vec< TypeTerm >
+    },
+
+    /*
+    Todo: Ref, RefMut
+    */
+}
+
+impl StructMember {
+    pub fn parse( dict: &mut impl TypeDict, ty: &DesugaredTypeTerm ) -> Option<Self> {
+        match ty {
+            DesugaredTypeTerm::App(args) => {
+                if args.len() != 2 {
+                    return None;
+                }
+/*
+                if args[0] != dict.parse("Struct.Field").expect("parse") {
+                    return None;
+                }
+*/
+                let symbol = match args[0] {
+                    DesugaredTypeTerm::Char(c) => c.to_string(),
+                    DesugaredTypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
+                    _ => {
+                        return None;
+                    }
+                };
+
+                let ty = args[1].clone().sugar(dict);
+
+                Some(StructMember { symbol, ty })
+            }
+            _ => {
+                None
+            }
+        }
+    }
+}
+
+impl EnumVariant {
+    pub fn parse( dict: &mut impl TypeDict, ty: &DesugaredTypeTerm ) -> Option<Self> {
+        match ty {
+            DesugaredTypeTerm::App(args) => {
+                if args.len() != 2 {
+                    return None;
+                }
+/*
+                if args[0] != dict.parse("Enum.Variant").expect("parse") {
+                    return None;
+                }
+*/
+                let symbol = match args[0] {
+                    DesugaredTypeTerm::Char(c) => c.to_string(),
+                    DesugaredTypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
+                    _ => {
+                        return None;
+                    }
+                };
+
+                let ty = args[1].clone().sugar(dict);
+
+                Some(EnumVariant { symbol, ty })
+            }
+            _ => {
+                None
+            }
+        }
+    }
+}
+
+impl DesugaredTypeTerm {
+    pub fn sugar(self: DesugaredTypeTerm, dict: &mut impl crate::TypeDict) -> TypeTerm {
+        dict.add_varname("StructRepr".into());
+        dict.add_varname("EnumRepr".into());
+        dict.add_varname("SeqRepr".into());
+
+        match self {
+            DesugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
+            DesugaredTypeTerm::Num(n) => TypeTerm::Num(n),
+            DesugaredTypeTerm::Char(c) => TypeTerm::Char(c),
+            DesugaredTypeTerm::App(args) => if let Some(first) = args.first() {
+                if first == &dict.parse_desugared("Func").unwrap() {
+                    TypeTerm::Func( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
+                }
+                else if first == &dict.parse_desugared("Morph").unwrap() {
+                    TypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
+                }
+                else if first == &dict.parse_desugared("Seq").unwrap() {
+                    TypeTerm::Seq{
+                        seq_repr: None,
+                        items: args[1..].into_iter()
+                            .map(|t| t.clone().sugar(dict))
+                            .collect()
+                    }
+                }
+                else if first == &dict.parse_desugared("Struct").unwrap() {
+                    TypeTerm::Struct{
+                        struct_repr: None,
+                        members: args[1..].into_iter()
+                            .map(|t| StructMember::parse(dict, t).expect("cant parse field"))
+                            .collect()
+                    }
+                }
+                else if first == &dict.parse_desugared("Enum").unwrap() {
+                    TypeTerm::Enum{
+                        enum_repr: None,
+                        variants: args[1..].into_iter()
+                            .map(|t| EnumVariant::parse(dict, t).expect("cant parse variant"))
+                            .collect()
+                    }
+                }
+                else if let DesugaredTypeTerm::Ladder(mut rungs) = first.clone() {
+                    if rungs.len() > 0 {
+                        match rungs.remove(0) {
+                            DesugaredTypeTerm::TypeID(tyid) => {
+                                if tyid == dict.get_typeid(&"Seq".into()).expect("") {
+                                    TypeTerm::Seq {
+                                        seq_repr:
+                                            if rungs.len() > 0 {
+                                                Some(Box::new(
+                                                    TypeTerm::Ladder(rungs.into_iter()
+                                                        .map(|r| r.clone().sugar(dict))
+                                                        .collect()
+                                                    ).normalize()
+                                                ))
+                                            } else {
+                                                None
+                                            },
+                                        items: args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect()
+                                    }
+                                } else if tyid == dict.get_typeid(&"Struct".into()).expect("") {
+                                    TypeTerm::Struct {
+                                        struct_repr:
+                                            if rungs.len() > 0 {
+                                                Some(Box::new(
+                                                    TypeTerm::Ladder(rungs.into_iter()
+                                                        .map(|r| r.clone().sugar(dict))
+                                                        .collect()
+                                                    ).normalize()
+                                                ))
+                                            } else {
+                                                None
+                                            },
+                                        members: args[1..].into_iter()
+                                            .map(|t| StructMember::parse(dict, t).expect("cant parse field"))
+                                            .collect()
+                                    }
+                                } else if tyid == dict.get_typeid(&"Enum".into()).expect("") {
+                                    TypeTerm::Enum {
+                                        enum_repr:
+                                            if rungs.len() > 0 {
+                                                Some(Box::new(
+                                                    TypeTerm::Ladder(rungs.into_iter()
+                                                        .map(|r| r.clone().sugar(dict))
+                                                        .collect()
+                                                    ).normalize()
+                                                ))
+                                            } else {
+                                                None
+                                            },
+                                        variants: args[1..].into_iter()
+                                            .map(|t| EnumVariant::parse(dict, t).expect("cant parse field"))
+                                            .collect()
+                                    }
+                                } else {
+                                    TypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
+                                }
+                            }
+                            _ => {
+                                unreachable!();
+                            }
+                        }
+                    } else {
+                        unreachable!();
+                    }
+                }
+
+                else if first == &dict.parse_desugared("Spec").unwrap() {
+                    TypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
+                }
+                else if first == &dict.parse_desugared("Univ").unwrap() {
+                    TypeTerm::Univ(Box::new(
+                        TypeTerm::Spec(
+                            args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect()
+                        )
+                    ))
+                }
+                else {
+                    TypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
+                }
+            } else {
+                TypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
+            },
+            DesugaredTypeTerm::Ladder(rungs) =>
+               TypeTerm::Ladder(rungs.into_iter().map(|t| t.sugar(dict)).collect())
+        }
+    }
+}
+
+
+impl StructMember {
+    pub fn desugar(self, dict: &mut impl crate::TypeDict) -> DesugaredTypeTerm {
+        DesugaredTypeTerm::App(vec![
+            //dict.parse("Struct.Field").expect("parse"),
+            dict.parse_desugared(&self.symbol).expect("parse"),
+            self.ty.desugar(dict)
+        ])
+    }
+}
+
+impl EnumVariant {
+    pub fn desugar(self, dict: &mut impl crate::TypeDict) -> DesugaredTypeTerm {
+        DesugaredTypeTerm::App(vec![
+            //dict.parse("Enum.Variant").expect("parse"),
+            dict.parse_desugared(&self.symbol).expect("parse"),
+            self.ty.desugar(dict)
+        ])
+    }
+}
 
 impl TypeTerm {
     pub fn unit() -> Self {
         TypeTerm::Ladder(vec![])
     }
 
-    pub fn new(id: TypeID) -> Self {
-        TypeTerm::TypeID(id)
+    pub fn desugar(self, dict: &mut impl crate::TypeDict) -> DesugaredTypeTerm {
+        match self {
+            TypeTerm::TypeID(id) => DesugaredTypeTerm::TypeID(id),
+            TypeTerm::Num(n) => DesugaredTypeTerm::Num(n),
+            TypeTerm::Char(c) => DesugaredTypeTerm::Char(c),
+            TypeTerm::Univ(t) => t.desugar(dict),
+            TypeTerm::Spec(ts) => DesugaredTypeTerm::App(ts.into_iter().map(|t| t.desugar(dict)).collect()),
+            TypeTerm::Ladder(ts) => DesugaredTypeTerm::Ladder(ts.into_iter().map(|t|t.desugar(dict)).collect()),
+            TypeTerm::Func(ts) => DesugaredTypeTerm::App(
+                std::iter::once( dict.parse_desugared("Func").unwrap() ).chain(
+                    ts.into_iter().map(|t| t.desugar(dict))
+                ).collect()),
+            TypeTerm::Morph(ts) => DesugaredTypeTerm::App(
+                std::iter::once( dict.parse_desugared("Morph").unwrap() ).chain(
+                    ts.into_iter().map(|t| t.desugar(dict))
+                ).collect()),
+            TypeTerm::Struct{ struct_repr, members } => DesugaredTypeTerm::App(
+                std::iter::once(
+                    if let Some(sr) = struct_repr {
+                        DesugaredTypeTerm::Ladder(vec![
+                            dict.parse_desugared("Struct").unwrap(),
+                            sr.desugar(dict)
+                        ])
+                    } else {
+                        dict.parse_desugared("Struct").unwrap()
+                    }
+                ).chain(
+                    members.into_iter().map(|t| t.desugar(dict))
+                ).collect()),
+            TypeTerm::Enum{ enum_repr, variants } => DesugaredTypeTerm::App(
+                std::iter::once(
+                    if let Some(sr) = enum_repr {
+                        DesugaredTypeTerm::Ladder(vec![
+                            dict.parse_desugared("Enum").unwrap(),
+                            sr.desugar(dict)
+                        ])
+                    } else {
+                        dict.parse_desugared("Enum").unwrap()
+                    }
+                ).chain(
+                    variants.into_iter().map(|t| t.desugar(dict))
+                ).collect()),
+            TypeTerm::Seq{ seq_repr, items } => DesugaredTypeTerm::App(
+                std::iter::once(
+                    if let Some(sr) = seq_repr {
+                        DesugaredTypeTerm::Ladder(vec![
+                            dict.parse_desugared("Seq").unwrap(),
+                            sr.desugar(dict)
+                        ])
+                    } else {
+                        dict.parse_desugared("Seq").unwrap()
+                    }
+                ).chain(
+                    items.into_iter().map(|t| t.desugar(dict))
+                ).collect()),
+        }
     }
 
-    pub fn arg(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
+    pub fn contains_var(&self, var_id: u64) -> bool {
         match self {
-            TypeTerm::App(args) => {
-                args.push(t.into());
+            TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+            TypeTerm::Spec(args) |
+            TypeTerm::Func(args) |
+            TypeTerm::Morph(args) |
+            TypeTerm::Ladder(args) => {
+                for a in args.iter() {
+                    if a.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            TypeTerm::Univ(t) => {
+                t.contains_var(var_id)
+            }
+            TypeTerm::Struct { struct_repr, members } => {
+                if let Some(struct_repr) =  struct_repr {
+                    if struct_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for StructMember{ symbol, ty } in members {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            TypeTerm::Enum { enum_repr, variants } => {
+                if let Some(enum_repr) =  enum_repr {
+                    if enum_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for EnumVariant{ symbol, ty } in variants {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            TypeTerm::Seq { seq_repr, items } => {
+                if let Some(seq_repr) =  seq_repr {
+                    if seq_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for ty in items {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
             }
 
-            _ => {
-                *self = TypeTerm::App(vec![
-                    self.clone(),
-                    t.into()
-                ])                
-            }
+            TypeTerm::Num(_) |
+            TypeTerm::Char(_) |
+            TypeTerm::TypeID(TypeID::Fun(_)) => false
+        }
+    }
+
+    pub fn strip(self) -> TypeTerm {
+        if self.is_empty() {
+            return TypeTerm::unit();
         }
 
-        self
-    }
-
-    pub fn repr_as(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
         match self {
             TypeTerm::Ladder(rungs) => {
-                rungs.push(t.into());
-            }
+                let mut rungs :Vec<_> = rungs.into_iter()
+                    .filter_map(|mut r| {
+                        r = r.strip();
+                        if r != TypeTerm::unit() {
+                            Some(match r {
+                                TypeTerm::Ladder(r) => r,
+                                a => vec![ a ]
+                            })
+                        }
+                        else { None }
+                    })
+                .flatten()
+                .collect();
 
-            _ => {
-                *self = TypeTerm::Ladder(vec![
-                    self.clone(),
-                    t.into()
-                ])
+                if rungs.len() == 1 {
+                    rungs.pop().unwrap()
+                } else {
+                    TypeTerm::Ladder(rungs)
+                }
+            },
+            TypeTerm::Spec(args) => {
+                let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
+                if args.len() == 0 {
+                    TypeTerm::unit()
+                } else if args.len() == 1 {
+                    args.pop().unwrap()
+                } else {
+                    TypeTerm::Spec(args)
+                }
             }
+            TypeTerm::Seq{ mut seq_repr, mut items } => {
+                if let Some(seq_repr) = seq_repr.as_mut() {
+                    *seq_repr = Box::new(seq_repr.clone().strip());
+                }
+                for i in items.iter_mut() {
+                    *i = i.clone().strip();
+                }
+
+                TypeTerm::Seq { seq_repr, items }
+            }
+            atom => atom
         }
-
-        self
     }
 
-    pub fn num_arg(&mut self, v: i64) -> &mut Self {
-        self.arg(TypeTerm::Num(v))
-    }
 
-    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<TypeTerm>
-    ) -> &mut Self {
+    pub fn get_interface_type(&self) -> TypeTerm {
         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);
+                if let Some(top) = rungs.first() {
+                    top.get_interface_type()
+                } else {
+                    TypeTerm::unit()
                 }
             }
-            TypeTerm::App(args) => {
-                for r in args.iter_mut() {
-                    r.apply_substitution(subst);
-                }
-            }
-            _ => {}
-        }
+            TypeTerm::Spec(args)
+                => TypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
 
-        self
+            TypeTerm::Func(args)
+                => TypeTerm::Func(args.iter().map(|a| a.get_interface_type()).collect()),
+
+            TypeTerm::Morph(args)
+                => TypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
+
+            TypeTerm::Univ(t)
+                => TypeTerm::Univ(Box::new(t.get_interface_type())),
+
+            TypeTerm::Seq { seq_repr, items } => {
+                TypeTerm::Seq {
+                    seq_repr: if let Some(sr) = seq_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    items: items.iter().map(|t| t.get_interface_type()).collect()
+                }
+            }
+            TypeTerm::Struct { struct_repr, members } => {
+                TypeTerm::Struct {
+                    struct_repr: if let Some(sr) = struct_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    members: members.iter()
+                        .map(|StructMember{symbol,ty}|
+                            StructMember {symbol:symbol.clone(), ty:ty.get_interface_type() })
+                        .collect()
+                }
+            }
+            TypeTerm::Enum { enum_repr, variants } => {
+                TypeTerm::Enum {
+                    enum_repr: if let Some(sr) = enum_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    variants: variants.iter()
+                        .map(|EnumVariant{symbol,ty}|
+                            EnumVariant{ symbol:symbol.clone(), ty:ty.get_interface_type() })
+                        .collect()
+                }
+            }
+
+            TypeTerm::TypeID(tyid) => TypeTerm::TypeID(tyid.clone()),
+            TypeTerm::Num(n) => TypeTerm::Num(*n),
+            TypeTerm::Char(c) => TypeTerm::Char(*c)
+        }
+    }
+
+    pub fn get_floor_type(&self) -> (TypeTerm, TypeTerm) {
+        match self.clone() {
+            TypeTerm::Ladder(mut rungs) => {
+                if let Some(bot) = rungs.pop() {
+                    let (bot_ψ, bot_floor) = bot.get_floor_type();
+                    rungs.push(bot_ψ);
+                    (TypeTerm::Ladder(rungs).strip(), bot_floor.strip())
+                } else {
+                    (TypeTerm::unit(), TypeTerm::unit())
+                }
+            }
+            /*
+            SugaredTypeTerm::Spec(args)
+                => (SugaredTypeTerm::SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Func(args)
+                => SugaredTypeTerm::Func(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Morph(args)
+                => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Univ(t)
+                => SugaredTypeTerm::Univ(Box::new(t.get_floor_type())),
+
+            SugaredTypeTerm::Seq { seq_repr, items } => {
+                SugaredTypeTerm::Seq {
+                    seq_repr: if let Some(sr) = seq_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    items: items.iter().map(|t| t.get_floor_type()).collect()
+                }
+            }
+            SugaredTypeTerm::Struct { struct_repr, members } => {
+                SugaredTypeTerm::Struct {
+                    struct_repr: if let Some(sr) = struct_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    members: members.iter()
+                        .map(|SugaredStructMember{symbol,ty}|
+                            SugaredStructMember {symbol:symbol.clone(), ty:ty.get_floor_type() })
+                        .collect()
+                }
+            }
+            SugaredTypeTerm::Enum { enum_repr, variants } => {
+                SugaredTypeTerm::Enum {
+                    enum_repr: if let Some(sr) = enum_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    variants: variants.iter()
+                        .map(|SugaredEnumVariant{symbol,ty}|
+                            SugaredEnumVariant{ symbol:symbol.clone(), ty:ty.get_floor_type() })
+                        .collect()
+                }
+            }
+
+            SugaredTypeTerm::TypeID(tyid) => SugaredTypeTerm::TypeID(tyid.clone()),
+            SugaredTypeTerm::Num(n) => SugaredTypeTerm::Num(*n),
+            SugaredTypeTerm::Char(c) => SugaredTypeTerm::Char(*c)
+            */
+
+            other => (TypeTerm::unit(), other.clone().strip())
+        }
+    }
+
+    pub fn is_empty(&self) -> bool {
+        match self {
+            TypeTerm::TypeID(_) => false,
+            TypeTerm::Num(_) => false,
+            TypeTerm::Char(_) => false,
+            TypeTerm::Univ(t) => t.is_empty(),
+            TypeTerm::Spec(ts) |
+            TypeTerm::Ladder(ts) |
+            TypeTerm::Func(ts) |
+            TypeTerm::Morph(ts) => {
+                ts.iter().fold(true, |s,t| s && t.is_empty() )
+            }
+            TypeTerm::Seq{ seq_repr, items } => {
+                items.iter().fold(true, |s,t| s && t.is_empty() )
+            }
+            TypeTerm::Struct{ struct_repr, members } => {
+                members.iter()
+                    .fold(true, |s,member_decl| s && member_decl.ty.is_empty() )
+            }
+            TypeTerm::Enum{ enum_repr, variants } => {
+                variants.iter()
+                    .fold(true, |s,variant_decl| s && variant_decl.ty.is_empty() )
+            }
+        }
     }
 }
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/test/curry.rs

@@ -1,60 +1,60 @@
 use {
-    crate::{dict::*}
+    crate::{dict::*, parser::*}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 #[test]
 fn test_curry() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
-        dict.parse("<A B C>").unwrap().curry(),
-        dict.parse("<<A B> C>").unwrap()
+        dict.parse_desugared("<A B C>").unwrap().curry(),
+        dict.parse_desugared("<<A B> C>").unwrap()
     );
     assert_eq!(
-        dict.parse("<A B C D>").unwrap().curry(),
-        dict.parse("<<<A B> C> D>").unwrap()
+        dict.parse_desugared("<A B C D>").unwrap().curry(),
+        dict.parse_desugared("<<<A B> C> D>").unwrap()
     );
     assert_eq!(
-        dict.parse("<A B C D E F G H I J K>").unwrap().curry(),
-        dict.parse("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap()
+        dict.parse_desugared("<A B C D E F G H I J K>").unwrap().curry(),
+        dict.parse_desugared("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap()
     );
 
     assert_eq!(
-        dict.parse("<A~X B C>").unwrap().curry(),
-        dict.parse("<<A~X B> C>").unwrap()
+        dict.parse_desugared("<A~X B C>").unwrap().curry(),
+        dict.parse_desugared("<<A~X B> C>").unwrap()
     );
     assert_eq!(
-        dict.parse("<A B C~Y~Z> ~ K").unwrap().curry(),
-        dict.parse("< <A B> C~Y~Z > ~ K").unwrap()
+        dict.parse_desugared("<A B C~Y~Z> ~ K").unwrap().curry(),
+        dict.parse_desugared("< <A B> C~Y~Z > ~ K").unwrap()
     );
 }
 
 #[test]
 fn test_decurry() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
-        dict.parse("<<A B> C>").unwrap().decurry(),
-        dict.parse("<A B C>").unwrap()
+        dict.parse_desugared("<<A B> C>").unwrap().decurry(),
+        dict.parse_desugared("<A B C>").unwrap()
     );
     assert_eq!(
-        dict.parse("<<<A B> C> D>").unwrap().decurry(),
-        dict.parse("<A B C D>").unwrap(),
+        dict.parse_desugared("<<<A B> C> D>").unwrap().decurry(),
+        dict.parse_desugared("<A B C D>").unwrap(),
     );
     assert_eq!(
-        dict.parse("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap().decurry(),
-        dict.parse("<A B C D E F G H I J K>").unwrap()
+        dict.parse_desugared("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap().decurry(),
+        dict.parse_desugared("<A B C D E F G H I J K>").unwrap()
     );
-    
+
     assert_eq!(
-        dict.parse("<<A~X B> C>").unwrap().decurry(),
-        dict.parse("<A~X B C>").unwrap()
+        dict.parse_desugared("<<A~X B> C>").unwrap().decurry(),
+        dict.parse_desugared("<A~X B C>").unwrap()
     );
     assert_eq!(
-        dict.parse("<<A~X B> C~Y>~K").unwrap().decurry(),
-        dict.parse("<A~X B C~Y> ~K").unwrap()
+        dict.parse_desugared("<<A~X B> C~Y>~K").unwrap().decurry(),
+        dict.parse_desugared("<A~X B C~Y> ~K").unwrap()
     );
 }
 

src/test/halo.rs

@@ -0,0 +1,40 @@
+use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+/*
+#[test]
+fn test_common_halo() {
+    let mut dict = BimapTypeDict::new();
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse_desugared("A~B~C").expect("parse error"),
+            &dict.parse_desugared("A~B~C").expect("parse error")
+        ),
+        Some(dict.parse_desugared("A~B~C").expect("parse error"))
+    );
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse_desugared("A~B~X").expect("parse error"),
+            &dict.parse_desugared("A~B~Y").expect("parse error")
+        ),
+        Some(dict.parse_desugared("A~B").expect("parse error"))
+    );
+
+    assert_eq!(
+        crate::common_halo(
+            &dict.parse_desugared("A~<B C~D>").expect("parse error"),
+            &dict.parse_desugared("A~<B C~E>").expect("parse error")
+        ),
+        Some(dict.parse_desugared("A~<B C>").expect("parse error"))
+    );
+
+
+    assert_eq!(
+            crate::common_halo(
+                &dict.parse_desugared("A").expect("parse error"),
+                &dict.parse_desugared("A~<B C~E>").expect("parse error")
+            ),
+            Some(dict.parse_desugared("A").expect("parse error"))
+        );
+}
+*/

src/test/lnf.rs

@@ -1,57 +0,0 @@
-use crate::dict::TypeDict;
-
-#[test]
-fn test_flat() {
-    let mut dict = TypeDict::new();
-
-    assert!( dict.parse("A").expect("parse error").is_flat() );
-    assert!( dict.parse("10").expect("parse error").is_flat() );
-    assert!( dict.parse("'x'").expect("parse error").is_flat() );
-    assert!( dict.parse("<A B 23>").expect("parse error").is_flat() );
-    assert!( dict.parse("<A <B C 'x' D>>").expect("parse error").is_flat() );
-
-    assert!( ! dict.parse("A~B").expect("parse error").is_flat() );
-    assert!( ! dict.parse("<A B~C>").expect("parse error").is_flat() );
-    assert!( ! dict.parse("<A <B C~X D>>").expect("parse error").is_flat() );
-}
-
-#[test]
-fn test_normalize() {
-    let mut dict = TypeDict::new();
-
-    assert_eq!(
-        dict.parse("A~B~C").expect("parse error").normalize(),
-        dict.parse("A~B~C").expect("parse errror"),
-    );
-
-    assert_eq!(
-        dict.parse("<A B>~C").expect("parse error").normalize(),
-        dict.parse("<A B>~C").expect("parse errror"),
-    );
-
-    assert_eq!(
-        dict.parse("<A B~C>").expect("parse error").normalize(),
-        dict.parse("<A B>~<A C>").expect("parse errror"),
-    );
-
-    assert_eq!(
-        dict.parse("<A B~C D~E>").expect("parse error").normalize(),
-        dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror"),
-    );
-
-    assert_eq!(
-        dict.parse("<Seq <Digit 10>~Char>").expect("parse error").normalize(),
-        dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror"),
-    );
-
-
-    assert_eq!(
-        dict.parse("<A <B C~D~E> F~G H H>").expect("parse error").normalize(),
-        dict.parse("<A <B C> F H H>
-                   ~<A <B D> F H H>
-                   ~<A <B E> F H H>
-                   ~<A <B E> G H H>").expect("parse errror"),
-    );
-
-}
-

src/test/mod.rs

@@ -2,9 +2,9 @@
 pub mod lexer;
 pub mod parser;
 pub mod curry;
-pub mod lnf;
 pub mod pnf;
-pub mod subtype;
+//pub mod subtype;
 pub mod substitution;
 pub mod unification;
-
+pub mod morphism;
+pub mod halo;

src/test/morphism.rs

@@ -0,0 +1,507 @@
+use {
+    crate::{dict::*, morphism_base::MorphismBase,
+        morphism_path::ShortestPathProblem,
+        morphism::{MorphismInstance, Morphism, MorphismType},
+        parser::*, TypeTerm,
+        DesugaredTypeTerm
+    },
+    std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+    eprintln!("{{");
+
+    for (k,v) in m.iter() {
+        eprintln!("    {} --> {}",
+            dict.get_typename(k).unwrap(),
+            v.pretty(dict, 0)
+        );
+    }
+
+    eprintln!("}}");
+}
+
+fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance<DummyMorphism>>) {
+    for n in path.iter() {
+        eprintln!("
+morph {}
+--> {}
+with
+        ",
+        n.get_type().src_type.pretty(dict, 0),
+        n.get_type().dst_type.pretty(dict, 0),
+        );
+        print_subst(&n.get_subst(), dict)
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+struct DummyMorphism(MorphismType);
+impl Morphism for DummyMorphism {
+    fn get_type(&self) -> MorphismType {
+        self.0.clone()
+    }
+}
+
+fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
+    let mut dict = BimapTypeDict::new();
+    let mut base = MorphismBase::<DummyMorphism>::new();
+
+    dict.add_varname("Radix".into());
+    dict.add_varname("SrcRadix".into());
+    dict.add_varname("DstRadix".into());
+
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap().sugar(&mut dict)
+        })
+    );
+
+    (dict, base)
+}
+
+#[test]
+fn test_morphism_path1() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse_desugared("<Digit 10> ~ Char").unwrap().sugar(&mut dict),
+        dst_type: dict.parse_desugared("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
+    }).solve();
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType {
+                        src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+                    }),
+                }
+            ]
+    ));
+}
+
+
+#[test]
+fn test_morphism_path2() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse_desugared("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
+        dst_type: dict.parse_desugared("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+    }).solve();
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 10 BigEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                }
+            ]
+    ));
+}
+
+
+#[test]
+fn test_morphism_path3() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse_desugared("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
+        dst_type: dict.parse_desugared("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+    }).solve();
+
+    if let Some(path) = path.as_ref() {
+        print_path(&mut dict, path);
+    }
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 10 LittleEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                },
+
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType {
+                        src_type: dict.parse_desugared("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
+                    }),
+                }
+            ]
+    ));
+}
+
+
+
+#[test]
+fn test_morphism_path4() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse_desugared("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
+        dst_type: dict.parse_desugared("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().sugar(&mut dict)
+    }).solve();
+
+    if let Some(path) = path.as_ref() {
+        print_path(&mut dict, path);
+    }
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 10 LittleEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                },
+
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType {
+                        src_type: dict.parse_desugared("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
+                    }),
+                },
+
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 16 LittleEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                },
+            ]
+    ));
+}
+
+
+
+
+#[test]
+fn test_morphism_path_posint() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse_desugared("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().sugar(&mut dict),
+        dst_type: dict.parse_desugared("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().sugar(&mut dict),
+    }).solve();
+
+    if let Some(path) = path.as_ref() {
+        print_path(&mut dict, path);
+    }
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 10 BigEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                },
+
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType{
+                        src_type: dict.parse_desugared("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
+                    }),
+                },
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType{
+                        src_type: dict.parse_desugared("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict)
+                    }),
+                },
+                MorphismInstance::Primitive {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    ψ: TypeTerm::unit(),
+                    morph: DummyMorphism(MorphismType{
+                        src_type: dict.parse_desugared("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                        dst_type: dict.parse_desugared("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
+                    }),
+                },
+
+                MorphismInstance::MapSeq {
+                    ψ: dict.parse_desugared("ℕ ~ <PosInt 16 BigEndian>").expect("").sugar(&mut dict),
+                    seq_repr: None,
+                    item_morph: Box::new(MorphismInstance::Primitive {
+                        σ: vec![
+                            (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                        ].into_iter().collect(),
+                        ψ: TypeTerm::unit(),
+                        morph: DummyMorphism(MorphismType {
+                            src_type: dict.parse_desugared("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap().sugar(&mut dict),
+                            dst_type: dict.parse_desugared("<Digit Radix> ~ Char").unwrap().sugar(&mut dict)
+                        }),
+                    })
+                },
+            ]
+        )
+    );
+}
+
+#[test]
+fn morphism_test_seq_repr() {
+    let mut dict = BimapTypeDict::new();
+    let mut base = MorphismBase::<DummyMorphism>::new();
+
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse_desugared("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
+            dst_type: dict.parse_desugared("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
+        })
+    );
+
+    assert_eq!(
+        base.get_morphism_instance(&MorphismType {
+            src_type: dict.parse_desugared("<Seq~<ValueTerminated 0> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict),
+            dst_type: dict.parse_desugared("<Seq~<LengthPrefix native.UInt64> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict)
+        }),
+        Some(
+            MorphismInstance::Primitive {
+                ψ: dict.parse_desugared("<Seq Char~Ascii>").expect("").sugar(&mut dict),
+                σ: HashMap::new(),
+                morph: DummyMorphism(MorphismType{
+                    src_type: dict.parse_desugared("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
+                    dst_type: dict.parse_desugared("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
+                })
+            }
+        )
+    );
+}
+
+/*
+#[test]
+fn test_steiner_tree() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let mut steiner_tree_problem = crate::steiner_tree::SteinerTreeProblem::new(
+        // source reprs
+        vec![
+            dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+        ],
+
+        // destination reprs
+        vec![
+            dict.parse("ℕ ~ <PosInt 2 BigEndian> ~ <Seq <Digit 2> ~ Char>").unwrap(),
+            dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+            dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
+        ]
+    );
+
+    if let Some(solution) = steiner_tree_problem.solve_bfs( &base ) {
+        for e in solution.edges.iter() {
+            eprintln!(" :: {}\n--> {}", dict.unparse(&e.src_type), dict.unparse(&e.dst_type));
+        }
+    } else {
+        eprintln!("no solution");
+    }
+}
+
+
+use std::collections::HashMap;
+
+#[test]
+fn test_morphism_path_listedit()
+{
+    let mut dict = BimapTypeDict::new();
+    let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("List").expect("") ] );
+
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("Char").unwrap(),
+            dst_type: dict.parse("Char ~ EditTree").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("Char").unwrap(),
+            dst_type: dict.parse("Char ~ ReprTree").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("Char ~ ReprTree").unwrap(),
+            dst_type: dict.parse("Char").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List~Vec Char>").unwrap(),
+            dst_type: dict.parse("<List Char>").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List ReprTree>").unwrap(),
+            dst_type: dict.parse("<List~Vec ReprTree>").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
+            dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
+            dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
+        })
+    );
+
+
+    let path = ShortestPathProblem::new(&base, MorphismType {
+        src_type: dict.parse("<Seq~List~Vec <Digit 10>~Char>").unwrap(),
+        dst_type: dict.parse("<Seq~List <Digit 10>~Char> ~ EditTree").unwrap(),
+    }).solve();
+
+    if let Some(path) = path.as_ref() {
+        print_path(&mut dict, path);
+    }
+
+    assert_eq!(
+        path,
+        Some(vec![
+            MorphismInstance {
+                m: DummyMorphism(MorphismType{
+                    src_type: dict.parse("<List~Vec Char>").unwrap(),
+                    dst_type: dict.parse("<List Char>").unwrap()
+                }),
+                halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
+                σ: HashMap::new()
+            },
+            MorphismInstance {
+                m: DummyMorphism(MorphismType{
+                    src_type: dict.parse("<List Char>").unwrap(),
+                    dst_type: dict.parse("<List Char~ReprTree>").unwrap()
+                }),
+                halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
+                σ: HashMap::new()
+            },
+            MorphismInstance {
+                m: DummyMorphism(MorphismType{
+                    src_type: dict.parse("<List ReprTree>").unwrap(),
+                    dst_type: dict.parse("<List~Vec ReprTree>").unwrap()
+                }),
+                halo: dict.parse("<Seq~List <Digit 10>~Char>").unwrap(),
+                σ: HashMap::new()
+            },
+            MorphismInstance {
+                m: DummyMorphism(MorphismType{
+                    src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
+                    dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
+                }),
+                halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
+                σ: HashMap::new()
+            },
+        ])
+    );
+}
+*/

src/test/parser.rs

@@ -1,13 +1,13 @@
 
 use {
-    crate::{term::*, dict::*, parser::*}
+    crate::{desugared_term::*, dict::*, parser::*, TypeTerm}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 #[test]
 fn test_parser_id() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     dict.add_varname("T".into());
 
@@ -26,7 +26,7 @@ fn test_parser_id() {
 fn test_parser_num() {
     assert_eq!(
         Ok(TypeTerm::Num(1234)),
-        TypeDict::new().parse("1234")
+        BimapTypeDict::new().parse("1234")
     );
 }
 
@@ -34,22 +34,22 @@ fn test_parser_num() {
 fn test_parser_char() {
     assert_eq!(
         Ok(TypeTerm::Char('x')),
-        TypeDict::new().parse("'x'")
+        BimapTypeDict::new().parse("'x'")
     );
 }
 
 #[test]
 fn test_parser_app() {
     assert_eq!(
-        TypeDict::new().parse("<A B>"),
-        Ok(TypeTerm::App(vec![
+        BimapTypeDict::new().parse("<A B>"),
+        Ok(TypeTerm::Spec(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
         ]))
     );
     assert_eq!(
-        TypeDict::new().parse("<A B C>"),
-        Ok(TypeTerm::App(vec![
+        BimapTypeDict::new().parse("<A B C>"),
+        Ok(TypeTerm::Spec(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
             TypeTerm::TypeID(TypeID::Fun(2)),
@@ -60,7 +60,7 @@ fn test_parser_app() {
 #[test]
 fn test_parser_unexpected_close() {
     assert_eq!(
-        TypeDict::new().parse(">"),
+        BimapTypeDict::new().parse(">"),
         Err(ParseError::UnexpectedClose)
     );
 }
@@ -68,7 +68,7 @@ fn test_parser_unexpected_close() {
 #[test]
 fn test_parser_unexpected_token() {
     assert_eq!(
-        TypeDict::new().parse("A B"),
+        BimapTypeDict::new().parse("A B"),
         Err(ParseError::UnexpectedToken)
     );
 }
@@ -76,14 +76,14 @@ fn test_parser_unexpected_token() {
 #[test]
 fn test_parser_ladder() {
     assert_eq!(
-        TypeDict::new().parse("A~B"),
+        BimapTypeDict::new().parse("A~B"),
         Ok(TypeTerm::Ladder(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
         ]))
     );
     assert_eq!(
-        TypeDict::new().parse("A~B~C"),
+        BimapTypeDict::new().parse("A~B~C"),
         Ok(TypeTerm::Ladder(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
@@ -95,53 +95,53 @@ fn test_parser_ladder() {
 #[test]
 fn test_parser_ladder_outside() {
     assert_eq!(
-        TypeDict::new().parse("<A B>~C"),
+        BimapTypeDict::new().parse("<A B>~C"),
         Ok(TypeTerm::Ladder(vec![
-            TypeTerm::App(vec![
+            TypeTerm::Spec(vec![
                 TypeTerm::TypeID(TypeID::Fun(0)),
                 TypeTerm::TypeID(TypeID::Fun(1)),
             ]),
             TypeTerm::TypeID(TypeID::Fun(2)),
         ]))
-    );    
+    );
 }
 
 #[test]
 fn test_parser_ladder_inside() {
     assert_eq!(
-        TypeDict::new().parse("<A B~C>"),
-        Ok(TypeTerm::App(vec![
+        BimapTypeDict::new().parse("<A B~C>"),
+        Ok(TypeTerm::Spec(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::Ladder(vec![
                 TypeTerm::TypeID(TypeID::Fun(1)),
                 TypeTerm::TypeID(TypeID::Fun(2)),
             ])
         ]))
-    );    
+    );
 }
 
 #[test]
 fn test_parser_ladder_between() {
     assert_eq!(
-        TypeDict::new().parse("<A B~<C D>>"),
-        Ok(TypeTerm::App(vec![
+        BimapTypeDict::new().parse("<A B~<C D>>"),
+        Ok(TypeTerm::Spec(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::Ladder(vec![
                 TypeTerm::TypeID(TypeID::Fun(1)),
-                TypeTerm::App(vec![
+                TypeTerm::Spec(vec![
                     TypeTerm::TypeID(TypeID::Fun(2)),
                     TypeTerm::TypeID(TypeID::Fun(3)),
                 ])
             ])
         ]))
-    );    
+    );
 }
 
 
 #[test]
 fn test_parser_ladder_large() {
     assert_eq!(
-        TypeDict::new().parse(
+        BimapTypeDict::new().parse_desugared(
             "<Seq Date
                   ~<TimeSince UnixEpoch>
                   ~<Duration Seconds>
@@ -154,53 +154,52 @@ fn test_parser_ladder_large() {
               ~<Seq Byte>"),
 
         Ok(
-            TypeTerm::Ladder(vec![
-                TypeTerm::App(vec![
-                    TypeTerm::TypeID(TypeID::Fun(0)),
-                    TypeTerm::Ladder(vec![
-                        TypeTerm::TypeID(TypeID::Fun(1)),
-                        TypeTerm::App(vec![
-                            TypeTerm::TypeID(TypeID::Fun(2)),
-                            TypeTerm::TypeID(TypeID::Fun(3))
+            DesugaredTypeTerm::Ladder(vec![
+                DesugaredTypeTerm::App(vec![
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(0)),
+                    DesugaredTypeTerm::Ladder(vec![
+                        DesugaredTypeTerm::TypeID(TypeID::Fun(1)),
+                        DesugaredTypeTerm::App(vec![
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(2)),
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(3))
                         ]),
-                        TypeTerm::App(vec![
-                            TypeTerm::TypeID(TypeID::Fun(4)),
-                            TypeTerm::TypeID(TypeID::Fun(5))
+                        DesugaredTypeTerm::App(vec![
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(4)),
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(5))
                         ]),
-                        TypeTerm::TypeID(TypeID::Fun(6)),
-                        TypeTerm::App(vec![
-                            TypeTerm::TypeID(TypeID::Fun(7)),
-                            TypeTerm::Num(10),
-                            TypeTerm::TypeID(TypeID::Fun(8))
+                        DesugaredTypeTerm::TypeID(TypeID::Fun(6)),
+                        DesugaredTypeTerm::App(vec![
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(7)),
+                            DesugaredTypeTerm::Num(10),
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(8))
                         ]),
-                        TypeTerm::App(vec![
-                            TypeTerm::TypeID(TypeID::Fun(0)),
-                            TypeTerm::Ladder(vec![
-                                TypeTerm::App(vec![
-                                    TypeTerm::TypeID(TypeID::Fun(9)),
-                                    TypeTerm::Num(10)
+                        DesugaredTypeTerm::App(vec![
+                            DesugaredTypeTerm::TypeID(TypeID::Fun(0)),
+                            DesugaredTypeTerm::Ladder(vec![
+                                DesugaredTypeTerm::App(vec![
+                                    DesugaredTypeTerm::TypeID(TypeID::Fun(9)),
+                                    DesugaredTypeTerm::Num(10)
                                 ]),
-                                TypeTerm::TypeID(TypeID::Fun(10))
+                                DesugaredTypeTerm::TypeID(TypeID::Fun(10))
                             ])
                         ])
                     ])
                 ]),
-                TypeTerm::App(vec![
-                    TypeTerm::TypeID(TypeID::Fun(11)),
-                    TypeTerm::TypeID(TypeID::Fun(10)),
-                    TypeTerm::Char(':')
+                DesugaredTypeTerm::App(vec![
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(11)),
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(10)),
+                    DesugaredTypeTerm::Char(':')
                 ]),
-                TypeTerm::App(vec![
-                    TypeTerm::TypeID(TypeID::Fun(0)),
-                    TypeTerm::TypeID(TypeID::Fun(10))
+                DesugaredTypeTerm::App(vec![
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(0)),
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(10))
                 ]),
-                TypeTerm::TypeID(TypeID::Fun(12)),
-                TypeTerm::App(vec![
-                    TypeTerm::TypeID(TypeID::Fun(0)),
-                    TypeTerm::TypeID(TypeID::Fun(13))
+                DesugaredTypeTerm::TypeID(TypeID::Fun(12)),
+                DesugaredTypeTerm::App(vec![
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(0)),
+                    DesugaredTypeTerm::TypeID(TypeID::Fun(13))
                 ])
             ])
         )
     );
 }
-

src/test/pnf.rs

@@ -1,59 +1,117 @@
-use crate::dict::TypeDict;
+use crate::{dict::BimapTypeDict, parser::*};
 
 #[test]
-fn test_param_normalize() {
-    let mut dict = TypeDict::new();
+fn test_normalize_id() {
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
         dict.parse("A~B~C").expect("parse error"),
-        dict.parse("A~B~C").expect("parse error").param_normalize(),
+        dict.parse("A~B~C").expect("parse error").normalize(),
     );
 
     assert_eq!(
         dict.parse("<A B>~C").expect("parse error"),
-        dict.parse("<A B>~C").expect("parse error").param_normalize(),
+        dict.parse("<A B>~C").expect("parse error").normalize(),
     );
+}
+
+#[test]
+fn test_normalize_spec() {
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
         dict.parse("<A B~C>").expect("parse error"),
-        dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
+        dict.parse("<A B>~<A C>").expect("parse error").normalize(),
     );
 
     assert_eq!(
         dict.parse("<A~Y B>").expect("parse error"),
-        dict.parse("<A B>~<Y B>").expect("parse error").param_normalize(),
+        dict.parse("<A~Y B>~<Y B>").expect("parse error").normalize(),
     );
 
     assert_eq!(
         dict.parse("<A B~C D~E>").expect("parse error"),
-        dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").param_normalize(),
+        dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").normalize(),
     );
 
     assert_eq!(
         dict.parse("<A~X B~C D~E>").expect("parse error"),
-        dict.parse("<A B D>~<A B~C E>~<X C E>").expect("parse errror").param_normalize(),
-    );
-
-    assert_eq!(
-        dict.parse("<Seq <Digit 10>~Char>").expect("parse error"),
-        dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").param_normalize(),
-    );
-
-    assert_eq!(
-        dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~x86.UInt8>").expect("parse error").param_normalize(),
-        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
-    );
-    assert_eq!(
-        dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> x86.UInt8>").expect("parse error").param_normalize(),
-        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
-    );
-
-    assert_eq!(
-        dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
-        dict.parse("<A <B C> F H H>
-                   ~<A <B D> F H H>
-                   ~<A~Y <B E> F H H>").expect("parse errror")
-               .param_normalize(),
+        dict.parse("<A~X B D>~<A~X B~C E>~<X C E>").expect("parse errror").normalize(),
     );
 }
 
+#[test]
+fn test_normalize_seq() {
+    let mut dict = BimapTypeDict::new();
+    assert_eq!(
+        dict.parse("<Seq Char~Ascii>").expect("parse error"),
+        dict.parse("<Seq Char>~<Seq Ascii>").expect("parse errror").normalize(),
+    );
+
+    eprintln!("---------------");
+    assert_eq!(
+        dict.parse("<Seq <Digit 10>~Char>").expect("parse error"),
+        dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").normalize(),
+    );
+    eprintln!("---------------");
+    assert_eq!(
+        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error"),
+        dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~native.UInt8>").expect("parse error").normalize(),
+    );
+
+    eprintln!("---------------");
+    assert_eq!(
+        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error"),
+        dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> native.UInt8>").expect("parse error").normalize(),
+    );
+}
+
+#[test]
+fn test_normalize_complex_spec() {
+    let mut dict = BimapTypeDict::new();
+    assert_eq!(
+        dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
+        dict.parse("<A~Y <B C> F H H>
+                   ~<A~Y <B D> F H H>
+                   ~<Y <B E> F H H>").expect("parse errror")
+               .normalize(),
+    );
+}
+
+#[test]
+fn test_normalize_struct() {
+    let mut dict = BimapTypeDict::new();
+    assert_eq!(
+        dict.parse("< Struct~Aligned
+                <  a   TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64  >
+                <  b   Angle ~ Degrees ~ ℝ ~ native.Float32 >
+            >
+            ").expect("parse error"),
+        dict.parse("
+            < Struct <a TimePoint> <b Angle> >
+        ~   < Struct  <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
+        ~   < Struct~Aligned  <a native.UInt64> <b native.Float32> >
+        ").expect("parse errror")
+
+            .normalize(),
+    );
+}
+
+#[test]
+fn test_normalize_enum() {
+    let mut dict = BimapTypeDict::new();
+    assert_eq!(
+        dict.parse("< Enum
+                <  a   TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64  >
+                <  b   Angle ~ Degrees ~ ℝ ~ native.Float32 >
+            >
+            ").expect("parse error"),
+        dict.parse("
+            < Enum <a TimePoint> <b Angle> >
+        ~   < Enum  <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
+        ~   < Enum  <a native.UInt64> <b native.Float32> >
+        ").expect("parse errror")
+
+            .normalize(),
+    );
+}

src/test/substitution.rs

@@ -1,32 +1,30 @@
 
 use {
-    crate::{dict::*, term::*},
-    std::iter::FromIterator
+    crate::{dict::*, desugared_term::*, parser::*, unparser::*, substitution::*},
+    std::iter::FromIterator,
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 #[test]
 fn test_subst() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     let mut σ = std::collections::HashMap::new();
 
     // T  -->  ℕ
     σ.insert
         (dict.add_varname(String::from("T")),
-         dict.parse("ℕ").unwrap());
+         dict.parse_desugared("ℕ").unwrap().sugar(&mut dict));
 
     // U  -->  <Seq Char>
     σ.insert
         (dict.add_varname(String::from("U")),
-         dict.parse("<Seq Char>").unwrap());
+         dict.parse_desugared("<Seq Char>").unwrap().sugar(&mut dict));
 
 
     assert_eq!(
-        dict.parse("<Seq T~U>").unwrap()
-            .apply_substitution(&|typid|{ σ.get(typid).cloned() }).clone(),
-        dict.parse("<Seq ℕ~<Seq Char>>").unwrap()
+        dict.parse_desugared("<Seq T~U>").unwrap().sugar(&mut dict).apply_subst(&σ).clone(),
+        dict.parse_desugared("<Seq ℕ~<Seq Char>>").unwrap().sugar(&mut dict)
     );
 }
-

src/test/subtype.rs

@@ -1,97 +1,97 @@
-use crate::dict::TypeDict;
-
+use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+/*
 #[test]
 fn test_semantic_subtype() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
-        dict.parse("A~B~C").expect("parse error")
+        dict.parse_desugared("A~B~C").expect("parse error")
             .is_semantic_subtype_of(
-                &dict.parse("A~B~C").expect("parse errror")
+                &dict.parse_desugared("A~B~C").expect("parse errror")
             ),
-        Some((0, dict.parse("A~B~C").expect("parse errror")))
+        Some((0, dict.parse_desugared("A~B~C").expect("parse errror")))
     );
 
     assert_eq!(
-        dict.parse("A~B1~C1").expect("parse error")
+        dict.parse_desugared("A~B1~C1").expect("parse error")
             .is_semantic_subtype_of(
-                &dict.parse("A~B2~C2").expect("parse errror")
+                &dict.parse_desugared("A~B2~C2").expect("parse errror")
             ),
-        Some((0, dict.parse("A~B1~C1").expect("parse errror")))
+        Some((0, dict.parse_desugared("A~B1~C1").expect("parse errror")))
     );
-    
+
     assert_eq!(
-        dict.parse("A~B~C1").expect("parse error")
+        dict.parse_desugared("A~B~C1").expect("parse error")
             .is_semantic_subtype_of(
-                &dict.parse("B~C2").expect("parse errror")  
+                &dict.parse_desugared("B~C2").expect("parse errror")
             ),
-        Some((1, dict.parse("B~C1").expect("parse errror")))
+        Some((1, dict.parse_desugared("B~C1").expect("parse errror")))
     );
 }
 
 #[test]
 fn test_syntactic_subtype() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     assert_eq!(
-        dict.parse("A~B~C").expect("parse error")
+        dict.parse_desugared("A~B~C").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("A~B~C").expect("parse errror")  
+                &dict.parse_desugared("A~B~C").expect("parse errror")
             ),
         Ok(0)
     );
 
     assert_eq!(
-        dict.parse("A~B~C").expect("parse error")
+        dict.parse_desugared("A~B~C").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("B~C").expect("parse errror")  
+                &dict.parse_desugared("B~C").expect("parse errror")
             ),
         Ok(1)
     );
 
     assert_eq!(
-        dict.parse("A~B~C~D~E").expect("parse error")
+        dict.parse_desugared("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("C~D").expect("parse errror")  
+                &dict.parse_desugared("C~D").expect("parse errror")
             ),
         Ok(2)
     );
 
     assert_eq!(
-        dict.parse("A~B~C~D~E").expect("parse error")
+        dict.parse_desugared("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("C~G").expect("parse errror")  
+                &dict.parse_desugared("C~G").expect("parse errror")
             ),
         Err((2,3))
     );
 
     assert_eq!(
-        dict.parse("A~B~C~D~E").expect("parse error")
+        dict.parse_desugared("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("G~F~K").expect("parse errror")  
+                &dict.parse_desugared("G~F~K").expect("parse errror")
             ),
         Err((0,0))
     );
 
     assert_eq!(
-        dict.parse("<Duration Seconds>~ℕ").expect("parse error")
+        dict.parse_desugared("<Duration Seconds>~ℕ").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("ℕ").expect("parse errror")
+                &dict.parse_desugared("ℕ").expect("parse errror")
             ),
         Ok(1)
     );
 
     assert_eq!(
-        dict.parse("
+        dict.parse_desugared("
 <Duration Seconds>
 ~ℕ
 ~<PosInt 10 BigEndian>
 ~< Seq   <Digit 10> ~ Char >"
         ).expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("<Seq Char>").expect("parse errror")
+                &dict.parse_desugared("<Seq Char>").expect("parse errror")
             ),
         Ok(4)
     );
 }
-
+*/

src/test/unification.rs

@@ -1,13 +1,13 @@
 
 use {
-    crate::{dict::*, term::*, unification::*},
+    crate::{dict::*, parser::*, constraint_system::ConstraintError},
     std::iter::FromIterator
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
     dict.add_varname(String::from("T"));
     dict.add_varname(String::from("U"));
     dict.add_varname(String::from("V"));
@@ -23,8 +23,8 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
         let σ = σ.unwrap();
 
         assert_eq!(
-            t1.apply_substitution(&|v| σ.get(v).cloned()),
-            t2.apply_substitution(&|v| σ.get(v).cloned())
+            t1.apply_subst(&σ),
+            t2.apply_subst(&σ)
         );
     } else {
         assert!(! σ.is_ok());
@@ -33,7 +33,7 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
 
 #[test]
 fn test_unification_error() {
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
     dict.add_varname(String::from("T"));
 
     assert_eq!(
@@ -42,7 +42,7 @@ fn test_unification_error() {
             &dict.parse("<B T>").unwrap()
         ),
 
-        Err(UnificationError {
+        Err(ConstraintError {
             addr: vec![0],
             t1: dict.parse("A").unwrap(),
             t2: dict.parse("B").unwrap()
@@ -55,12 +55,25 @@ fn test_unification_error() {
             &dict.parse("<V <U B> T>").unwrap()
         ),
 
-        Err(UnificationError {
+        Err(ConstraintError {
             addr: vec![1, 1],
             t1: dict.parse("A").unwrap(),
             t2: dict.parse("B").unwrap()
         })
     );
+
+    assert_eq!(
+        crate::unify(
+            &dict.parse("T").unwrap(),
+            &dict.parse("<Seq T>").unwrap()
+        ),
+
+        Err(ConstraintError {
+            addr: vec![],
+            t1: dict.parse("T").unwrap(),
+            t2: dict.parse("<Seq T>").unwrap()
+        })
+    );
 }
 
 #[test]
@@ -68,15 +81,19 @@ fn test_unification() {
     test_unify("A", "A", true);
     test_unify("A", "B", false);
     test_unify("<Seq T>", "<Seq Ascii~Char>", true);
-    test_unify("<Seq T>", "<U Char>", true);
+
+    // this worked easily with desugared terms,
+    // but is a weird edge case with sugared terms
+    // not relevant now
+    //test_unify("<Seq T>", "<U Char>", true);
 
     test_unify(
-        "<Seq Path~<Seq Char>>~<SepSeq Char '\n'>~<Seq Char>",
-        "<Seq T~<Seq Char>>~<SepSeq Char '\n'>~<Seq Char>",
+        "<Seq Path~<Seq Char>>~<SepSeq Char '\\n'>~<Seq Char>",
+        "<Seq T~<Seq Char>>~<SepSeq Char '\\n'>~<Seq Char>",
         true
     );
 
-    let mut dict = TypeDict::new();
+    let mut dict = BimapTypeDict::new();
 
     dict.add_varname(String::from("T"));
     dict.add_varname(String::from("U"));
@@ -84,11 +101,20 @@ fn test_unification() {
     dict.add_varname(String::from("W"));
 
     assert_eq!(
-        UnificationProblem::new(vec![
-            (dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
-            (dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
+        ConstraintSystem::new_eq(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs: dict.parse("U").unwrap(),
+                rhs: dict.parse("<Seq Char>").unwrap()
+            },
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs: dict.parse("T").unwrap(),
+                rhs: dict.parse("<Seq U>").unwrap()
+            }
         ]).solve(),
-        Ok(
+        Ok((
+            vec![],
             vec![
                 // T
                 (TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
@@ -96,15 +122,24 @@ fn test_unification() {
                 // U
                 (TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
             ].into_iter().collect()
-        )
+        ))
     );
 
     assert_eq!(
-        UnificationProblem::new(vec![
-            (dict.parse("<Seq T>").unwrap(), dict.parse("<Seq W~<Seq Char>>").unwrap()),
-            (dict.parse("<Seq ℕ>").unwrap(), dict.parse("<Seq W>").unwrap()),
+        ConstraintSystem::new_eq(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("<Seq T>").unwrap(),
+                rhs : dict.parse("<Seq W~<Seq Char>>").unwrap()
+            },
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("<Seq ℕ>").unwrap(),
+                rhs : dict.parse("<Seq W>").unwrap(),
+            }
         ]).solve(),
-        Ok(
+        Ok((
+            vec![],
             vec![
                 // W
                 (TypeID::Var(3), dict.parse("ℕ").unwrap()),
@@ -112,7 +147,371 @@ fn test_unification() {
                 // T
                 (TypeID::Var(0), dict.parse("ℕ~<Seq Char>").unwrap())
             ].into_iter().collect()
-        )
+        ))
     );
 }
 
+#[test]
+fn test_subtype_unification1() {
+    let mut dict = BimapTypeDict::new();
+    dict.add_varname(String::from("T"));
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("A ~ B").unwrap(),
+                rhs : dict.parse("B").unwrap()
+            }
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A").unwrap() ],
+            vec![].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("A ~ B ~ C ~ D").unwrap(),
+                rhs : dict.parse("C ~ D").unwrap()
+            }
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A ~ B").unwrap() ],
+            vec![].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("A ~ B ~ C ~ D").unwrap(),
+                rhs : dict.parse("T ~ D").unwrap()
+            }
+        ]).solve(),
+        Ok((
+            vec![ TypeTerm::unit() ],
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(),
+                    dict.parse("A ~ B ~ C").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("A ~ B ~ C ~ D").unwrap(),
+                rhs : dict.parse("B ~ T ~ D").unwrap(),
+            }
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A").unwrap() ],
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("C").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}
+
+#[test]
+fn test_subtype_unification2() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname(String::from("T"));
+    dict.add_varname(String::from("U"));
+    dict.add_varname(String::from("V"));
+    dict.add_varname(String::from("W"));
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair{
+                addr: Vec::new(),
+                lhs: dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(),
+                rhs: dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap(),
+            }
+        ]).solve(),
+        Ok((
+            vec![
+                dict.parse("<Seq <Digit 10>>").unwrap()
+            ],
+            vec![
+                // T
+                (TypeID::Var(0), dict.parse("<LengthPrefix x86.UInt64>").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs: dict.parse("U").unwrap(),
+                rhs: dict.parse("<Seq Char>").unwrap()
+            },
+            ConstraintPair {
+                addr : Vec::new(),
+                lhs :  dict.parse("T").unwrap(),
+                rhs : dict.parse("<Seq U>").unwrap(),
+            }
+        ]).solve(),
+        Ok((
+            vec![
+                TypeTerm::unit(),
+                TypeTerm::unit(),
+            ],
+            vec![
+                // T
+                (TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
+
+                // U
+                (TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    eprintln!("=&==========&======&=====&=====&==");
+
+    if let Ok((ψ,σ)) =
+        ConstraintSystem::new_sub(vec![
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("<Seq T>").unwrap(),
+                rhs : dict.parse("<Seq W~<Seq Char>>").unwrap(),
+            },
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("<Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>").unwrap(),
+                rhs : dict.parse("<<LengthPrefix x86.UInt64> W>").unwrap()
+            }
+        ]).solve() {
+            for ( k,v) in σ.iter() {
+                eprintln!(" {:?} ==> {} ",
+                    dict.get_typename(&k),
+                    v.pretty(&dict, 0));
+            }
+
+        assert_eq!(ψ,
+            vec![
+                TypeTerm::unit(),
+                dict.parse("<Seq ℕ>").unwrap(),
+            ]);
+        assert_eq!(σ,
+            vec![
+                // W
+                (TypeID::Var(3), dict.parse("ℕ~<PosInt 10 BigEndian>").unwrap()),
+
+                // T
+                (TypeID::Var(0), dict.parse("ℕ~<PosInt 10 BigEndian>~<Seq Char>").unwrap())
+            ].into_iter().collect()
+        );
+    } else {
+        assert!(false);
+    }
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("<Seq~List~Vec <Digit 16>~Char>").expect(""),
+            &dict.parse("<List~Vec Char>").expect("")
+        ),
+        Ok((
+            dict.parse("<Seq~List <Digit 16>>").expect(""),
+            vec![].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List~Vec <Digit 16>~Char>").expect(""),
+            &dict.parse("<List~Vec Char>").expect("")
+        ),
+        Ok((
+            dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>>").expect(""),
+            vec![].into_iter().collect()
+        ))
+    );
+}
+
+
+#[test]
+fn test_trait_not_subtype() {
+    let mut dict = BimapTypeDict::new();
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("A ~ B").expect(""),
+            &dict.parse("A ~ B ~ C").expect("")
+        ),
+        Err(ConstraintError {
+            addr: vec![1],
+            t1: dict.parse("B").expect(""),
+            t2: dict.parse("C").expect("")
+        })
+    );
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("<Seq~List~Vec <Digit 10>~Char>").expect(""),
+            &dict.parse("<Seq~List~Vec Char~ReprTree>").expect("")
+        ),
+        Err(ConstraintError {
+            addr: vec![1],
+            t1: dict.parse("Char").expect(""),
+            t2: dict.parse("ReprTree").expect("")
+        })
+    );
+}
+
+#[test]
+fn test_reprtree_list_subtype() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname("Item".into());
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect(""),
+            &dict.parse("<List~Vec Item~ReprTree>").expect("")
+        ),
+        Ok((
+            TypeTerm::unit(),
+            vec![
+                (dict.get_typeid(&"Item".into()).unwrap(), dict.parse("<Digit 10>~Char").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}
+
+#[test]
+pub fn test_subtype_delim() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname(String::from("T"));
+    dict.add_varname(String::from("Delim"));
+
+    assert_eq!(
+        ConstraintSystem::new_sub(vec![
+
+            ConstraintPair {
+                addr: Vec::new(),
+                // given type
+                lhs : dict.parse("
+                  < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
+                ~ < ValueSep ':' Char~Ascii~UInt8 >
+                ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
+                ").expect(""),
+
+                // expected type
+                rhs : dict.parse("
+                  < Seq <Seq T> >
+                ~ < ValueSep Delim T >
+                ~ < Seq~<LengthPrefix UInt64> T >
+                ").expect("")
+            },
+
+            // subtype bounds
+            ConstraintPair {
+                addr: Vec::new(),
+                lhs : dict.parse("T").expect(""),
+                rhs : dict.parse("UInt8").expect("")
+            },
+            /* todo
+            (
+                dict.parse("<TypeOf Delim>").expect(""),
+                dict.parse("T").expect("")
+            ),
+            */
+        ]).solve(),
+        Ok((
+            // halo types for each rhs in the sub-equations
+            vec![
+                dict.parse("<Seq <Seq <Digit 10>>>").expect(""),
+                dict.parse("Char~Ascii").expect(""),
+            ],
+
+            // variable substitution
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("Char~Ascii~UInt8").expect("")),
+                (dict.get_typeid(&"Delim".into()).unwrap(), TypeTerm::Char(':')),
+            ].into_iter().collect()
+        ))
+    );
+}
+
+
+
+use crate::{subtype_unify, term::*, constraint_system::{ConstraintPair, ConstraintSystem}};
+
+#[test]
+fn test_list_subtype_sugared() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname("Item".into());
+
+    let subtype_constraints = vec![
+        ConstraintPair::new(
+            dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect(""),
+            dict.parse("<List~Vec Item~ReprTree>").expect("")
+        )
+    ];
+
+    assert_eq!(
+        ConstraintSystem::new_sub(subtype_constraints).solve(),
+        Ok((
+            vec![ TypeTerm::Ladder(vec![]) ],
+            vec![
+                (dict.get_typeid(&"Item".into()).unwrap(),
+                    dict.parse("<Digit 10>~Char").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}
+
+#[test]
+pub fn test_subtype_delim_sugared() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname(String::from("T"));
+    dict.add_varname(String::from("Delim"));
+
+    let subtype_constraints = vec![
+        ConstraintPair::new(
+            dict.parse("
+              < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
+            ~ < ValueSep ':' Char~Ascii~UInt8 >
+            ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
+            ").expect(""),
+
+            dict.parse("
+              < Seq <Seq T> >
+            ~ < ValueSep Delim T >
+            ~ < Seq~<LengthPrefix UInt64> T >
+            ").expect(""),
+        ),
+        ConstraintPair::new(
+            dict.parse("T").expect(""),
+            dict.parse("UInt8").expect("")
+        ),
+    ];
+
+    assert_eq!(
+        ConstraintSystem::new_sub(subtype_constraints).solve(),
+        Ok((
+            // halo types for each rhs in the sub-equations
+            vec![
+                dict.parse("<Seq <Seq <Digit 10>>>").expect(""),
+                dict.parse("Char~Ascii").expect(""),
+            ],
+
+            // variable substitution
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("Char~Ascii~UInt8").expect("")),
+                (dict.get_typeid(&"Delim".into()).unwrap(), TypeTerm::Char(':')),
+            ].into_iter().collect()
+        ))
+    );
+}

src/unification.rs

@@ -1,100 +0,0 @@
-use {
-    std::collections::HashMap,
-    crate::{term::*, dict::*}
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone, Eq, PartialEq, Debug)]
-pub struct UnificationError {
-    pub addr: Vec<usize>,
-    pub t1: TypeTerm,
-    pub t2: TypeTerm
-}
-
-pub struct UnificationProblem {
-    eqs: Vec<(TypeTerm, TypeTerm, Vec<usize>)>,
-    σ: HashMap<TypeID, TypeTerm>
-}
-
-impl UnificationProblem {
-    pub fn new(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
-        UnificationProblem {
-            eqs: eqs.iter().map(|(lhs,rhs)| (lhs.clone(),rhs.clone(),vec![])).collect(),
-            σ: HashMap::new()
-        }
-    }
-
-    pub fn eval_equation(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<(), UnificationError> {
-        match (lhs.clone(), rhs.clone()) {
-            (TypeTerm::TypeID(TypeID::Var(varid)), t) |
-            (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
-                self.σ.insert(TypeID::Var(varid), t.clone());
-
-                // update all values in substitution
-                let mut new_σ = HashMap::new();
-                for (v, tt) in self.σ.iter() {
-                    let mut tt = tt.clone();
-                    tt.apply_substitution(&|v| self.σ.get(v).cloned());
-                    new_σ.insert(v.clone(), tt);
-                }
-                self.σ = new_σ;
-
-                Ok(())
-            }
-
-            (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
-                if a1 == a2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
-            }
-            (TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
-                if n1 == n2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
-            }
-            (TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
-                if c1 == c2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
-            }
-
-            (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
-            (TypeTerm::App(a1), TypeTerm::App(a2)) => {
-                if a1.len() == a2.len() {
-                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
-                        let mut new_addr = addr.clone();
-                        new_addr.push(i);
-                        self.eqs.push((x, y, new_addr));
-                    }
-                    Ok(())
-                } else {
-                    Err(UnificationError{ addr, t1: lhs, t2: rhs })
-                }
-            }
-
-            (TypeTerm::Ladder(l1), TypeTerm::Ladder(l2)) => {
-                Err(UnificationError{ addr, t1: lhs, t2: rhs })
-            }
-
-            _ => Err(UnificationError{ addr, t1: lhs, t2: rhs})
-        }
-    }
-
-    pub fn solve(mut self) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
-        while self.eqs.len() > 0 {
-            while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
-                lhs.apply_substitution(&|v| self.σ.get(v).cloned());
-                rhs.apply_substitution(&|v| self.σ.get(v).cloned());
-                self.eval_equation(lhs, rhs, addr)?;
-            }
-        }
-
-        Ok(self.σ)
-    }
-}
-
-pub fn unify(
-    t1: &TypeTerm,
-    t2: &TypeTerm
-) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
-    let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
-    unification.solve()
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-

src/unparser.rs

@@ -1,20 +1,24 @@
-use crate::{dict::*, term::*};
+use crate::{dict::*, desugared_term::*};
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeDict {
-    pub fn unparse(&self, t: &TypeTerm) -> String {
+pub trait UnparseLadderType {
+    fn unparse(&self, t: &DesugaredTypeTerm) -> String;
+}
+
+impl<T: TypeDict> UnparseLadderType for T {
+    fn unparse(&self, t: &DesugaredTypeTerm) -> String {
         match t {
-            TypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
-            TypeTerm::Num(n) => format!("{}", n),
-            TypeTerm::Char(c) => match c {
+            DesugaredTypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
+            DesugaredTypeTerm::Num(n) => format!("{}", n),
+            DesugaredTypeTerm::Char(c) => match c {
                 '\0' => "'\\0'".into(),
                 '\n' => "'\\n'".into(),
                 '\t' => "'\\t'".into(),
                 '\'' => "'\\''".into(),
                 c => format!("'{}'", c)
             },
-            TypeTerm::Ladder(rungs) => {
+            DesugaredTypeTerm::Ladder(rungs) => {
                 let mut s = String::new();
                 let mut first = true;
                 for r in rungs.iter() {
@@ -26,7 +30,7 @@ impl TypeDict {
                 }
                 s
             }
-            TypeTerm::App(args) => {
+            DesugaredTypeTerm::App(args) => {
                 let mut s = String::new();
                 s.push('<');
                 let mut first = true;