Compare commits
4 commits
a9967f8183
...
b7832aed94
| Author | SHA1 | Date | |
|---|---|---|---|
b7832aed94
|
|||
|
69ec5ad8bb
|
|||
|
2ecbc84233
|
|||
|
78c83cc481
|
6 changed files with 437 additions and 157 deletions
|
|
@ -127,11 +127,14 @@ impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
|
|||
// morphisms source type,
|
||||
// i.e. check if `src_type` is a subtype of `m_src_type`
|
||||
if let Ok((ψ, σ)) = crate::unification_sugared::subtype_unify(src_type, &m_src_type) {
|
||||
morphs.push(MorphismInstance2::Primitive { ψ, σ, morph: m.clone() });
|
||||
let morph_inst = MorphismInstance2::Primitive { ψ, σ, morph: m.clone() };
|
||||
//eprintln!("..found direct morph to {:?}", morph_inst.get_type().dst_type);
|
||||
morphs.push(morph_inst);
|
||||
}
|
||||
|
||||
/* 2. check complex types */
|
||||
if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
|
||||
else if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
|
||||
//eprintln!("found complex morph to {:?}", complex_morph.get_type().dst_type);
|
||||
morphs.push(complex_morph);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -166,6 +166,14 @@ impl SugaredMorphismType {
|
|||
dst_type: self.dst_type.clone().apply_subst(σ).clone()
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
pub fn normalize(&self) -> SugaredMorphismType {
|
||||
SugaredMorphismType {
|
||||
src_type: self.src_type.clone().normalize(),
|
||||
dst_type: self.dst_type.clone().normalize(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub trait SugaredMorphism : Sized {
|
||||
|
|
@ -231,9 +239,9 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
if path.len() > 0 {
|
||||
let s = self.get_subst();
|
||||
SugaredMorphismType {
|
||||
src_type: path.first().unwrap().get_type().src_type.clone().apply_subst(&s).clone(),
|
||||
dst_type: path.last().unwrap().get_type().dst_type.clone().apply_subst(&s).clone()
|
||||
}
|
||||
src_type: path.first().unwrap().get_type().src_type.clone(),
|
||||
dst_type: path.last().unwrap().get_type().dst_type.clone()
|
||||
}.apply_subst(&s)
|
||||
} else {
|
||||
SugaredMorphismType {
|
||||
src_type: SugaredTypeTerm::TypeID(TypeID::Fun(45454)),
|
||||
|
|
@ -247,12 +255,12 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
ψ.clone(),
|
||||
SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
|
||||
items: vec![ item_morph.get_type().src_type ]}
|
||||
]).strip(),
|
||||
]),
|
||||
dst_type: SugaredTypeTerm::Ladder(vec![
|
||||
ψ.clone(),
|
||||
SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
|
||||
items: vec![ item_morph.get_type().dst_type ]}
|
||||
]).strip()
|
||||
])
|
||||
}
|
||||
}
|
||||
MorphismInstance2::MapStruct { ψ, src_struct_repr, dst_struct_repr, member_morph } => {
|
||||
|
|
@ -265,7 +273,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
|
||||
}).collect()
|
||||
}
|
||||
]).strip(),
|
||||
]),
|
||||
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
|
||||
SugaredTypeTerm::Struct{
|
||||
struct_repr: dst_struct_repr.clone(),
|
||||
|
|
@ -273,7 +281,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
|
||||
}).collect()
|
||||
}
|
||||
]).strip()
|
||||
])
|
||||
}
|
||||
}
|
||||
MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
|
||||
|
|
@ -286,7 +294,7 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
|
||||
}).collect()
|
||||
}
|
||||
]).strip(),
|
||||
]),
|
||||
dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
|
||||
SugaredTypeTerm::Struct{
|
||||
struct_repr: enum_repr.clone(),
|
||||
|
|
@ -294,10 +302,10 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
|
|||
SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
|
||||
}).collect()
|
||||
}
|
||||
]).strip()
|
||||
])
|
||||
}
|
||||
}
|
||||
}
|
||||
}.normalize()
|
||||
}
|
||||
|
||||
pub fn get_subst(&self) -> std::collections::HashMap< TypeID, SugaredTypeTerm > {
|
||||
|
|
|
|||
|
|
@ -1,8 +1,10 @@
|
|||
use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
|
||||
use crate::{sugar::SugaredTypeTerm, unification_sugared, SugaredEnumVariant, SugaredStructMember};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm > ) -> Vec< SugaredTypeTerm > {
|
||||
eprintln!("splice ladders {:?} <<<====>>> {:?} ", upper, lower);
|
||||
// check for overlap
|
||||
for i in 0 .. upper.len() {
|
||||
if upper[i] == lower[0] {
|
||||
let mut result_ladder = Vec::<SugaredTypeTerm>::new();
|
||||
|
|
@ -12,6 +14,7 @@ pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< Sugare
|
|||
}
|
||||
}
|
||||
|
||||
// no overlap found, just concatenate ladders
|
||||
upper.append(&mut lower);
|
||||
upper
|
||||
}
|
||||
|
|
@ -24,132 +27,302 @@ impl SugaredTypeTerm {
|
|||
/// <Seq <Digit 10>>~<Seq Char>
|
||||
/// ⇒ <Seq <Digit 10>~Char>
|
||||
/// ```
|
||||
pub fn param_normalize(mut self) -> Self {
|
||||
|
||||
pub fn normalize(mut self) -> Self {
|
||||
match self {
|
||||
SugaredTypeTerm::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) {
|
||||
(SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
|
||||
if bot_args.len() == last_args.len() {
|
||||
let mut new_rung_params = Vec::new();
|
||||
let mut require_break = false;
|
||||
if rungs.len() == 0 {
|
||||
return SugaredTypeTerm::unit();
|
||||
} else if rungs.len() == 1 {
|
||||
return rungs.pop().unwrap().normalize();
|
||||
}
|
||||
|
||||
if bot_args.len() > 0 {
|
||||
todo!();
|
||||
/*
|
||||
if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
|
||||
for i in 0 .. bot_args.len() {
|
||||
let mut new_rungs = Vec::new();
|
||||
let mut r2 = rungs.pop().unwrap().strip();
|
||||
while let Some(r1) = rungs.pop() {
|
||||
let r1 = r1.strip();
|
||||
match (r1.clone(), r2.clone()) {
|
||||
(SugaredTypeTerm::Seq { seq_repr: seq_repr1, items: items1 },
|
||||
SugaredTypeTerm::Seq { seq_repr: seq_repr2, items: items2 })
|
||||
=> {
|
||||
r2 = SugaredTypeTerm::Seq {
|
||||
seq_repr:
|
||||
if seq_repr1.is_some() || seq_repr2.is_some() {
|
||||
let sr1 = if let Some(seq_repr1) = seq_repr1 { *seq_repr1.clone() }
|
||||
else { SugaredTypeTerm::unit() };
|
||||
let sr2 = if let Some(seq_repr2) = seq_repr2 { *seq_repr2 }
|
||||
else { SugaredTypeTerm::unit() };
|
||||
|
||||
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 {
|
||||
SugaredTypeTerm::Ladder(spliced_type_ladder)
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
};
|
||||
|
||||
new_rung_params.push( spliced_type.param_normalize() );
|
||||
}
|
||||
|
||||
} else {
|
||||
new_rung_params.push(
|
||||
SugaredTypeTerm::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 {
|
||||
SugaredTypeTerm::Ladder(spliced_type_ladder)
|
||||
} else {
|
||||
SugaredTypeTerm::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( SugaredTypeTerm::Spec(new_rung_params) );
|
||||
Some(Box::new(
|
||||
if sr1 == sr2 {
|
||||
sr1
|
||||
} else if sr1 == SugaredTypeTerm::unit() {
|
||||
sr2
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ sr1, sr2 ]).normalize()
|
||||
}))
|
||||
} else {
|
||||
rungs.pop();
|
||||
rungs.push(SugaredTypeTerm::Spec(new_rung_params));
|
||||
}
|
||||
None
|
||||
},
|
||||
items:
|
||||
items1.into_iter()
|
||||
.zip(items2.into_iter())
|
||||
.map(|(item1, item2)| {
|
||||
if item1 == item2 {
|
||||
item1
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ item1.clone(), item2 ])
|
||||
}
|
||||
})
|
||||
.collect()
|
||||
};
|
||||
}
|
||||
|
||||
} else {
|
||||
new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
|
||||
(SugaredTypeTerm::Seq { seq_repr, items },
|
||||
SugaredTypeTerm::Spec( mut args )
|
||||
) => {
|
||||
if args.len() == items.len()+1 {
|
||||
r2 = SugaredTypeTerm::Seq {
|
||||
seq_repr: Some(Box::new(SugaredTypeTerm::Ladder(vec![
|
||||
if let Some(seq_repr) = seq_repr {
|
||||
*seq_repr.clone()
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
},
|
||||
args.remove(0)
|
||||
]).normalize())),
|
||||
|
||||
items: items.into_iter()
|
||||
.zip(args.into_iter())
|
||||
.map(|(i1, i2)| {
|
||||
if i1 == i2 {
|
||||
i1
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ i1, i2 ]).normalize()
|
||||
}
|
||||
})
|
||||
.collect()
|
||||
};
|
||||
} else {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
|
||||
SugaredTypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
|
||||
|
||||
let mut condensed_struct_repr = None;
|
||||
let mut condensed_members = Vec::new();
|
||||
let mut require_break = false;
|
||||
|
||||
|
||||
if let Some(struct_repr1) = struct_repr1 {
|
||||
if let Some(struct_repr2) = struct_repr2 {
|
||||
condensed_struct_repr = Some(Box::new(SugaredTypeTerm::Ladder(
|
||||
vec![
|
||||
struct_repr1.as_ref().clone(),
|
||||
struct_repr2.as_ref().clone()
|
||||
]
|
||||
).normalize()))
|
||||
} else {
|
||||
condensed_struct_repr = Some(Box::new(struct_repr1.as_ref().clone()));
|
||||
}
|
||||
} else {
|
||||
condensed_struct_repr = struct_repr2.clone();
|
||||
}
|
||||
|
||||
for SugaredStructMember{ symbol: symbol2, ty: ty2 } in members2.iter() {
|
||||
let mut found = false;
|
||||
for SugaredStructMember{ symbol: symbol1, ty: ty1 } in members1.iter() {
|
||||
if symbol2 == symbol1 {
|
||||
condensed_members.push(SugaredStructMember {
|
||||
symbol: symbol1.clone(),
|
||||
ty: SugaredTypeTerm::Ladder(vec![
|
||||
ty1.clone(),
|
||||
ty2.clone()
|
||||
]).normalize()
|
||||
});
|
||||
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
(bottom, last_buf) => {
|
||||
new_rungs.push( bottom );
|
||||
|
||||
if ! found {
|
||||
require_break = true;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
new_rungs.push( bottom );
|
||||
|
||||
if require_break {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
} else {
|
||||
r2 = SugaredTypeTerm::Struct {
|
||||
struct_repr: condensed_struct_repr,
|
||||
members: condensed_members
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
|
||||
SugaredTypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
|
||||
let mut condensed_enum_repr = None;
|
||||
let mut condensed_variants = Vec::new();
|
||||
let mut require_break = false;
|
||||
|
||||
if let Some(enum_repr1) = enum_repr1 {
|
||||
if let Some(enum_repr2) = enum_repr2 {
|
||||
condensed_enum_repr = Some(Box::new(SugaredTypeTerm::Ladder(
|
||||
vec![
|
||||
enum_repr1.as_ref().clone(),
|
||||
enum_repr2.as_ref().clone()
|
||||
]
|
||||
).normalize()))
|
||||
} else {
|
||||
condensed_enum_repr = Some(Box::new(enum_repr1.as_ref().clone()));
|
||||
}
|
||||
} else {
|
||||
condensed_enum_repr = enum_repr2.clone();
|
||||
}
|
||||
|
||||
for SugaredEnumVariant{ symbol: symbol2, ty: ty2 } in variants2.iter() {
|
||||
let mut found = false;
|
||||
for SugaredEnumVariant{ symbol: symbol1, ty: ty1 } in variants1.iter() {
|
||||
if symbol2 == symbol1 {
|
||||
condensed_variants.push(SugaredEnumVariant {
|
||||
symbol: symbol1.clone(),
|
||||
ty: SugaredTypeTerm::Ladder(vec![
|
||||
ty1.clone(),
|
||||
ty2.clone()
|
||||
]).normalize()
|
||||
});
|
||||
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if ! found {
|
||||
require_break = true;
|
||||
}
|
||||
}
|
||||
|
||||
if require_break {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
} else {
|
||||
r2 = SugaredTypeTerm::Enum {
|
||||
enum_repr: condensed_enum_repr,
|
||||
variants: condensed_variants
|
||||
};
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Spec(args1), SugaredTypeTerm::Spec(args2)) => {
|
||||
if args1.len() == args2.len() {
|
||||
if let Ok((ψ,σ)) = unification_sugared::subtype_unify(&args1[0], &args2[0]) {
|
||||
let mut new_args = Vec::new();
|
||||
|
||||
for (a1, a2) in args1.into_iter().zip(args2.into_iter()) {
|
||||
new_args.push(SugaredTypeTerm::Ladder(vec![ a1, a2 ]).normalize());
|
||||
}
|
||||
|
||||
r2 = SugaredTypeTerm::Spec(new_args);
|
||||
//new_rungs.push(r2.clone());
|
||||
} else {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
}
|
||||
} else {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Univ(args1), SugaredTypeTerm::Univ(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Func(args1), SugaredTypeTerm::Func(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Morph(args1), SugaredTypeTerm::Morph(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Ladder(rr1), SugaredTypeTerm::Ladder(rr2)) => {
|
||||
if rr1.len() > 0 {
|
||||
let l = splice_ladders(rr1, rr2);
|
||||
r2 = SugaredTypeTerm::Ladder(l).normalize();
|
||||
}
|
||||
}
|
||||
|
||||
(atomic1, SugaredTypeTerm::Ladder(mut rr2)) => {
|
||||
if !atomic1.is_empty() {
|
||||
if rr2.first() != Some(&atomic1) {
|
||||
rr2.insert(0, atomic1);
|
||||
}
|
||||
}
|
||||
r2 = SugaredTypeTerm::Ladder(rr2).normalize();
|
||||
}
|
||||
|
||||
|
||||
(SugaredTypeTerm::Ladder(mut rr1), atomic2) => {
|
||||
if !atomic2.is_empty() {
|
||||
if rr1.last() != Some(&atomic2) {
|
||||
rr1.push(atomic2);
|
||||
}
|
||||
}
|
||||
r2 = SugaredTypeTerm::Ladder(rr1).normalize();
|
||||
}
|
||||
|
||||
|
||||
(atomic1, atomic2) => {
|
||||
if atomic1.is_empty() {
|
||||
} else if atomic1 == atomic2 {
|
||||
} else if atomic2.is_empty() {
|
||||
r2 = atomic1;
|
||||
} else {
|
||||
new_rungs.push(atomic2);
|
||||
r2 = atomic1;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if new_rungs.len() > 0 {
|
||||
new_rungs.push(r2);
|
||||
new_rungs.reverse();
|
||||
|
||||
if new_rungs.len() > 1 {
|
||||
SugaredTypeTerm::Ladder(new_rungs)
|
||||
} else if new_rungs.len() == 1 {
|
||||
new_rungs[0].clone()
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
}
|
||||
return SugaredTypeTerm::Ladder(new_rungs);
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
return r2;
|
||||
}
|
||||
}
|
||||
|
||||
SugaredTypeTerm::Spec(params) => {
|
||||
SugaredTypeTerm::Spec(
|
||||
params.into_iter()
|
||||
.map(|p| p.param_normalize())
|
||||
.map(|p| p.normalize())
|
||||
.collect())
|
||||
}
|
||||
|
||||
SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
|
||||
seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
|
||||
items: items.into_iter().map(|p| p.param_normalize()).collect()
|
||||
seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.normalize())) } else { None },
|
||||
items: items.into_iter().map(|p| p.normalize()).collect()
|
||||
},
|
||||
SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
|
||||
struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
|
||||
SugaredTypeTerm::Struct { struct_repr, members } => SugaredTypeTerm::Struct {
|
||||
struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.normalize())) } else { None },
|
||||
members: members.into_iter()
|
||||
.map(|SugaredStructMember{symbol, ty}|
|
||||
SugaredStructMember{ symbol, ty: ty.param_normalize() })
|
||||
SugaredStructMember{ symbol, ty: ty.normalize() })
|
||||
.collect()
|
||||
},
|
||||
SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
|
||||
enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
|
||||
SugaredTypeTerm::Enum { enum_repr, variants } => SugaredTypeTerm::Enum{
|
||||
enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.normalize())) } else { None },
|
||||
variants: variants.into_iter()
|
||||
.map(|SugaredEnumVariant{symbol, ty}|
|
||||
SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
|
||||
SugaredEnumVariant{ symbol, ty: ty.normalize() })
|
||||
.collect()
|
||||
},
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
use {
|
||||
crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}
|
||||
crate::{dict::*, morphism::*, morphism_base::*, morphism_base_sugared::SugaredMorphismBase, morphism_path::*, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, parser::*, unparser::*, SugaredTypeTerm, TypeTerm}, std::collections::HashMap
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
|
@ -339,6 +339,37 @@ fn test_morphism_path_posint() {
|
|||
)
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn morphism_test_seq_repr() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
let mut base = SugaredMorphismBase::<DummyMorphism>::new();
|
||||
|
||||
base.add_morphism(
|
||||
DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
|
||||
})
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
base.get_morphism_instance(&SugaredMorphismType {
|
||||
src_type: dict.parse("<Seq~<ValueTerminated 0> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict),
|
||||
dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> Char~Ascii~native.UInt8>").expect("parse").sugar(&mut dict)
|
||||
}),
|
||||
Some(
|
||||
MorphismInstance2::Primitive {
|
||||
ψ: dict.parse("<Seq Char~Ascii>").expect("").sugar(&mut dict),
|
||||
σ: HashMap::new(),
|
||||
morph: DummyMorphism(SugaredMorphismType{
|
||||
src_type: dict.parse("<Seq~<ValueTerminated 0> native.UInt8>").unwrap().sugar(&mut dict),
|
||||
dst_type: dict.parse("<Seq~<LengthPrefix native.UInt64> native.UInt8>").unwrap().sugar(&mut dict)
|
||||
})
|
||||
}
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
/*
|
||||
#[test]
|
||||
fn test_steiner_tree() {
|
||||
|
|
|
|||
153
src/test/pnf.rs
153
src/test/pnf.rs
|
|
@ -1,58 +1,117 @@
|
|||
use crate::{dict::BimapTypeDict, parser::*};
|
||||
|
||||
#[test]
|
||||
fn test_param_normalize() {
|
||||
fn test_normalize_id() {
|
||||
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(),
|
||||
dict.parse("A~B~C").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("A~B~C").expect("parse error").sugar(&mut dict).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(),
|
||||
dict.parse("<A B>~C").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A B>~C").expect("parse error").sugar(&mut dict).normalize(),
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_normalize_spec() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("<A B~C>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A B>~<A C>").expect("parse error").sugar(&mut dict).normalize(),
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("<A~Y B>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A~Y B>~<Y B>").expect("parse error").sugar(&mut dict).normalize(),
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("<A B~C D~E>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").sugar(&mut dict).normalize(),
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("<A~X B~C D~E>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A~X B D>~<A~X B~C E>~<X C E>").expect("parse errror").sugar(&mut dict).normalize(),
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_normalize_seq() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
assert_eq!(
|
||||
dict.parse("<Seq Char~Ascii>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<Seq Char>~<Seq Ascii>").expect("parse errror").sugar(&mut dict).normalize(),
|
||||
);
|
||||
|
||||
eprintln!("---------------");
|
||||
assert_eq!(
|
||||
dict.parse("<Seq <Digit 10>~Char>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").sugar(&mut dict).normalize(),
|
||||
);
|
||||
eprintln!("---------------");
|
||||
assert_eq!(
|
||||
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~native.UInt8>").expect("parse error").sugar(&mut dict).normalize(),
|
||||
);
|
||||
|
||||
eprintln!("---------------");
|
||||
assert_eq!(
|
||||
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~native.UInt8>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> native.UInt8>").expect("parse error").sugar(&mut dict).normalize(),
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_normalize_complex_spec() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
assert_eq!(
|
||||
dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("<A~Y <B C> F H H>
|
||||
~<A~Y <B D> F H H>
|
||||
~<Y <B E> F H H>").expect("parse errror").sugar(&mut dict)
|
||||
.normalize(),
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_normalize_struct() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
assert_eq!(
|
||||
dict.parse("< Struct~Aligned
|
||||
< a TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64 >
|
||||
< b Angle ~ Degrees ~ ℝ ~ native.Float32 >
|
||||
>
|
||||
").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("
|
||||
< Struct <a TimePoint> <b Angle> >
|
||||
~ < Struct <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
|
||||
~ < Struct~Aligned <a native.UInt64> <b native.Float32> >
|
||||
").expect("parse errror")
|
||||
.sugar(&mut dict)
|
||||
.normalize(),
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_normalize_enum() {
|
||||
let mut dict = BimapTypeDict::new();
|
||||
assert_eq!(
|
||||
dict.parse("< Enum
|
||||
< a TimePoint~<TimeSince UnixEpoch>~Seconds~native.UInt64 >
|
||||
< b Angle ~ Degrees ~ ℝ ~ native.Float32 >
|
||||
>
|
||||
").expect("parse error").sugar(&mut dict),
|
||||
dict.parse("
|
||||
< Enum <a TimePoint> <b Angle> >
|
||||
~ < Enum <a <TimeSince UnixEpoch>~Seconds> <b Angle~Degrees~ℝ> >
|
||||
~ < Enum <a native.UInt64> <b native.Float32> >
|
||||
").expect("parse errror")
|
||||
.sugar(&mut dict)
|
||||
.normalize(),
|
||||
);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ pub struct SugaredUnificationError {
|
|||
pub t2: SugaredTypeTerm
|
||||
}
|
||||
|
||||
// todo : rename -> ConstraintPair
|
||||
#[derive(Clone)]
|
||||
pub struct SugaredUnificationPair {
|
||||
addr: Vec<usize>,
|
||||
|
|
@ -26,6 +27,7 @@ impl SugaredUnificationPair {
|
|||
}
|
||||
}
|
||||
|
||||
// todo : Rename -> ConstraintSystem
|
||||
pub struct SugaredUnificationProblem {
|
||||
// dict: &'a Dict,
|
||||
|
||||
|
|
@ -358,9 +360,13 @@ impl SugaredUnificationProblem {
|
|||
new_addr.push(0);
|
||||
|
||||
if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
|
||||
//eprintln!("subtype unify: rhs has seq-repr: {:?}", rhs_seq_repr);
|
||||
if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
|
||||
//eprintln!("check if it maches lhs seq-repr: {:?}", lhs_seq_repr);
|
||||
let _seq_repr_ψ = self.eval_subtype(SugaredUnificationPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
|
||||
//eprintln!("..yes!");
|
||||
} else {
|
||||
//eprintln!("...but lhs has none.");
|
||||
return Err(SugaredUnificationError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
|
@ -668,7 +674,7 @@ impl SugaredUnificationProblem {
|
|||
}
|
||||
|
||||
// solve subtypes
|
||||
// eprintln!("------ 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.σ);
|
||||
|
|
@ -688,7 +694,7 @@ impl SugaredUnificationProblem {
|
|||
|
||||
self.reapply_subst();
|
||||
|
||||
// eprintln!("------ MAKE HALOS -----");
|
||||
//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();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue