From 4f758b8021ad4f6bd2790c8aad090de5cdafe566 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 2 Oct 2024 22:37:06 +0200 Subject: [PATCH] add sugared terms & pretty printing --- Cargo.toml | 5 ++ src/dict.rs | 4 ++ src/lib.rs | 5 ++ src/pretty.rs | 148 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/sugar.rs | 95 ++++++++++++++++++++++++++++++++ src/term.rs | 2 +- 6 files changed, 258 insertions(+), 1 deletion(-) create mode 100644 src/pretty.rs create mode 100644 src/sugar.rs 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 93bb6ec..419d599 100644 --- a/src/dict.rs +++ b/src/dict.rs @@ -54,6 +54,10 @@ impl TypeDict { pub fn get_typeid(&self, tn: &String) -> Option { self.typenames.mλ.get(tn).cloned() } + + pub fn get_varname(&self, var_id: u64) -> Option { + self.typenames.my.get(&TypeID::Var(var_id)).cloned() + } } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> diff --git a/src/lib.rs b/src/lib.rs index 5cdff81..c1f8d05 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; @@ -16,9 +17,13 @@ pub mod steiner_tree; #[cfg(test)] mod test; +#[cfg(feature = "pretty")] +mod pretty; + pub use { dict::*, term::*, + sugar::*, unification::*, morphism::* }; 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) -> &mut Self { match self { TypeTerm::Ladder(rungs) => { - rungs.push(t.into()); + rungs.push(t.into()); } _ => {