turn Morphism into trait and add find_morphism() function
This commit is contained in:
parent
42286bcadc
commit
811adde1b9
3 changed files with 106 additions and 41 deletions
|
@ -18,6 +18,7 @@ mod test;
|
||||||
pub use {
|
pub use {
|
||||||
dict::*,
|
dict::*,
|
||||||
term::*,
|
term::*,
|
||||||
unification::*
|
unification::*,
|
||||||
|
morphism::*
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -8,20 +8,27 @@ use {
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
|
#[derive(Clone, PartialEq, Eq, Debug)]
|
||||||
pub struct MorphismType {
|
pub struct MorphismType {
|
||||||
pub src_type: TypeTerm,
|
pub src_type: TypeTerm,
|
||||||
pub dst_type: TypeTerm,
|
pub dst_type: TypeTerm,
|
||||||
}
|
}
|
||||||
|
|
||||||
pub struct MorphismBase<Morphism: Clone> {
|
pub trait Morphism : Sized {
|
||||||
morphisms: Vec< (MorphismType, Morphism) >,
|
fn get_type(&self) -> MorphismType;
|
||||||
|
fn list_map_morphism(&self, list_typeid: TypeID) -> Option< Self >;
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
|
pub struct MorphismBase<M: Morphism + Clone> {
|
||||||
|
morphisms: Vec< M >,
|
||||||
list_typeid: TypeID
|
list_typeid: TypeID
|
||||||
}
|
}
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
impl MorphismType {
|
impl MorphismType {
|
||||||
fn normalize(self) -> Self {
|
pub fn normalize(self) -> Self {
|
||||||
MorphismType {
|
MorphismType {
|
||||||
src_type: self.src_type.normalize(),
|
src_type: self.src_type.normalize(),
|
||||||
dst_type: self.dst_type.normalize()
|
dst_type: self.dst_type.normalize()
|
||||||
|
@ -31,7 +38,7 @@ impl MorphismType {
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
impl<Morphism: Clone> MorphismBase<Morphism> {
|
impl<M: Morphism + Clone> MorphismBase<M> {
|
||||||
pub fn new(list_typeid: TypeID) -> Self {
|
pub fn new(list_typeid: TypeID) -> Self {
|
||||||
MorphismBase {
|
MorphismBase {
|
||||||
morphisms: Vec::new(),
|
morphisms: Vec::new(),
|
||||||
|
@ -39,8 +46,8 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn add_morphism(&mut self, morph_type: MorphismType, morphism: Morphism) {
|
pub fn add_morphism(&mut self, m: M) {
|
||||||
self.morphisms.push( (morph_type.normalize(), morphism) );
|
self.morphisms.push( m );
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn enum_morphisms(&self, src_type: &TypeTerm)
|
pub fn enum_morphisms(&self, src_type: &TypeTerm)
|
||||||
|
@ -49,17 +56,15 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
|
||||||
let mut dst_types = Vec::new();
|
let mut dst_types = Vec::new();
|
||||||
|
|
||||||
// first enumerate all "direct" morphisms,
|
// first enumerate all "direct" morphisms,
|
||||||
for (ty,m) in self.morphisms.iter() {
|
for m in self.morphisms.iter() {
|
||||||
if let Ok(σ) = crate::unification::unify(
|
if let Ok(σ) = crate::unification::unify(
|
||||||
&ty.src_type,
|
&m.get_type().src_type,
|
||||||
&src_type.clone().normalize()
|
&src_type.clone().normalize()
|
||||||
) {
|
) {
|
||||||
let dst_type =
|
let dst_type =
|
||||||
ty.dst_type.clone()
|
m.get_type().dst_type.clone()
|
||||||
.apply_substitution(
|
.apply_substitution( &|x| σ.get(x).cloned() )
|
||||||
&|x| σ.get(x).cloned()
|
.clone();
|
||||||
)
|
|
||||||
.clone();
|
|
||||||
|
|
||||||
dst_types.push( (σ, dst_type) );
|
dst_types.push( (σ, dst_type) );
|
||||||
}
|
}
|
||||||
|
@ -173,26 +178,68 @@ impl<Morphism: Clone> MorphismBase<Morphism> {
|
||||||
None
|
None
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
pub fn find_morphism(&self, ty: &MorphismType)
|
pub fn find_morphism(&self, ty: &MorphismType)
|
||||||
-> Option< Morphism > {
|
-> Option< ( M, HashMap<TypeID, TypeTerm> ) > {
|
||||||
|
|
||||||
// TODO
|
// try list-map morphism
|
||||||
|
if let Ok(σ) = UnificationProblem::new(vec![
|
||||||
|
(ty.src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(100)) ])),
|
||||||
|
(ty.dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(self.list_typeid), TypeTerm::TypeID(TypeID::Var(101)) ])),
|
||||||
|
]).solve() {
|
||||||
|
|
||||||
None
|
// 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();
|
||||||
|
|
||||||
pub fn find_list_map_morphism(&self, item_ty: &MorphismType)
|
if let Some((m, σ)) = self.find_morphism( &item_morph_type ) {
|
||||||
-> Option< Morphism > {
|
if let Some(list_morph) = m.list_map_morphism( self.list_typeid ) {
|
||||||
|
return Some( (list_morph, σ) );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
// TODO
|
// otherwise
|
||||||
|
for m in self.morphisms.iter() {
|
||||||
|
let unification_problem = UnificationProblem::new(
|
||||||
|
vec![
|
||||||
|
( ty.src_type.clone().normalize(), m.get_type().src_type.clone() ),
|
||||||
|
( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone() )
|
||||||
|
]
|
||||||
|
);
|
||||||
|
|
||||||
|
let unification_result = unification_problem.solve();
|
||||||
|
if let Ok(σ) = unification_result {
|
||||||
|
return Some((m.clone(), σ));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
None
|
None
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
|
pub fn find_morphism_with_subtyping(&self, ty: &MorphismType)
|
||||||
-> Option<( Morphism, TypeTerm, HashMap<TypeID, TypeTerm> )> {
|
-> Option<( M, TypeTerm, HashMap<TypeID, TypeTerm> )> {
|
||||||
|
let mut src_lnf = ty.src_type.clone().get_lnf_vec();
|
||||||
|
let mut dst_lnf = ty.dst_type.clone().get_lnf_vec();
|
||||||
|
let mut halo = vec![];
|
||||||
|
|
||||||
// TODO
|
while src_lnf.len() > 0 && dst_lnf.len() > 0 {
|
||||||
|
if let Some((m, σ)) = self.find_morphism(&MorphismType{
|
||||||
|
src_type: TypeTerm::Ladder(src_lnf.clone()),
|
||||||
|
dst_type: TypeTerm::Ladder(dst_lnf.clone())
|
||||||
|
}) {
|
||||||
|
return Some((m, TypeTerm::Ladder(halo), σ));
|
||||||
|
} else {
|
||||||
|
if src_lnf[0] == dst_lnf[0] {
|
||||||
|
src_lnf.remove(0);
|
||||||
|
halo.push(dst_lnf.remove(0));
|
||||||
|
} else {
|
||||||
|
return None;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
None
|
None
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,55 +1,72 @@
|
||||||
use {
|
use {
|
||||||
crate::{dict::*, morphism::*}
|
crate::{dict::*, morphism::*, TypeTerm}
|
||||||
};
|
};
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
|
struct DummyMorphism(MorphismType);
|
||||||
|
|
||||||
|
impl Morphism for DummyMorphism {
|
||||||
|
fn get_type(&self) -> MorphismType {
|
||||||
|
self.0.clone().normalize()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn list_map_morphism(&self, list_typeid: TypeID) -> Option<DummyMorphism> {
|
||||||
|
Some(DummyMorphism(MorphismType {
|
||||||
|
src_type: TypeTerm::App(vec![
|
||||||
|
TypeTerm::TypeID( list_typeid ),
|
||||||
|
self.0.src_type.clone()
|
||||||
|
]),
|
||||||
|
|
||||||
|
dst_type: TypeTerm::App(vec![
|
||||||
|
TypeTerm::TypeID( list_typeid ),
|
||||||
|
self.0.dst_type.clone()
|
||||||
|
])
|
||||||
|
}))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn test_morphism_path() {
|
fn test_morphism_path() {
|
||||||
let mut dict = TypeDict::new();
|
let mut dict = TypeDict::new();
|
||||||
let mut base = MorphismBase::<u64>::new( dict.add_typename("Seq".into()) );
|
let mut base = MorphismBase::<DummyMorphism>::new( dict.add_typename("Seq".into()) );
|
||||||
|
|
||||||
dict.add_varname("Radix".into());
|
dict.add_varname("Radix".into());
|
||||||
dict.add_varname("SrcRadix".into());
|
dict.add_varname("SrcRadix".into());
|
||||||
dict.add_varname("DstRadix".into());
|
dict.add_varname("DstRadix".into());
|
||||||
|
|
||||||
base.add_morphism(
|
base.add_morphism(
|
||||||
MorphismType{
|
DummyMorphism(MorphismType{
|
||||||
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
|
src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
|
||||||
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
|
dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
|
||||||
},
|
})
|
||||||
11
|
|
||||||
);
|
);
|
||||||
base.add_morphism(
|
base.add_morphism(
|
||||||
MorphismType{
|
DummyMorphism(MorphismType{
|
||||||
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
|
src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
|
||||||
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
|
dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
|
||||||
},
|
})
|
||||||
22
|
|
||||||
);
|
);
|
||||||
base.add_morphism(
|
base.add_morphism(
|
||||||
MorphismType{
|
DummyMorphism(MorphismType{
|
||||||
src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
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()
|
dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||||
},
|
})
|
||||||
333
|
|
||||||
);
|
);
|
||||||
base.add_morphism(
|
base.add_morphism(
|
||||||
MorphismType{
|
DummyMorphism(MorphismType{
|
||||||
src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
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()
|
dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||||
},
|
})
|
||||||
444
|
|
||||||
);
|
);
|
||||||
base.add_morphism(
|
base.add_morphism(
|
||||||
MorphismType{
|
DummyMorphism(MorphismType{
|
||||||
src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap(),
|
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()
|
dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap()
|
||||||
},
|
})
|
||||||
555
|
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
base.find_morphism_path(MorphismType {
|
base.find_morphism_path(MorphismType {
|
||||||
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
|
||||||
|
|
Loading…
Reference in a new issue