diff --git a/Cargo.toml b/Cargo.toml index 0a57fd3..429541c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,3 +4,8 @@ edition = "2018" name = "laddertypes" version = "0.1.0" +[dependencies] +tiny-ansi = { version = "0.1.0", optional = true } + +[features] +pretty = ["dep:tiny-ansi"] diff --git a/README.md b/README.md index d4dc395..fa7cd86 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,8 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc) ## Ladder Types +### Motivation + In order to implement complex datastructures and algorithms, usually many layers of abstraction are built ontop of each other. Consequently higher-level data types are encoded into lower-level data @@ -57,6 +59,48 @@ this: 1696093021:1696093039:1528324679:1539892301:1638141920:1688010253 ``` +### Syntax + +In their core form, type-terms can be one of the following: +- (**Atomic Type**) | `SomeTypeName` +- (**Literal Integer**) | `0` | `1` | `2` | ... +- (**Literal Character**) | `'a'` | `'b'` | `'c'` | ... +- (**Literal String**) | `"abc"` +- (**Parameter Application**) | `<T1 T2>` given `T1` and `T2` are type-terms +- (**Ladder**) | `T1 ~ T2` given `T1` and `T2` are type-terms + +Ontop of that, the following syntax-sugar is defined: + +#### Complex Types +- `[ T ]` <===> `<Seq T>` +- `{ a:A b:B }` <===> `<Struct <"a" A> <"b" B>>` +- `a:A | b:B` <===> `<Enum <"a" A> <"b" B>>` + +#### Function Types +- `A -> B` <===> `<Fn A B>` + +#### Reference Types +- `*A` <===> `<Ptr A>` +- `&A` <===> `<ConstRef A>` +- `&!A` <===> `<MutRef A>` + + +### Equivalences + +#### Currying +`<<A B> C>` <===> `<A B C>` + +#### Ladder-Normal-Form +exhaustively apply `<A B~C>` ===> `<A B>~<A C>` + +e.g. `[<Digit 10>]~[Char]~[Ascii]` is in **LNF** + +#### Parameter-Normal-Form +exhaustively apply `<A B>~<A C>` ===> `<A B~C>` + +e.g. `[<Digit 10>~Char~Ascii]` is in **PNF** + + ## How to use this crate ```rust @@ -73,6 +117,19 @@ fn main() { } ``` +## Roadmap + +- [x] (Un-)Parsing +- [x] (De-)Currying +- [x] Unification +- [x] Ladder-Normal-Form +- [x] Parameter-Normal-Form +- [ ] (De)-Sugaring + - [ ] Seq + - [ ] Enum + - [ ] Struct + - [ ] References + - [ ] Function ## License [GPLv3](COPYING) diff --git a/src/dict.rs b/src/dict.rs index 83b63ee..419d599 100644 --- a/src/dict.rs +++ b/src/dict.rs @@ -2,7 +2,7 @@ use crate::bimap::Bimap; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ -#[derive(Eq, PartialEq, Hash, Clone, Debug)] +#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)] pub enum TypeID { Fun(u64), Var(u64) @@ -54,6 +54,10 @@ impl TypeDict { pub fn get_typeid(&self, tn: &String) -> Option<TypeID> { self.typenames.mλ.get(tn).cloned() } + + pub fn get_varname(&self, var_id: u64) -> Option<String> { + self.typenames.my.get(&TypeID::Var(var_id)).cloned() + } } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> diff --git a/src/lib.rs b/src/lib.rs index 1a270cc..2e9a163 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -5,17 +5,22 @@ pub mod term; 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; #[cfg(test)] mod test; +#[cfg(feature = "pretty")] +mod pretty; + pub use { dict::*, term::*, - unification::* + sugar::*, + unification::*, }; - diff --git a/src/pnf.rs b/src/pnf.rs new file mode 100644 index 0000000..4576be5 --- /dev/null +++ b/src/pnf.rs @@ -0,0 +1,113 @@ +use crate::term::TypeTerm; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ + +impl TypeTerm { + /// transmute type into Parameter-Normal-Form (PNF) + /// + /// Example: + /// ```ignore + /// <Seq <Digit 10>>~<Seq Char> + /// ⇒ <Seq <Digit 10>~Char> + /// ``` + pub fn param_normalize(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(); + } + + // take top-rung + match rungs.remove(0) { + TypeTerm::App(params_top) => { + let mut params_ladders = Vec::new(); + let mut tail : Vec<TypeTerm> = Vec::new(); + + // 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() + } + } + + TypeTerm::App(params) => { + TypeTerm::App( + params.into_iter() + .map(|p| p.param_normalize()) + .collect()) + } + + atomic => atomic + } + } +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ diff --git a/src/pretty.rs b/src/pretty.rs new file mode 100644 index 0000000..1a4aa60 --- /dev/null +++ b/src/pretty.rs @@ -0,0 +1,148 @@ +use { + crate::TypeDict, + 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) => { + format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue() + }, + + SugaredTypeTerm::Num(n) => { + format!("{}", n).bright_cyan() + } + + SugaredTypeTerm::Char(c) => { + 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().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::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 + } + } + } +} + + diff --git a/src/sugar.rs b/src/sugar.rs new file mode 100644 index 0000000..4d13f78 --- /dev/null +++ b/src/sugar.rs @@ -0,0 +1,95 @@ +use { + crate::{TypeTerm, TypeID} +}; + +pub enum SugaredTypeTerm { + TypeID(TypeID), + Num(i64), + Char(char), + Univ(Box< SugaredTypeTerm >), + Spec(Vec< SugaredTypeTerm >), + Func(Vec< SugaredTypeTerm >), + Morph(Vec< SugaredTypeTerm >), + Ladder(Vec< SugaredTypeTerm >), + Struct(Vec< SugaredTypeTerm >), + Enum(Vec< SugaredTypeTerm >), + Seq(Vec< SugaredTypeTerm >) +} + +impl TypeTerm { + pub fn sugar(self: TypeTerm, dict: &mut crate::TypeDict) -> SugaredTypeTerm { + match self { + TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id), + TypeTerm::Num(n) => SugaredTypeTerm::Num(n), + TypeTerm::Char(c) => SugaredTypeTerm::Char(c), + TypeTerm::App(args) => if let Some(first) = args.first() { + if first == &dict.parse("Func").unwrap() { + SugaredTypeTerm::Func( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Morph").unwrap() { + SugaredTypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Struct").unwrap() { + SugaredTypeTerm::Struct( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Enum").unwrap() { + SugaredTypeTerm::Enum( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Seq").unwrap() { + SugaredTypeTerm::Seq( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Spec").unwrap() { + SugaredTypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() ) + } + else if first == &dict.parse("Univ").unwrap() { + SugaredTypeTerm::Univ(Box::new( + SugaredTypeTerm::Spec( + args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() + ) + )) + } + else { + SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect()) + } + } else { + SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect()) + }, + TypeTerm::Ladder(rungs) => + SugaredTypeTerm::Ladder(rungs.into_iter().map(|t| t.sugar(dict)).collect()) + } + } +} + +impl SugaredTypeTerm { + pub fn desugar(self, dict: &mut crate::TypeDict) -> TypeTerm { + match self { + SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id), + SugaredTypeTerm::Num(n) => TypeTerm::Num(n), + SugaredTypeTerm::Char(c) => TypeTerm::Char(c), + SugaredTypeTerm::Univ(t) => t.desugar(dict), + SugaredTypeTerm::Spec(ts) => TypeTerm::App(ts.into_iter().map(|t| t.desugar(dict)).collect()), + SugaredTypeTerm::Ladder(ts) => TypeTerm::Ladder(ts.into_iter().map(|t|t.desugar(dict)).collect()), + SugaredTypeTerm::Func(ts) => TypeTerm::App( + std::iter::once( dict.parse("Func").unwrap() ).chain( + ts.into_iter().map(|t| t.desugar(dict)) + ).collect()), + SugaredTypeTerm::Morph(ts) => TypeTerm::App( + std::iter::once( dict.parse("Morph").unwrap() ).chain( + ts.into_iter().map(|t| t.desugar(dict)) + ).collect()), + SugaredTypeTerm::Struct(ts) => TypeTerm::App( + std::iter::once( dict.parse("Struct").unwrap() ).chain( + ts.into_iter().map(|t| t.desugar(dict)) + ).collect()), + SugaredTypeTerm::Enum(ts) => TypeTerm::App( + std::iter::once( dict.parse("Enum").unwrap() ).chain( + ts.into_iter().map(|t| t.desugar(dict)) + ).collect()), + SugaredTypeTerm::Seq(ts) => TypeTerm::App( + std::iter::once( dict.parse("Seq").unwrap() ).chain( + ts.into_iter().map(|t| t.desugar(dict)) + ).collect()), + } + } +} + diff --git a/src/term.rs b/src/term.rs index f5e8f5f..29c7d27 100644 --- a/src/term.rs +++ b/src/term.rs @@ -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()); } _ => { diff --git a/src/test/mod.rs b/src/test/mod.rs index d116412..29c14bc 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -3,6 +3,7 @@ pub mod lexer; pub mod parser; pub mod curry; pub mod lnf; +pub mod pnf; pub mod subtype; pub mod substitution; pub mod unification; diff --git a/src/test/pnf.rs b/src/test/pnf.rs new file mode 100644 index 0000000..2303b3e --- /dev/null +++ b/src/test/pnf.rs @@ -0,0 +1,41 @@ +use crate::dict::TypeDict; + +#[test] +fn test_param_normalize() { + let mut dict = TypeDict::new(); + + assert_eq!( + dict.parse("A~B~C").expect("parse error"), + dict.parse("A~B~C").expect("parse error").param_normalize(), + ); + + assert_eq!( + dict.parse("<A B>~C").expect("parse error"), + dict.parse("<A B>~C").expect("parse error").param_normalize(), + ); + + assert_eq!( + dict.parse("<A B~C>").expect("parse error"), + dict.parse("<A B>~<A C>").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("<Seq <Digit 10>~Char>").expect("parse error"), + dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").param_normalize(), + ); + + assert_eq!( + 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 <B E> F H H> + ~<A <B E> G H H>").expect("parse errror") + .param_normalize(), + ); +} +