Merge branch 'topic-morphism-base' into dev
This commit is contained in:
commit
804741cd62
11 changed files with 942 additions and 47 deletions
|
@ -2,6 +2,8 @@
|
|||
pub mod bimap;
|
||||
pub mod dict;
|
||||
pub mod term;
|
||||
pub mod substitution;
|
||||
|
||||
pub mod lexer;
|
||||
pub mod parser;
|
||||
pub mod unparser;
|
||||
|
@ -11,6 +13,9 @@ 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;
|
||||
|
@ -21,6 +26,8 @@ mod pretty;
|
|||
pub use {
|
||||
dict::*,
|
||||
term::*,
|
||||
substitution::*,
|
||||
sugar::*,
|
||||
unification::*,
|
||||
morphism::*
|
||||
};
|
||||
|
|
63
src/morphism.rs
Normal file
63
src/morphism.rs
Normal file
|
@ -0,0 +1,63 @@
|
|||
use {
|
||||
crate::{
|
||||
subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
|
||||
},
|
||||
std::{collections::HashMap, u64}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Debug)]
|
||||
pub struct MorphismType {
|
||||
pub src_type: TypeTerm,
|
||||
pub dst_type: TypeTerm,
|
||||
}
|
||||
|
||||
impl MorphismType {
|
||||
pub fn normalize(self) -> Self {
|
||||
MorphismType {
|
||||
src_type: self.src_type.normalize().param_normalize(),
|
||||
dst_type: self.dst_type.normalize().param_normalize()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
pub trait Morphism : Sized {
|
||||
fn get_type(&self) -> MorphismType;
|
||||
fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
|
||||
|
||||
fn weight(&self) -> u64 {
|
||||
1
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, Debug, PartialEq)]
|
||||
pub struct MorphismInstance<M: Morphism + Clone> {
|
||||
pub halo: TypeTerm,
|
||||
pub m: M,
|
||||
pub σ: HashMap<TypeID, TypeTerm>
|
||||
}
|
||||
|
||||
impl<M: Morphism + Clone> MorphismInstance<M> {
|
||||
pub fn get_type(&self) -> MorphismType {
|
||||
MorphismType {
|
||||
src_type: TypeTerm::Ladder(vec![
|
||||
self.halo.clone(),
|
||||
self.m.get_type().src_type.clone()
|
||||
]).apply_substitution(&self.σ)
|
||||
.clone(),
|
||||
|
||||
dst_type: TypeTerm::Ladder(vec![
|
||||
self.halo.clone(),
|
||||
self.m.get_type().dst_type.clone()
|
||||
]).apply_substitution(&self.σ)
|
||||
.clone()
|
||||
}.normalize()
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
183
src/morphism_base.rs
Normal file
183
src/morphism_base.rs
Normal file
|
@ -0,0 +1,183 @@
|
|||
use {
|
||||
crate::{
|
||||
subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm,
|
||||
morphism::{MorphismType, Morphism, MorphismInstance}
|
||||
},
|
||||
std::{collections::HashMap, u64}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct MorphismBase<M: Morphism + Clone> {
|
||||
morphisms: Vec< M >,
|
||||
seq_types: Vec< TypeTerm >
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
impl<M: Morphism + Clone> MorphismBase<M> {
|
||||
pub fn new(seq_types: Vec<TypeTerm>) -> Self {
|
||||
MorphismBase {
|
||||
morphisms: Vec::new(),
|
||||
seq_types
|
||||
}
|
||||
}
|
||||
|
||||
pub fn add_morphism(&mut self, m: M) {
|
||||
self.morphisms.push( m );
|
||||
}
|
||||
|
||||
pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
|
||||
-> Vec< MorphismInstance<M> >
|
||||
{
|
||||
let mut dst_types = Vec::new();
|
||||
for m in self.morphisms.iter() {
|
||||
if let Ok((halo, σ)) = crate::unification::subtype_unify(
|
||||
&src_type.clone().param_normalize(),
|
||||
&m.get_type().src_type.param_normalize(),
|
||||
) {
|
||||
dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
|
||||
}
|
||||
}
|
||||
dst_types
|
||||
}
|
||||
|
||||
pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
|
||||
-> Vec< MorphismInstance<M> > {
|
||||
let src_type = src_type.clone().param_normalize();
|
||||
let mut dst_types = Vec::new();
|
||||
|
||||
// Check if we have a List type, and if so, see what the Item type is
|
||||
// TODO: function for generating fresh variables
|
||||
let item_variable = TypeID::Var(800);
|
||||
|
||||
for seq_type in self.seq_types.iter() {
|
||||
if let Ok((halo, σ)) = crate::unification::subtype_unify(
|
||||
&src_type,
|
||||
&TypeTerm::App(vec![
|
||||
seq_type.clone(),
|
||||
TypeTerm::TypeID(item_variable)
|
||||
])
|
||||
) {
|
||||
let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
|
||||
for item_morph_inst in self.enum_morphisms( &src_item_type ) {
|
||||
|
||||
let mut dst_halo_ladder = vec![ halo.clone() ];
|
||||
if item_morph_inst.halo != TypeTerm::unit() {
|
||||
dst_halo_ladder.push(
|
||||
TypeTerm::App(vec![
|
||||
seq_type.clone().get_lnf_vec().first().unwrap().clone(),
|
||||
item_morph_inst.halo.clone()
|
||||
]));
|
||||
}
|
||||
|
||||
if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
|
||||
dst_types.push(
|
||||
MorphismInstance {
|
||||
halo: TypeTerm::Ladder(dst_halo_ladder).strip().param_normalize(),
|
||||
m: map_morph,
|
||||
σ: item_morph_inst.σ
|
||||
}
|
||||
);
|
||||
} else {
|
||||
eprintln!("could not get map morphism");
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
dst_types
|
||||
}
|
||||
|
||||
pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
|
||||
let mut dst_types = Vec::new();
|
||||
dst_types.append(&mut self.enum_direct_morphisms(src_type));
|
||||
dst_types.append(&mut self.enum_map_morphisms(src_type));
|
||||
dst_types
|
||||
}
|
||||
|
||||
pub fn find_direct_morphism(&self,
|
||||
ty: &MorphismType,
|
||||
dict: &mut impl TypeDict
|
||||
) -> Option< MorphismInstance<M> > {
|
||||
eprintln!("find direct morph");
|
||||
for m in self.morphisms.iter() {
|
||||
let ty = ty.clone().normalize();
|
||||
let morph_type = m.get_type().normalize();
|
||||
|
||||
eprintln!("find direct morph:\n {} <= {}",
|
||||
dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
|
||||
);
|
||||
|
||||
if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
|
||||
eprintln!("halo: {}", dict.unparse(&halo));
|
||||
|
||||
let dst_type = TypeTerm::Ladder(vec![
|
||||
halo.clone(),
|
||||
morph_type.dst_type.clone()
|
||||
]).normalize().param_normalize();
|
||||
|
||||
eprintln!("-----------> {} <= {}",
|
||||
dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
|
||||
);
|
||||
|
||||
if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
|
||||
eprintln!("match. halo2 = {}", dict.unparse(&halo2));
|
||||
return Some(MorphismInstance {
|
||||
m: m.clone(),
|
||||
halo,
|
||||
σ,
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
None
|
||||
}
|
||||
|
||||
pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
|
||||
for seq_type in self.seq_types.iter() {
|
||||
if let Ok((halos, σ)) = UnificationProblem::new_sub(vec![
|
||||
(ty.src_type.clone().param_normalize(),
|
||||
TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
|
||||
|
||||
(TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
|
||||
ty.dst_type.clone().param_normalize()),
|
||||
]).solve() {
|
||||
// TODO: use real fresh variable names
|
||||
let item_morph_type = MorphismType {
|
||||
src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
|
||||
dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
|
||||
}.normalize();
|
||||
|
||||
//eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
|
||||
if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
|
||||
if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
|
||||
return Some( MorphismInstance {
|
||||
m: list_morph,
|
||||
σ,
|
||||
halo: halos[0].clone()
|
||||
} );
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
|
||||
pub fn find_morphism(&self, ty: &MorphismType,
|
||||
dict: &mut impl TypeDict
|
||||
)
|
||||
-> Option< MorphismInstance<M> > {
|
||||
if let Some(m) = self.find_direct_morphism(ty, dict) {
|
||||
return Some(m);
|
||||
}
|
||||
if let Some(m) = self.find_map_morphism(ty, dict) {
|
||||
return Some(m);
|
||||
}
|
||||
None
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
136
src/morphism_path.rs
Normal file
136
src/morphism_path.rs
Normal file
|
@ -0,0 +1,136 @@
|
|||
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
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
64
src/substitution.rs
Normal file
64
src/substitution.rs
Normal file
|
@ -0,0 +1,64 @@
|
|||
|
||||
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
|
||||
}
|
||||
}
|
29
src/term.rs
29
src/term.rs
|
@ -95,35 +95,6 @@ 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,
|
||||
subst: &impl Fn(&TypeID) -> Option<TypeTerm>
|
||||
) -> &mut Self {
|
||||
match self {
|
||||
TypeTerm::TypeID(typid) => {
|
||||
if let Some(t) = subst(typid) {
|
||||
*self = t;
|
||||
}
|
||||
}
|
||||
|
||||
TypeTerm::Ladder(rungs) => {
|
||||
for r in rungs.iter_mut() {
|
||||
r.apply_substitution(subst);
|
||||
}
|
||||
}
|
||||
TypeTerm::App(args) => {
|
||||
for r in args.iter_mut() {
|
||||
r.apply_substitution(subst);
|
||||
}
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
|
||||
self
|
||||
}
|
||||
|
||||
/* strip away empty ladders
|
||||
* & unwrap singletons
|
||||
|
|
|
@ -7,4 +7,5 @@ pub mod pnf;
|
|||
pub mod subtype;
|
||||
pub mod substitution;
|
||||
pub mod unification;
|
||||
pub mod morphism;
|
||||
|
||||
|
|
471
src/test/morphism.rs
Normal file
471
src/test/morphism.rs
Normal file
|
@ -0,0 +1,471 @@
|
|||
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()
|
||||
},
|
||||
])
|
||||
);
|
||||
}
|
|
@ -1,7 +1,7 @@
|
|||
|
||||
use {
|
||||
crate::{dict::*, term::*, parser::*, unparser::*},
|
||||
std::iter::FromIterator
|
||||
crate::{dict::*, term::*, parser::*, unparser::*, substitution::*},
|
||||
std::iter::FromIterator,
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
@ -24,8 +24,7 @@ fn test_subst() {
|
|||
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("<Seq T~U>").unwrap()
|
||||
.apply_substitution(&|typid|{ σ.get(typid).cloned() }).clone(),
|
||||
dict.parse("<Seq T~U>").unwrap().apply_subst(&σ).clone(),
|
||||
dict.parse("<Seq ℕ~<Seq Char>>").unwrap()
|
||||
);
|
||||
}
|
||||
|
|
|
@ -23,8 +23,8 @@ fn test_unify(ts1: &str, ts2: &str, expect_unificator: bool) {
|
|||
let σ = σ.unwrap();
|
||||
|
||||
assert_eq!(
|
||||
t1.apply_substitution(&|v| σ.get(v).cloned()),
|
||||
t2.apply_substitution(&|v| σ.get(v).cloned())
|
||||
t1.apply_subst(&σ),
|
||||
t2.apply_subst(&σ)
|
||||
);
|
||||
} else {
|
||||
assert!(! σ.is_ok());
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
use {
|
||||
crate::{dict::*, term::*}, std::{collections::HashMap, env::consts::ARCH}
|
||||
crate::{dict::*, term::*}, std::{collections::HashMap}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
@ -79,7 +79,7 @@ impl UnificationProblem {
|
|||
let mut new_σ = HashMap::new();
|
||||
for (v, tt) in self.σ.iter() {
|
||||
let mut tt = tt.clone().normalize();
|
||||
tt.apply_substitution(&|v| self.σ.get(v).cloned());
|
||||
tt.apply_subst(&self.σ);
|
||||
tt = tt.normalize();
|
||||
//eprintln!("update σ : {:?} --> {:?}", v, tt);
|
||||
new_σ.insert(v.clone(), tt);
|
||||
|
@ -224,7 +224,7 @@ impl UnificationProblem {
|
|||
// error
|
||||
UnificationError
|
||||
> {
|
||||
eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
|
||||
// eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
|
||||
match (unification_pair.lhs.clone(), unification_pair.rhs.clone()) {
|
||||
|
||||
/*
|
||||
|
@ -414,7 +414,7 @@ impl UnificationProblem {
|
|||
Ok(halo) => {
|
||||
if halo == TypeTerm::unit() {
|
||||
let mut y = y.clone();
|
||||
y.apply_substitution(&|k| self.σ.get(k).cloned());
|
||||
y.apply_subst(&self.σ);
|
||||
y = y.strip();
|
||||
let mut top = y.get_lnf_vec().first().unwrap().clone();
|
||||
halo_args.push(top.clone());
|
||||
|
@ -425,7 +425,7 @@ impl UnificationProblem {
|
|||
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_substitution(&|k| self.σ.get(k).cloned());
|
||||
a.apply_subst(&self.σ);
|
||||
a = a.get_lnf_vec().first().unwrap().clone();
|
||||
argrs.push(a);
|
||||
} else {
|
||||
|
@ -434,7 +434,7 @@ impl UnificationProblem {
|
|||
a2[n_halos_required-1].clone().get_lnf_vec().first().unwrap().clone()
|
||||
]);
|
||||
|
||||
x.apply_substitution(&|k| self.σ.get(k).cloned());
|
||||
x.apply_subst(&self.σ);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -464,8 +464,8 @@ impl UnificationProblem {
|
|||
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_substitution(&|v| self.σ.get(v).cloned());
|
||||
equal_pair.rhs.apply_substitution(&|v| self.σ.get(v).cloned());
|
||||
equal_pair.lhs.apply_subst(&self.σ);
|
||||
equal_pair.rhs.apply_subst(&self.σ);
|
||||
|
||||
self.eval_equation(equal_pair)?;
|
||||
}
|
||||
|
@ -473,8 +473,8 @@ impl UnificationProblem {
|
|||
// solve subtypes
|
||||
// eprintln!("------ SOLVE SUBTYPES ---- ");
|
||||
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
|
||||
subtype_pair.lhs.apply_substitution(&|v| self.σ.get(v).cloned());
|
||||
subtype_pair.rhs.apply_substitution(&|v| self.σ.get(v).cloned());
|
||||
subtype_pair.lhs.apply_subst(&self.σ);
|
||||
subtype_pair.rhs.apply_subst(&self.σ);
|
||||
let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
|
||||
}
|
||||
|
||||
|
@ -494,8 +494,8 @@ impl UnificationProblem {
|
|||
// 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_substitution(&|v| self.σ.get(v).cloned()).clone().strip();
|
||||
subtype_pair.rhs = subtype_pair.rhs.apply_substitution(&|v| self.σ.get(v).cloned()).clone().strip();
|
||||
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);
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue