2023-10-01 18:04:04 +02:00
|
|
|
use crate::TypeID;
|
2023-10-01 17:03:47 +02:00
|
|
|
|
|
|
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
|
|
|
|
|
|
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
|
|
|
pub enum TypeTerm {
|
|
|
|
|
|
|
|
/* Atomic Terms */
|
|
|
|
|
|
|
|
// Base types from dictionary
|
|
|
|
TypeID(TypeID),
|
|
|
|
|
|
|
|
// Literals
|
|
|
|
Num(i64),
|
|
|
|
Char(char),
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/* Complex Terms */
|
|
|
|
|
|
|
|
// Type Parameters
|
|
|
|
// avoid currying to save space & indirection
|
|
|
|
App(Vec< TypeTerm >),
|
|
|
|
|
|
|
|
// Type Ladders
|
|
|
|
Ladder(Vec< TypeTerm >),
|
|
|
|
}
|
|
|
|
|
|
|
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
|
|
|
|
|
|
impl TypeTerm {
|
|
|
|
pub fn unit() -> Self {
|
|
|
|
TypeTerm::Ladder(vec![])
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn new(id: TypeID) -> Self {
|
|
|
|
TypeTerm::TypeID(id)
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn arg(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
|
|
|
|
match self {
|
|
|
|
TypeTerm::App(args) => {
|
2023-10-02 01:27:50 +02:00
|
|
|
args.push(t.into());
|
2023-10-01 17:03:47 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
_ => {
|
|
|
|
*self = TypeTerm::App(vec![
|
|
|
|
self.clone(),
|
|
|
|
t.into()
|
|
|
|
])
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
self
|
|
|
|
}
|
|
|
|
|
2023-10-02 01:28:22 +02:00
|
|
|
pub fn repr_as(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
|
|
|
|
match self {
|
|
|
|
TypeTerm::Ladder(rungs) => {
|
|
|
|
rungs.push(t.into());
|
|
|
|
}
|
|
|
|
|
|
|
|
_ => {
|
|
|
|
*self = TypeTerm::Ladder(vec![
|
|
|
|
self.clone(),
|
|
|
|
t.into()
|
|
|
|
])
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
self
|
|
|
|
}
|
|
|
|
|
2023-10-01 17:03:47 +02:00
|
|
|
pub fn num_arg(&mut self, v: i64) -> &mut Self {
|
|
|
|
self.arg(TypeTerm::Num(v))
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn char_arg(&mut self, c: char) -> &mut Self {
|
|
|
|
self.arg(TypeTerm::Char(c))
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2023-10-02 01:27:50 +02:00
|
|
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
|
|
|
|