add find_semantic_subtype_matches() as potential alternative to is_semantic_subtype_of()

.github/workflows/cargo-test.yml

@@ -2,20 +2,21 @@ name: Rust
 
 on:
   push:
-    branches: ["dev"]
+    branches: [ "dev" ]
   pull_request:
-    branches: ["dev"]
+    branches: [ "dev" ]
 
 env:
   CARGO_TERM_COLOR: always
 
 jobs:
   build:
+
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v3
-      - name: Build
-        run: cargo build --verbose --features pretty
-      - name: Run tests
-        run: cargo test --verbose --features pretty
+    - uses: actions/checkout@v3
+    - name: Build
+      run: cargo build --verbose
+    - name: Run tests
+      run: cargo test --verbose

Cargo.toml

@@ -4,8 +4,3 @@ edition = "2018"
 name = "laddertypes"
 version = "0.1.0"
 
-[dependencies]
-tiny-ansi = { version = "0.1.0", optional = true }
-
-[features]
-pretty = ["dep:tiny-ansi"]

src/bimap.rs

@@ -2,7 +2,6 @@ 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/dict.rs

@@ -2,42 +2,15 @@ use crate::bimap::Bimap;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)]
+#[derive(Eq, PartialEq, Hash, Clone, Debug)]
 pub enum TypeID {
     Fun(u64),
     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: &String) -> TypeID {
-        if let Some(id) = self.get_typeid(tn) {
-            id
-        } else {
-            self.add_typename(tn.clone())
-        }
-    }
-}
-
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-#[derive(Debug)]
-pub struct BimapTypeDict {
+pub struct TypeDict {
     typenames: Bimap<String, TypeID>,
     type_lit_counter: u64,
     type_var_counter: u64,
@@ -45,66 +18,42 @@ pub struct BimapTypeDict {
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl BimapTypeDict {
+impl TypeDict {
     pub fn new() -> Self {
-        BimapTypeDict {
+        TypeDict {
             typenames: Bimap::new(),
             type_lit_counter: 0,
             type_var_counter: 0,
         }
     }
-}
 
-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 {
+    pub fn add_varname(&mut self, tn: String) -> TypeID {
         let tyid = TypeID::Var(self.type_var_counter);
         self.type_var_counter += 1;
-        self.insert(tn, tyid.clone());
+        self.typenames.insert(tn, tyid.clone());
         tyid
     }
 
-    fn add_typename(&mut self, tn: String) -> TypeID {
+    pub fn add_typename(&mut self, tn: String) -> TypeID {
         let tyid = TypeID::Fun(self.type_lit_counter);
         self.type_lit_counter += 1;
-        self.insert(tn, tyid.clone());
+        self.typenames.insert(tn, tyid.clone());
         tyid
     }
 
-    fn get_typename(&self, tid: &TypeID) -> Option<String> {
+    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> {
         self.typenames.my.get(tid).cloned()
     }
 
-    fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+    pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
         self.typenames.mλ.get(tn).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

@@ -2,32 +2,21 @@
 pub mod bimap;
 pub mod dict;
 pub mod term;
-pub mod substitution;
-
 pub mod lexer;
 pub mod parser;
 pub mod unparser;
-pub mod sugar;
 pub mod curry;
 pub mod lnf;
 pub mod pnf;
 pub mod subtype;
 pub mod unification;
-pub mod morphism;
-pub mod morphism_base;
-pub mod morphism_path;
 
 #[cfg(test)]
 mod test;
 
-#[cfg(feature = "pretty")]
-mod pretty;
-
 pub use {
     dict::*,
     term::*,
-    substitution::*,
-    sugar::*,
-    unification::*,
-    morphism::*
+    unification::*
 };
+

src/morphism.rs

@@ -1,63 +0,0 @@
-use {
-    crate::{
-        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
-    },
-    std::{collections::HashMap, u64}
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone, PartialEq, Eq, Debug)]
-pub struct MorphismType {
-    pub src_type: TypeTerm,
-    pub dst_type: TypeTerm,
-}
-
-impl MorphismType {
-    pub fn normalize(self) -> Self {
-        MorphismType {
-            src_type: self.src_type.normalize().param_normalize(),
-            dst_type: self.dst_type.normalize().param_normalize()
-        }
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-pub trait Morphism : Sized {
-    fn get_type(&self) -> MorphismType;
-    fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
-
-    fn weight(&self) -> u64 {
-        1
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone, Debug, PartialEq)]
-pub struct MorphismInstance<M: Morphism + Clone> {
-    pub halo: TypeTerm,
-    pub m: M,
-    pub σ: HashMap<TypeID, TypeTerm>
-}
-
-impl<M: Morphism + Clone> MorphismInstance<M> {
-    pub fn get_type(&self) -> MorphismType {
-        MorphismType {
-            src_type: TypeTerm::Ladder(vec![
-                self.halo.clone(),
-                self.m.get_type().src_type.clone()
-            ]).apply_substitution(&self.σ)
-            .clone(),
-
-            dst_type: TypeTerm::Ladder(vec![
-                self.halo.clone(),
-                self.m.get_type().dst_type.clone()
-            ]).apply_substitution(&self.σ)
-            .clone()
-        }.normalize()
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_base.rs

@@ -1,183 +0,0 @@
-use {
-    crate::{
-        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm,
-        morphism::{MorphismType, Morphism, MorphismInstance}
-    },
-    std::{collections::HashMap, u64}
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone)]
-pub struct MorphismBase<M: Morphism + Clone> {
-    morphisms: Vec< M >,
-    seq_types: Vec< TypeTerm >
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl<M: Morphism + Clone> MorphismBase<M> {
-    pub fn new(seq_types: Vec<TypeTerm>) -> Self {
-        MorphismBase {
-            morphisms: Vec::new(),
-            seq_types
-        }
-    }
-
-    pub fn add_morphism(&mut self, m: M) {
-        self.morphisms.push( m );
-    }
-
-    pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
-    -> Vec< MorphismInstance<M> >
-    {
-        let mut dst_types = Vec::new();
-        for m in self.morphisms.iter() {
-            if let Ok((halo, σ)) = crate::unification::subtype_unify(
-                &src_type.clone().param_normalize(),
-                &m.get_type().src_type.param_normalize(),
-            ) {
-                dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
-            }
-        }
-        dst_types
-    }
-
-    pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
-    -> Vec< MorphismInstance<M> > {
-        let src_type = src_type.clone().param_normalize();
-        let mut dst_types = Vec::new();
-
-        // Check if we have a List type, and if so, see what the Item type is
-        // TODO: function for generating fresh variables
-        let item_variable = TypeID::Var(800);
-
-        for seq_type in self.seq_types.iter() {
-            if let Ok((halo, σ)) = crate::unification::subtype_unify(
-                &src_type,
-                &TypeTerm::App(vec![
-                    seq_type.clone(),
-                    TypeTerm::TypeID(item_variable)
-                ])
-            ) {
-                let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
-                for item_morph_inst in self.enum_morphisms( &src_item_type ) {
-
-                    let mut dst_halo_ladder = vec![ halo.clone() ];
-                    if item_morph_inst.halo != TypeTerm::unit() {
-                        dst_halo_ladder.push(
-                            TypeTerm::App(vec![
-                                seq_type.clone().get_lnf_vec().first().unwrap().clone(),
-                                item_morph_inst.halo.clone()
-                            ]));
-                    }
-
-                    if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
-                        dst_types.push(
-                            MorphismInstance {
-                                halo: TypeTerm::Ladder(dst_halo_ladder).strip().param_normalize(),
-                                m: map_morph,
-                                σ: item_morph_inst.σ
-                            }
-                        );
-                    } else {
-                        eprintln!("could not get map morphism");
-                    }
-                }
-            }
-        }
-
-        dst_types
-    }
-
-    pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
-        let mut dst_types = Vec::new();
-        dst_types.append(&mut self.enum_direct_morphisms(src_type));
-        dst_types.append(&mut self.enum_map_morphisms(src_type));
-        dst_types
-    }
-
-    pub fn find_direct_morphism(&self,
-        ty: &MorphismType,
-        dict: &mut impl TypeDict
-    ) -> Option< MorphismInstance<M> > {
-        eprintln!("find direct morph");
-        for m in self.morphisms.iter() {
-            let ty = ty.clone().normalize();
-            let morph_type = m.get_type().normalize();
-
-            eprintln!("find direct morph:\n   {}  <=   {}",
-                            dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
-                        );
-
-            if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
-                eprintln!("halo: {}", dict.unparse(&halo));
-
-                let dst_type = TypeTerm::Ladder(vec![
-                    halo.clone(),
-                    morph_type.dst_type.clone()
-                ]).normalize().param_normalize();
-
-                eprintln!("----------->   {}  <=   {}",
-                    dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
-                );
-
-                if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
-                    eprintln!("match. halo2 = {}", dict.unparse(&halo2));
-                    return Some(MorphismInstance {
-                        m: m.clone(),
-                        halo,
-                        σ,
-                    });
-                }
-            }
-        }
-        None
-    }
-
-    pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
-        for seq_type in self.seq_types.iter() {
-            if let Ok((halos, σ)) = UnificationProblem::new_sub(vec![
-                (ty.src_type.clone().param_normalize(),
-                    TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
-
-                (TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
-                    ty.dst_type.clone().param_normalize()),
-            ]).solve() {
-                // TODO: use real fresh variable names
-                let item_morph_type = MorphismType {
-                    src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
-                    dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
-                }.normalize();
-
-                //eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
-                if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
-                    if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
-                        return Some( MorphismInstance {
-                            m: list_morph,
-                            σ,
-                            halo: halos[0].clone()
-                        } );
-                    }
-                }
-            }
-        }
-
-        None
-    }
-
-    pub fn find_morphism(&self, ty: &MorphismType,
-        dict: &mut impl TypeDict
-    )
-    -> Option< MorphismInstance<M> > {
-        if let Some(m) = self.find_direct_morphism(ty, dict) {
-            return Some(m);
-        }
-        if let Some(m) = self.find_map_morphism(ty, dict) {
-            return Some(m);
-        }
-        None
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_path.rs

@@ -1,136 +0,0 @@
-use {
-    crate::{
-        morphism::{MorphismType, Morphism, MorphismInstance},
-        morphism_base::MorphismBase,
-        dict::*,
-        term::*
-    }
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone)]
-pub struct MorphismPath<M: Morphism + Clone> {
-    pub weight: u64,
-    pub cur_type: TypeTerm,
-    pub morphisms: Vec< MorphismInstance<M> >
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-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 solve(&mut self) -> Option< Vec<MorphismInstance<M>> > {
-        while ! self.queue.is_empty() {
-            self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
-
-            if let Some(mut cur_path) = self.queue.pop() {
-                if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
-                    /* found path,
-                     * now apply substitution and trim to variables in terms of each step
-                     */
-                    for n in cur_path.morphisms.iter_mut() {
-                        let src_type = n.m.get_type().src_type;
-                        let dst_type = n.m.get_type().dst_type;
-
-                        let mut new_σ = std::collections::HashMap::new();
-                        for (k,v) in σ.iter() {
-                            if let TypeID::Var(varid) = k {
-                                if src_type.contains_var(*varid)
-                                || dst_type.contains_var(*varid) {
-                                    new_σ.insert(
-                                        k.clone(),
-                                        v.clone().apply_substitution(&σ).clone().strip()
-                                    );
-                                }
-                            }
-                        }
-                        for (k,v) in n.σ.iter() {
-                            if let TypeID::Var(varid) = k {
-                                if src_type.contains_var(*varid)
-                                || dst_type.contains_var(*varid) {
-                                    new_σ.insert(
-                                        k.clone(),
-                                        v.clone().apply_substitution(&σ).clone().strip()
-                                    );
-                                }
-                            }
-                        }
-
-                        n.halo = n.halo.clone().apply_substitution(&σ).clone().strip().param_normalize();
-
-                        n.σ = new_σ;
-                    }
-
-                    return Some(cur_path.morphisms);
-                }
-
-                //eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
-                for mut next_morph_inst in self.morphism_base.enum_morphisms(&cur_path.cur_type) {
-                    let dst_type = next_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 = cur_path.clone();
-                    for n in new_path.morphisms.iter_mut() {
-                        let mut new_σ = std::collections::HashMap::new();
-
-                        for (k,v) in next_morph_inst.σ.iter() {
-                            new_σ.insert(
-                                k.clone(),
-                                v.clone().apply_substitution(&next_morph_inst.σ).clone()
-                            );
-                        }
-
-                        for (k,v) in n.σ.iter() {
-                            new_σ.insert(
-                                k.clone(),
-                                v.clone().apply_substitution(&next_morph_inst.σ).clone()
-                            );
-                        }
-
-                        n.halo = n.halo.clone().apply_substitution(&next_morph_inst.σ).clone().strip().param_normalize();
-
-                        n.σ = new_σ;
-                    }
-
-                    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 += next_morph_inst.m.weight();
-                        new_path.cur_type = dst_type;
-
-                        new_path.morphisms.push(next_morph_inst);
-                        self.queue.push(new_path);
-                    }
-                }
-            }
-        }
-        None
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/parser.rs

@@ -18,23 +18,10 @@ pub enum ParseError {
     UnexpectedToken
 }
 
-pub trait ParseLadderType {
-    fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError>;
-    
-    fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
-    where It: Iterator<Item = char>;
-
-    fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
-    where It: Iterator<Item = char>;
-
-    fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
-    where It: Iterator<Item = char>;
-}
-
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl<T: TypeDict> ParseLadderType for T {
-    fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
+impl TypeDict {
+    pub fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
         let mut tokens = LadderTypeLexer::from(s.chars()).peekable();
 
         match self.parse_ladder(&mut tokens) {

src/pnf.rs

@@ -2,20 +2,6 @@ use crate::term::TypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm >  ) -> Vec< TypeTerm > {
-    for i in 0 .. upper.len() {
-        if upper[i] == lower[0] {
-            let mut result_ladder = Vec::<TypeTerm>::new();
-            result_ladder.append(&mut upper[0..i].iter().cloned().collect());
-            result_ladder.append(&mut lower);
-            return result_ladder;
-        }
-    }
-
-    upper.append(&mut lower);
-    upper
-}
-
 impl TypeTerm {
     /// transmute type into Parameter-Normal-Form (PNF)
     ///
@@ -24,99 +10,88 @@ impl TypeTerm {
     /// <Seq <Digit 10>>~<Seq Char>
     /// ⇒ <Seq <Digit 10>~Char>
     /// ```
-    pub fn param_normalize(mut self) -> Self {
+    pub fn param_normalize(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 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 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) );
-                                        } else {
-                                            rungs.pop();
-                                            rungs.push(TypeTerm::App(new_rung_params));
-                                        }
-
-                                    } else {
-                                        new_rungs.push( TypeTerm::App(bot_args) );
-                                    }
-                                }
-                                (bottom, last_buf) => {
-                                    new_rungs.push( bottom );
-                                }
-                            }
-                        } else {
-                            new_rungs.push( bottom );
-                        }
+                    // normalize all rungs separately
+                    for r in rungs.iter_mut() {
+                        *r = r.clone().param_normalize();
                     }
 
-                    new_rungs.reverse();
+                    // take top-rung
+                    match rungs.remove(0) {
+                        TypeTerm::App(params_top) => {
+                            let mut params_ladders = Vec::new();
+                            let mut tail : Vec<TypeTerm> = Vec::new();
 
-                    if new_rungs.len() > 1 {
-                        TypeTerm::Ladder(new_rungs)
-                    } else if new_rungs.len() == 1 {
-                        new_rungs[0].clone()
-                    } else {
-                        TypeTerm::unit()
+                            // append all other rungs to ladders inside
+                            // the application
+                            for p in params_top {
+                                params_ladders.push(vec![ p ]);
+                            }
+
+                            for r in rungs {
+                                match r {
+                                    TypeTerm::App(mut params_rung) => {
+                                        if params_rung.len() > 0 {
+                                            let mut first_param = params_rung.remove(0); 
+
+                                            if first_param == params_ladders[0][0] {
+                                               for (l, p) in params_ladders.iter_mut().skip(1).zip(params_rung) {
+                                                   l.push(p.param_normalize());
+                                               }
+                                            } else {
+                                               params_rung.insert(0, first_param);
+                                               tail.push(TypeTerm::App(params_rung));
+                                            }
+                                        }
+                                    }
+
+                                    TypeTerm::Ladder(mut rs) => {
+                                        for r in rs {
+                                            tail.push(r.param_normalize());
+                                        }
+                                    }
+
+                                    atomic => {
+                                        tail.push(atomic);
+                                    }
+                                }
+                            }
+
+                            let head = TypeTerm::App(
+                                params_ladders.into_iter()
+                                    .map(
+                                        |mut l| {
+                                            l.dedup();
+                                            match l.len() {
+                                                0 => TypeTerm::unit(),
+                                                1 => l.remove(0),
+                                                _ => TypeTerm::Ladder(l).param_normalize()
+                                            }
+                                        }
+                                    )
+                                    .collect()
+                            );
+
+                            if tail.len() > 0 {
+                                tail.insert(0, head);
+                                TypeTerm::Ladder(tail)
+                            } else {
+                                head
+                            }
+                        }
+
+                        TypeTerm::Ladder(mut r) => {
+                            r.append(&mut rungs);
+                            TypeTerm::Ladder(r)
+                        }
+
+                        atomic => {
+                            rungs.insert(0, atomic);
+                            TypeTerm::Ladder(rungs)
+                        }
                     }
                 } else {
                     TypeTerm::unit()

src/pretty.rs

@@ -1,157 +0,0 @@
-use {
-    crate::{TypeDict, dict::TypeID},
-    crate::sugar::SugaredTypeTerm,
-    tiny_ansi::TinyAnsi
-};
-
-impl SugaredTypeTerm {
-    pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
-        let indent_width = 4;
-        match self {
-            SugaredTypeTerm::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).green().bold()
-            }
-
-            SugaredTypeTerm::Char(c) => {
-                match c {
-                    '\0' => format!("'\\0'"),
-                    '\n' => format!("'\\n'"),
-                    _ => format!("'{}'", c)
-                }
-            }
-
-            SugaredTypeTerm::Univ(t) => {
-                format!("{} {} . {}",
-                    "∀".yellow().bold(),
-                    dict.get_varname(0).unwrap_or("??".into()).bright_blue(),
-                    t.pretty(dict,indent)
-                )
-            }
-
-            SugaredTypeTerm::Spec(args) => {
-                let mut s = String::new();
-                s.push_str(&"<".yellow());
-                for i in 0..args.len() {
-                    let arg = &args[i];
-                    if i > 0 {
-                        s.push(' ');
-                    }
-                    s.push_str( &arg.pretty(dict,indent+1) );
-                }
-                s.push_str(&">".yellow());
-                s
-            }
-
-            SugaredTypeTerm::Struct(args) => {
-                let mut s = String::new();
-                s.push_str(&"{".yellow().bold());
-                for arg in args {
-                    s.push('\n');
-                    for x in 0..(indent+1)*indent_width {
-                        s.push(' ');
-                    }
-                    s.push_str(&arg.pretty(dict, indent + 1));
-                    s.push_str(&";\n".bright_yellow());
-                }
-
-                s.push('\n');
-                for x in 0..indent*indent_width {
-                    s.push(' ');
-                }
-                s.push_str(&"}".yellow().bold());
-                s
-            }
-
-            SugaredTypeTerm::Enum(args) => {
-                let mut s = String::new();
-                s.push_str(&"(".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
-                    s.push('\n');
-                    for x in 0..(indent+1)*indent_width {
-                        s.push(' ');
-                    }
-                    if i > 0 {
-                        s.push_str(&"| ".yellow().bold());
-                    }
-                    s.push_str(&arg.pretty(dict, indent + 1));
-                }
-
-                s.push('\n');
-                for x in 0..indent*indent_width {
-                    s.push(' ');
-                }
-                s.push_str(&")".yellow().bold());
-                s
-            }
-
-            SugaredTypeTerm::Seq(args) => {
-                let mut s = String::new();
-                s.push_str(&"[ ".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
-                    if i > 0 {
-                        s.push(' ');
-                    }
-                    s.push_str(&arg.pretty(dict, indent+1));
-                }
-                s.push_str(&" ]".yellow().bold());
-                s
-            }
-
-            SugaredTypeTerm::Morph(args) => {
-                let mut s = String::new();
-                for arg in args {
-                    s.push_str(&"  ~~morph~~>  ".bright_yellow());
-                    s.push_str(&arg.pretty(dict, indent));
-                }
-                s
-            }
-
-            SugaredTypeTerm::Func(args) => {
-                let mut s = String::new();
-                for i in 0..args.len() {
-                    let arg = &args[i];
-                    if i > 0{
-                        s.push('\n');
-                        for x in 0..(indent*indent_width) {
-                            s.push(' ');
-                        }
-                        s.push_str(&"-->  ".bright_yellow());
-                    } else {
-//                        s.push_str("   ");
-                    }
-                    s.push_str(&arg.pretty(dict, indent));
-                }
-                s
-            }
-
-            SugaredTypeTerm::Ladder(rungs) => {
-                let mut s = String::new();
-                for i in 0..rungs.len() {
-                    let rung = &rungs[i];
-                    if i > 0{
-                        s.push('\n');
-                        for x in 0..(indent*indent_width) {
-                            s.push(' ');
-                        }
-                        s.push_str(&"~ ".yellow());
-                    }
-                    s.push_str(&rung.pretty(dict, indent));
-                }
-                s
-            }
-        }
-    }
-}

src/substitution.rs

@@ -1,64 +0,0 @@
-
-use crate::{
-    TypeID,
-    TypeTerm
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-pub trait Substitution {
-    fn get(&self, t: &TypeID) -> Option< TypeTerm >;
-}
-
-impl<S: Fn(&TypeID)->Option<TypeTerm>> Substitution for S {
-    fn get(&self, t: &TypeID) -> Option< TypeTerm > {
-        (self)(t)
-    }
-}
-
-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()
-    }
-}
-
-pub type HashMapSubst = std::collections::HashMap< TypeID, TypeTerm >;
-
-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::TypeID(typid) => {
-                if let Some(t) = σ.get(typid) {
-                    *self = t;
-                }
-            }
-
-            TypeTerm::Ladder(rungs) => {
-                for r in rungs.iter_mut() {
-                    r.apply_subst(σ);
-                }
-            }
-            TypeTerm::App(args) => {
-                for r in args.iter_mut() {
-                    r.apply_subst(σ);
-                }
-            }
-            _ => {}
-        }
-
-        self
-    }
-}

src/subtype.rs

@@ -2,7 +2,49 @@ use crate::term::TypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeTerm {    
+impl TypeTerm {
+    pub fn find_semantic_subtype_matches(&self, expected_type: &TypeTerm)
+    -> Option<(TypeTerm, TypeTerm, TypeTerm)>
+    {
+        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] {
+                // found first match.
+                // now find first mismatch.
+                for j in i..usize::min(provided_lnf.len(), i+expected_lnf.len()) {
+                    if provided_lnf[j] != expected_lnf[ j-i ] {
+
+                        eprintln!("found match at {}, mismatch at {}", i, j);
+                        let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. j ].into_iter().cloned().collect() );
+                        let provided_reprladder = TypeTerm::Ladder( provided_lnf[ j .. ].into_iter().cloned().collect() );
+                        let expected_reprladder = TypeTerm::Ladder( expected_lnf[ j-i .. ].into_iter().cloned().collect() );
+                        return Some((syntactic_subladder, provided_reprladder, expected_reprladder));
+                    }
+                }
+
+                eprintln!("only syntactic subtype");
+
+                // syntactic subtype
+                let n = {
+                    if provided_lnf.len() + i < expected_lnf.len() {
+                        1
+                    } else {
+                        2
+                    }
+                };
+
+                let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. provided_lnf.len()-1 ].into_iter().cloned().collect() );
+                let provided_reprladder = TypeTerm::Ladder( provided_lnf[ provided_lnf.len()-n .. ].into_iter().cloned().collect() );
+                let expected_reprladder = TypeTerm::Ladder( expected_lnf[ provided_lnf.len()-n-i .. ].into_iter().cloned().collect() );
+                return Some((syntactic_subladder, provided_reprladder, expected_reprladder));
+            }
+        }
+
+        None
+    }
+    
     // returns ladder-step of first match and provided representation-type
     pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
         let provided_lnf = self.clone().get_lnf_vec();

src/sugar.rs

@@ -1,114 +0,0 @@
-use {
-    crate::{TypeTerm, TypeID, parser::ParseLadderType}
-};
-
-#[derive(Clone)]
-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 impl 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 impl 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()),
-        }
-    }
-
-    pub fn is_empty(&self) -> bool {
-        match self {
-            SugaredTypeTerm::TypeID(_) => false,
-            SugaredTypeTerm::Num(_) => false,
-            SugaredTypeTerm::Char(_) => false,
-            SugaredTypeTerm::Univ(t) => t.is_empty(),
-            SugaredTypeTerm::Spec(ts) |
-            SugaredTypeTerm::Ladder(ts) |
-            SugaredTypeTerm::Func(ts) |
-            SugaredTypeTerm::Morph(ts) |
-            SugaredTypeTerm::Struct(ts) |
-            SugaredTypeTerm::Enum(ts) |
-            SugaredTypeTerm::Seq(ts) => {
-                ts.iter().fold(true, |s,t|s&&t.is_empty())
-            }
-        }
-    }
-}
-

src/term.rs

@@ -14,7 +14,7 @@ pub enum TypeTerm {
     Num(i64),
     Char(char),
 
-
+    
 
     /* Complex Terms */
 
@@ -47,7 +47,7 @@ impl TypeTerm {
                 *self = TypeTerm::App(vec![
                     self.clone(),
                     t.into()
-                ])
+                ])                
             }
         }
 
@@ -57,7 +57,7 @@ impl TypeTerm {
     pub fn repr_as(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
         match self {
             TypeTerm::Ladder(rungs) => {
-                rungs.push(t.into());
+                rungs.push(t.into());                
             }
 
             _ => {
@@ -79,77 +79,34 @@ impl TypeTerm {
         self.arg(TypeTerm::Char(c))
     }
 
-    pub fn contains_var(&self, var_id: u64) -> bool {
+    /// 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 {
         match self {
-            TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
-            TypeTerm::App(args) |
-            TypeTerm::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 {
-            TypeTerm::Ladder(rungs) => {
-                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();
-
-                if rungs.len() == 1 {
-                    rungs.pop().unwrap()
-                } else {
-                    TypeTerm::Ladder(rungs)
-                }
-            },
-            TypeTerm::App(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::App(args)
+            TypeTerm::TypeID(typid) => {
+                if let Some(t) = subst(typid) {
+                    *self = t;
                 }
             }
-            atom => atom
-        }
-    }
 
-    pub fn get_interface_type(&self) -> TypeTerm {
-        match self {
             TypeTerm::Ladder(rungs) => {
-                if let Some(top) = rungs.first() {
-                    top.get_interface_type()
-                } else {
-                    TypeTerm::unit()
+                for r in rungs.iter_mut() {
+                    r.apply_substitution(subst);
                 }
             }
             TypeTerm::App(args) => {
-                TypeTerm::App(args.iter().map(|a| a.get_interface_type()).collect())
+                for r in args.iter_mut() {
+                    r.apply_substitution(subst);
+                }
             }
-            atom => atom.clone()
+            _ => {}
         }
+
+        self
     }
 }
 

src/test/curry.rs

@@ -1,12 +1,12 @@
 use {
-    crate::{dict::*, parser::*}
+    crate::{dict::*}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 #[test]
 fn test_curry() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("<A B C>").unwrap().curry(),
@@ -33,7 +33,7 @@ fn test_curry() {
 
 #[test]
 fn test_decurry() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("<<A B> C>").unwrap().decurry(),
@@ -47,7 +47,7 @@ fn test_decurry() {
         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()
     );
-
+    
     assert_eq!(
         dict.parse("<<A~X B> C>").unwrap().decurry(),
         dict.parse("<A~X B C>").unwrap()

src/test/lnf.rs

@@ -1,8 +1,8 @@
-use crate::{dict::{BimapTypeDict}, parser::*};
+use crate::dict::TypeDict;
 
 #[test]
 fn test_flat() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert!( dict.parse("A").expect("parse error").is_flat() );
     assert!( dict.parse("10").expect("parse error").is_flat() );
@@ -17,7 +17,7 @@ fn test_flat() {
 
 #[test]
 fn test_normalize() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("A~B~C").expect("parse error").normalize(),
@@ -54,3 +54,4 @@ fn test_normalize() {
     );
 
 }
+

src/test/mod.rs

@@ -7,5 +7,4 @@ pub mod pnf;
 pub mod subtype;
 pub mod substitution;
 pub mod unification;
-pub mod morphism;
 

src/test/morphism.rs

@@ -1,471 +0,0 @@
-use {
-    crate::{dict::*, morphism::*, parser::*, unparser::*, TypeTerm, morphism_base::*, morphism_path::*}
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-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(),
-            dict.unparse(v)
-        );
-    }
-
-    eprintln!("}}");
-}
-
-fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance<DummyMorphism>>) {
-    for n in path.iter() {
-        eprintln!("
-ψ = {}
-morph {}
---> {}
-with
-        ",
-        n.halo.clone().sugar(dict).pretty(dict, 0),
-        n.m.get_type().src_type.sugar(dict).pretty(dict, 0),
-        n.m.get_type().dst_type.sugar(dict).pretty(dict, 0),
-        );
-        print_subst(&n.σ, dict)
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-#[derive(Clone, Debug, PartialEq)]
-struct DummyMorphism(MorphismType);
-
-impl Morphism for DummyMorphism {
-    fn get_type(&self) -> MorphismType {
-        self.0.clone().normalize()
-    }
-
-    fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
-        Some(DummyMorphism(MorphismType {
-            src_type: TypeTerm::App(vec![
-                seq_type.clone(),
-                self.0.src_type.clone()
-            ]),
-
-            dst_type: TypeTerm::App(vec![
-                seq_type.clone(),
-                self.0.dst_type.clone()
-            ])
-        }))
-    }
-}
-
-fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
-    let mut dict = BimapTypeDict::new();
-    let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
-
-    dict.add_varname("Radix".into());
-    dict.add_varname("SrcRadix".into());
-    dict.add_varname("DstRadix".into());
-
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
-            dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
-        })
-    );
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
-            dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
-        })
-    );
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
-            dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
-        })
-    );
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
-            dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
-        })
-    );
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap(),
-            dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap()
-        })
-    );
-
-    (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("<Digit 10> ~ Char").unwrap(),
-        dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
-    }).solve();
-
-    assert_eq!(
-        path,
-        Some(
-            vec![
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
-                        dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
-                    }),
-                }
-            ]
-    ));
-}
-
-
-#[test]
-fn test_morphism_path2() {
-    let (mut dict, mut base) = morphism_test_setup();
-
-    let path = ShortestPathProblem::new(&base, MorphismType {
-        src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-        dst_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-    }).solve();
-
-    assert_eq!(
-        path,
-        Some(
-            vec![
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect(""),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                }
-            ]
-    ));
-}
-
-
-#[test]
-fn test_morphism_path3() {
-    let (mut dict, mut base) = morphism_test_setup();
-
-    let path = ShortestPathProblem::new(&base, MorphismType {
-        src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-        dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-    }).solve();
-
-    if let Some(path) = path.as_ref() {
-        print_path(&mut dict, path);
-    }
-
-    assert_eq!(
-        path,
-        Some(
-            vec![
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
-                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                }
-            ]
-    ));
-}
-
-
-
-#[test]
-fn test_morphism_path4() {
-    let (mut dict, mut base) = morphism_test_setup();
-
-    let path = ShortestPathProblem::new(&base, MorphismType {
-        src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-        dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
-    }).solve();
-
-    if let Some(path) = path.as_ref() {
-        print_path(&mut dict, path);
-    }
-
-    assert_eq!(
-        path,
-        Some(
-            vec![
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
-                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 16 LittleEndian>").expect(""),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),                        
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
-                    }),
-                },
-                
-            ]
-    ));
-}
-
-
-
-
-#[test]
-fn test_morphism_path_posint() {
-    let (mut dict, mut base) = morphism_test_setup();
-
-    let path = ShortestPathProblem::new(&base, MorphismType {
-        src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-        dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap(),
-    }).solve();
-
-    if let Some(path) = path.as_ref() {
-        print_path(&mut dict, path);
-    }
-
-    assert_eq!(
-        path,
-        Some(
-            vec![
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
-                    m: DummyMorphism(MorphismType {
-                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType{
-                        src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
-                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType{
-                        src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                    }),
-                },
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
-                    ].into_iter().collect(),
-                    halo: TypeTerm::unit(),
-                    m: DummyMorphism(MorphismType{
-                        src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                    }),
-                },
-                MorphismInstance {
-                    σ: vec![
-                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
-                    ].into_iter().collect(),
-                    halo: dict.parse("ℕ ~ <PosInt 16 BigEndian>").unwrap(),
-                    m: DummyMorphism(MorphismType{
-                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
-                        dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
-                    })
-                }
-            ]
-        )
-    );
-/*
-    assert_eq!(
-        base.find_morphism_path(MorphismType {
-            src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-            dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
-        }),
-        Some(
-            vec![
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
-            ]
-        )
-    );
-    */
-
-
-/*
-    assert_eq!(
-        base.find_morphism_with_subtyping(
-            &MorphismType {
-                src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-                dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-            }
-        ),
-
-        Some((
-                DummyMorphism(MorphismType{
-                    src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                    dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                }),
-
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian>").unwrap(),
-
-                vec![
-                    (dict.get_typeid(&"Radix".into()).unwrap(),
-                    dict.parse("10").unwrap())
-                ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
-        ))
-    );
-    */
-}
-
-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("<List~Vec Char>").unwrap(),
-            dst_type: dict.parse("<List Char>").unwrap()
-        })
-    );
-    base.add_morphism(
-        DummyMorphism(MorphismType{
-            src_type: dict.parse("<List Char>").unwrap(),
-            dst_type: dict.parse("<List Char~ReprTree>").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

@@ -7,7 +7,7 @@ use {
 
 #[test]
 fn test_parser_id() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     dict.add_varname("T".into());
 
@@ -26,7 +26,7 @@ fn test_parser_id() {
 fn test_parser_num() {
     assert_eq!(
         Ok(TypeTerm::Num(1234)),
-        BimapTypeDict::new().parse("1234")
+        TypeDict::new().parse("1234")
     );
 }
 
@@ -34,21 +34,21 @@ fn test_parser_num() {
 fn test_parser_char() {
     assert_eq!(
         Ok(TypeTerm::Char('x')),
-        BimapTypeDict::new().parse("'x'")
+        TypeDict::new().parse("'x'")
     );
 }
 
 #[test]
 fn test_parser_app() {
     assert_eq!(
-        BimapTypeDict::new().parse("<A B>"),
+        TypeDict::new().parse("<A B>"),
         Ok(TypeTerm::App(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
         ]))
     );
     assert_eq!(
-        BimapTypeDict::new().parse("<A B C>"),
+        TypeDict::new().parse("<A B C>"),
         Ok(TypeTerm::App(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
@@ -60,7 +60,7 @@ fn test_parser_app() {
 #[test]
 fn test_parser_unexpected_close() {
     assert_eq!(
-        BimapTypeDict::new().parse(">"),
+        TypeDict::new().parse(">"),
         Err(ParseError::UnexpectedClose)
     );
 }
@@ -68,7 +68,7 @@ fn test_parser_unexpected_close() {
 #[test]
 fn test_parser_unexpected_token() {
     assert_eq!(
-        BimapTypeDict::new().parse("A B"),
+        TypeDict::new().parse("A B"),
         Err(ParseError::UnexpectedToken)
     );
 }
@@ -76,14 +76,14 @@ fn test_parser_unexpected_token() {
 #[test]
 fn test_parser_ladder() {
     assert_eq!(
-        BimapTypeDict::new().parse("A~B"),
+        TypeDict::new().parse("A~B"),
         Ok(TypeTerm::Ladder(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
         ]))
     );
     assert_eq!(
-        BimapTypeDict::new().parse("A~B~C"),
+        TypeDict::new().parse("A~B~C"),
         Ok(TypeTerm::Ladder(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::TypeID(TypeID::Fun(1)),
@@ -95,7 +95,7 @@ fn test_parser_ladder() {
 #[test]
 fn test_parser_ladder_outside() {
     assert_eq!(
-        BimapTypeDict::new().parse("<A B>~C"),
+        TypeDict::new().parse("<A B>~C"),
         Ok(TypeTerm::Ladder(vec![
             TypeTerm::App(vec![
                 TypeTerm::TypeID(TypeID::Fun(0)),
@@ -103,13 +103,13 @@ fn test_parser_ladder_outside() {
             ]),
             TypeTerm::TypeID(TypeID::Fun(2)),
         ]))
-    );
+    );    
 }
 
 #[test]
 fn test_parser_ladder_inside() {
     assert_eq!(
-        BimapTypeDict::new().parse("<A B~C>"),
+        TypeDict::new().parse("<A B~C>"),
         Ok(TypeTerm::App(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::Ladder(vec![
@@ -117,13 +117,13 @@ fn test_parser_ladder_inside() {
                 TypeTerm::TypeID(TypeID::Fun(2)),
             ])
         ]))
-    );
+    );    
 }
 
 #[test]
 fn test_parser_ladder_between() {
     assert_eq!(
-        BimapTypeDict::new().parse("<A B~<C D>>"),
+        TypeDict::new().parse("<A B~<C D>>"),
         Ok(TypeTerm::App(vec![
             TypeTerm::TypeID(TypeID::Fun(0)),
             TypeTerm::Ladder(vec![
@@ -134,14 +134,14 @@ fn test_parser_ladder_between() {
                 ])
             ])
         ]))
-    );
+    );    
 }
 
 
 #[test]
 fn test_parser_ladder_large() {
     assert_eq!(
-        BimapTypeDict::new().parse(
+        TypeDict::new().parse(
             "<Seq Date
                   ~<TimeSince UnixEpoch>
                   ~<Duration Seconds>
@@ -203,3 +203,4 @@ fn test_parser_ladder_large() {
         )
     );
 }
+

src/test/pnf.rs

@@ -1,8 +1,8 @@
-use crate::{dict::BimapTypeDict, parser::*};
+use crate::dict::TypeDict;
 
 #[test]
 fn test_param_normalize() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("A~B~C").expect("parse error"),
@@ -19,40 +19,23 @@ fn test_param_normalize() {
         dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
     );
 
-    assert_eq!(
-        dict.parse("<A~Y B>").expect("parse error"),
-        dict.parse("<A B>~<Y B>").expect("parse error").param_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(),
     );
 
-    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~D~E> F~G 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")
+                   ~<A <B E> F H H>
+                   ~<A <B E> G H H>").expect("parse errror")
                .param_normalize(),
     );
 }
+

src/test/substitution.rs

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

src/test/subtype.rs

@@ -1,8 +1,8 @@
-use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+use crate::dict::TypeDict;
 
 #[test]
 fn test_semantic_subtype() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("A~B~C").expect("parse error")
@@ -19,11 +19,11 @@ fn test_semantic_subtype() {
             ),
         Some((0, dict.parse("A~B1~C1").expect("parse errror")))
     );
-
+    
     assert_eq!(
         dict.parse("A~B~C1").expect("parse error")
             .is_semantic_subtype_of(
-                &dict.parse("B~C2").expect("parse errror")
+                &dict.parse("B~C2").expect("parse errror")  
             ),
         Some((1, dict.parse("B~C1").expect("parse errror")))
     );
@@ -31,12 +31,12 @@ fn test_semantic_subtype() {
 
 #[test]
 fn test_syntactic_subtype() {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     assert_eq!(
         dict.parse("A~B~C").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("A~B~C").expect("parse errror")
+                &dict.parse("A~B~C").expect("parse errror")  
             ),
         Ok(0)
     );
@@ -44,7 +44,7 @@ fn test_syntactic_subtype() {
     assert_eq!(
         dict.parse("A~B~C").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("B~C").expect("parse errror")
+                &dict.parse("B~C").expect("parse errror")  
             ),
         Ok(1)
     );
@@ -52,7 +52,7 @@ fn test_syntactic_subtype() {
     assert_eq!(
         dict.parse("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("C~D").expect("parse errror")
+                &dict.parse("C~D").expect("parse errror")  
             ),
         Ok(2)
     );
@@ -60,7 +60,7 @@ fn test_syntactic_subtype() {
     assert_eq!(
         dict.parse("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("C~G").expect("parse errror")
+                &dict.parse("C~G").expect("parse errror")  
             ),
         Err((2,3))
     );
@@ -68,7 +68,7 @@ fn test_syntactic_subtype() {
     assert_eq!(
         dict.parse("A~B~C~D~E").expect("parse error")
             .is_syntactic_subtype_of(
-                &dict.parse("G~F~K").expect("parse errror")
+                &dict.parse("G~F~K").expect("parse errror")  
             ),
         Err((0,0))
     );
@@ -94,3 +94,4 @@ fn test_syntactic_subtype() {
         Ok(4)
     );
 }
+

src/test/unification.rs

@@ -1,13 +1,13 @@
 
 use {
-    crate::{dict::*, parser::*, unparser::*, term::*, unification::*},
+    crate::{dict::*, term::*, unification::*},
     std::iter::FromIterator
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
 fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::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_subst(&σ),
-            t2.apply_subst(&σ)
+            t1.apply_substitution(&|v| σ.get(v).cloned()),
+            t2.apply_substitution(&|v| σ.get(v).cloned())
         );
     } 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 = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
     dict.add_varname(String::from("T"));
 
     assert_eq!(
@@ -61,19 +61,6 @@ fn test_unification_error() {
             t2: dict.parse("B").unwrap()
         })
     );
-
-    assert_eq!(
-        crate::unify(
-            &dict.parse("T").unwrap(),
-            &dict.parse("<Seq T>").unwrap()
-        ),
-
-        Err(UnificationError {
-            addr: vec![],
-            t1: dict.parse("T").unwrap(),
-            t2: dict.parse("<Seq T>").unwrap()
-        })
-    );
 }
 
 #[test]
@@ -89,7 +76,7 @@ fn test_unification() {
         true
     );
 
-    let mut dict = BimapTypeDict::new();
+    let mut dict = TypeDict::new();
 
     dict.add_varname(String::from("T"));
     dict.add_varname(String::from("U"));
@@ -97,12 +84,11 @@ fn test_unification() {
     dict.add_varname(String::from("W"));
 
     assert_eq!(
-        UnificationProblem::new_eq(vec![
+        UnificationProblem::new(vec![
             (dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
             (dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
         ]).solve(),
-        Ok((
-            vec![],
+        Ok(
             vec![
                 // T
                 (TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
@@ -110,16 +96,15 @@ fn test_unification() {
                 // U
                 (TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
             ].into_iter().collect()
-        ))
+        )
     );
 
     assert_eq!(
-        UnificationProblem::new_eq(vec![
+        UnificationProblem::new(vec![
             (dict.parse("<Seq T>").unwrap(), dict.parse("<Seq W~<Seq Char>>").unwrap()),
             (dict.parse("<Seq ℕ>").unwrap(), dict.parse("<Seq W>").unwrap()),
         ]).solve(),
-        Ok((
-            vec![],
+        Ok(
             vec![
                 // W
                 (TypeID::Var(3), dict.parse("ℕ").unwrap()),
@@ -127,254 +112,7 @@ 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!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("A ~ B").unwrap(),
-                dict.parse("B").unwrap()),
-        ]).solve(),
-        Ok((
-            vec![ dict.parse("A").unwrap() ],
-            vec![].into_iter().collect()
-        ))
-    );
-
-    assert_eq!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("A ~ B ~ C ~ D").unwrap(),
-                dict.parse("C ~ D").unwrap()),
-        ]).solve(),
-        Ok((
-            vec![ dict.parse("A ~ B").unwrap() ],
-            vec![].into_iter().collect()
-        ))
-    );
-
-    assert_eq!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("A ~ B ~ C ~ D").unwrap(),
-                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!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("A ~ B ~ C ~ D").unwrap(),
-                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!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(),
-                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!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
-            (dict.parse("T").unwrap(), 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()
-        ))
-    );
-
-    assert_eq!(
-        UnificationProblem::new_sub(vec![
-            (dict.parse("<Seq T>").unwrap(),
-                dict.parse("<Seq W~<Seq Char>>").unwrap()),
-            (dict.parse("<Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>").unwrap(),
-                dict.parse("<<LengthPrefix x86.UInt64> W>").unwrap()),
-        ]).solve(),
-        Ok((
-            vec![
-                TypeTerm::unit(),
-                dict.parse("<Seq ℕ>").unwrap(),
-            ],
-            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()
-        ))
-    );
-
-    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(UnificationError {
-            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(UnificationError {
-            addr: vec![1,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!(
-        UnificationProblem::new_sub(vec![
-
-            (
-                //given type
-                dict.parse("
-                  < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
-                ~ < ValueSep ':' Char~Ascii~UInt8 >
-                ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
-                ").expect(""),
-
-                //expected type
-                dict.parse("
-                  < Seq <Seq T> >
-                ~ < ValueSep Delim T >
-                ~ < Seq~<LengthPrefix UInt64> T >
-                ").expect("")
-            ),
-
-            // subtype bounds
-            (
-                dict.parse("T").expect(""),
-                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()
-        ))
-    );
-}

src/unification.rs

@@ -1,5 +1,6 @@
 use {
-    crate::{dict::*, term::*}, std::{collections::HashMap}
+    std::collections::HashMap,
+    crate::{term::*, dict::*}
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -11,502 +12,79 @@ pub struct UnificationError {
     pub t2: TypeTerm
 }
 
-#[derive(Clone, Debug)]
-pub struct UnificationPair {
-    addr: Vec<usize>,
-    halo: TypeTerm,
-
-    lhs: TypeTerm,
-    rhs: TypeTerm,
-}
-
-#[derive(Debug)]
 pub struct UnificationProblem {
-    σ: HashMap<TypeID, TypeTerm>,
-    upper_bounds: HashMap< u64, TypeTerm >,
-    lower_bounds: HashMap< u64, TypeTerm >,
-    equal_pairs: Vec<UnificationPair>,
-    subtype_pairs: Vec<UnificationPair>,
-    trait_pairs: Vec<UnificationPair>
+    eqs: Vec<(TypeTerm, TypeTerm, Vec<usize>)>,
+    σ: HashMap<TypeID, TypeTerm>
 }
 
 impl UnificationProblem {
-    pub fn new(
-        equal_pairs: Vec<(TypeTerm, TypeTerm)>,
-        subtype_pairs: Vec<(TypeTerm, TypeTerm)>,
-        trait_pairs: Vec<(TypeTerm, TypeTerm)>
-    ) -> Self {
+    pub fn new(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
         UnificationProblem {
-            σ: HashMap::new(),
-
-            equal_pairs: equal_pairs.into_iter().map(|(lhs,rhs)|
-                UnificationPair{
-                    lhs,rhs,
-                    halo: TypeTerm::unit(),
-                    addr: Vec::new()
-                }).collect(),
-
-            subtype_pairs: subtype_pairs.into_iter().map(|(lhs,rhs)|
-                UnificationPair{
-                    lhs,rhs,
-                    halo: TypeTerm::unit(),
-                    addr: Vec::new()
-                }).collect(),
-
-            trait_pairs: trait_pairs.into_iter().map(|(lhs,rhs)|
-                UnificationPair{
-                    lhs,rhs,
-                    halo: TypeTerm::unit(),
-                    addr: Vec::new()
-                }).collect(),
-
-            upper_bounds: HashMap::new(),
-            lower_bounds: HashMap::new(),
+            eqs: eqs.iter().map(|(lhs,rhs)| (lhs.clone(),rhs.clone(),vec![])).collect(),
+            σ: HashMap::new()
         }
     }
 
-    pub fn new_eq(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
-        UnificationProblem::new( eqs, Vec::new(), Vec::new() )
-    }
-
-    pub fn new_sub(subs: Vec<(TypeTerm, TypeTerm)>) -> Self {
-        UnificationProblem::new( Vec::new(), subs, Vec::new() )
-    }
-
-
-    /// 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().normalize();
-            tt.apply_subst(&self.σ);
-            tt = tt.normalize();
-            //eprintln!("update σ : {:?} --> {:?}", v, tt);
-            new_σ.insert(v.clone(), tt);
-        }
-        self.σ = new_σ;
-    }
-
-
-    pub fn eval_equation(&mut self, unification_pair: UnificationPair) -> Result<(), UnificationError> {
-        match (&unification_pair.lhs, &unification_pair.rhs) {
+    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))) => {
-                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(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
+                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: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+                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: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+                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: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+                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().rev() {
-                        let mut new_addr = unification_pair.addr.clone();
+                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+                        let mut new_addr = addr.clone();
                         new_addr.push(i);
-                        self.equal_pairs.push(
-                            UnificationPair {
-                                lhs: x,
-                                rhs: y,
-                                halo: TypeTerm::unit(),
-                                addr: new_addr
-                            });
+                        self.eqs.push((x, y, new_addr));
                     }
                     Ok(())
                 } else {
-                    Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                    Err(UnificationError{ addr, t1: lhs, t2: rhs })
                 }
             }
 
-            _ => Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+            (TypeTerm::Ladder(l1), TypeTerm::Ladder(l2)) => {
+                Err(UnificationError{ addr, t1: lhs, t2: rhs })
+            }
+
+            _ => Err(UnificationError{ addr, t1: lhs, t2: 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(
-                UnificationPair {
-                    lhs: lower_bound.clone(),
-                    rhs: new_lower_bound.clone(),
-                    halo: TypeTerm::unit(),
-                    addr: vec![]
-                }
-            ) {
-//                            eprintln!("found more general lower bound");
-//                            eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
-                // generalize variable type to supertype
-                self.lower_bounds.insert(v, new_lower_bound);
-                Ok(())
-            } else if let Ok(halo) = self.eval_subtype(
-                UnificationPair{
-                    lhs: new_lower_bound,
-                    rhs: lower_bound,
-                    halo: TypeTerm::unit(),
-                    addr: vec![]
-                }
-            ) {
-//                            eprintln!("OK, is already larger type");
-                 Ok(())
-            } else {
-//                            eprintln!("violated subtype restriction");
-                Err(())
+    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)?;
             }
-        } else {
-//                        eprintln!("set var {}'s lowerbound to {:?}", varid, t.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(
-                UnificationPair {
-                    lhs: new_upper_bound.clone(),
-                    rhs: upper_bound,
-                    halo: TypeTerm::unit(),
-                    addr: vec![]
-                }
-            ) {
-                // found a lower upper bound
-                self.upper_bounds.insert(v, new_upper_bound);
-                Ok(())
-            } else {
-                Err(())
-            }
-        } else {
-            self.upper_bounds.insert(v, new_upper_bound);
-            Ok(())
-        }
-    }
-
-    pub fn eval_subtype(&mut self, unification_pair: UnificationPair) -> Result<
-        // ok: halo type
-        TypeTerm,
-        // error
-        UnificationError
-    > {
-        // eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
-        match (unification_pair.lhs.clone(), unification_pair.rhs.clone()) {
-
-            /*
-             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(UnificationError{ 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(UnificationError{ 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(UnificationError{ 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(UnificationError{ 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(UnificationError{ 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() {
-
-                                        // TODO
-
-                                    } else {
-                                        // 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(UnificationError {
-                                            addr,
-                                            t1: lhs,
-                                            t2: rhs
-                                        });
-                                    }
-                                } else {
-                                    return Err(UnificationError {
-                                        addr,
-                                        t1: lhs,
-                                        t2: rhs
-                                    });
-                                }
-                            }
-                            (lhs, rhs) => {
-                                if let Ok(ψ) = self.eval_subtype(
-                                    UnificationPair {
-                                        lhs: lhs.clone(), rhs: rhs.clone(),
-                                        addr:addr.clone(), halo: TypeTerm::unit()
-                                    }
-                                ) {
-                                    // ok.
-                                    //eprintln!("rungs are subtypes. continue");
-                                    halo_ladder.push(ψ);
-                                } else {
-                                    return Err(UnificationError {
-                                        addr,
-                                        t1: lhs,
-                                        t2: rhs
-                                    });
-                                }
-                            }
-                        }
-                    } else {
-                        // not a subtype,
-                        return Err(UnificationError {
-                            addr: vec![],
-                            t1: unification_pair.lhs,
-                            t2: unification_pair.rhs
-                        });
-                    }
-                }
-                //eprintln!("left ladder fully consumed");
-
-                for (i,t) in l1_iter {
-                    halo_ladder.push(t);
-                }
-                halo_ladder.reverse();
-                Ok(TypeTerm::Ladder(halo_ladder).strip().param_normalize())
-            },
-
-            (t, TypeTerm::Ladder(a1)) => {
-                Err(UnificationError{ addr: unification_pair.addr, t1: t, t2: TypeTerm::Ladder(a1) })
-            }
-
-            (TypeTerm::Ladder(mut a1), t) => {
-                let mut new_addr = unification_pair.addr.clone();
-                new_addr.push( a1.len() -1 );
-                if let Ok(halo) = self.eval_subtype(
-                    UnificationPair {
-                        lhs: a1.pop().unwrap(),
-                        rhs: t.clone(),
-                        halo: TypeTerm::unit(),
-                        addr: new_addr
-                    }
-                ) {
-                    a1.push(halo);
-                    if a1.len() == 1 {
-                        Ok(a1.pop().unwrap())
-                    } else {
-                        Ok(TypeTerm::Ladder(a1))
-                    }
-                } else {
-                    Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::Ladder(a1), t2: t })
-                }
-            }
-
-
-            /*
-             Application
-            */
-
-            (TypeTerm::App(a1), TypeTerm::App(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(
-                            UnificationPair {
-                                lhs: x.clone(),
-                                rhs: y.clone(),
-                                halo: TypeTerm::unit(),
-                                addr: new_addr,
-                            }
-                        ) {
-                            Ok(halo) => {
-                            if halo == TypeTerm::unit() {
-                                let mut y = y.clone();
-                                y.apply_subst(&self.σ);
-                                y = y.strip();
-                                let mut top = y.get_lnf_vec().first().unwrap().clone();
-                                halo_args.push(top.clone());
-                                //eprintln!("add top {:?}", top);
-                            } else {
-                                //eprintln!("add halo {:?}", halo);
-                                if n_halos_required > 0 {
-                                    let x = &mut halo_args[n_halos_required-1];
-                                    if let TypeTerm::Ladder(argrs) = x {
-                                        let mut a = a2[n_halos_required-1].clone();
-                                        a.apply_subst(&self.σ);
-                                        a = a.get_lnf_vec().first().unwrap().clone();
-                                        argrs.push(a);
-                                    } else {
-                                        *x = TypeTerm::Ladder(vec![
-                                            x.clone(),
-                                            a2[n_halos_required-1].clone().get_lnf_vec().first().unwrap().clone()
-                                        ]);
-
-                                        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::App(halo_args))
-                    } else {
-                        Ok(TypeTerm::unit())
-                    }
-                } else {
-                    Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
-                }
-            }
-
-            _ => Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
-        }
-    }
-
-    pub fn solve(mut self) -> Result<(Vec<TypeTerm>, HashMap<TypeID, TypeTerm>), UnificationError> {
-        // 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().strip();
-            subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone().strip();
-
-            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.σ))
+        Ok(self.σ)
     }
 }
 
@@ -514,16 +92,9 @@ pub fn unify(
     t1: &TypeTerm,
     t2: &TypeTerm
 ) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
-    let unification = UnificationProblem::new_eq(vec![ (t1.clone(), t2.clone()) ]);
-    Ok(unification.solve()?.1)
-}
-
-pub fn subtype_unify(
-    t1: &TypeTerm,
-    t2: &TypeTerm
-) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
-    let unification = UnificationProblem::new_sub(vec![ (t1.clone(), t2.clone()) ]);
-    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
+    let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
+    unification.solve()
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+

src/unparser.rs

@@ -2,12 +2,8 @@ use crate::{dict::*, term::*};
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-pub trait UnparseLadderType {
-    fn unparse(&self, t: &TypeTerm) -> String;
-}
-
-impl<T: TypeDict> UnparseLadderType for T {
-    fn unparse(&self, t: &TypeTerm) -> String {
+impl TypeDict {
+    pub fn unparse(&self, t: &TypeTerm) -> String {
         match t {
             TypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
             TypeTerm::Num(n) => format!("{}", n),