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

wip

Browse source
This commit is contained in:
Michael Sippel 2025-05-31 20:48:22 +02:00
parent 0d09c74e47
commit d5b84c8a32
Signed by: senvas
GPG key ID: F96CF119C34B64A6
4 changed files with 229 additions and 108 deletions

18
src/constraint_system.rs
View file

@ -313,15 +313,6 @@ impl ConstraintSystem {
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(ConstraintError{ 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() {
@ -332,6 +323,15 @@ impl ConstraintSystem {
}
(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(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
}
}
/*
Atoms
*/

10
src/morphism.rs
View file

@ -218,6 +218,16 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
self.get_type().strip_halo()
}
pub fn from_chain(τ: TypeTerm, path: &Vec<MorphismInstance<M>>) -> Self {
if path.len() == 0 {
MorphismInstance::Id { τ }
} else if path.len() == 1 {
path[0].clone()
} else {
MorphismInstance::Chain { path: path.clone() }
}
}
pub fn get_weight(&self) -> u64 {
match self {
MorphismInstance::Id { τ } => 0,

218
src/morphism_graph.rs
View file

@ -3,18 +3,17 @@ use {
Morphism, MorphismBase, MorphismInstance, MorphismType, Substitution, TypeDict, TypeID, TypeTerm,
morphism_base::DecomposedMorphismType
},
std::{char::decode_utf16, collections::HashMap, sync::{Arc,RwLock}}
std::{collections::HashMap, sync::{Arc,RwLock}}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub struct MorphismGraph<M: Morphism+Clone+std::fmt::Debug> {
pub struct MorphismGraph<M: Morphism+Clone> {
solved_paths: HashMap< MorphismType, MorphismInstance<M> >,
base: MorphismBase<M>
}
#[derive(Debug)]
pub struct GraphSearch<M: Morphism+Clone+std::fmt::Debug> {
pub struct GraphSearch<M: Morphism+Clone> {
goal: MorphismType,
solution: Option< MorphismInstance<M> >,
explore_queue: Vec< Arc<RwLock<SearchNode<M>>> >,
@ -23,7 +22,7 @@ pub struct GraphSearch<M: Morphism+Clone+std::fmt::Debug> {
}
#[derive(Clone, Debug, PartialEq)]
pub enum GraphSearchState<M: Morphism+Clone+std::fmt::Debug> {
pub enum GraphSearchState<M: Morphism+Clone> {
Solved( MorphismInstance<M> ),
Continue,
Err( GraphSearchError )
@ -37,8 +36,7 @@ pub enum GraphSearchError {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
/// represents a partial path during search in the morphism graph
#[derive(Debug)]
pub struct SearchNode<M: Morphism+Clone+std::fmt::Debug> {
pub struct SearchNode<M: Morphism+Clone> {
/// predecessor node
pred: Option< Arc<RwLock< SearchNode<M> >> >,
@ -52,8 +50,7 @@ pub struct SearchNode<M: Morphism+Clone+std::fmt::Debug> {
ψ: TypeTerm,
}
#[derive(Debug)]
pub enum Step<M: Morphism+Clone+std::fmt::Debug> {
pub enum Step<M: Morphism+Clone> {
Id { τ: TypeTerm },
Inst{ m: MorphismInstance<M> },
Specialize { σ: HashMap<TypeID, TypeTerm> },
@ -62,7 +59,19 @@ pub enum Step<M: Morphism+Clone+std::fmt::Debug> {
MapEnum { variants: Vec< (String, GraphSearch<M>) > }
}
pub trait SearchNodeExt<M: Morphism+Clone+std::fmt::Debug> {
pub enum SolvedStep<M: Morphism+Clone> {
Id { τ: TypeTerm },
Inst{ m: MorphismInstance<M> },
Specialize { σ: HashMap<TypeID, TypeTerm> },
MapSeq { item: MorphismInstance<M> },
MapStruct { members: Vec< (String, MorphismInstance<M>) > },
MapEnum { variants: Vec< (String, MorphismInstance<M>) > }
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait SearchNodeExt<M: Morphism+Clone> {
fn specialize(&self, σ: HashMap<TypeID, TypeTerm>) -> Arc<RwLock<SearchNode<M>>>;
fn chain(&self, ψ: TypeTerm, σ: HashMap<TypeID, TypeTerm>, m: M) -> Arc<RwLock<SearchNode<M>>>;
fn set_sub(&self, ψ: TypeTerm) -> Arc<RwLock<SearchNode<M>>>;
@ -80,7 +89,7 @@ pub trait SearchNodeExt<M: Morphism+Clone+std::fmt::Debug> {
fn creates_loop(&self) -> bool;
}
impl<M: Morphism+Clone+std::fmt::Debug> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
fn get_weight(&self) -> u64 {
self.read().unwrap().weight
+ match &self.read().unwrap().step {
@ -179,20 +188,56 @@ impl<M: Morphism+Clone+std::fmt::Debug> SearchNodeExt<M> for Arc<RwLock<SearchNo
fn chain(&self, ψ: TypeTerm, σ: HashMap<TypeID, TypeTerm>, m: M) -> Arc<RwLock<SearchNode<M>>> {
let m = MorphismInstance::Primitive { m: m.clone() };
let mut parent = self.clone();
{
let mut σ = σ.clone().filter(|(v,t)|
if let TypeID::Var(v) = v {
self.get_type().dst_type.contains_var(*v)
} else {
false
});
if !σ.is_empty() {
parent = parent.specialize(σ);
}
}
let mut σ_src = σ.clone().filter(|(v,t)|
if let TypeID::Var(v) = v {
m.get_type().src_type.contains_var(*v) &&
!self.get_type().dst_type.contains_var(*v)
} else {
false
});
let mut σ_dst = σ.clone().filter(|(v,t)|
if let TypeID::Var(v) = v {
m.get_type().dst_type.contains_var(*v)
//&& !self.get_type().dst_type.contains_var(*v)
} else {
false
});
let mut n = Arc::new(RwLock::new(SearchNode {
pred: Some(self.clone()),
pred: Some(parent),
weight: self.get_weight(),
ty: MorphismType {
src_type: self.get_type().src_type,
dst_type: m.get_type().dst_type
},
step: Step::Inst{ m },
step: Step::Inst{ m:
if σ_src.is_empty() {
m
} else {
MorphismInstance::Specialize { σ: σ_src, m: Box::new(m) }
}
},
ψ: TypeTerm::unit(),//self.read().unwrap().ψ.clone()
}));
n.set_sub(ψ);
if !σ.is_empty() {
n = n.specialize(σ);
if !σ_dst.is_empty() {
n = n.specialize(σ_dst);
}
n
@ -238,93 +283,81 @@ impl<M: Morphism+Clone+std::fmt::Debug> SearchNodeExt<M> for Arc<RwLock<SearchNo
}
fn to_morphism_instance(&self) -> Option< MorphismInstance<M> > {
let mut begin = TypeTerm::unit();
let mut path = Vec::new();
let mut subst = HashMap::new();
let mut steps = Vec::new();
let mut cur_node = Some(self.clone());
while let Some(n) = cur_node {
let n = n.read().unwrap();
match &n.step {
Step::Id { τ } => { begin = τ.clone(); },
Step::Inst{ m } => {
let mut m = m.clone();
let σ = subst.clone().filter_morphtype(&m.get_type());
/*
if !σ.is_empty() {
m = MorphismInstance::Specialize { σ, m: Box::new(m) }
}
*/
if ! n.ψ.is_empty() {
m = MorphismInstance::Sub { ψ: n.ψ.clone(), m: Box::new(m) };
}
path.push(m.clone());
},
Step::Specialize { σ } => {
subst = subst.append(&σ);
}
Step::MapSeq { item } => {
let mut m = MorphismInstance::MapSeq {
seq_repr: None,
item_morph: Box::new(item.get_solution().expect(""))
};
if ! n.ψ.is_empty() {
m = MorphismInstance::Sub { ψ: n.ψ.clone(), m: Box::new(m) };
}
/*
let σ = subst.clone().filter_morphtype(&m.get_type());
if !σ.is_empty() {
m = MorphismInstance::Specialize { σ, m: Box::new(m) }
}
*/
path.push(m);
}
Step::MapStruct { members } => {
todo!();
//path.push(MorphismInstance::MapStruct { src_struct_repr: (), dst_struct_repr: (), member_morph: () })
}
Step::MapEnum { variants } => {
todo!();
}
}
steps.push((n.ψ.clone(),
match &n.step {
Step::Id { τ } => SolvedStep::Id { τ: τ.clone() },
Step::Inst { m } => SolvedStep::Inst { m: m.clone() },
Step::Specialize { σ } => SolvedStep::Specialize { σ: σ.clone() },
Step::MapSeq { item } => SolvedStep::MapSeq { item: item.get_solution().unwrap() },
Step::MapStruct { members } => SolvedStep::MapStruct { members: members.iter().map(|(n,m)| (n.clone(), m.get_solution().unwrap())).collect() },
Step::MapEnum { variants } => SolvedStep::MapEnum { variants: variants.iter().map(|(n,m)| (n.clone(), m.get_solution().unwrap())).collect() },
}));
cur_node = n.pred.clone();
}
path.reverse();
steps.reverse();
for m in path.iter_mut() {
let σ = subst.clone().filter_morphtype(&m.get_type());
if !σ.is_empty() {
*m = MorphismInstance::Specialize { σ, m: Box::new(m.clone()) };
let mut begin = TypeTerm::unit();
let mut path = Vec::new();
eprintln!("to_morph_instance:\n==");
for (ψ, s) in steps {
match s {
SolvedStep::Id { τ } => {
eprintln!("to_morph_instance: ID {:?}", τ);
begin = τ.clone(); },
SolvedStep::Inst{ m } => {
eprintln!("to_morph_instance: Inst {:?} -- {:?}", ψ, m.get_type());
let mut m = m.clone();
if ! ψ.is_empty() {
m = MorphismInstance::Sub { ψ, m: Box::new(m) };
}
path.push(m.clone());
},
SolvedStep::Specialize { σ } => {
eprintln!("to_morph_instance: Specialize {:?}", σ);
if path.len() > 0 && !σ.is_empty() {
let m = MorphismInstance::from_chain(begin.clone(), &path);
path = vec![
MorphismInstance::Specialize { σ: σ.clone(), m: Box::new(m) }
];
}
}
SolvedStep::MapSeq { item } => {
let mut m = MorphismInstance::MapSeq {
seq_repr: None,
item_morph: Box::new(item)
};
if ! ψ.is_empty() {
m = MorphismInstance::Sub { ψ, m: Box::new(m) };
}
path.push(m);
}
SolvedStep::MapStruct { members } => {
todo!();
//path.push(MorphismInstance::MapStruct { src_struct_repr: (), dst_struct_repr: (), member_morph: () })
}
SolvedStep::MapEnum { variants } => {
todo!();
}
}
}
let mut m =
if path.len() == 0 {
MorphismInstance::Id { τ: begin }
} else if path.len() == 1 {
path[0].clone()
} else {
MorphismInstance::Chain { path }
};
subst = subst.filter_morphtype(&m.get_type());
if !subst.is_empty() {
m = MorphismInstance::Specialize { σ: subst, m: Box::new(m) };
}
Some(m)
Some(MorphismInstance::from_chain(begin, &path))
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl<M: Morphism+Clone+std::fmt::Debug> MorphismGraph<M> {
impl<M: Morphism+Clone> MorphismGraph<M> {
pub fn new(base: MorphismBase<M>) -> Self {
MorphismGraph {
solved_paths: HashMap::new(),
@ -347,7 +380,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> MorphismGraph<M> {
}
}
impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
impl<M: Morphism+Clone> GraphSearch<M> {
pub fn new(goal: MorphismType) -> Self {
GraphSearch {
goal: goal.clone(),
@ -402,7 +435,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
)
}
);
/*
if !self.skip_preview {
eprintln!("===== TOP 5 PATHS =====\nGoal:\n {} -> {}",
goal.src_type.pretty(dict, 0),
@ -419,7 +452,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
} else {
self.skip_preview = false;
}
*/
self.explore_queue.pop()
}
@ -445,6 +478,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
}
if node.creates_loop() {
eprintln!("Creates loop.");
return GraphSearchState::Continue;
}
@ -470,7 +504,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
decompositions.push(d);
}
//eprintln!("{} decompositions", decompositions.len());
eprintln!("{} decompositions", decompositions.len());
let mut done = Vec::new();
for (ψ,decomposition) in decompositions {
@ -490,7 +524,7 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
/* 2. Try to advance current path */
for (ψ,σ,m) in base.enum_morphisms_from(&node.get_type().dst_type) {
//eprintln!("add direct path");
eprintln!("add direct path");
self.explore_queue.push( node.chain(ψ,σ,m) );
}
@ -500,3 +534,5 @@ impl<M: Morphism+Clone+std::fmt::Debug> GraphSearch<M> {
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

91
src/test/morphism.rs
View file

@ -8,9 +8,6 @@ use {
std::collections::HashMap
};
#[cfg(test)]
use pretty_assertions::{assert_eq, assert_ne};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Clone, Debug, PartialEq, Eq)]
@ -107,7 +104,8 @@ fn test_morphgraph_prim() {
}, &mut dict),
Ok(
MorphismInstance::Specialize { σ: vec![
MorphismInstance::Spe
cialize { σ: vec![
(dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10))
].into_iter().collect(), m: Box::new(
MorphismInstance::Primitive {
@ -162,6 +160,78 @@ fn test_morphgraph_chain() {
}
#[test]
fn test_morphgraph_spec() {
let mut dict = BimapTypeDict::new();
let mut base = MorphismBase::<DummyMorphism>::new();
dict.add_varname("X".into());
dict.add_varname("Y".into());
base.add_morphism(DummyMorphism(MorphismType{
src_type: dict.parse("T ~ A").expect(""),
dst_type: dict.parse("T ~ <B X> ~ U").expect("")
}));
base.add_morphism(DummyMorphism(MorphismType{
src_type: dict.parse("T ~ <B Y> ~ U").expect(""),
dst_type: dict.parse("T ~ <B Y> ~ V").expect("")
}));
let morph_graph = MorphismGraph::new(base);
assert_eq!(
morph_graph.search(MorphismType {
src_type: dict.parse("T ~ A").unwrap(),
dst_type: dict.parse("T ~ <B test> ~ U").unwrap(),
}, &mut dict),
Ok(
MorphismInstance::Specialize {
σ: vec![
( dict.get_typeid(&"X".into()).unwrap(), dict.parse("test").expect("parse") )
].into_iter().collect(),
m: Box::new(MorphismInstance::Primitive { m: DummyMorphism(MorphismType {
src_type: dict.parse("T ~ A").expect("parse"),
dst_type: dict.parse("T ~ <B X> ~ U").expect("parse")
}) })
}
)
);
assert_eq!(
morph_graph.search(MorphismType {
src_type: dict.parse("T ~ A").unwrap(),
dst_type: dict.parse("T ~ <B test> ~ V").unwrap(),
}, &mut dict),
Ok(
MorphismInstance::Specialize {
σ: vec![
( dict.get_typeid(&"Y".into()).unwrap(), dict.parse("test").expect("parse") )
].into_iter().collect(),
m: Box::new(
MorphismInstance::Chain {
path: vec![
MorphismInstance::Specialize {
σ: vec![
( dict.get_typeid(&"X".into()).unwrap(), dict.parse("Y").expect("parse") )
].into_iter().collect(),
m: Box::new(MorphismInstance::Primitive { m: DummyMorphism(MorphismType {
src_type: dict.parse("T ~ A").expect("parse"),
dst_type: dict.parse("T ~ <B X> ~ U").expect("parse")
}) }) },
MorphismInstance::Primitive { m: DummyMorphism(MorphismType {
src_type: dict.parse("T ~ <B Y> ~ U").expect("parse"),
dst_type: dict.parse("T ~ <B Y> ~ V").expect("parse")
}) }
]
}
)
}
)
);
}
#[test]
fn test_morphgraph_map_seq() {
let mut dict = BimapTypeDict::new();
@ -239,6 +309,11 @@ fn test_morphism_path2() {
dst_type: dict.parse("ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
}, &mut dict),
Ok(
MorphismInstance::Specialize {
σ: vec![
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
].into_iter().collect(),
m: Box::new(
MorphismInstance::Chain {
path: vec![
MorphismInstance::Sub {
@ -264,10 +339,9 @@ fn test_morphism_path2() {
},
MorphismInstance::Specialize {
σ: vec![
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
(dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
(dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10))
].into_iter().collect(),
m: Box::new(
m: Box::new(
MorphismInstance::Primitive{
m: DummyMorphism(MorphismType {
src_type: dict.parse_desugared("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().sugar(&mut dict),
@ -277,7 +351,8 @@ fn test_morphism_path2() {
)
}
]
}
})
}
));
}