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 1a270cc..e073b0b 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 subtype;
@@ -13,9 +14,12 @@ pub mod unification;
#[cfg(test)]
mod test;
+#[cfg(feature = "pretty")]
+mod pretty;
+
pub use {
dict::*,
term::*,
- unification::*
+ sugar::*,
+ unification::*,
};
-
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());
}
_ => {