From 7b22bdc170d53e83e4aa5d5f9dc24e5dba42aa77 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 2 Oct 2023 18:48:04 +0200 Subject: [PATCH] implement ladder normalization --- src/lib.rs | 1 + src/lnf.rs | 112 ++++++++++++++++++++++++++++++++++++++++++++++++ src/test/lnf.rs | 45 ++++++++++++++++++- 3 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 src/lnf.rs diff --git a/src/lib.rs b/src/lib.rs index 0319a0c..d46d35b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -5,6 +5,7 @@ pub mod term; pub mod lexer; pub mod parser; pub mod curry; +pub mod lnf; #[cfg(test)] mod test; diff --git a/src/lnf.rs b/src/lnf.rs new file mode 100644 index 0000000..8acd421 --- /dev/null +++ b/src/lnf.rs @@ -0,0 +1,112 @@ +use crate::term::TypeTerm; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + +impl TypeTerm { + /// does the type contain ladders (false) or is it 'flat' (true) ? + /// + /// Example: + /// ```>``` is flat, but + /// ```~Char``` is not + pub fn is_flat(&self) -> bool { + match self { + TypeTerm::TypeID(_) => true, + TypeTerm::Num(_) => true, + TypeTerm::Char(_) => true, + TypeTerm::App(args) => args.iter().fold(true, |s,x| s && x.is_flat()), + TypeTerm::Ladder(_) => false + } + } + + /// transmute type into Ladder-Normal-Form (LNF) + /// + /// Example: + /// ```ignore + /// ~Char> + /// ⇒ >~ + /// ``` + pub fn normalize(self) -> Self { + let mut new_ladder = Vec::::new(); + + match self { + TypeTerm::Ladder(args) => { + for x in args.into_iter() { + new_ladder.push(x.normalize()); + } + } + + TypeTerm::App(args) => { + let mut args_iter = args.into_iter(); + + new_ladder.push( TypeTerm::App(vec![]) ); + + for arg in args_iter { + match arg.clone() { + TypeTerm::Ladder(rungs) => { + // duplicate last element for each rung + let l = new_ladder.len(); + for _ in 1..rungs.len() { + new_ladder.push( new_ladder.last().unwrap().clone() ); + } + + for (i,r) in new_ladder.iter_mut().enumerate() { + match r { + TypeTerm::App(al) => { + if i < l { + al.push(rungs[0].clone()); + } else { + al.push(rungs[i-l+1].clone()); + } + } + _ => unreachable!() + } + } + } + mut other => { + other = other.normalize(); + for rung in new_ladder.iter_mut() { + match rung { + TypeTerm::App(al) => { + al.push(other.clone()); + } + _ => unreachable!() + } + } + } + } + } + } + + atom => { + new_ladder.push(atom); + } + } + + match new_ladder.len() { + 0 => TypeTerm::unit(), + 1 => new_ladder.into_iter().next().unwrap(), + _ => TypeTerm::Ladder( new_ladder ) + } + } + + /// transmute type into a `Vec` containing + /// all rungs of the type in LNF + /// + /// Example: + /// ```~Char>``` gives + /// ```ignore + /// vec![ >, ] + /// ``` + pub fn get_lnf_vec(self) -> Vec { + match self.normalize() { + TypeTerm::Ladder( v ) => { + v + }, + _ => { + unreachable!(); + } + } + } +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ diff --git a/src/test/lnf.rs b/src/test/lnf.rs index 0915387..486c0d6 100644 --- a/src/test/lnf.rs +++ b/src/test/lnf.rs @@ -1,6 +1,47 @@ +use crate::dict::TypeDict; #[test] -fn test_lnf() { - // todo +fn test_flat() { + let mut dict = TypeDict::new(); + + assert!( dict.parse("A").expect("parse error").is_flat() ); + assert!( dict.parse("10").expect("parse error").is_flat() ); + assert!( dict.parse("'x'").expect("parse error").is_flat() ); + assert!( dict.parse("").expect("parse error").is_flat() ); + assert!( dict.parse(">").expect("parse error").is_flat() ); + + assert!( ! dict.parse("A~B").expect("parse error").is_flat() ); + assert!( ! dict.parse("").expect("parse error").is_flat() ); + assert!( ! dict.parse(">").expect("parse error").is_flat() ); +} + +#[test] +fn test_normalize() { + let mut dict = TypeDict::new(); + + assert_eq!( + dict.parse("A~B~C").expect("parse error").normalize(), + dict.parse("A~B~C").expect("parse errror"), + ); + + assert_eq!( + dict.parse("~C").expect("parse error").normalize(), + dict.parse("~C").expect("parse errror"), + ); + + assert_eq!( + dict.parse("").expect("parse error").normalize(), + dict.parse("~").expect("parse errror"), + ); + + assert_eq!( + dict.parse("").expect("parse error").normalize(), + dict.parse("~~").expect("parse errror"), + ); + + assert_eq!( + dict.parse("~Char>").expect("parse error").normalize(), + dict.parse(">~").expect("parse errror"), + ); }