rewrite param_normalize()

src/pnf.rs

@@ -2,7 +2,7 @@ use crate::term::TypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm >  ) -> Vec< 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();
@@ -24,65 +24,76 @@ impl TypeTerm {
     /// <Seq <Digit 10>>~<Seq Char>
     /// ⇒ <Seq <Digit 10>~Char>
     /// ```
-    pub fn param_normalize(self) -> Self {
+    pub fn param_normalize(mut self) -> Self {
         match self {
             TypeTerm::Ladder(mut rungs) => {
                 if rungs.len() > 0 {
-                    /*
-                    // normalize all rungs separately
-                    for r in rungs.iter_mut() {
-                        *r = r.clone().param_normalize();
-                    }
-*/
                     let mut new_rungs = Vec::new();
                     while let Some(bottom) = rungs.pop() {
-                        //eprintln!("popped bottom {:?}", bottom);
                         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 different_idx = None;
                                         let mut new_rung_params = Vec::new();
-
                                         let mut require_break = false;
 
-                                        for i in 0 .. bot_args.len() {
-                                            if let Ok(rung_idx) = bot_args[i].is_syntactic_subtype_of(&last_args[i]) {
-                                                let spliced_type_ladder = splice_ladders(
-                                                    last_args[i].clone().get_lnf_vec(),
-                                                    bot_args[i].clone().get_lnf_vec()
+                                        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()
                                                 );
 
-                                                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()
-                                                };
+                                                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 );
-                                            } else {
-                                                if different_idx.is_none() {
-                                                    let spliced_type = TypeTerm::Ladder(vec![
-                                                        last_args[i].clone(),
-                                                        bot_args[i].clone()
-                                                    ]);
-                                                    new_rung_params.push( spliced_type );
-                                                    different_idx = Some(i);
-                                                } else {
-                                                    require_break = true;
+                                                        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) );
-                                            new_rung_params = Vec::new();
                                         } else {
                                             rungs.pop();
                                             rungs.push(TypeTerm::App(new_rung_params));
-                                            new_rung_params = Vec::new();
                                         }
 
                                     } else {

src/test/pnf.rs

@@ -29,6 +29,11 @@ fn test_param_normalize() {
         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(),
@@ -44,12 +49,10 @@ fn test_param_normalize() {
     );
 
     assert_eq!(
-        dict.parse("<A~Y <B C~D~E> F~G H H>").expect("parse error"),
+        dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
         dict.parse("<A <B C> F H H>
                    ~<A <B D> F H H>
-                   ~<A <B E> F H H>
-                   ~<A <B E> G H H>
-                   ~<Y <B E> G H H>").expect("parse errror")
+                   ~<A~Y <B E> F H H>").expect("parse errror")
                .param_normalize(),
     );
 }

src/unification.rs

@@ -67,10 +67,6 @@ impl UnificationProblem {
                 }
             }
 
-            (TypeTerm::Ladder(l1), TypeTerm::Ladder(l2)) => {
-                Err(UnificationError{ addr, t1: lhs, t2: rhs })
-            }
-
             _ => Err(UnificationError{ addr, t1: lhs, t2: rhs})
         }
     }