src/dict.rs

@@ -2,7 +2,7 @@ use crate::bimap::Bimap;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)]
+#[derive(Eq, PartialEq, Hash, Clone, Debug)]
 pub enum TypeID {
     Fun(u64),
     Var(u64)

src/lib.rs

@@ -10,7 +10,6 @@ pub mod lnf;
 pub mod pnf;
 pub mod subtype;
 pub mod unification;
-pub mod morphism;
 
 #[cfg(test)]
 mod test;

src/morphism.rs

@@ -1,204 +0,0 @@
-use {
-    crate::{
-        TypeTerm, TypeID,
-        unification::UnificationProblem,
-    },
-    std::collections::HashMap
-};
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-pub struct MorphismType {
-    pub src_type: TypeTerm,
-    pub dst_type: TypeTerm,
-}
-
-pub struct MorphismBase<Morphism: Clone> {
-    morphisms: Vec< (MorphismType, Morphism) >,
-    list_typeid: TypeID
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl MorphismType {
-    fn normalize(self) -> Self {
-        MorphismType {
-            src_type: self.src_type.normalize(),
-            dst_type: self.dst_type.normalize()
-        }
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-
-impl<Morphism: Clone> MorphismBase<Morphism> {
-    pub fn new() -> Self {
-        MorphismBase {
-            morphisms: Vec::new(),
-
-            // FIXME: magic number
-            list_typeid: TypeID::Fun(10)
-        }
-    }
-
-    pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) {
-        self.morphisms.push( (morph_type.normalize(), morphism) );
-    }
-
-    pub fn enum_morphisms(&self, src_type: &TypeTerm)
-    -> Vec< (HashMap<TypeID, TypeTerm>, TypeTerm) >
-    {
-        let mut dst_types = Vec::new();
-
-        // first enumerate all "direct" morphisms,
-        for (ty,m) in self.morphisms.iter() {
-            if let Ok(σ) = crate::unification::unify(
-                &ty.src_type,
-                &src_type.clone().normalize()
-            ) {
-                let dst_type = 
-                    ty.dst_type.clone()
-                        .apply_substitution(
-                            &|x| σ.get(x).cloned()
-                        )
-                        .clone();
-
-                dst_types.push( (σ, dst_type) );
-            }
-        }
-
-        // ..then all "list-map" morphisms.
-        // 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(100);
-
-        if let Ok(σ) = crate::unification::unify(
-            &TypeTerm::App(vec![
-                TypeTerm::TypeID(self.list_typeid),
-                TypeTerm::TypeID(item_variable)
-            ]),
-            &src_type.clone().param_normalize(),
-        ) {
-            let src_item_type = σ.get(&item_variable).unwrap().clone();
-
-            for (γ, dst_item_type) in self.enum_morphisms( &src_item_type ) {
-                let dst_type =
-                        TypeTerm::App(vec![
-                            TypeTerm::TypeID(self.list_typeid),
-                            dst_item_type.clone()
-                                .apply_substitution(
-                                    &|x| γ.get(x).cloned()
-                                ).clone()
-                        ]).normalize();
-
-                dst_types.push( (γ.clone(), dst_type) );
-            }
-        }
-
-        dst_types
-    }
-
-    pub fn enum_morphisms_with_subtyping(&self, src_type: &TypeTerm)
-    -> Vec< (TypeTerm, TypeTerm) >
-    {
-        let mut src_lnf = src_type.clone().get_lnf_vec();
-        let mut halo_lnf = vec![];
-        let mut dst_types = Vec::new();
-
-        while src_lnf.len() > 0 {
-            let src_type = TypeTerm::Ladder( src_lnf.clone() );
-            let halo_type = TypeTerm::Ladder( halo_lnf.clone() );
-
-            for (σ, t) in self.enum_morphisms( &src_type ) {
-                dst_types.push(
-                    (halo_type.clone()
-                        .apply_substitution(
-                            &|x| σ.get(x).cloned()
-                        ).clone(),
-                    t.clone()
-                        .apply_substitution(
-                            &|x| σ.get(x).cloned()
-                        ).clone()
-                    )
-                );
-            }
-
-            // continue with next supertype
-            halo_lnf.push(src_lnf.remove(0));
-        }
-
-        dst_types
-    }
-
-    /* performs DFS to find a morphism-path for a given type
-     * will return the first matching path, not the shortest
-     */
-    pub fn find_morphism_path(&self, ty: MorphismType)
-    -> Option< Vec<TypeTerm> >
-    {
-        let ty = ty.normalize();
-        let mut visited = Vec::new();
-        let mut queue = vec![
-            vec![ ty.src_type.clone().normalize() ]
-        ];
-
-        while let Some(current_path) = queue.pop() {       
-            let current_type = current_path.last().unwrap();
-
-            if ! visited.contains( current_type ) {
-                visited.push( current_type.clone() );
-
-                for (h, t) in self.enum_morphisms_with_subtyping(&current_type) {
-                    let tt = TypeTerm::Ladder( vec![ h, t ] ).normalize();
-
-                    if ! visited.contains( &tt ) {
-                        let unification_result = crate::unification::unify(&tt, &ty.dst_type);
-                        let mut new_path = current_path.clone();
-
-                        new_path.push( tt );
-
-                        if let Ok(σ) = unification_result {
-                            new_path = new_path.into_iter().map(
-                                |mut t: TypeTerm| t.apply_substitution(&|x| σ.get(x).cloned()).clone()
-                            ).collect::<Vec<TypeTerm>>();
-
-                            return Some(new_path);
-                        } else {
-                            queue.push( new_path );
-                        }
-                    }
-                }
-            }
-        }
-
-        None
-    }
-
-    pub fn find_morphism(&self, ty: &MorphismType)
-    -> Option< Morphism > {
-
-        // TODO
-
-        None
-    }
-
-    pub fn find_list_map_morphism(&self, item_ty: &MorphismType)
-    -> Option< Morphism > {
-
-        // TODO
-
-        None
-    }
-
-    pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
-    -> Option<( Morphism, TypeTerm, HashMap<TypeID, TypeTerm> )> {
-
-        // TODO
-
-        None
-    }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-