Compare commits

..

1 commit

Author SHA1 Message Date
3903cbdecd
wip sugar 2024-05-01 11:54:55 +02:00
12 changed files with 257 additions and 273 deletions

View file

@ -5,8 +5,6 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc)
## Ladder Types ## Ladder Types
### Motivation
In order to implement complex datastructures and algorithms, usually In order to implement complex datastructures and algorithms, usually
many layers of abstraction are built ontop of each other. many layers of abstraction are built ontop of each other.
Consequently higher-level data types are encoded into lower-level data Consequently higher-level data types are encoded into lower-level data
@ -59,48 +57,6 @@ this:
1696093021:1696093039:1528324679:1539892301:1638141920:1688010253 1696093021:1696093039:1528324679:1539892301:1638141920:1688010253
``` ```
### Syntax
In their core form, type-terms can be one of the following:
- (**Atomic Type**) | `SomeTypeName`
- (**Literal Integer**) | `0` | `1` | `2` | ...
- (**Literal Character**) | `'a'` | `'b'` | `'c'` | ...
- (**Literal String**) | `"abc"`
- (**Parameter Application**) | `<T1 T2>` given `T1` and `T2` are type-terms
- (**Ladder**) | `T1 ~ T2` given `T1` and `T2` are type-terms
Ontop of that, the following syntax-sugar is defined:
#### Complex Types
- `[ T ]` <===> `<Seq T>`
- `{ a:A b:B }` <===> `<Struct <"a" A> <"b" B>>`
- `a:A | b:B` <===> `<Enum <"a" A> <"b" B>>`
#### Function Types
- `A -> B` <===> `<Fn A B>`
#### Reference Types
- `*A` <===> `<Ptr A>`
- `&A` <===> `<ConstRef A>`
- `&!A` <===> `<MutRef A>`
### Equivalences
#### Currying
`<<A B> C>` <===> `<A B C>`
#### Ladder-Normal-Form
exhaustively apply `<A B~C>` ===> `<A B>~<A C>`
e.g. `[<Digit 10>]~[Char]~[Ascii]` is in **LNF**
#### Parameter-Normal-Form
exhaustively apply `<A B>~<A C>` ===> `<A B~C>`
e.g. `[<Digit 10>~Char~Ascii]` is in **PNF**
## How to use this crate ## How to use this crate
```rust ```rust
@ -117,19 +73,6 @@ fn main() {
} }
``` ```
## Roadmap
- [x] (Un-)Parsing
- [x] (De-)Currying
- [x] Unification
- [x] Ladder-Normal-Form
- [x] Parameter-Normal-Form
- [ ] (De)-Sugaring
- [ ] Seq
- [ ] Enum
- [ ] Struct
- [ ] References
- [ ] Function
## License ## License
[GPLv3](COPYING) [GPLv3](COPYING)

View file

@ -1,8 +1,11 @@
use crate::bimap::Bimap; use crate::{
bimap::Bimap,
sugar::SUGARID_LIMIT
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Eq, PartialEq, Hash, Clone, Debug)] #[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)]
pub enum TypeID { pub enum TypeID {
Fun(u64), Fun(u64),
Var(u64) Var(u64)
@ -20,11 +23,19 @@ pub struct TypeDict {
impl TypeDict { impl TypeDict {
pub fn new() -> Self { pub fn new() -> Self {
TypeDict { let mut dict = TypeDict {
typenames: Bimap::new(), typenames: Bimap::new(),
type_lit_counter: 0, type_lit_counter: 0,
type_var_counter: 0, type_var_counter: 0,
} };
dict.add_typename("Seq".into());
dict.add_typename("Enum".into());
dict.add_typename("Struct".into());
assert_eq!( dict.type_lit_counter, SUGARID_LIMIT );
dict
} }
pub fn add_varname(&mut self, tn: String) -> TypeID { pub fn add_varname(&mut self, tn: String) -> TypeID {

View file

@ -6,9 +6,9 @@ pub enum LadderTypeToken {
Symbol( String ), Symbol( String ),
Char( char ), Char( char ),
Num( i64 ), Num( i64 ),
Open, Open, OpenSeq, OpenStruct,
Close, Close, CloseSeq, CloseStruct,
Ladder, Ladder, Enum
} }
#[derive(PartialEq, Eq, Clone, Debug)] #[derive(PartialEq, Eq, Clone, Debug)]
@ -75,6 +75,11 @@ where It: Iterator<Item = char>
match c { match c {
'<' => { self.chars.next(); return Some(Ok(LadderTypeToken::Open)); }, '<' => { self.chars.next(); return Some(Ok(LadderTypeToken::Open)); },
'>' => { self.chars.next(); return Some(Ok(LadderTypeToken::Close)); }, '>' => { self.chars.next(); return Some(Ok(LadderTypeToken::Close)); },
'[' => { self.chars.next(); return Some(Ok(LadderTypeToken::OpenSeq)); },
']' => { self.chars.next(); return Some(Ok(LadderTypeToken::CloseSeq)); },
'{' => { self.chars.next(); return Some(Ok(LadderTypeToken::OpenStruct)); },
'}' => { self.chars.next(); return Some(Ok(LadderTypeToken::CloseStruct)); },
'|' => { self.chars.next(); return Some(Ok(LadderTypeToken::Enum)); },
'~' => { self.chars.next(); return Some(Ok(LadderTypeToken::Ladder)); }, '~' => { self.chars.next(); return Some(Ok(LadderTypeToken::Ladder)); },
'\'' => { self.chars.next(); state = LexerState::Char(None); }, '\'' => { self.chars.next(); state = LexerState::Char(None); },
c => { c => {

View file

@ -6,8 +6,8 @@ pub mod lexer;
pub mod parser; pub mod parser;
pub mod unparser; pub mod unparser;
pub mod curry; pub mod curry;
pub mod sugar;
pub mod lnf; pub mod lnf;
pub mod pnf;
pub mod subtype; pub mod subtype;
pub mod unification; pub mod unification;

View file

@ -3,6 +3,7 @@ use {
crate::{ crate::{
dict::*, dict::*,
term::*, term::*,
sugar::*,
lexer::* lexer::*
} }
}; };
@ -21,7 +22,7 @@ pub enum ParseError {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl TypeDict { impl TypeDict {
pub fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> { pub fn parse(&mut self, s: &str) -> Result<SugaredTypeTerm, ParseError> {
let mut tokens = LadderTypeLexer::from(s.chars()).peekable(); let mut tokens = LadderTypeLexer::from(s.chars()).peekable();
match self.parse_ladder(&mut tokens) { match self.parse_ladder(&mut tokens) {
@ -36,7 +37,7 @@ impl TypeDict {
} }
} }
fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<SugaredTypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = char>
{ {
let mut args = Vec::new(); let mut args = Vec::new();
@ -44,7 +45,11 @@ impl TypeDict {
match tok { match tok {
Ok(LadderTypeToken::Close) => { Ok(LadderTypeToken::Close) => {
tokens.next(); tokens.next();
return Ok(TypeTerm::App(args)); return Ok(SugaredTypeTerm::App(args));
}
Ok(LadderTypeToken::CloseSeq) |
Ok(LadderTypeToken::CloseStruct) => {
return Err(ParseError::UnexpectedToken)
} }
_ => { _ => {
match self.parse_ladder(tokens) { match self.parse_ladder(tokens) {
@ -57,29 +62,59 @@ impl TypeDict {
Err(ParseError::UnexpectedEnd) Err(ParseError::UnexpectedEnd)
} }
fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_seq<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<SugaredTypeTerm, ParseError>
where It: Iterator<Item = char>
{
let mut pattern = Vec::new();
while let Some(tok) = tokens.peek() {
match tok {
Ok(LadderTypeToken::CloseSeq) => {
tokens.next();
return Ok(SugaredTypeTerm::Seq(pattern));
}
Ok(LadderTypeToken::Close) |
Ok(LadderTypeToken::CloseStruct) => {
return Err(ParseError::UnexpectedToken)
}
_ => {
match self.parse_ladder(tokens) {
Ok(a) => { pattern.push(a); }
Err(err) => { return Err(err); }
}
}
}
}
Err(ParseError::UnexpectedEnd)
}
fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<SugaredTypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = char>
{ {
match tokens.next() { match tokens.next() {
Some(Ok(LadderTypeToken::Open)) => self.parse_app(tokens), Some(Ok(LadderTypeToken::Open)) => self.parse_app(tokens),
Some(Ok(LadderTypeToken::OpenSeq)) => self.parse_app(tokens),
Some(Ok(LadderTypeToken::OpenStruct)) => self.parse_app(tokens),
Some(Ok(LadderTypeToken::Enum)) => self.parse_app(tokens),
Some(Ok(LadderTypeToken::Close)) => Err(ParseError::UnexpectedClose), Some(Ok(LadderTypeToken::Close)) => Err(ParseError::UnexpectedClose),
Some(Ok(LadderTypeToken::CloseStruct)) => Err(ParseError::UnexpectedToken),
Some(Ok(LadderTypeToken::CloseSeq)) => Err(ParseError::UnexpectedToken),
Some(Ok(LadderTypeToken::Ladder)) => Err(ParseError::UnexpectedLadder), Some(Ok(LadderTypeToken::Ladder)) => Err(ParseError::UnexpectedLadder),
Some(Ok(LadderTypeToken::Symbol(s))) => Some(Ok(LadderTypeToken::Symbol(s))) =>
Ok(TypeTerm::TypeID( Ok(SugaredTypeTerm::TypeID(
if let Some(tyid) = self.get_typeid(&s) { if let Some(tyid) = self.get_typeid(&s) {
tyid tyid
} else { } else {
self.add_typename(s) self.add_typename(s)
} }
)), )),
Some(Ok(LadderTypeToken::Char(c))) => Ok(TypeTerm::Char(c)), Some(Ok(LadderTypeToken::Char(c))) => Ok(SugaredTypeTerm::Char(c)),
Some(Ok(LadderTypeToken::Num(n))) => Ok(TypeTerm::Num(n)), Some(Ok(LadderTypeToken::Num(n))) => Ok(SugaredTypeTerm::Num(n)),
Some(Err(err)) => Err(ParseError::LexError(err)), Some(Err(err)) => Err(ParseError::LexError(err)),
None => Err(ParseError::UnexpectedEnd) None => Err(ParseError::UnexpectedEnd)
} }
} }
fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<SugaredTypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = char>
{ {
let mut rungs = Vec::new(); let mut rungs = Vec::new();
@ -115,7 +150,7 @@ impl TypeDict {
match rungs.len() { match rungs.len() {
0 => Err(ParseError::UnexpectedEnd), 0 => Err(ParseError::UnexpectedEnd),
1 => Ok(rungs[0].clone()), 1 => Ok(rungs[0].clone()),
_ => Ok(TypeTerm::Ladder(rungs)), _ => Ok(SugaredTypeTerm::Ladder(rungs)),
} }
} }
} }

View file

@ -1,113 +0,0 @@
use crate::term::TypeTerm;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl TypeTerm {
/// transmute type into Parameter-Normal-Form (PNF)
///
/// Example:
/// ```ignore
/// <Seq <Digit 10>>~<Seq Char>
/// ⇒ <Seq <Digit 10>~Char>
/// ```
pub fn param_normalize(self) -> Self {
match self {
TypeTerm::Ladder(mut rungs) => {
if rungs.len() > 0 {
// normalize all rungs separately
for r in rungs.iter_mut() {
*r = r.clone().param_normalize();
}
// take top-rung
match rungs.remove(0) {
TypeTerm::App(params_top) => {
let mut params_ladders = Vec::new();
let mut tail : Vec<TypeTerm> = Vec::new();
// append all other rungs to ladders inside
// the application
for p in params_top {
params_ladders.push(vec![ p ]);
}
for r in rungs {
match r {
TypeTerm::App(mut params_rung) => {
if params_rung.len() > 0 {
let mut first_param = params_rung.remove(0);
if first_param == params_ladders[0][0] {
for (l, p) in params_ladders.iter_mut().skip(1).zip(params_rung) {
l.push(p.param_normalize());
}
} else {
params_rung.insert(0, first_param);
tail.push(TypeTerm::App(params_rung));
}
}
}
TypeTerm::Ladder(mut rs) => {
for r in rs {
tail.push(r.param_normalize());
}
}
atomic => {
tail.push(atomic);
}
}
}
let head = TypeTerm::App(
params_ladders.into_iter()
.map(
|mut l| {
l.dedup();
match l.len() {
0 => TypeTerm::unit(),
1 => l.remove(0),
_ => TypeTerm::Ladder(l).param_normalize()
}
}
)
.collect()
);
if tail.len() > 0 {
tail.insert(0, head);
TypeTerm::Ladder(tail)
} else {
head
}
}
TypeTerm::Ladder(mut r) => {
r.append(&mut rungs);
TypeTerm::Ladder(r)
}
atomic => {
rungs.insert(0, atomic);
TypeTerm::Ladder(rungs)
}
}
} else {
TypeTerm::unit()
}
}
TypeTerm::App(params) => {
TypeTerm::App(
params.into_iter()
.map(|p| p.param_normalize())
.collect())
}
atomic => atomic
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

134
src/sugar.rs Normal file
View file

@ -0,0 +1,134 @@
use crate::{
TypeTerm,
TypeID
};
pub const SEQ_SUGARID : TypeID = TypeID::Fun(0);
pub const ENUM_SUGARID : TypeID = TypeID::Fun(1);
pub const STRUCT_SUGARID : TypeID = TypeID::Fun(2);
pub const SUGARID_LIMIT : u64 = 3;
#[derive(Clone)]
pub enum SugaredTypeTerm {
/* 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< SugaredTypeTerm >),
// Type Ladders
Ladder(Vec< SugaredTypeTerm >),
/* Sugar Terms */
Seq( Vec<SugaredTypeTerm> ),
Enum( Vec<SugaredTypeTerm> ),
Struct( Vec<SugaredTypeTerm> )
}
#[derive(Clone)]
struct TypeAssignment {
id: Option<String>,
ty: TypeTerm,
}
#[derive(Clone)]
struct LayoutSugar {
Seq( Vec<TypeAssignment> ),
Enum( Vec<TypeAssignment> ),
Struct( Vec<TypeAssignment> )
}
impl SugaredTypeTerm {
pub fn desugar(self) -> TypeTerm {
match self {
SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
SugaredTypeTerm::Num(n) => TypeTerm::Num(n),
SugaredTypeTerm::Char(c) => TypeTerm::Char(c),
SugaredTypeTerm::App(params) => TypeTerm::App(params.into_iter().map(|p| p.desugar()).collect()),
SugaredTypeTerm::Ladder(rungs) => TypeTerm::Ladder(rungs.into_iter().map(|p| p.desugar()).collect()),
SugaredTypeTerm::Seq(pattern) => {
let mut params : Vec<TypeTerm> = pattern.into_iter().map(|p| p.desugar()).collect();
params.insert(0, TypeTerm::TypeID(SEQ_SUGARID));
TypeTerm::App(params)
}
SugaredTypeTerm::Enum(options) => {
let mut params : Vec<TypeTerm> = options.into_iter().map(|o| o.desugar()).collect();
params.insert(0, TypeTerm::TypeID(ENUM_SUGARID));
TypeTerm::App(params)
}
SugaredTypeTerm::Struct(members) => {
let mut params : Vec<TypeTerm> = members.into_iter().map(|m| m.desugar()).collect();
params.insert(0, TypeTerm::TypeID(STRUCT_SUGARID));
TypeTerm::App(params)
}
}
}
// normalize any unsugared parts into sugared form
pub fn sugar(self) -> SugaredTypeTerm {
// todo: optimize
self.desugar().sugar()
}
}
impl TypeTerm {
pub fn sugar(self) -> SugaredTypeTerm {
match self {
TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
TypeTerm::Char(c) => SugaredTypeTerm::Char(c),
TypeTerm::App(mut params) => {
if params.len() > 0 {
let prim = params.remove(0);
match prim {
TypeTerm::TypeID( SEQ_SUGARID ) =>
SugaredTypeTerm::Seq(
params
.into_iter()
.map(|p| p.sugar())
.collect()
),
TypeTerm::TypeID( ENUM_SUGARID ) =>
SugaredTypeTerm::Enum(
params
.into_iter()
.map(|p| p.sugar())
.collect()
),
TypeTerm::TypeID( STRUCT_SUGARID ) =>
SugaredTypeTerm::Struct(
params
.into_iter()
.map(|p| p.sugar())
.collect()
),
other => SugaredTypeTerm::App(
params.into_iter().map(|p| p.sugar()).collect()
)
}
} else {
SugaredTypeTerm::App(vec![])
}
},
TypeTerm::Ladder(rungs) => {
SugaredTypeTerm::Ladder(rungs.into_iter().map(|r| r.sugar()).collect())
}
}
}
}

View file

@ -2,8 +2,8 @@
pub mod lexer; pub mod lexer;
pub mod parser; pub mod parser;
pub mod curry; pub mod curry;
pub mod sugar;
pub mod lnf; pub mod lnf;
pub mod pnf;
pub mod subtype; pub mod subtype;
pub mod substitution; pub mod substitution;
pub mod unification; pub mod unification;

View file

@ -1,6 +1,6 @@
use { use {
crate::{term::*, dict::*, parser::*} crate::{term::*, dict::*, parser::*, sugar::SUGARID_LIMIT}
}; };
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@ -17,7 +17,7 @@ fn test_parser_id() {
); );
assert_eq!( assert_eq!(
Ok(TypeTerm::TypeID(TypeID::Fun(0))), Ok(TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0))),
dict.parse("A") dict.parse("A")
); );
} }
@ -43,16 +43,16 @@ fn test_parser_app() {
assert_eq!( assert_eq!(
TypeDict::new().parse("<A B>"), TypeDict::new().parse("<A B>"),
Ok(TypeTerm::App(vec![ Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
])) ]))
); );
assert_eq!( assert_eq!(
TypeDict::new().parse("<A B C>"), TypeDict::new().parse("<A B C>"),
Ok(TypeTerm::App(vec![ Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
])) ]))
); );
} }
@ -78,16 +78,16 @@ fn test_parser_ladder() {
assert_eq!( assert_eq!(
TypeDict::new().parse("A~B"), TypeDict::new().parse("A~B"),
Ok(TypeTerm::Ladder(vec![ Ok(TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
])) ]))
); );
assert_eq!( assert_eq!(
TypeDict::new().parse("A~B~C"), TypeDict::new().parse("A~B~C"),
Ok(TypeTerm::Ladder(vec![ Ok(TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
])) ]))
); );
} }
@ -98,12 +98,12 @@ fn test_parser_ladder_outside() {
TypeDict::new().parse("<A B>~C"), TypeDict::new().parse("<A B>~C"),
Ok(TypeTerm::Ladder(vec![ Ok(TypeTerm::Ladder(vec![
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
]), ]),
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
])) ]))
); );
} }
#[test] #[test]
@ -111,10 +111,10 @@ fn test_parser_ladder_inside() {
assert_eq!( assert_eq!(
TypeDict::new().parse("<A B~C>"), TypeDict::new().parse("<A B~C>"),
Ok(TypeTerm::App(vec![ Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
]) ])
])) ]))
); );
@ -125,12 +125,12 @@ fn test_parser_ladder_between() {
assert_eq!( assert_eq!(
TypeDict::new().parse("<A B~<C D>>"), TypeDict::new().parse("<A B~<C D>>"),
Ok(TypeTerm::App(vec![ Ok(TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
TypeTerm::TypeID(TypeID::Fun(3)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+3)),
]) ])
]) ])
])) ]))
@ -156,48 +156,48 @@ fn test_parser_ladder_large() {
Ok( Ok(
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(2)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
TypeTerm::TypeID(TypeID::Fun(3)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+3))
]), ]),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(4)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+4)),
TypeTerm::TypeID(TypeID::Fun(5)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+5))
]), ]),
TypeTerm::TypeID(TypeID::Fun(6)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+6)),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(7)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+7)),
TypeTerm::Num(10), TypeTerm::Num(10),
TypeTerm::TypeID(TypeID::Fun(8)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+8))
]), ]),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(9)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+9)),
TypeTerm::Num(10) TypeTerm::Num(10)
]), ]),
TypeTerm::TypeID(TypeID::Fun(10)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10))
]) ])
]) ])
]) ])
]), ]),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(11)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+11)),
TypeTerm::TypeID(TypeID::Fun(10)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10)),
TypeTerm::Char(':') TypeTerm::Char(':')
]), ]),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(10)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10))
]), ]),
TypeTerm::TypeID(TypeID::Fun(12)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+12)),
TypeTerm::App(vec![ TypeTerm::App(vec![
TypeTerm::TypeID(TypeID::Fun(0)), TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::TypeID(TypeID::Fun(13)) TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+13))
]) ])
]) ])
) )

View file

@ -1,41 +0,0 @@
use crate::dict::TypeDict;
#[test]
fn test_param_normalize() {
let mut dict = TypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error"),
dict.parse("A~B~C").expect("parse error").param_normalize(),
);
assert_eq!(
dict.parse("<A B>~C").expect("parse error"),
dict.parse("<A B>~C").expect("parse error").param_normalize(),
);
assert_eq!(
dict.parse("<A B~C>").expect("parse error"),
dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
);
assert_eq!(
dict.parse("<A B~C D~E>").expect("parse error"),
dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").param_normalize(),
);
assert_eq!(
dict.parse("<Seq <Digit 10>~Char>").expect("parse error"),
dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").param_normalize(),
);
assert_eq!(
dict.parse("<A <B C~D~E> F~G H H>").expect("parse error"),
dict.parse("<A <B C> F H H>
~<A <B D> F H H>
~<A <B E> F H H>
~<A <B E> G H H>").expect("parse errror")
.param_normalize(),
);
}

10
src/test/sugar.rs Normal file
View file

@ -0,0 +1,10 @@
#[test]
fn test_sugar() {
let mut dict = crate::TypeDict::new();
}

View file

@ -13,8 +13,8 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
dict.add_varname(String::from("V")); dict.add_varname(String::from("V"));
dict.add_varname(String::from("W")); dict.add_varname(String::from("W"));
let mut t1 = dict.parse(ts1).unwrap(); let mut t1 = dict.parse(ts1).unwrap().desugar();
let mut t2 = dict.parse(ts2).unwrap(); let mut t2 = dict.parse(ts2).unwrap().desugar();
let σ = crate::unify( &t1, &t2 ); let σ = crate::unify( &t1, &t2 );
if expect_unificator { if expect_unificator {