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/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 970c555..2e9a163 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -5,6 +5,7 @@ pub mod term;
pub mod lexer;
pub mod parser;
pub mod unparser;
+pub mod sugar;
pub mod curry;
pub mod lnf;
pub mod pnf;
@@ -14,9 +15,12 @@ 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
index 4576be5..d3a6b20 100644
--- a/src/pnf.rs
+++ b/src/pnf.rs
@@ -2,6 +2,20 @@ 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)
///
@@ -10,88 +24,99 @@ 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() {
+ 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;
- // 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 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() {
- // append all other rungs to ladders inside
- // the application
- for p in params_top {
- params_ladders.push(vec![ p ]);
- }
+ 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()
+ };
- for r in rungs {
- match r {
- TypeTerm::App(mut params_rung) => {
- if params_rung.len() > 0 {
- let mut first_param = params_rung.remove(0);
+ new_rung_params.push( spliced_type.param_normalize() );
+ }
- 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));
+ 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;
+ }
+ }
}
}
- }
- TypeTerm::Ladder(mut rs) => {
- for r in rs {
- tail.push(r.param_normalize());
+ if require_break {
+ new_rungs.push( TypeTerm::App(new_rung_params) );
+ } else {
+ rungs.pop();
+ rungs.push(TypeTerm::App(new_rung_params));
}
- }
- atomic => {
- tail.push(atomic);
+ } else {
+ new_rungs.push( TypeTerm::App(bot_args) );
}
}
+ (bottom, last_buf) => {
+ new_rungs.push( bottom );
+ }
}
-
- 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
- }
+ } else {
+ new_rungs.push( bottom );
}
+ }
- TypeTerm::Ladder(mut r) => {
- r.append(&mut rungs);
- TypeTerm::Ladder(r)
- }
+ new_rungs.reverse();
- atomic => {
- rungs.insert(0, atomic);
- TypeTerm::Ladder(rungs)
- }
+ if new_rungs.len() > 1 {
+ TypeTerm::Ladder(new_rungs)
+ } else if new_rungs.len() == 1 {
+ new_rungs[0].clone()
+ } else {
+ TypeTerm::unit()
}
} else {
TypeTerm::unit()
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/pnf.rs b/src/test/pnf.rs
index 2303b3e..e668849 100644
--- a/src/test/pnf.rs
+++ b/src/test/pnf.rs
@@ -19,22 +19,40 @@ 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("<A <B C~D~E> F~G H H>").expect("parse error"),
+ 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> F H H>
~<A <B D> F H H>
- ~<A <B E> F H H>
- ~<A <B E> G H H>").expect("parse errror")
+ ~<A~Y <B E> F H H>").expect("parse errror")
.param_normalize(),
);
}