Compare commits

...

2 commits

Author SHA1 Message Date
ba7e921a5e
term strip(): flatten ladders 2025-06-01 00:36:19 +02:00
c4a26d11da
term: add check if term is empty 2025-06-01 00:35:41 +02:00
2 changed files with 60 additions and 2 deletions

View file

@ -92,5 +92,23 @@ impl SugaredTypeTerm {
).collect()),
}
}
pub fn is_empty(&self) -> bool {
match self {
SugaredTypeTerm::TypeID(_) => false,
SugaredTypeTerm::Num(_) => false,
SugaredTypeTerm::Char(_) => false,
SugaredTypeTerm::Univ(t) => t.is_empty(),
SugaredTypeTerm::Spec(ts) |
SugaredTypeTerm::Ladder(ts) |
SugaredTypeTerm::Func(ts) |
SugaredTypeTerm::Morph(ts) |
SugaredTypeTerm::Struct(ts) |
SugaredTypeTerm::Enum(ts) |
SugaredTypeTerm::Seq(ts) => {
ts.iter().fold(true, |s,t|s&&t.is_empty())
}
}
}
}

View file

@ -14,7 +14,7 @@ pub enum TypeTerm {
Num(i64),
Char(char),
/* Complex Terms */
@ -47,7 +47,7 @@ impl TypeTerm {
*self = TypeTerm::App(vec![
self.clone(),
t.into()
])
])
}
}
@ -124,6 +124,46 @@ impl TypeTerm {
self
}
/* strip away empty ladders
* & unwrap singletons
*/
pub fn strip(self) -> Self {
match self {
TypeTerm::Ladder(rungs) => {
let mut rungs :Vec<_> = rungs.into_iter()
.filter_map(|mut r| {
r = r.strip();
if r != TypeTerm::unit() {
Some(match r {
TypeTerm::Ladder(r) => r,
a => vec![ a ]
})
}
else { None }
})
.flatten()
.collect();
if rungs.len() == 1 {
rungs.pop().unwrap()
} else {
TypeTerm::Ladder(rungs)
}
},
TypeTerm::App(args) => {
let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
if args.len() == 0 {
TypeTerm::unit()
} else if args.len() == 1 {
args.pop().unwrap()
} else {
TypeTerm::App(args)
}
}
atom => atom
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\