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

Compare commits

..

1 commit
dev ... topic-marc

Author SHA1 Message Date
Michael Sippel
5b45f164fb
macro wip 2024-02-27 03:37:09 +01:00
27 changed files with 215 additions and 2412 deletions

15
.github/workflows/cargo-test.yml vendored
View file

@ -2,20 +2,21 @@ name: Rust
on: on:
push: push:
branches: ["dev"] branches: [ "dev" ]
pull_request: pull_request:
branches: ["dev"] branches: [ "dev" ]
env: env:
CARGO_TERM_COLOR: always CARGO_TERM_COLOR: always
jobs: jobs:
build: build:
runs-on: ubuntu-latest runs-on: ubuntu-latest
steps: steps:
- uses: actions/checkout@v3 - uses: actions/checkout@v3
- name: Build - name: Build
run: cargo build --verbose --features pretty run: cargo build --verbose
- name: Run tests - name: Run tests
run: cargo test --verbose --features pretty run: cargo test --verbose

9
Cargo.toml
View file

@ -4,8 +4,9 @@ edition = "2018"
name = "laddertypes" name = "laddertypes"
version = "0.1.0" version = "0.1.0"
[dependencies] #[lib]
tiny-ansi = { version = "0.1.0", optional = true } #proc-macro = true
[dependencies]
laddertype-macro = { path = "./laddertype-macro" }
[features]
pretty = ["dep:tiny-ansi"]

57
README.md
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)

1
src/bimap.rs
View file

@ -2,7 +2,6 @@ use std::{collections::HashMap, hash::Hash};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Debug)]
pub struct Bimap<V: Eq + Hash, Λ: Eq + Hash> { pub struct Bimap<V: Eq + Hash, Λ: Eq + Hash> {
pub mλ: HashMap<V, Λ>, pub mλ: HashMap<V, Λ>,
pub my: HashMap<Λ, V>, pub my: HashMap<Λ, V>,

83
src/dict.rs
View file

@ -2,42 +2,15 @@ use crate::bimap::Bimap;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)] #[derive(Eq, PartialEq, Hash, Clone, Debug)]
pub enum TypeID { pub enum TypeID {
Fun(u64), Fun(u64),
Var(u64) Var(u64)
} }
pub trait TypeDict : Send + Sync {
fn insert(&mut self, name: String, id: TypeID);
fn add_varname(&mut self, vn: String) -> TypeID;
fn add_typename(&mut self, tn: String) -> TypeID;
fn get_typeid(&self, tn: &String) -> Option<TypeID>;
fn get_typename(&self, tid: &TypeID) -> Option<String>;
fn get_varname(&self, var_id: u64) -> Option<String> {
self.get_typename(&TypeID::Var(var_id))
}
fn add_synonym(&mut self, new: String, old: String) {
if let Some(tyid) = self.get_typeid(&old) {
self.insert(new, tyid);
}
}
fn get_typeid_creat(&mut self, tn: &String) -> TypeID {
if let Some(id) = self.get_typeid(tn) {
id
} else {
self.add_typename(tn.clone())
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Debug)] pub struct TypeDict {
pub struct BimapTypeDict {
typenames: Bimap<String, TypeID>, typenames: Bimap<String, TypeID>,
type_lit_counter: u64, type_lit_counter: u64,
type_var_counter: u64, type_var_counter: u64,
@ -45,66 +18,42 @@ pub struct BimapTypeDict {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl BimapTypeDict { impl TypeDict {
pub fn new() -> Self { pub fn new() -> Self {
BimapTypeDict { TypeDict {
typenames: Bimap::new(), typenames: Bimap::new(),
type_lit_counter: 0, type_lit_counter: 0,
type_var_counter: 0, type_var_counter: 0,
} }
} }
}
impl TypeDict for BimapTypeDict { pub fn add_varname(&mut self, tn: String) -> TypeID {
fn insert(&mut self, name: String, id: TypeID) {
self.typenames.insert(name, id);
}
fn add_varname(&mut self, tn: String) -> TypeID {
let tyid = TypeID::Var(self.type_var_counter); let tyid = TypeID::Var(self.type_var_counter);
self.type_var_counter += 1; self.type_var_counter += 1;
self.insert(tn, tyid.clone()); self.typenames.insert(tn, tyid.clone());
tyid tyid
} }
fn add_typename(&mut self, tn: String) -> TypeID { pub fn add_typename(&mut self, tn: String) -> TypeID {
let tyid = TypeID::Fun(self.type_lit_counter); let tyid = TypeID::Fun(self.type_lit_counter);
self.type_lit_counter += 1; self.type_lit_counter += 1;
self.insert(tn, tyid.clone()); self.typenames.insert(tn, tyid.clone());
tyid tyid
} }
fn get_typename(&self, tid: &TypeID) -> Option<String> { pub fn add_synonym(&mut self, new: String, old: String) {
if let Some(tyid) = self.get_typeid(&old) {
self.typenames.insert(new, tyid);
}
}
pub fn get_typename(&self, tid: &TypeID) -> Option<String> {
self.typenames.my.get(tid).cloned() self.typenames.my.get(tid).cloned()
} }
fn get_typeid(&self, tn: &String) -> Option<TypeID> { pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
self.typenames.mλ.get(tn).cloned() self.typenames.mλ.get(tn).cloned()
} }
} }
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
use std::sync::Arc;
use std::ops::{Deref, DerefMut};
use std::sync::RwLock;
impl<T: TypeDict> TypeDict for Arc<RwLock<T>> {
fn insert(&mut self, name: String, id: TypeID) {
self.write().unwrap().insert(name, id);
}
fn add_varname(&mut self, vn: String) -> TypeID {
self.write().unwrap().add_varname(vn)
}
fn add_typename(&mut self, tn: String) -> TypeID {
self.write().unwrap().add_typename(tn)
}
fn get_typename(&self, tid: &TypeID)-> Option<String> {
self.read().unwrap().get_typename(tid)
}
fn get_typeid(&self, tn: &String) -> Option<TypeID> {
self.read().unwrap().get_typeid(tn)
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>

16
src/lib.rs
View file

@ -2,32 +2,20 @@
pub mod bimap; pub mod bimap;
pub mod dict; pub mod dict;
pub mod term; pub mod term;
pub mod substitution;
pub mod lexer; pub mod lexer;
pub mod parser; pub mod parser;
pub mod unparser; pub mod unparser;
pub mod sugar;
pub mod curry; pub mod curry;
pub mod lnf; pub mod lnf;
pub mod pnf;
pub mod subtype; pub mod subtype;
pub mod unification; pub mod unification;
pub mod morphism;
pub mod morphism_base;
pub mod morphism_path;
#[cfg(test)] #[cfg(test)]
mod test; mod test;
#[cfg(feature = "pretty")]
mod pretty;
pub use { pub use {
dict::*, dict::*,
term::*, term::*,
substitution::*, unification::*
sugar::*,
unification::*,
morphism::*
}; };

63
src/morphism.rs
View file

@ -1,63 +0,0 @@
use {
crate::{
subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
},
std::{collections::HashMap, u64}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone, PartialEq, Eq, Debug)]
pub struct MorphismType {
pub src_type: TypeTerm,
pub dst_type: TypeTerm,
}
impl MorphismType {
pub fn normalize(self) -> Self {
MorphismType {
src_type: self.src_type.normalize().param_normalize(),
dst_type: self.dst_type.normalize().param_normalize()
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait Morphism : Sized {
fn get_type(&self) -> MorphismType;
fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
fn weight(&self) -> u64 {
1
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone, Debug, PartialEq)]
pub struct MorphismInstance<M: Morphism + Clone> {
pub halo: TypeTerm,
pub m: M,
pub σ: HashMap<TypeID, TypeTerm>
}
impl<M: Morphism + Clone> MorphismInstance<M> {
pub fn get_type(&self) -> MorphismType {
MorphismType {
src_type: TypeTerm::Ladder(vec![
self.halo.clone(),
self.m.get_type().src_type.clone()
]).apply_substitution(&self.σ)
.clone(),
dst_type: TypeTerm::Ladder(vec![
self.halo.clone(),
self.m.get_type().dst_type.clone()
]).apply_substitution(&self.σ)
.clone()
}.normalize()
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

183
src/morphism_base.rs
View file

@ -1,183 +0,0 @@
use {
crate::{
subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm,
morphism::{MorphismType, Morphism, MorphismInstance}
},
std::{collections::HashMap, u64}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone)]
pub struct MorphismBase<M: Morphism + Clone> {
morphisms: Vec< M >,
seq_types: Vec< TypeTerm >
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<M: Morphism + Clone> MorphismBase<M> {
pub fn new(seq_types: Vec<TypeTerm>) -> Self {
MorphismBase {
morphisms: Vec::new(),
seq_types
}
}
pub fn add_morphism(&mut self, m: M) {
self.morphisms.push( m );
}
pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
-> Vec< MorphismInstance<M> >
{
let mut dst_types = Vec::new();
for m in self.morphisms.iter() {
if let Ok((halo, σ)) = crate::unification::subtype_unify(
&src_type.clone().param_normalize(),
&m.get_type().src_type.param_normalize(),
) {
dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
}
}
dst_types
}
pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
-> Vec< MorphismInstance<M> > {
let src_type = src_type.clone().param_normalize();
let mut dst_types = Vec::new();
// Check if we have a List type, and if so, see what the Item type is
// TODO: function for generating fresh variables
let item_variable = TypeID::Var(800);
for seq_type in self.seq_types.iter() {
if let Ok((halo, σ)) = crate::unification::subtype_unify(
&src_type,
&TypeTerm::App(vec![
seq_type.clone(),
TypeTerm::TypeID(item_variable)
])
) {
let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
for item_morph_inst in self.enum_morphisms( &src_item_type ) {
let mut dst_halo_ladder = vec![ halo.clone() ];
if item_morph_inst.halo != TypeTerm::unit() {
dst_halo_ladder.push(
TypeTerm::App(vec![
seq_type.clone().get_lnf_vec().first().unwrap().clone(),
item_morph_inst.halo.clone()
]));
}
if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
dst_types.push(
MorphismInstance {
halo: TypeTerm::Ladder(dst_halo_ladder).strip().param_normalize(),
m: map_morph,
σ: item_morph_inst.σ
}
);
} else {
eprintln!("could not get map morphism");
}
}
}
}
dst_types
}
pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
let mut dst_types = Vec::new();
dst_types.append(&mut self.enum_direct_morphisms(src_type));
dst_types.append(&mut self.enum_map_morphisms(src_type));
dst_types
}
pub fn find_direct_morphism(&self,
ty: &MorphismType,
dict: &mut impl TypeDict
) -> Option< MorphismInstance<M> > {
eprintln!("find direct morph");
for m in self.morphisms.iter() {
let ty = ty.clone().normalize();
let morph_type = m.get_type().normalize();
eprintln!("find direct morph:\n {} <= {}",
dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
);
if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
eprintln!("halo: {}", dict.unparse(&halo));
let dst_type = TypeTerm::Ladder(vec![
halo.clone(),
morph_type.dst_type.clone()
]).normalize().param_normalize();
eprintln!("-----------> {} <= {}",
dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
);
if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
eprintln!("match. halo2 = {}", dict.unparse(&halo2));
return Some(MorphismInstance {
m: m.clone(),
halo,
σ,
});
}
}
}
None
}
pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
for seq_type in self.seq_types.iter() {
if let Ok((halos, σ)) = UnificationProblem::new_sub(vec![
(ty.src_type.clone().param_normalize(),
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
(TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
ty.dst_type.clone().param_normalize()),
]).solve() {
// TODO: use real fresh variable names
let item_morph_type = MorphismType {
src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
}.normalize();
//eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
return Some( MorphismInstance {
m: list_morph,
σ,
halo: halos[0].clone()
} );
}
}
}
}
None
}
pub fn find_morphism(&self, ty: &MorphismType,
dict: &mut impl TypeDict
)
-> Option< MorphismInstance<M> > {
if let Some(m) = self.find_direct_morphism(ty, dict) {
return Some(m);
}
if let Some(m) = self.find_map_morphism(ty, dict) {
return Some(m);
}
None
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

136
src/morphism_path.rs
View file

@ -1,136 +0,0 @@
use {
crate::{
morphism::{MorphismType, Morphism, MorphismInstance},
morphism_base::MorphismBase,
dict::*,
term::*
}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone)]
pub struct MorphismPath<M: Morphism + Clone> {
pub weight: u64,
pub cur_type: TypeTerm,
pub morphisms: Vec< MorphismInstance<M> >
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub struct ShortestPathProblem<'a, M: Morphism + Clone> {
pub morphism_base: &'a MorphismBase<M>,
pub goal: TypeTerm,
queue: Vec< MorphismPath<M> >
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
pub fn new(morphism_base: &'a MorphismBase<M>, ty: MorphismType) -> Self {
ShortestPathProblem {
morphism_base,
queue: vec![
MorphismPath::<M> { weight: 0, cur_type: ty.src_type, morphisms: vec![] }
],
goal: ty.dst_type
}
}
pub fn solve(&mut self) -> Option< Vec<MorphismInstance<M>> > {
while ! self.queue.is_empty() {
self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
if let Some(mut cur_path) = self.queue.pop() {
if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
/* found path,
* now apply substitution and trim to variables in terms of each step
*/
for n in cur_path.morphisms.iter_mut() {
let src_type = n.m.get_type().src_type;
let dst_type = n.m.get_type().dst_type;
let mut new_σ = std::collections::HashMap::new();
for (k,v) in σ.iter() {
if let TypeID::Var(varid) = k {
if src_type.contains_var(*varid)
|| dst_type.contains_var(*varid) {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&σ).clone().strip()
);
}
}
}
for (k,v) in n.σ.iter() {
if let TypeID::Var(varid) = k {
if src_type.contains_var(*varid)
|| dst_type.contains_var(*varid) {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&σ).clone().strip()
);
}
}
}
n.halo = n.halo.clone().apply_substitution(&σ).clone().strip().param_normalize();
n.σ = new_σ;
}
return Some(cur_path.morphisms);
}
//eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
for mut next_morph_inst in self.morphism_base.enum_morphisms(&cur_path.cur_type) {
let dst_type = next_morph_inst.get_type().dst_type;
// eprintln!("try morph to {}", dst_type.clone().sugar(type_dict).pretty(type_dict, 0));
let mut creates_loop = false;
let mut new_path = cur_path.clone();
for n in new_path.morphisms.iter_mut() {
let mut new_σ = std::collections::HashMap::new();
for (k,v) in next_morph_inst.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&next_morph_inst.σ).clone()
);
}
for (k,v) in n.σ.iter() {
new_σ.insert(
k.clone(),
v.clone().apply_substitution(&next_morph_inst.σ).clone()
);
}
n.halo = n.halo.clone().apply_substitution(&next_morph_inst.σ).clone().strip().param_normalize();
n.σ = new_σ;
}
for m in new_path.morphisms.iter() {
if m.get_type().src_type == dst_type {
creates_loop = true;
break;
}
}
if ! creates_loop {
new_path.weight += next_morph_inst.m.weight();
new_path.cur_type = dst_type;
new_path.morphisms.push(next_morph_inst);
self.queue.push(new_path);
}
}
}
}
None
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

35
src/parser.rs
View file

@ -18,25 +18,16 @@ pub enum ParseError {
UnexpectedToken UnexpectedToken
} }
pub trait ParseLadderType {
fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError>;
fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char>;
fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char>;
fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char>;
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<T: TypeDict> ParseLadderType for T { impl TypeDict {
fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> { pub fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
let mut tokens = LadderTypeLexer::from(s.chars()).peekable(); let mut tokens = LadderTypeLexer::from(s.chars());
self.parse_tokens( tokens.peekable() )
}
pub fn parse_tokens<It>(&mut self, mut tokens: Peekable<It>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = Result<LadderTypeToken, LexError>> {
match self.parse_ladder(&mut tokens) { match self.parse_ladder(&mut tokens) {
Ok(t) => { Ok(t) => {
if let Some(_tok) = tokens.peek() { if let Some(_tok) = tokens.peek() {
@ -49,8 +40,8 @@ impl<T: TypeDict> ParseLadderType for T {
} }
} }
fn parse_app<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_app<It>(&mut self, tokens: &mut Peekable<It>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = Result<LadderTypeToken, LexError>>
{ {
let mut args = Vec::new(); let mut args = Vec::new();
while let Some(tok) = tokens.peek() { while let Some(tok) = tokens.peek() {
@ -70,8 +61,8 @@ impl<T: TypeDict> ParseLadderType for T {
Err(ParseError::UnexpectedEnd) Err(ParseError::UnexpectedEnd)
} }
fn parse_rung<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_rung<It>(&mut self, tokens: &mut Peekable<It>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = Result<LadderTypeToken, LexError>>
{ {
match tokens.next() { match tokens.next() {
Some(Ok(LadderTypeToken::Open)) => self.parse_app(tokens), Some(Ok(LadderTypeToken::Open)) => self.parse_app(tokens),
@ -92,8 +83,8 @@ impl<T: TypeDict> ParseLadderType for T {
} }
} }
fn parse_ladder<It>(&mut self, tokens: &mut Peekable<LadderTypeLexer<It>>) -> Result<TypeTerm, ParseError> fn parse_ladder<It>(&mut self, tokens: &mut Peekable<It>) -> Result<TypeTerm, ParseError>
where It: Iterator<Item = char> where It: Iterator<Item = Result<LadderTypeToken, LexError>>
{ {
let mut rungs = Vec::new(); let mut rungs = Vec::new();

138
src/pnf.rs
View file

@ -1,138 +0,0 @@
use crate::term::TypeTerm;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm > ) -> Vec< TypeTerm > {
for i in 0 .. upper.len() {
if upper[i] == lower[0] {
let mut result_ladder = Vec::<TypeTerm>::new();
result_ladder.append(&mut upper[0..i].iter().cloned().collect());
result_ladder.append(&mut lower);
return result_ladder;
}
}
upper.append(&mut lower);
upper
}
impl TypeTerm {
/// transmute type into Parameter-Normal-Form (PNF)
///
/// Example:
/// ```ignore
/// <Seq <Digit 10>>~<Seq Char>
/// ⇒ <Seq <Digit 10>~Char>
/// ```
pub fn param_normalize(mut self) -> Self {
match self {
TypeTerm::Ladder(mut rungs) => {
if rungs.len() > 0 {
let mut new_rungs = Vec::new();
while let Some(bottom) = rungs.pop() {
if let Some(last_but) = rungs.last_mut() {
match (bottom, last_but) {
(TypeTerm::App(bot_args), TypeTerm::App(last_args)) => {
if bot_args.len() == last_args.len() {
let mut new_rung_params = Vec::new();
let mut require_break = false;
if bot_args.len() > 0 {
if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
for i in 0 .. bot_args.len() {
let spliced_type_ladder = splice_ladders(
last_args[i].clone().get_lnf_vec(),
bot_args[i].clone().get_lnf_vec()
);
let spliced_type =
if spliced_type_ladder.len() == 1 {
spliced_type_ladder[0].clone()
} else if spliced_type_ladder.len() > 1 {
TypeTerm::Ladder(spliced_type_ladder)
} else {
TypeTerm::unit()
};
new_rung_params.push( spliced_type.param_normalize() );
}
} else {
new_rung_params.push(
TypeTerm::Ladder(vec![
last_args[0].clone(),
bot_args[0].clone()
]).normalize()
);
for i in 1 .. bot_args.len() {
if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
let spliced_type_ladder = splice_ladders(
last_args[i].clone().get_lnf_vec(),
bot_args[i].clone().get_lnf_vec()
);
let spliced_type =
if spliced_type_ladder.len() == 1 {
spliced_type_ladder[0].clone()
} else if spliced_type_ladder.len() > 1 {
TypeTerm::Ladder(spliced_type_ladder)
} else {
TypeTerm::unit()
};
new_rung_params.push( spliced_type.param_normalize() );
} else {
new_rung_params.push( bot_args[i].clone() );
require_break = true;
}
}
}
}
if require_break {
new_rungs.push( TypeTerm::App(new_rung_params) );
} else {
rungs.pop();
rungs.push(TypeTerm::App(new_rung_params));
}
} else {
new_rungs.push( TypeTerm::App(bot_args) );
}
}
(bottom, last_buf) => {
new_rungs.push( bottom );
}
}
} else {
new_rungs.push( bottom );
}
}
new_rungs.reverse();
if new_rungs.len() > 1 {
TypeTerm::Ladder(new_rungs)
} else if new_rungs.len() == 1 {
new_rungs[0].clone()
} else {
TypeTerm::unit()
}
} else {
TypeTerm::unit()
}
}
TypeTerm::App(params) => {
TypeTerm::App(
params.into_iter()
.map(|p| p.param_normalize())
.collect())
}
atomic => atomic
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

157
src/pretty.rs
View file

@ -1,157 +0,0 @@
use {
crate::{TypeDict, dict::TypeID},
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) => {
match id {
TypeID::Var(varid) => {
format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_magenta()
},
TypeID::Fun(funid) => {
format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).blue().bold()
}
}
},
SugaredTypeTerm::Num(n) => {
format!("{}", n).green().bold()
}
SugaredTypeTerm::Char(c) => {
match c {
'\0' => format!("'\\0'"),
'\n' => format!("'\\n'"),
_ => 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());
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());
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
}
}
}
}

64
src/substitution.rs
View file

@ -1,64 +0,0 @@
use crate::{
TypeID,
TypeTerm
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait Substitution {
fn get(&self, t: &TypeID) -> Option< TypeTerm >;
}
impl<S: Fn(&TypeID)->Option<TypeTerm>> Substitution for S {
fn get(&self, t: &TypeID) -> Option< TypeTerm > {
(self)(t)
}
}
impl Substitution for std::collections::HashMap< TypeID, TypeTerm > {
fn get(&self, t: &TypeID) -> Option< TypeTerm > {
(self as &std::collections::HashMap< TypeID, TypeTerm >).get(t).cloned()
}
}
pub type HashMapSubst = std::collections::HashMap< TypeID, TypeTerm >;
impl TypeTerm {
/// recursively apply substitution to all subterms,
/// which will replace all occurences of variables which map
/// some type-term in `subst`
pub fn apply_substitution(
&mut self,
σ: &impl Substitution
) -> &mut Self {
self.apply_subst(σ)
}
pub fn apply_subst(
&mut self,
σ: &impl Substitution
) -> &mut Self {
match self {
TypeTerm::TypeID(typid) => {
if let Some(t) = σ.get(typid) {
*self = t;
}
}
TypeTerm::Ladder(rungs) => {
for r in rungs.iter_mut() {
r.apply_subst(σ);
}
}
TypeTerm::App(args) => {
for r in args.iter_mut() {
r.apply_subst(σ);
}
}
_ => {}
}
self
}
}

114
src/sugar.rs
View file

@ -1,114 +0,0 @@
use {
crate::{TypeTerm, TypeID, parser::ParseLadderType}
};
#[derive(Clone)]
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 impl 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 impl 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()),
}
}
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())
}
}
}
}

79
src/term.rs
View file

@ -79,77 +79,34 @@ impl TypeTerm {
self.arg(TypeTerm::Char(c)) self.arg(TypeTerm::Char(c))
} }
pub fn contains_var(&self, var_id: u64) -> bool { /// recursively apply substitution to all subterms,
/// which will replace all occurences of variables which map
/// some type-term in `subst`
pub fn apply_substitution(
&mut self,
subst: &impl Fn(&TypeID) -> Option<TypeTerm>
) -> &mut Self {
match self { match self {
TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v), TypeTerm::TypeID(typid) => {
TypeTerm::App(args) | if let Some(t) = subst(typid) {
TypeTerm::Ladder(args) => { *self = t;
for a in args.iter() {
if a.contains_var(var_id) {
return true;
}
}
false
}
_ => false
}
}
/* 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
}
}
pub fn get_interface_type(&self) -> TypeTerm {
match self {
TypeTerm::Ladder(rungs) => { TypeTerm::Ladder(rungs) => {
if let Some(top) = rungs.first() { for r in rungs.iter_mut() {
top.get_interface_type() r.apply_substitution(subst);
} else {
TypeTerm::unit()
} }
} }
TypeTerm::App(args) => { TypeTerm::App(args) => {
TypeTerm::App(args.iter().map(|a| a.get_interface_type()).collect()) for r in args.iter_mut() {
r.apply_substitution(subst);
}
} }
atom => atom.clone() _ => {}
} }
self
} }
} }

6
src/test/curry.rs
View file

@ -1,12 +1,12 @@
use { use {
crate::{dict::*, parser::*} crate::{dict::*}
}; };
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test] #[test]
fn test_curry() { fn test_curry() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert_eq!( assert_eq!(
dict.parse("<A B C>").unwrap().curry(), dict.parse("<A B C>").unwrap().curry(),
@ -33,7 +33,7 @@ fn test_curry() {
#[test] #[test]
fn test_decurry() { fn test_decurry() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert_eq!( assert_eq!(
dict.parse("<<A B> C>").unwrap().decurry(), dict.parse("<<A B> C>").unwrap().decurry(),

1
src/test/lexer.rs
View file

@ -153,4 +153,3 @@ fn test_lexer_large() {
assert_eq!( lex.next(), None ); assert_eq!( lex.next(), None );
} }

7
src/test/lnf.rs
View file

@ -1,8 +1,8 @@
use crate::{dict::{BimapTypeDict}, parser::*}; use crate::dict::TypeDict;
#[test] #[test]
fn test_flat() { fn test_flat() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert!( dict.parse("A").expect("parse error").is_flat() ); assert!( dict.parse("A").expect("parse error").is_flat() );
assert!( dict.parse("10").expect("parse error").is_flat() ); assert!( dict.parse("10").expect("parse error").is_flat() );
@ -17,7 +17,7 @@ fn test_flat() {
#[test] #[test]
fn test_normalize() { fn test_normalize() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert_eq!( assert_eq!(
dict.parse("A~B~C").expect("parse error").normalize(), dict.parse("A~B~C").expect("parse error").normalize(),
@ -54,3 +54,4 @@ fn test_normalize() {
); );
} }

2
src/test/mod.rs
View file

@ -3,9 +3,7 @@ pub mod lexer;
pub mod parser; pub mod parser;
pub mod curry; pub mod curry;
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;
pub mod morphism;

471
src/test/morphism.rs
View file

@ -1,471 +0,0 @@
use {
crate::{dict::*, morphism::*, parser::*, unparser::*, TypeTerm, morphism_base::*, morphism_path::*}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
eprintln!("{{");
for (k,v) in m.iter() {
eprintln!(" {} --> {}",
dict.get_typename(k).unwrap(),
dict.unparse(v)
);
}
eprintln!("}}");
}
fn print_path(dict: &mut impl TypeDict, path: &Vec<MorphismInstance<DummyMorphism>>) {
for n in path.iter() {
eprintln!("
ψ = {}
morph {}
--> {}
with
",
n.halo.clone().sugar(dict).pretty(dict, 0),
n.m.get_type().src_type.sugar(dict).pretty(dict, 0),
n.m.get_type().dst_type.sugar(dict).pretty(dict, 0),
);
print_subst(&n.σ, dict)
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone, Debug, PartialEq)]
struct DummyMorphism(MorphismType);
impl Morphism for DummyMorphism {
fn get_type(&self) -> MorphismType {
self.0.clone().normalize()
}
fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
Some(DummyMorphism(MorphismType {
src_type: TypeTerm::App(vec![
seq_type.clone(),
self.0.src_type.clone()
]),
dst_type: TypeTerm::App(vec![
seq_type.clone(),
self.0.dst_type.clone()
])
}))
}
}
fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
let mut dict = BimapTypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
dict.add_varname("Radix".into());
dict.add_varname("SrcRadix".into());
dict.add_varname("DstRadix".into());
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap()
})
);
(dict, base)
}
#[test]
fn test_morphism_path1() {
let (mut dict, mut base) = morphism_test_setup();
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("<Digit 10> ~ Char").unwrap(),
dst_type: dict.parse("<Digit 10> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
}).solve();
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
}),
}
]
));
}
#[test]
fn test_morphism_path2() {
let (mut dict, mut base) = morphism_test_setup();
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
}).solve();
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").expect(""),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
}
]
));
}
#[test]
fn test_morphism_path3() {
let (mut dict, mut base) = morphism_test_setup();
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
}).solve();
if let Some(path) = path.as_ref() {
print_path(&mut dict, path);
}
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType {
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
}
]
));
}
#[test]
fn test_morphism_path4() {
let (mut dict, mut base) = morphism_test_setup();
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
}).solve();
if let Some(path) = path.as_ref() {
print_path(&mut dict, path);
}
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 LittleEndian>").expect(""),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType {
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 16 LittleEndian>").expect(""),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
}),
},
]
));
}
#[test]
fn test_morphism_path_posint() {
let (mut dict, mut base) = morphism_test_setup();
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap(),
}).solve();
if let Some(path) = path.as_ref() {
print_path(&mut dict, path);
}
assert_eq!(
path,
Some(
vec![
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
m: DummyMorphism(MorphismType {
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
halo: TypeTerm::unit(),
m: DummyMorphism(MorphismType{
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
}),
},
MorphismInstance {
σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
].into_iter().collect(),
halo: dict.parse("ℕ ~ <PosInt 16 BigEndian>").unwrap(),
m: DummyMorphism(MorphismType{
src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
})
}
]
)
);
/*
assert_eq!(
base.find_morphism_path(MorphismType {
src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
}),
Some(
vec![
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
]
)
);
*/
/*
assert_eq!(
base.find_morphism_with_subtyping(
&MorphismType {
src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}
),
Some((
DummyMorphism(MorphismType{
src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
}),
dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian>").unwrap(),
vec![
(dict.get_typeid(&"Radix".into()).unwrap(),
dict.parse("10").unwrap())
].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
))
);
*/
}
use std::collections::HashMap;
#[test]
fn test_morphism_path_listedit()
{
let mut dict = BimapTypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("List").expect("") ] );
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("Char").unwrap(),
dst_type: dict.parse("Char ~ EditTree").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<List~Vec Char>").unwrap(),
dst_type: dict.parse("<List Char>").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<List Char>").unwrap(),
dst_type: dict.parse("<List Char~ReprTree>").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<List ReprTree>").unwrap(),
dst_type: dict.parse("<List~Vec ReprTree>").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
})
);
base.add_morphism(
DummyMorphism(MorphismType{
src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
})
);
let path = ShortestPathProblem::new(&base, MorphismType {
src_type: dict.parse("<Seq~List~Vec <Digit 10>~Char>").unwrap(),
dst_type: dict.parse("<Seq~List <Digit 10>~Char> ~ EditTree").unwrap(),
}).solve();
if let Some(path) = path.as_ref() {
print_path(&mut dict, path);
}
assert_eq!(
path,
Some(vec![
MorphismInstance {
m: DummyMorphism(MorphismType{
src_type: dict.parse("<List~Vec Char>").unwrap(),
dst_type: dict.parse("<List Char>").unwrap()
}),
halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
σ: HashMap::new()
},
MorphismInstance {
m: DummyMorphism(MorphismType{
src_type: dict.parse("<List Char>").unwrap(),
dst_type: dict.parse("<List Char~ReprTree>").unwrap()
}),
halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
σ: HashMap::new()
},
MorphismInstance {
m: DummyMorphism(MorphismType{
src_type: dict.parse("<List ReprTree>").unwrap(),
dst_type: dict.parse("<List~Vec ReprTree>").unwrap()
}),
halo: dict.parse("<Seq~List <Digit 10>~Char>").unwrap(),
σ: HashMap::new()
},
MorphismInstance {
m: DummyMorphism(MorphismType{
src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
}),
halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
σ: HashMap::new()
},
])
);
}

80
src/test/parser.rs
View file

@ -7,7 +7,7 @@ use {
#[test] #[test]
fn test_parser_id() { fn test_parser_id() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
dict.add_varname("T".into()); dict.add_varname("T".into());
@ -26,7 +26,7 @@ fn test_parser_id() {
fn test_parser_num() { fn test_parser_num() {
assert_eq!( assert_eq!(
Ok(TypeTerm::Num(1234)), Ok(TypeTerm::Num(1234)),
BimapTypeDict::new().parse("1234") TypeDict::new().parse("1234")
); );
} }
@ -34,21 +34,21 @@ fn test_parser_num() {
fn test_parser_char() { fn test_parser_char() {
assert_eq!( assert_eq!(
Ok(TypeTerm::Char('x')), Ok(TypeTerm::Char('x')),
BimapTypeDict::new().parse("'x'") TypeDict::new().parse("'x'")
); );
} }
#[test] #[test]
fn test_parser_app() { fn test_parser_app() {
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(1)),
])) ]))
); );
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(1)),
@ -60,7 +60,7 @@ fn test_parser_app() {
#[test] #[test]
fn test_parser_unexpected_close() { fn test_parser_unexpected_close() {
assert_eq!( assert_eq!(
BimapTypeDict::new().parse(">"), TypeDict::new().parse(">"),
Err(ParseError::UnexpectedClose) Err(ParseError::UnexpectedClose)
); );
} }
@ -68,7 +68,7 @@ fn test_parser_unexpected_close() {
#[test] #[test]
fn test_parser_unexpected_token() { fn test_parser_unexpected_token() {
assert_eq!( assert_eq!(
BimapTypeDict::new().parse("A B"), TypeDict::new().parse("A B"),
Err(ParseError::UnexpectedToken) Err(ParseError::UnexpectedToken)
); );
} }
@ -76,14 +76,14 @@ fn test_parser_unexpected_token() {
#[test] #[test]
fn test_parser_ladder() { fn test_parser_ladder() {
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(1)),
])) ]))
); );
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::TypeID(TypeID::Fun(1)), TypeTerm::TypeID(TypeID::Fun(1)),
@ -95,7 +95,7 @@ fn test_parser_ladder() {
#[test] #[test]
fn test_parser_ladder_outside() { fn test_parser_ladder_outside() {
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
@ -109,7 +109,7 @@ fn test_parser_ladder_outside() {
#[test] #[test]
fn test_parser_ladder_inside() { fn test_parser_ladder_inside() {
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
@ -123,7 +123,7 @@ fn test_parser_ladder_inside() {
#[test] #[test]
fn test_parser_ladder_between() { fn test_parser_ladder_between() {
assert_eq!( assert_eq!(
BimapTypeDict::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(0)),
TypeTerm::Ladder(vec![ TypeTerm::Ladder(vec![
@ -141,9 +141,9 @@ fn test_parser_ladder_between() {
#[test] #[test]
fn test_parser_ladder_large() { fn test_parser_ladder_large() {
assert_eq!( assert_eq!(
BimapTypeDict::new().parse( TypeDict::new().parse(
"<Seq Date "<Seq Date
~<TimeSince UnixEpoch> ~<TimeSince UnixEpoch>
~<Duration Seconds> ~<Duration Seconds>
~ℕ ~ℕ
~<PosInt 10 BigEndian> ~<PosInt 10 BigEndian>
@ -203,3 +203,55 @@ fn test_parser_ladder_large() {
) )
); );
} }
macro_rules! lt_tokenize {
($symbol:ident) => {
crate::lexer::LadderTypeToken::Symbol( "$symbol".into() )
}
(< $rest::tt) => {
crate::lexer::LadderTypeToken::Open,
lt_tokenize!($rest)
}
(> $rest::tt) => {
crate::lexer::LadderTypeToken::Close,
lt_tokenize!($rest)
}
(~ $rest::tt) => {
crate::lexer::LadderTypeToken::Ladder,
lt_tokenize!($rest)
}
}
macro_rules! lt_parse {
($dict:ident, $tokens:tt*) => {
$dict.parse_tokens(
vec![
lt_tokenize!($tokens)
].into_iter().peekable()
)
}
}
#[test]
fn test_proc_macro() {
use laddertype_macro::laddertype;
use crate::lexer::LadderTypeToken;
let mut dict = TypeDict::new();
let t1 = dict.parse_tokens(vec![
Ok(crate::lexer::LadderTypeToken::Open),
Ok(crate::lexer::LadderTypeToken::Symbol("Seq".into())),
Ok(crate::lexer::LadderTypeToken::Symbol("Char".into())),
Ok(crate::lexer::LadderTypeToken::Close)
].into_iter().peekable());
let t2 = dict.parse_tokens(vec![
lt_tokenize!{ <Seq Char> }
].into_iter().peekable());
//lt_parse!( dict, <Seq Char> );
assert_eq!(t1, t2);
}

58
src/test/pnf.rs
View file

@ -1,58 +0,0 @@
use crate::{dict::BimapTypeDict, parser::*};
#[test]
fn test_param_normalize() {
let mut dict = BimapTypeDict::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~Y B>").expect("parse error"),
dict.parse("<A B>~<Y B>").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("<A~X B~C D~E>").expect("parse error"),
dict.parse("<A B D>~<A B~C E>~<X 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("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~x86.UInt8>").expect("parse error").param_normalize(),
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
);
assert_eq!(
dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> x86.UInt8>").expect("parse error").param_normalize(),
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
);
assert_eq!(
dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
dict.parse("<A <B C> F H H>
~<A <B D> F H H>
~<A~Y <B E> F H H>").expect("parse errror")
.param_normalize(),
);
}

10
src/test/substitution.rs
View file

@ -1,14 +1,14 @@
use { use {
crate::{dict::*, term::*, parser::*, unparser::*, substitution::*}, crate::{dict::*, term::*},
std::iter::FromIterator, std::iter::FromIterator
}; };
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test] #[test]
fn test_subst() { fn test_subst() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
let mut σ = std::collections::HashMap::new(); let mut σ = std::collections::HashMap::new();
@ -24,7 +24,9 @@ fn test_subst() {
assert_eq!( assert_eq!(
dict.parse("<Seq T~U>").unwrap().apply_subst(&σ).clone(), dict.parse("<Seq T~U>").unwrap()
.apply_substitution(&|typid|{ σ.get(typid).cloned() }).clone(),
dict.parse("<Seq ℕ~<Seq Char>>").unwrap() dict.parse("<Seq ℕ~<Seq Char>>").unwrap()
); );
} }

7
src/test/subtype.rs
View file

@ -1,8 +1,8 @@
use crate::{dict::BimapTypeDict, parser::*, unparser::*}; use crate::dict::TypeDict;
#[test] #[test]
fn test_semantic_subtype() { fn test_semantic_subtype() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert_eq!( assert_eq!(
dict.parse("A~B~C").expect("parse error") dict.parse("A~B~C").expect("parse error")
@ -31,7 +31,7 @@ fn test_semantic_subtype() {
#[test] #[test]
fn test_syntactic_subtype() { fn test_syntactic_subtype() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
assert_eq!( assert_eq!(
dict.parse("A~B~C").expect("parse error") dict.parse("A~B~C").expect("parse error")
@ -94,3 +94,4 @@ fn test_syntactic_subtype() {
Ok(4) Ok(4)
); );
} }

286
src/test/unification.rs
View file

@ -1,13 +1,13 @@
use { use {
crate::{dict::*, parser::*, unparser::*, term::*, unification::*}, crate::{dict::*, term::*, unification::*},
std::iter::FromIterator std::iter::FromIterator
}; };
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) { fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
dict.add_varname(String::from("T")); dict.add_varname(String::from("T"));
dict.add_varname(String::from("U")); dict.add_varname(String::from("U"));
dict.add_varname(String::from("V")); dict.add_varname(String::from("V"));
@ -23,8 +23,8 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
let σ = σ.unwrap(); let σ = σ.unwrap();
assert_eq!( assert_eq!(
t1.apply_subst(&σ), t1.apply_substitution(&|v| σ.get(v).cloned()),
t2.apply_subst(&σ) t2.apply_substitution(&|v| σ.get(v).cloned())
); );
} else { } else {
assert!(! σ.is_ok()); assert!(! σ.is_ok());
@ -33,7 +33,7 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
#[test] #[test]
fn test_unification_error() { fn test_unification_error() {
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
dict.add_varname(String::from("T")); dict.add_varname(String::from("T"));
assert_eq!( assert_eq!(
@ -61,19 +61,6 @@ fn test_unification_error() {
t2: dict.parse("B").unwrap() t2: dict.parse("B").unwrap()
}) })
); );
assert_eq!(
crate::unify(
&dict.parse("T").unwrap(),
&dict.parse("<Seq T>").unwrap()
),
Err(UnificationError {
addr: vec![],
t1: dict.parse("T").unwrap(),
t2: dict.parse("<Seq T>").unwrap()
})
);
} }
#[test] #[test]
@ -89,7 +76,7 @@ fn test_unification() {
true true
); );
let mut dict = BimapTypeDict::new(); let mut dict = TypeDict::new();
dict.add_varname(String::from("T")); dict.add_varname(String::from("T"));
dict.add_varname(String::from("U")); dict.add_varname(String::from("U"));
@ -97,12 +84,11 @@ fn test_unification() {
dict.add_varname(String::from("W")); dict.add_varname(String::from("W"));
assert_eq!( assert_eq!(
UnificationProblem::new_eq(vec![ UnificationProblem::new(vec![
(dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()), (dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
(dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()), (dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
]).solve(), ]).solve(),
Ok(( Ok(
vec![],
vec![ vec![
// T // T
(TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()), (TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
@ -110,16 +96,15 @@ fn test_unification() {
// U // U
(TypeID::Var(1), dict.parse("<Seq Char>").unwrap()) (TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
].into_iter().collect() ].into_iter().collect()
)) )
); );
assert_eq!( assert_eq!(
UnificationProblem::new_eq(vec![ UnificationProblem::new(vec![
(dict.parse("<Seq T>").unwrap(), dict.parse("<Seq W~<Seq Char>>").unwrap()), (dict.parse("<Seq T>").unwrap(), dict.parse("<Seq W~<Seq Char>>").unwrap()),
(dict.parse("<Seq ℕ>").unwrap(), dict.parse("<Seq W>").unwrap()), (dict.parse("<Seq ℕ>").unwrap(), dict.parse("<Seq W>").unwrap()),
]).solve(), ]).solve(),
Ok(( Ok(
vec![],
vec![ vec![
// W // W
(TypeID::Var(3), dict.parse("ℕ").unwrap()), (TypeID::Var(3), dict.parse("ℕ").unwrap()),
@ -127,254 +112,7 @@ fn test_unification() {
// T // T
(TypeID::Var(0), dict.parse("ℕ~<Seq Char>").unwrap()) (TypeID::Var(0), dict.parse("ℕ~<Seq Char>").unwrap())
].into_iter().collect() ].into_iter().collect()
)) )
); );
} }
#[test]
fn test_subtype_unification1() {
let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("A ~ B").unwrap(),
dict.parse("B").unwrap()),
]).solve(),
Ok((
vec![ dict.parse("A").unwrap() ],
vec![].into_iter().collect()
))
);
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("A ~ B ~ C ~ D").unwrap(),
dict.parse("C ~ D").unwrap()),
]).solve(),
Ok((
vec![ dict.parse("A ~ B").unwrap() ],
vec![].into_iter().collect()
))
);
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("A ~ B ~ C ~ D").unwrap(),
dict.parse("T ~ D").unwrap()),
]).solve(),
Ok((
vec![ TypeTerm::unit() ],
vec![
(dict.get_typeid(&"T".into()).unwrap(), dict.parse("A ~ B ~ C").unwrap())
].into_iter().collect()
))
);
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("A ~ B ~ C ~ D").unwrap(),
dict.parse("B ~ T ~ D").unwrap()),
]).solve(),
Ok((
vec![ dict.parse("A").unwrap() ],
vec![
(dict.get_typeid(&"T".into()).unwrap(), dict.parse("C").unwrap())
].into_iter().collect()
))
);
}
#[test]
fn test_subtype_unification2() {
let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("U"));
dict.add_varname(String::from("V"));
dict.add_varname(String::from("W"));
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(),
dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()),
]).solve(),
Ok((
vec![
dict.parse("<Seq <Digit 10>>").unwrap()
],
vec![
// T
(TypeID::Var(0), dict.parse("<LengthPrefix x86.UInt64>").unwrap())
].into_iter().collect()
))
);
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
(dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
]).solve(),
Ok((
vec![
TypeTerm::unit(),
TypeTerm::unit(),
],
vec![
// T
(TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
// U
(TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
].into_iter().collect()
))
);
assert_eq!(
UnificationProblem::new_sub(vec![
(dict.parse("<Seq T>").unwrap(),
dict.parse("<Seq W~<Seq Char>>").unwrap()),
(dict.parse("<Seq~<LengthPrefix x86.UInt64> ℕ~<PosInt 10 BigEndian>>").unwrap(),
dict.parse("<<LengthPrefix x86.UInt64> W>").unwrap()),
]).solve(),
Ok((
vec![
TypeTerm::unit(),
dict.parse("<Seq ℕ>").unwrap(),
],
vec![
// W
(TypeID::Var(3), dict.parse("ℕ~<PosInt 10 BigEndian>").unwrap()),
// T
(TypeID::Var(0), dict.parse("ℕ~<PosInt 10 BigEndian>~<Seq Char>").unwrap())
].into_iter().collect()
))
);
assert_eq!(
subtype_unify(
&dict.parse("<Seq~List~Vec <Digit 16>~Char>").expect(""),
&dict.parse("<List~Vec Char>").expect("")
),
Ok((
dict.parse("<Seq~List <Digit 16>>").expect(""),
vec![].into_iter().collect()
))
);
assert_eq!(
subtype_unify(
&dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List~Vec <Digit 16>~Char>").expect(""),
&dict.parse("<List~Vec Char>").expect("")
),
Ok((
dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>>").expect(""),
vec![].into_iter().collect()
))
);
}
#[test]
fn test_trait_not_subtype() {
let mut dict = BimapTypeDict::new();
assert_eq!(
subtype_unify(
&dict.parse("A ~ B").expect(""),
&dict.parse("A ~ B ~ C").expect("")
),
Err(UnificationError {
addr: vec![1],
t1: dict.parse("B").expect(""),
t2: dict.parse("C").expect("")
})
);
assert_eq!(
subtype_unify(
&dict.parse("<Seq~List~Vec <Digit 10>~Char>").expect(""),
&dict.parse("<Seq~List~Vec Char~ReprTree>").expect("")
),
Err(UnificationError {
addr: vec![1,1],
t1: dict.parse("Char").expect(""),
t2: dict.parse("ReprTree").expect("")
})
);
}
#[test]
fn test_reprtree_list_subtype() {
let mut dict = BimapTypeDict::new();
dict.add_varname("Item".into());
assert_eq!(
subtype_unify(
&dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect(""),
&dict.parse("<List~Vec Item~ReprTree>").expect("")
),
Ok((
TypeTerm::unit(),
vec![
(dict.get_typeid(&"Item".into()).unwrap(), dict.parse("<Digit 10>~Char").unwrap())
].into_iter().collect()
))
);
}
#[test]
pub fn test_subtype_delim() {
let mut dict = BimapTypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("Delim"));
assert_eq!(
UnificationProblem::new_sub(vec![
(
//given type
dict.parse("
< Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
~ < ValueSep ':' Char~Ascii~UInt8 >
~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
").expect(""),
//expected type
dict.parse("
< Seq <Seq T> >
~ < ValueSep Delim T >
~ < Seq~<LengthPrefix UInt64> T >
").expect("")
),
// subtype bounds
(
dict.parse("T").expect(""),
dict.parse("UInt8").expect("")
),
/* todo
(
dict.parse("<TypeOf Delim>").expect(""),
dict.parse("T").expect("")
),
*/
]).solve(),
Ok((
// halo types for each rhs in the sub-equations
vec![
dict.parse("<Seq <Seq <Digit 10>>>").expect(""),
dict.parse("Char~Ascii").expect(""),
],
// variable substitution
vec![
(dict.get_typeid(&"T".into()).unwrap(), dict.parse("Char~Ascii~UInt8").expect("")),
(dict.get_typeid(&"Delim".into()).unwrap(), TypeTerm::Char(':')),
].into_iter().collect()
))
);
}

513
src/unification.rs
View file

@ -1,5 +1,6 @@
use { use {
crate::{dict::*, term::*}, std::{collections::HashMap} std::collections::HashMap,
crate::{term::*, dict::*}
}; };
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@ -11,502 +12,79 @@ pub struct UnificationError {
pub t2: TypeTerm pub t2: TypeTerm
} }
#[derive(Clone, Debug)]
pub struct UnificationPair {
addr: Vec<usize>,
halo: TypeTerm,
lhs: TypeTerm,
rhs: TypeTerm,
}
#[derive(Debug)]
pub struct UnificationProblem { pub struct UnificationProblem {
σ: HashMap<TypeID, TypeTerm>, eqs: Vec<(TypeTerm, TypeTerm, Vec<usize>)>,
upper_bounds: HashMap< u64, TypeTerm >, σ: HashMap<TypeID, TypeTerm>
lower_bounds: HashMap< u64, TypeTerm >,
equal_pairs: Vec<UnificationPair>,
subtype_pairs: Vec<UnificationPair>,
trait_pairs: Vec<UnificationPair>
} }
impl UnificationProblem { impl UnificationProblem {
pub fn new( pub fn new(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
equal_pairs: Vec<(TypeTerm, TypeTerm)>,
subtype_pairs: Vec<(TypeTerm, TypeTerm)>,
trait_pairs: Vec<(TypeTerm, TypeTerm)>
) -> Self {
UnificationProblem { UnificationProblem {
σ: HashMap::new(), eqs: eqs.iter().map(|(lhs,rhs)| (lhs.clone(),rhs.clone(),vec![])).collect(),
σ: HashMap::new()
equal_pairs: equal_pairs.into_iter().map(|(lhs,rhs)|
UnificationPair{
lhs,rhs,
halo: TypeTerm::unit(),
addr: Vec::new()
}).collect(),
subtype_pairs: subtype_pairs.into_iter().map(|(lhs,rhs)|
UnificationPair{
lhs,rhs,
halo: TypeTerm::unit(),
addr: Vec::new()
}).collect(),
trait_pairs: trait_pairs.into_iter().map(|(lhs,rhs)|
UnificationPair{
lhs,rhs,
halo: TypeTerm::unit(),
addr: Vec::new()
}).collect(),
upper_bounds: HashMap::new(),
lower_bounds: HashMap::new(),
} }
} }
pub fn new_eq(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self { pub fn eval_equation(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<(), UnificationError> {
UnificationProblem::new( eqs, Vec::new(), Vec::new() ) match (lhs.clone(), rhs.clone()) {
}
pub fn new_sub(subs: Vec<(TypeTerm, TypeTerm)>) -> Self {
UnificationProblem::new( Vec::new(), subs, Vec::new() )
}
/// update all values in substitution
pub fn reapply_subst(&mut self) {
let mut new_σ = HashMap::new();
for (v, tt) in self.σ.iter() {
let mut tt = tt.clone().normalize();
tt.apply_subst(&self.σ);
tt = tt.normalize();
//eprintln!("update σ : {:?} --> {:?}", v, tt);
new_σ.insert(v.clone(), tt);
}
self.σ = new_σ;
}
pub fn eval_equation(&mut self, unification_pair: UnificationPair) -> Result<(), UnificationError> {
match (&unification_pair.lhs, &unification_pair.rhs) {
(TypeTerm::TypeID(TypeID::Var(varid)), t) | (TypeTerm::TypeID(TypeID::Var(varid)), t) |
(t, TypeTerm::TypeID(TypeID::Var(varid))) => { (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
if ! t.contains_var( *varid ) { self.σ.insert(TypeID::Var(varid), t.clone());
self.σ.insert(TypeID::Var(*varid), t.clone());
self.reapply_subst(); // update all values in substitution
Ok(()) let mut new_σ = HashMap::new();
} else if t == &TypeTerm::TypeID(TypeID::Var(*varid)) { for (v, tt) in self.σ.iter() {
Ok(()) let mut tt = tt.clone();
} else { tt.apply_substitution(&|v| self.σ.get(v).cloned());
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() }) new_σ.insert(v.clone(), tt);
} }
self.σ = new_σ;
Ok(())
} }
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => { (TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
if a1 == a2 { Ok(()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) } if a1 == a2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
} }
(TypeTerm::Num(n1), TypeTerm::Num(n2)) => { (TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
if n1 == n2 { Ok(()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) } if n1 == n2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
} }
(TypeTerm::Char(c1), TypeTerm::Char(c2)) => { (TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
if c1 == c2 { Ok(()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) } if c1 == c2 { Ok(()) } else { Err(UnificationError{ addr, t1: lhs, t2: rhs}) }
} }
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) | (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
(TypeTerm::App(a1), TypeTerm::App(a2)) => { (TypeTerm::App(a1), TypeTerm::App(a2)) => {
if a1.len() == a2.len() { if a1.len() == a2.len() {
for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() { for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
let mut new_addr = unification_pair.addr.clone(); let mut new_addr = addr.clone();
new_addr.push(i); new_addr.push(i);
self.equal_pairs.push( self.eqs.push((x, y, new_addr));
UnificationPair {
lhs: x,
rhs: y,
halo: TypeTerm::unit(),
addr: new_addr
});
} }
Ok(()) Ok(())
} else { } else {
Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) Err(UnificationError{ addr, t1: lhs, t2: rhs })
} }
} }
_ => Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) (TypeTerm::Ladder(l1), TypeTerm::Ladder(l2)) => {
Err(UnificationError{ addr, t1: lhs, t2: rhs })
}
_ => Err(UnificationError{ addr, t1: lhs, t2: rhs})
} }
} }
pub fn solve(mut self) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
while self.eqs.len() > 0 {
pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> { while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
lhs.apply_substitution(&|v| self.σ.get(v).cloned());
if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) { rhs.apply_substitution(&|v| self.σ.get(v).cloned());
return Ok(()); self.eval_equation(lhs, rhs, addr)?;
}
if new_lower_bound.contains_var(v) {
// loop
return Err(());
}
if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
// eprintln!("var already exists. check max. type");
if let Ok(halo) = self.eval_subtype(
UnificationPair {
lhs: lower_bound.clone(),
rhs: new_lower_bound.clone(),
halo: TypeTerm::unit(),
addr: vec![]
}
) {
// eprintln!("found more general lower bound");
// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
// generalize variable type to supertype
self.lower_bounds.insert(v, new_lower_bound);
Ok(())
} else if let Ok(halo) = self.eval_subtype(
UnificationPair{
lhs: new_lower_bound,
rhs: lower_bound,
halo: TypeTerm::unit(),
addr: vec![]
}
) {
// eprintln!("OK, is already larger type");
Ok(())
} else {
// eprintln!("violated subtype restriction");
Err(())
} }
} else {
// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
self.lower_bounds.insert(v, new_lower_bound);
Ok(())
}
}
pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> {
if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) {
return Ok(());
} }
if new_upper_bound.contains_var(v) { Ok(self.σ)
// loop
return Err(());
}
if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
if let Ok(_halo) = self.eval_subtype(
UnificationPair {
lhs: new_upper_bound.clone(),
rhs: upper_bound,
halo: TypeTerm::unit(),
addr: vec![]
}
) {
// found a lower upper bound
self.upper_bounds.insert(v, new_upper_bound);
Ok(())
} else {
Err(())
}
} else {
self.upper_bounds.insert(v, new_upper_bound);
Ok(())
}
}
pub fn eval_subtype(&mut self, unification_pair: UnificationPair) -> Result<
// ok: halo type
TypeTerm,
// error
UnificationError
> {
// eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
match (unification_pair.lhs.clone(), unification_pair.rhs.clone()) {
/*
Variables
*/
(t, TypeTerm::TypeID(TypeID::Var(v))) => {
//eprintln!("t <= variable");
if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
Ok(TypeTerm::unit())
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
}
}
(TypeTerm::TypeID(TypeID::Var(v)), t) => {
//eprintln!("variable <= t");
if self.add_upper_subtype_bound(v, t.clone()).is_ok() {
Ok(TypeTerm::unit())
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
}
}
/*
Atoms
*/
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
if a1 == a2 { Ok(TypeTerm::unit()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs}) }
}
(TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
if n1 == n2 { Ok(TypeTerm::unit()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
}
(TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
if c1 == c2 { Ok(TypeTerm::unit()) } else { Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
}
/*
Ladders
*/
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
let mut l1_iter = a1.into_iter().enumerate().rev();
let mut l2_iter = a2.into_iter().rev();
let mut halo_ladder = Vec::new();
while let Some(rhs) = l2_iter.next() {
//eprintln!("take rhs = {:?}", rhs);
if let Some((i, lhs)) = l1_iter.next() {
//eprintln!("take lhs ({}) = {:?}", i, lhs);
let mut addr = unification_pair.addr.clone();
addr.push(i);
//eprintln!("addr = {:?}", addr);
match (lhs.clone(), rhs.clone()) {
(t, TypeTerm::TypeID(TypeID::Var(v))) => {
if self.add_upper_subtype_bound(v,t.clone()).is_ok() {
let mut new_upper_bound_ladder = vec![ t ];
if let Some(next_rhs) = l2_iter.next() {
// TODO
} else {
// take everything
while let Some((i,t)) = l1_iter.next() {
new_upper_bound_ladder.push(t);
}
}
new_upper_bound_ladder.reverse();
if self.add_upper_subtype_bound(v, TypeTerm::Ladder(new_upper_bound_ladder)).is_ok() {
// ok
} else {
return Err(UnificationError {
addr,
t1: lhs,
t2: rhs
});
}
} else {
return Err(UnificationError {
addr,
t1: lhs,
t2: rhs
});
}
}
(lhs, rhs) => {
if let Ok(ψ) = self.eval_subtype(
UnificationPair {
lhs: lhs.clone(), rhs: rhs.clone(),
addr:addr.clone(), halo: TypeTerm::unit()
}
) {
// ok.
//eprintln!("rungs are subtypes. continue");
halo_ladder.push(ψ);
} else {
return Err(UnificationError {
addr,
t1: lhs,
t2: rhs
});
}
}
}
} else {
// not a subtype,
return Err(UnificationError {
addr: vec![],
t1: unification_pair.lhs,
t2: unification_pair.rhs
});
}
}
//eprintln!("left ladder fully consumed");
for (i,t) in l1_iter {
halo_ladder.push(t);
}
halo_ladder.reverse();
Ok(TypeTerm::Ladder(halo_ladder).strip().param_normalize())
},
(t, TypeTerm::Ladder(a1)) => {
Err(UnificationError{ addr: unification_pair.addr, t1: t, t2: TypeTerm::Ladder(a1) })
}
(TypeTerm::Ladder(mut a1), t) => {
let mut new_addr = unification_pair.addr.clone();
new_addr.push( a1.len() -1 );
if let Ok(halo) = self.eval_subtype(
UnificationPair {
lhs: a1.pop().unwrap(),
rhs: t.clone(),
halo: TypeTerm::unit(),
addr: new_addr
}
) {
a1.push(halo);
if a1.len() == 1 {
Ok(a1.pop().unwrap())
} else {
Ok(TypeTerm::Ladder(a1))
}
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::Ladder(a1), t2: t })
}
}
/*
Application
*/
(TypeTerm::App(a1), TypeTerm::App(a2)) => {
if a1.len() == a2.len() {
let mut halo_args = Vec::new();
let mut n_halos_required = 0;
for (i, (mut x, mut y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
let mut new_addr = unification_pair.addr.clone();
new_addr.push(i);
x = x.strip();
// eprintln!("before strip: {:?}", y);
y = y.strip();
// eprintln!("after strip: {:?}", y);
// eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
match self.eval_subtype(
UnificationPair {
lhs: x.clone(),
rhs: y.clone(),
halo: TypeTerm::unit(),
addr: new_addr,
}
) {
Ok(halo) => {
if halo == TypeTerm::unit() {
let mut y = y.clone();
y.apply_subst(&self.σ);
y = y.strip();
let mut top = y.get_lnf_vec().first().unwrap().clone();
halo_args.push(top.clone());
//eprintln!("add top {:?}", top);
} else {
//eprintln!("add halo {:?}", halo);
if n_halos_required > 0 {
let x = &mut halo_args[n_halos_required-1];
if let TypeTerm::Ladder(argrs) = x {
let mut a = a2[n_halos_required-1].clone();
a.apply_subst(&self.σ);
a = a.get_lnf_vec().first().unwrap().clone();
argrs.push(a);
} else {
*x = TypeTerm::Ladder(vec![
x.clone(),
a2[n_halos_required-1].clone().get_lnf_vec().first().unwrap().clone()
]);
x.apply_subst(&self.σ);
}
}
halo_args.push(halo);
n_halos_required += 1;
}
},
Err(err) => { return Err(err); }
}
}
if n_halos_required > 0 {
//eprintln!("halo args : {:?}", halo_args);
Ok(TypeTerm::App(halo_args))
} else {
Ok(TypeTerm::unit())
}
} else {
Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
}
}
_ => Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
}
}
pub fn solve(mut self) -> Result<(Vec<TypeTerm>, HashMap<TypeID, TypeTerm>), UnificationError> {
// solve equations
while let Some( mut equal_pair ) = self.equal_pairs.pop() {
equal_pair.lhs.apply_subst(&self.σ);
equal_pair.rhs.apply_subst(&self.σ);
self.eval_equation(equal_pair)?;
}
// solve subtypes
// eprintln!("------ SOLVE SUBTYPES ---- ");
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs.apply_subst(&self.σ);
subtype_pair.rhs.apply_subst(&self.σ);
let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
}
// add variables from subtype bounds
for (var_id, t) in self.upper_bounds.iter() {
// eprintln!("VAR {} upper bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
for (var_id, t) in self.lower_bounds.iter() {
// eprintln!("VAR {} lower bound {:?}", var_id, t);
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
}
self.reapply_subst();
// eprintln!("------ MAKE HALOS -----");
let mut halo_types = Vec::new();
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone().strip();
subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone().strip();
let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
halo_types.push(halo);
}
// solve traits
while let Some( trait_pair ) = self.trait_pairs.pop() {
unimplemented!();
}
Ok((halo_types, self.σ))
} }
} }
@ -514,16 +92,9 @@ pub fn unify(
t1: &TypeTerm, t1: &TypeTerm,
t2: &TypeTerm t2: &TypeTerm
) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> { ) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
let unification = UnificationProblem::new_eq(vec![ (t1.clone(), t2.clone()) ]); let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
Ok(unification.solve()?.1) unification.solve()
}
pub fn subtype_unify(
t1: &TypeTerm,
t2: &TypeTerm
) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
let unification = UnificationProblem::new_sub(vec![ (t1.clone(), t2.clone()) ]);
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
} }
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

8
src/unparser.rs
View file

@ -2,12 +2,8 @@ use crate::{dict::*, term::*};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\ //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait UnparseLadderType { impl TypeDict {
fn unparse(&self, t: &TypeTerm) -> String; pub fn unparse(&self, t: &TypeTerm) -> String {
}
impl<T: TypeDict> UnparseLadderType for T {
fn unparse(&self, t: &TypeTerm) -> String {
match t { match t {
TypeTerm::TypeID(id) => self.get_typename(id).unwrap(), TypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
TypeTerm::Num(n) => format!("{}", n), TypeTerm::Num(n) => format!("{}", n),