syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

add sugared terms & pretty printing

Browse source
This commit is contained in:
Michael Sippel 2024-10-02 22:37:06 +02:00
parent db7e0173c4
commit 4f758b8021
Signed by: senvas
GPG key ID: F96CF119C34B64A6
6 changed files with 258 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
Cargo.toml
View file

@ -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"]

4
src/dict.rs
View file

@ -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()
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>

5
src/lib.rs
View file

@ -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::*
};

148
src/pretty.rs Normal file
View file

@ -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
}
}
}
}

95
src/sugar.rs Normal file
View file

@ -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()),
}
}
}

2
src/term.rs
View file

@ -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());
}
_ => {