diff --git a/.github/workflows/cargo-test.yml b/.github/workflows/cargo-test.yml
index 8328dcf..a69c7e3 100644
--- a/.github/workflows/cargo-test.yml
+++ b/.github/workflows/cargo-test.yml
@@ -2,20 +2,21 @@ name: Rust
on:
push:
- branches: ["dev"]
+ branches: [ "dev" ]
pull_request:
- branches: ["dev"]
+ branches: [ "dev" ]
env:
CARGO_TERM_COLOR: always
jobs:
build:
+
runs-on: ubuntu-latest
steps:
- - uses: actions/checkout@v3
- - name: Build
- run: cargo build --verbose --features pretty
- - name: Run tests
- run: cargo test --verbose --features pretty
+ - uses: actions/checkout@v3
+ - name: Build
+ run: cargo build --verbose
+ - name: Run tests
+ run: cargo test --verbose
diff --git a/README.md b/README.md
index fa7cd86..d4dc395 100644
--- a/README.md
+++ b/README.md
@@ -5,8 +5,6 @@ Rust Implementation of Ladder-Types (parsing, unification, rewriting, etc)
## Ladder Types
-### Motivation
-
In order to implement complex datastructures and algorithms, usually
many layers of abstraction are built ontop of each other.
Consequently higher-level data types are encoded into lower-level data
@@ -59,48 +57,6 @@ this:
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
```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
[GPLv3](COPYING)
diff --git a/src/bimap.rs b/src/bimap.rs
index 9d0a96c..9ea311a 100644
--- a/src/bimap.rs
+++ b/src/bimap.rs
@@ -2,7 +2,6 @@ use std::{collections::HashMap, hash::Hash};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-#[derive(Debug)]
pub struct Bimap<V: Eq + Hash, Λ: Eq + Hash> {
pub mλ: HashMap<V, Λ>,
pub my: HashMap<Λ, V>,
diff --git a/src/dict.rs b/src/dict.rs
index e5cb464..a28573c 100644
--- a/src/dict.rs
+++ b/src/dict.rs
@@ -1,4 +1,7 @@
-use crate::bimap::Bimap;
+use crate::{
+ bimap::Bimap,
+ sugar::SUGARID_LIMIT
+};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -8,36 +11,9 @@ pub enum TypeID {
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 BimapTypeDict {
+pub struct TypeDict {
typenames: Bimap<String, TypeID>,
type_lit_counter: u64,
type_var_counter: u64,
@@ -45,65 +21,53 @@ pub struct BimapTypeDict {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl BimapTypeDict {
+impl TypeDict {
pub fn new() -> Self {
- BimapTypeDict {
+ let mut dict = TypeDict {
typenames: Bimap::new(),
type_lit_counter: 0,
type_var_counter: 0,
- }
- }
-}
+ };
-impl TypeDict for BimapTypeDict {
- fn insert(&mut self, name: String, id: TypeID) {
- self.typenames.insert(name, id);
+ dict.add_typename("Seq".into());
+ dict.add_typename("Enum".into());
+ dict.add_typename("Struct".into());
+
+ assert_eq!( dict.type_lit_counter, SUGARID_LIMIT );
+
+ dict
}
- fn add_varname(&mut self, tn: String) -> TypeID {
+ pub fn add_varname(&mut self, tn: String) -> TypeID {
let tyid = TypeID::Var(self.type_var_counter);
self.type_var_counter += 1;
- self.insert(tn, tyid.clone());
+ self.typenames.insert(tn, tyid.clone());
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);
self.type_lit_counter += 1;
- self.insert(tn, tyid.clone());
+ self.typenames.insert(tn, tyid.clone());
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()
}
- fn get_typeid(&self, tn: &String) -> Option<TypeID> {
+ pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
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)
+ pub fn get_varname(&self, var_id: u64) -> Option<String> {
+ self.typenames.my.get(&TypeID::Var(var_id)).cloned()
}
}
diff --git a/src/lexer.rs b/src/lexer.rs
index 8c56a0d..62b8efe 100644
--- a/src/lexer.rs
+++ b/src/lexer.rs
@@ -6,9 +6,9 @@ pub enum LadderTypeToken {
Symbol( String ),
Char( char ),
Num( i64 ),
- Open,
- Close,
- Ladder,
+ Open, OpenSeq, OpenStruct,
+ Close, CloseSeq, CloseStruct,
+ Ladder, Enum
}
#[derive(PartialEq, Eq, Clone, Debug)]
@@ -75,6 +75,11 @@ where It: Iterator<Item = char>
match c {
'<' => { self.chars.next(); return Some(Ok(LadderTypeToken::Open)); },
'>' => { 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(); state = LexerState::Char(None); },
c => {
diff --git a/src/lib.rs b/src/lib.rs
index 98cb5a2..a23069f 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -2,20 +2,15 @@
pub mod bimap;
pub mod dict;
pub mod term;
-pub mod substitution;
-
pub mod lexer;
pub mod parser;
pub mod unparser;
pub mod sugar;
pub mod curry;
+pub mod sugar;
pub mod lnf;
-pub mod pnf;
pub mod subtype;
pub mod unification;
-pub mod morphism;
-pub mod morphism_base;
-pub mod morphism_path;
#[cfg(test)]
mod test;
@@ -26,8 +21,6 @@ mod pretty;
pub use {
dict::*,
term::*,
- substitution::*,
sugar::*,
unification::*,
- morphism::*
};
diff --git a/src/morphism.rs b/src/morphism.rs
deleted file mode 100644
index 06361dc..0000000
--- a/src/morphism.rs
+++ /dev/null
@@ -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()
- }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/morphism_base.rs b/src/morphism_base.rs
deleted file mode 100644
index 91dcba0..0000000
--- a/src/morphism_base.rs
+++ /dev/null
@@ -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
- }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/morphism_path.rs b/src/morphism_path.rs
deleted file mode 100644
index 60f5321..0000000
--- a/src/morphism_path.rs
+++ /dev/null
@@ -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
- }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/parser.rs b/src/parser.rs
index 6160ca6..87ed5c1 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -3,6 +3,7 @@ use {
crate::{
dict::*,
term::*,
+ sugar::*,
lexer::*
}
};
@@ -18,23 +19,10 @@ pub enum ParseError {
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 {
- fn parse(&mut self, s: &str) -> Result<TypeTerm, ParseError> {
+impl TypeDict {
+ pub fn parse(&mut self, s: &str) -> Result<SugaredTypeTerm, ParseError> {
let mut tokens = LadderTypeLexer::from(s.chars()).peekable();
match self.parse_ladder(&mut tokens) {
@@ -49,7 +37,7 @@ 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<LadderTypeLexer<It>>) -> Result<SugaredTypeTerm, ParseError>
where It: Iterator<Item = char>
{
let mut args = Vec::new();
@@ -57,7 +45,11 @@ impl<T: TypeDict> ParseLadderType for T {
match tok {
Ok(LadderTypeToken::Close) => {
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) {
@@ -70,29 +62,59 @@ impl<T: TypeDict> ParseLadderType for T {
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>
{
match tokens.next() {
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::CloseStruct)) => Err(ParseError::UnexpectedToken),
+ Some(Ok(LadderTypeToken::CloseSeq)) => Err(ParseError::UnexpectedToken),
Some(Ok(LadderTypeToken::Ladder)) => Err(ParseError::UnexpectedLadder),
Some(Ok(LadderTypeToken::Symbol(s))) =>
- Ok(TypeTerm::TypeID(
+ Ok(SugaredTypeTerm::TypeID(
if let Some(tyid) = self.get_typeid(&s) {
tyid
} else {
self.add_typename(s)
}
)),
- Some(Ok(LadderTypeToken::Char(c))) => Ok(TypeTerm::Char(c)),
- Some(Ok(LadderTypeToken::Num(n))) => Ok(TypeTerm::Num(n)),
+ Some(Ok(LadderTypeToken::Char(c))) => Ok(SugaredTypeTerm::Char(c)),
+ Some(Ok(LadderTypeToken::Num(n))) => Ok(SugaredTypeTerm::Num(n)),
Some(Err(err)) => Err(ParseError::LexError(err)),
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>
{
let mut rungs = Vec::new();
@@ -128,7 +150,7 @@ impl<T: TypeDict> ParseLadderType for T {
match rungs.len() {
0 => Err(ParseError::UnexpectedEnd),
1 => Ok(rungs[0].clone()),
- _ => Ok(TypeTerm::Ladder(rungs)),
+ _ => Ok(SugaredTypeTerm::Ladder(rungs)),
}
}
}
diff --git a/src/pnf.rs b/src/pnf.rs
deleted file mode 100644
index d3a6b20..0000000
--- a/src/pnf.rs
+++ /dev/null
@@ -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
- }
- }
-}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/pretty.rs b/src/pretty.rs
index 40a7541..1a4aa60 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -1,5 +1,5 @@
use {
- crate::{TypeDict, dict::TypeID},
+ crate::TypeDict,
crate::sugar::SugaredTypeTerm,
tiny_ansi::TinyAnsi
};
@@ -9,26 +9,15 @@ impl SugaredTypeTerm {
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()
- }
- }
+ format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue()
},
SugaredTypeTerm::Num(n) => {
- format!("{}", n).green().bold()
+ format!("{}", n).bright_cyan()
}
SugaredTypeTerm::Char(c) => {
- match c {
- '\0' => format!("'\\0'"),
- '\n' => format!("'\\n'"),
- _ => format!("'{}'", c)
- }
+ format!("'{}'", c)
}
SugaredTypeTerm::Univ(t) => {
@@ -41,7 +30,7 @@ impl SugaredTypeTerm {
SugaredTypeTerm::Spec(args) => {
let mut s = String::new();
- s.push_str(&"<".yellow());
+ s.push_str(&"<".yellow().bold());
for i in 0..args.len() {
let arg = &args[i];
if i > 0 {
@@ -49,7 +38,7 @@ impl SugaredTypeTerm {
}
s.push_str( &arg.pretty(dict,indent+1) );
}
- s.push_str(&">".yellow());
+ s.push_str(&">".yellow().bold());
s
}
@@ -127,7 +116,7 @@ impl SugaredTypeTerm {
s.push('\n');
for x in 0..(indent*indent_width) {
s.push(' ');
- }
+ }
s.push_str(&"--> ".bright_yellow());
} else {
// s.push_str(" ");
@@ -155,3 +144,5 @@ impl SugaredTypeTerm {
}
}
}
+
+
diff --git a/src/substitution.rs b/src/substitution.rs
deleted file mode 100644
index 80de6bf..0000000
--- a/src/substitution.rs
+++ /dev/null
@@ -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
- }
-}
diff --git a/src/sugar.rs b/src/sugar.rs
deleted file mode 100644
index 77c04cb..0000000
--- a/src/sugar.rs
+++ /dev/null
@@ -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())
- }
- }
- }
-}
-
diff --git a/src/term.rs b/src/term.rs
index edbb18d..29c7d27 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -14,7 +14,7 @@ pub enum TypeTerm {
Num(i64),
Char(char),
-
+
/* Complex Terms */
@@ -47,7 +47,7 @@ impl TypeTerm {
*self = TypeTerm::App(vec![
self.clone(),
t.into()
- ])
+ ])
}
}
@@ -79,77 +79,34 @@ impl TypeTerm {
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 {
- TypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
- TypeTerm::App(args) |
- TypeTerm::Ladder(args) => {
- 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)
+ TypeTerm::TypeID(typid) => {
+ if let Some(t) = subst(typid) {
+ *self = t;
}
}
- atom => atom
- }
- }
- pub fn get_interface_type(&self) -> TypeTerm {
- match self {
TypeTerm::Ladder(rungs) => {
- if let Some(top) = rungs.first() {
- top.get_interface_type()
- } else {
- TypeTerm::unit()
+ for r in rungs.iter_mut() {
+ r.apply_substitution(subst);
}
}
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
}
}
diff --git a/src/test/curry.rs b/src/test/curry.rs
index a814ab2..c728a37 100644
--- a/src/test/curry.rs
+++ b/src/test/curry.rs
@@ -1,12 +1,12 @@
use {
- crate::{dict::*, parser::*}
+ crate::{dict::*}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test]
fn test_curry() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
assert_eq!(
dict.parse("<A B C>").unwrap().curry(),
@@ -33,7 +33,7 @@ fn test_curry() {
#[test]
fn test_decurry() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
assert_eq!(
dict.parse("<<A B> C>").unwrap().decurry(),
@@ -47,7 +47,7 @@ fn test_decurry() {
dict.parse("<<<<<<<<<<A B> C> D> E> F> G> H> I> J> K>").unwrap().decurry(),
dict.parse("<A B C D E F G H I J K>").unwrap()
);
-
+
assert_eq!(
dict.parse("<<A~X B> C>").unwrap().decurry(),
dict.parse("<A~X B C>").unwrap()
diff --git a/src/test/lnf.rs b/src/test/lnf.rs
index 4b2a7c2..1c81a55 100644
--- a/src/test/lnf.rs
+++ b/src/test/lnf.rs
@@ -1,8 +1,8 @@
-use crate::{dict::{BimapTypeDict}, parser::*};
+use crate::dict::TypeDict;
#[test]
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("10").expect("parse error").is_flat() );
@@ -17,7 +17,7 @@ fn test_flat() {
#[test]
fn test_normalize() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error").normalize(),
@@ -54,3 +54,4 @@ fn test_normalize() {
);
}
+
diff --git a/src/test/mod.rs b/src/test/mod.rs
index 41f5e71..ea52c7d 100644
--- a/src/test/mod.rs
+++ b/src/test/mod.rs
@@ -2,10 +2,9 @@
pub mod lexer;
pub mod parser;
pub mod curry;
+pub mod sugar;
pub mod lnf;
-pub mod pnf;
pub mod subtype;
pub mod substitution;
pub mod unification;
-pub mod morphism;
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
deleted file mode 100644
index 99747f5..0000000
--- a/src/test/morphism.rs
+++ /dev/null
@@ -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()
- },
- ])
- );
-}
diff --git a/src/test/parser.rs b/src/test/parser.rs
index f650ae3..49deb7c 100644
--- a/src/test/parser.rs
+++ b/src/test/parser.rs
@@ -1,13 +1,13 @@
use {
- crate::{term::*, dict::*, parser::*}
+ crate::{term::*, dict::*, parser::*, sugar::SUGARID_LIMIT}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test]
fn test_parser_id() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
dict.add_varname("T".into());
@@ -17,7 +17,7 @@ fn test_parser_id() {
);
assert_eq!(
- Ok(TypeTerm::TypeID(TypeID::Fun(0))),
+ Ok(TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0))),
dict.parse("A")
);
}
@@ -26,7 +26,7 @@ fn test_parser_id() {
fn test_parser_num() {
assert_eq!(
Ok(TypeTerm::Num(1234)),
- BimapTypeDict::new().parse("1234")
+ TypeDict::new().parse("1234")
);
}
@@ -34,25 +34,25 @@ fn test_parser_num() {
fn test_parser_char() {
assert_eq!(
Ok(TypeTerm::Char('x')),
- BimapTypeDict::new().parse("'x'")
+ TypeDict::new().parse("'x'")
);
}
#[test]
fn test_parser_app() {
assert_eq!(
- BimapTypeDict::new().parse("<A B>"),
+ TypeDict::new().parse("<A B>"),
Ok(TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
]))
);
assert_eq!(
- BimapTypeDict::new().parse("<A B C>"),
+ TypeDict::new().parse("<A B C>"),
Ok(TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(1)),
- TypeTerm::TypeID(TypeID::Fun(2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
]))
);
}
@@ -60,7 +60,7 @@ fn test_parser_app() {
#[test]
fn test_parser_unexpected_close() {
assert_eq!(
- BimapTypeDict::new().parse(">"),
+ TypeDict::new().parse(">"),
Err(ParseError::UnexpectedClose)
);
}
@@ -68,7 +68,7 @@ fn test_parser_unexpected_close() {
#[test]
fn test_parser_unexpected_token() {
assert_eq!(
- BimapTypeDict::new().parse("A B"),
+ TypeDict::new().parse("A B"),
Err(ParseError::UnexpectedToken)
);
}
@@ -76,18 +76,18 @@ fn test_parser_unexpected_token() {
#[test]
fn test_parser_ladder() {
assert_eq!(
- BimapTypeDict::new().parse("A~B"),
+ TypeDict::new().parse("A~B"),
Ok(TypeTerm::Ladder(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
]))
);
assert_eq!(
- BimapTypeDict::new().parse("A~B~C"),
+ TypeDict::new().parse("A~B~C"),
Ok(TypeTerm::Ladder(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(1)),
- TypeTerm::TypeID(TypeID::Fun(2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
]))
);
}
@@ -95,13 +95,13 @@ fn test_parser_ladder() {
#[test]
fn test_parser_ladder_outside() {
assert_eq!(
- BimapTypeDict::new().parse("<A B>~C"),
+ TypeDict::new().parse("<A B>~C"),
Ok(TypeTerm::Ladder(vec![
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
]),
- TypeTerm::TypeID(TypeID::Fun(2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
]))
);
}
@@ -109,39 +109,39 @@ fn test_parser_ladder_outside() {
#[test]
fn test_parser_ladder_inside() {
assert_eq!(
- BimapTypeDict::new().parse("<A B~C>"),
+ TypeDict::new().parse("<A B~C>"),
Ok(TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![
- TypeTerm::TypeID(TypeID::Fun(1)),
- TypeTerm::TypeID(TypeID::Fun(2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
])
]))
- );
+ );
}
#[test]
fn test_parser_ladder_between() {
assert_eq!(
- BimapTypeDict::new().parse("<A B~<C D>>"),
+ TypeDict::new().parse("<A B~<C D>>"),
Ok(TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![
- TypeTerm::TypeID(TypeID::Fun(1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(2)),
- TypeTerm::TypeID(TypeID::Fun(3)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+3)),
])
])
]))
- );
+ );
}
#[test]
fn test_parser_ladder_large() {
assert_eq!(
- BimapTypeDict::new().parse(
+ TypeDict::new().parse(
"<Seq Date
~<TimeSince UnixEpoch>
~<Duration Seconds>
@@ -156,50 +156,51 @@ fn test_parser_ladder_large() {
Ok(
TypeTerm::Ladder(vec![
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![
- TypeTerm::TypeID(TypeID::Fun(1)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+1)),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(2)),
- TypeTerm::TypeID(TypeID::Fun(3))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+2)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+3))
]),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(4)),
- TypeTerm::TypeID(TypeID::Fun(5))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+4)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+5))
]),
- TypeTerm::TypeID(TypeID::Fun(6)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+6)),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(7)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+7)),
TypeTerm::Num(10),
- TypeTerm::TypeID(TypeID::Fun(8))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+8))
]),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
TypeTerm::Ladder(vec![
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(9)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+9)),
TypeTerm::Num(10)
]),
- TypeTerm::TypeID(TypeID::Fun(10))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10))
])
])
])
]),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(11)),
- TypeTerm::TypeID(TypeID::Fun(10)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+11)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10)),
TypeTerm::Char(':')
]),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(10))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+10))
]),
- TypeTerm::TypeID(TypeID::Fun(12)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+12)),
TypeTerm::App(vec![
- TypeTerm::TypeID(TypeID::Fun(0)),
- TypeTerm::TypeID(TypeID::Fun(13))
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+0)),
+ TypeTerm::TypeID(TypeID::Fun(SUGARID_LIMIT+13))
])
])
)
);
}
+
diff --git a/src/test/pnf.rs b/src/test/pnf.rs
deleted file mode 100644
index a1d5a33..0000000
--- a/src/test/pnf.rs
+++ /dev/null
@@ -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(),
- );
-}
diff --git a/src/test/substitution.rs b/src/test/substitution.rs
index 91aa810..7959b08 100644
--- a/src/test/substitution.rs
+++ b/src/test/substitution.rs
@@ -1,14 +1,14 @@
use {
- crate::{dict::*, term::*, parser::*, unparser::*, substitution::*},
- std::iter::FromIterator,
+ crate::{dict::*, term::*},
+ std::iter::FromIterator
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[test]
fn test_subst() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
let mut σ = std::collections::HashMap::new();
@@ -24,7 +24,9 @@ fn test_subst() {
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()
);
}
+
diff --git a/src/test/subtype.rs b/src/test/subtype.rs
index c993063..08cc5c7 100644
--- a/src/test/subtype.rs
+++ b/src/test/subtype.rs
@@ -1,8 +1,8 @@
-use crate::{dict::BimapTypeDict, parser::*, unparser::*};
+use crate::dict::TypeDict;
#[test]
fn test_semantic_subtype() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error")
@@ -19,11 +19,11 @@ fn test_semantic_subtype() {
),
Some((0, dict.parse("A~B1~C1").expect("parse errror")))
);
-
+
assert_eq!(
dict.parse("A~B~C1").expect("parse error")
.is_semantic_subtype_of(
- &dict.parse("B~C2").expect("parse errror")
+ &dict.parse("B~C2").expect("parse errror")
),
Some((1, dict.parse("B~C1").expect("parse errror")))
);
@@ -31,12 +31,12 @@ fn test_semantic_subtype() {
#[test]
fn test_syntactic_subtype() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
assert_eq!(
dict.parse("A~B~C").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("A~B~C").expect("parse errror")
+ &dict.parse("A~B~C").expect("parse errror")
),
Ok(0)
);
@@ -44,7 +44,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("B~C").expect("parse errror")
+ &dict.parse("B~C").expect("parse errror")
),
Ok(1)
);
@@ -52,7 +52,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("C~D").expect("parse errror")
+ &dict.parse("C~D").expect("parse errror")
),
Ok(2)
);
@@ -60,7 +60,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("C~G").expect("parse errror")
+ &dict.parse("C~G").expect("parse errror")
),
Err((2,3))
);
@@ -68,7 +68,7 @@ fn test_syntactic_subtype() {
assert_eq!(
dict.parse("A~B~C~D~E").expect("parse error")
.is_syntactic_subtype_of(
- &dict.parse("G~F~K").expect("parse errror")
+ &dict.parse("G~F~K").expect("parse errror")
),
Err((0,0))
);
@@ -94,3 +94,4 @@ fn test_syntactic_subtype() {
Ok(4)
);
}
+
diff --git a/src/test/sugar.rs b/src/test/sugar.rs
new file mode 100644
index 0000000..c6a9768
--- /dev/null
+++ b/src/test/sugar.rs
@@ -0,0 +1,10 @@
+
+#[test]
+fn test_sugar() {
+
+ let mut dict = crate::TypeDict::new();
+
+
+}
+
+
diff --git a/src/test/unification.rs b/src/test/unification.rs
index 99ea7ed..19c6768 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -1,20 +1,20 @@
use {
- crate::{dict::*, parser::*, unparser::*, term::*, unification::*},
+ crate::{dict::*, term::*, unification::*},
std::iter::FromIterator
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
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("U"));
dict.add_varname(String::from("V"));
dict.add_varname(String::from("W"));
- let mut t1 = dict.parse(ts1).unwrap();
- let mut t2 = dict.parse(ts2).unwrap();
+ let mut t1 = dict.parse(ts1).unwrap().desugar();
+ let mut t2 = dict.parse(ts2).unwrap().desugar();
let σ = crate::unify( &t1, &t2 );
if expect_unificator {
@@ -23,8 +23,8 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
let σ = σ.unwrap();
assert_eq!(
- t1.apply_subst(&σ),
- t2.apply_subst(&σ)
+ t1.apply_substitution(&|v| σ.get(v).cloned()),
+ t2.apply_substitution(&|v| σ.get(v).cloned())
);
} else {
assert!(! σ.is_ok());
@@ -33,7 +33,7 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
#[test]
fn test_unification_error() {
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
dict.add_varname(String::from("T"));
assert_eq!(
@@ -61,19 +61,6 @@ fn test_unification_error() {
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]
@@ -89,7 +76,7 @@ fn test_unification() {
true
);
- let mut dict = BimapTypeDict::new();
+ let mut dict = TypeDict::new();
dict.add_varname(String::from("T"));
dict.add_varname(String::from("U"));
@@ -97,12 +84,11 @@ fn test_unification() {
dict.add_varname(String::from("W"));
assert_eq!(
- UnificationProblem::new_eq(vec![
+ UnificationProblem::new(vec![
(dict.parse("U").unwrap(), dict.parse("<Seq Char>").unwrap()),
(dict.parse("T").unwrap(), dict.parse("<Seq U>").unwrap()),
]).solve(),
- Ok((
- vec![],
+ Ok(
vec![
// T
(TypeID::Var(0), dict.parse("<Seq <Seq Char>>").unwrap()),
@@ -110,16 +96,15 @@ fn test_unification() {
// U
(TypeID::Var(1), dict.parse("<Seq Char>").unwrap())
].into_iter().collect()
- ))
+ )
);
assert_eq!(
- UnificationProblem::new_eq(vec![
+ UnificationProblem::new(vec![
(dict.parse("<Seq T>").unwrap(), dict.parse("<Seq W~<Seq Char>>").unwrap()),
(dict.parse("<Seq ℕ>").unwrap(), dict.parse("<Seq W>").unwrap()),
]).solve(),
- Ok((
- vec![],
+ Ok(
vec![
// W
(TypeID::Var(3), dict.parse("ℕ").unwrap()),
@@ -127,254 +112,7 @@ fn test_unification() {
// T
(TypeID::Var(0), dict.parse("ℕ~<Seq Char>").unwrap())
].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()
- ))
- );
-}
diff --git a/src/unification.rs b/src/unification.rs
index ace94e7..abbc1fe 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -1,5 +1,6 @@
use {
- crate::{dict::*, term::*}, std::{collections::HashMap}
+ std::collections::HashMap,
+ crate::{term::*, dict::*}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -11,502 +12,79 @@ pub struct UnificationError {
pub t2: TypeTerm
}
-#[derive(Clone, Debug)]
-pub struct UnificationPair {
- addr: Vec<usize>,
- halo: TypeTerm,
-
- lhs: TypeTerm,
- rhs: TypeTerm,
-}
-
-#[derive(Debug)]
pub struct UnificationProblem {
- σ: HashMap<TypeID, TypeTerm>,
- upper_bounds: HashMap< u64, TypeTerm >,
- lower_bounds: HashMap< u64, TypeTerm >,
- equal_pairs: Vec<UnificationPair>,
- subtype_pairs: Vec<UnificationPair>,
- trait_pairs: Vec<UnificationPair>
+ eqs: Vec<(TypeTerm, TypeTerm, Vec<usize>)>,
+ σ: HashMap<TypeID, TypeTerm>
}
impl UnificationProblem {
- pub fn new(
- equal_pairs: Vec<(TypeTerm, TypeTerm)>,
- subtype_pairs: Vec<(TypeTerm, TypeTerm)>,
- trait_pairs: Vec<(TypeTerm, TypeTerm)>
- ) -> Self {
+ pub fn new(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
UnificationProblem {
- σ: 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(),
+ eqs: eqs.iter().map(|(lhs,rhs)| (lhs.clone(),rhs.clone(),vec![])).collect(),
+ σ: HashMap::new()
}
}
- pub fn new_eq(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
- UnificationProblem::new( eqs, Vec::new(), Vec::new() )
- }
-
- 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) {
+ pub fn eval_equation(&mut self, lhs: TypeTerm, rhs: TypeTerm, addr: Vec<usize>) -> Result<(), UnificationError> {
+ match (lhs.clone(), rhs.clone()) {
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
- if ! t.contains_var( *varid ) {
- self.σ.insert(TypeID::Var(*varid), t.clone());
- self.reapply_subst();
- Ok(())
- } else if t == &TypeTerm::TypeID(TypeID::Var(*varid)) {
- Ok(())
- } else {
- Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
+ self.σ.insert(TypeID::Var(varid), t.clone());
+
+ // update all values in substitution
+ let mut new_σ = HashMap::new();
+ for (v, tt) in self.σ.iter() {
+ let mut tt = tt.clone();
+ tt.apply_substitution(&|v| self.σ.get(v).cloned());
+ new_σ.insert(v.clone(), tt);
}
+ self.σ = new_σ;
+
+ Ok(())
}
(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)) => {
- 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)) => {
- 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::App(a1), TypeTerm::App(a2)) => {
if a1.len() == a2.len() {
- for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
- let mut new_addr = unification_pair.addr.clone();
+ for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+ let mut new_addr = addr.clone();
new_addr.push(i);
- self.equal_pairs.push(
- UnificationPair {
- lhs: x,
- rhs: y,
- halo: TypeTerm::unit(),
- addr: new_addr
- });
+ self.eqs.push((x, y, new_addr));
}
Ok(())
} 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 add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> {
-
- if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) {
- return Ok(());
- }
-
- 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(())
+ pub fn solve(mut self) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
+ while self.eqs.len() > 0 {
+ while let Some( (mut lhs,mut rhs,addr) ) = self.eqs.pop() {
+ lhs.apply_substitution(&|v| self.σ.get(v).cloned());
+ rhs.apply_substitution(&|v| self.σ.get(v).cloned());
+ self.eval_equation(lhs, rhs, addr)?;
}
- } 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) {
- // 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.σ))
+ Ok(self.σ)
}
}
@@ -514,16 +92,9 @@ pub fn unify(
t1: &TypeTerm,
t2: &TypeTerm
) -> Result<HashMap<TypeID, TypeTerm>, UnificationError> {
- let unification = UnificationProblem::new_eq(vec![ (t1.clone(), t2.clone()) ]);
- Ok(unification.solve()?.1)
-}
-
-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()), σ) )
+ let mut unification = UnificationProblem::new(vec![ (t1.clone(), t2.clone()) ]);
+ unification.solve()
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
diff --git a/src/unparser.rs b/src/unparser.rs
index b78494e..ccf754d 100644
--- a/src/unparser.rs
+++ b/src/unparser.rs
@@ -2,12 +2,8 @@ use crate::{dict::*, term::*};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-pub trait UnparseLadderType {
- fn unparse(&self, t: &TypeTerm) -> String;
-}
-
-impl<T: TypeDict> UnparseLadderType for T {
- fn unparse(&self, t: &TypeTerm) -> String {
+impl TypeDict {
+ pub fn unparse(&self, t: &TypeTerm) -> String {
match t {
TypeTerm::TypeID(id) => self.get_typename(id).unwrap(),
TypeTerm::Num(n) => format!("{}", n),