Compare commits

...

3 commits

6 changed files with 106 additions and 18 deletions

View file

@ -48,6 +48,7 @@ impl Context {
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl TypeDict for Arc<RwLock<Context>> {
fn add_typename(&mut self, tn: &str) -> u64 {
@ -114,6 +115,8 @@ impl TypeDict for Arc<RwLock<Context>> {
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl Substitution for Arc<RwLock<Context>> {
fn saturate(&mut self) {
let mut locked_self = self.read().unwrap();
@ -137,13 +140,38 @@ impl Substitution for Arc<RwLock<Context>> {
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait LayeredContext {
fn add_variable(&self, symbol: &str, kind: TypeKind ) -> u64;
fn bind(&self, var: u64, val: TypeTerm) -> Result<(), SubstError>;
fn scope(&self) -> Self;
fn shift_variables(&self, other: &Arc<RwLock<Context>>, t: TypeTerm) -> TypeTerm;
}
impl LayeredContext for Arc<RwLock<Context>> {
fn shift_variables(&self, other: &Arc<RwLock<Context>>, mut t: TypeTerm) -> TypeTerm {
let mut σ = HashMapSubst::new();
let l = self.read().unwrap().γ.len() as u64;
for (i,entry) in other.read().unwrap().γ.iter().enumerate() {
let i = i as u64;
// make variable name unique
let mut s = entry.symbol.clone();
while self.get_typeid(&s).is_some() {
s.push_str("'");
}
self.add_variable(&s, entry.kind.clone());
σ.insert(i, TypeTerm::Var(i + l));
}
t.apply_subst(&σ);
t
}
fn add_variable(&self, symbol: &str, kind: TypeKind ) -> u64 {
//self.write().unwrap().dict.add_varname(symbol.into());
let mut locked_self = self.write().unwrap();
@ -159,7 +187,8 @@ impl LayeredContext for Arc<RwLock<Context>> {
fn bind(&self, var: u64, val: TypeTerm) -> Result<(), SubstError> {
let mut locked_self = self.write().unwrap();
if (var as usize) < locked_self.γ.len() {
let l = locked_self.γ.len() as u64;
if var < l {
if locked_self.γ[var as usize].value.is_none() {
locked_self.γ[var as usize].value = Some(val);
Ok(())
@ -167,10 +196,10 @@ impl LayeredContext for Arc<RwLock<Context>> {
Err(SubstError::AlreadyAssigned)
}
} else {
let l = locked_self.γ.len() as u64;
if let Some(parent) = locked_self.parent.as_mut() {
parent.bind(var - l, val)
} else {
eprintln!("ERROR: assign invalid variable");
Err(SubstError::InvalidVariable)
}
}

View file

@ -182,13 +182,11 @@ impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
}
// all sub searches are solved
/*
n.ty = MorphismType {
bounds: Vec::new(),
src_type: TypeTerm::Struct { struct_repr, items: vec![ item_morph.get_type().src_type ] },
dst_type: TypeTerm::Struct { struct_repr, items: vec![ item_morph.get_type().dst_type ] },
src_type: TypeTerm::Struct { struct_repr: Some(Box::new(struct_repr.clone())), members: members.iter().map(|(s,g)| StructMember{ symbol:s.clone(), ty: g.get_solution().unwrap().get_type().src_type }).collect() },
dst_type: TypeTerm::Struct { struct_repr: Some(Box::new(struct_repr.clone())), members: members.iter().map(|(s,g)| StructMember{ symbol:s.clone(), ty: g.get_solution().unwrap().get_type().dst_type }).collect() },
};
*/
return Ok(false);
}
Step::MapEnum { enum_repr, variants } => {
@ -286,7 +284,10 @@ impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
let seq_repr = match self.read().unwrap().ty.dst_type.get_floor_type().1 {
TypeTerm::Seq { seq_repr, items } => {
seq_repr.unwrap().deref().clone()
match seq_repr.as_ref() {
Some(s) => s.deref().clone(),
None => TypeTerm::Id(0x59741) // <<= magic for native seq repr
}
}
_ => unreachable!()
};
@ -308,7 +309,10 @@ impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
let struct_repr = match self.read().unwrap().ty.dst_type.get_floor_type().1 {
TypeTerm::Struct { struct_repr, members } => {
struct_repr.unwrap().deref().clone()
match struct_repr.as_ref() {
Some(s) => s.deref().clone(),
None => TypeTerm::Id(0x59742) // <<= magic for native struct repr
}
}
_ => unreachable!()
};
@ -321,7 +325,9 @@ impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
src_type: TypeTerm::Struct { struct_repr: Some(Box::new(struct_repr.clone())), members: goals.iter().map(|(s,t)| StructMember{ symbol: s.clone(), ty: t.src_type.clone() }).collect() },
dst_type: TypeTerm::Struct { struct_repr: Some(Box::new(struct_repr.clone())), members: goals.iter().map(|(s,t)| StructMember{ symbol: s.clone(), ty: t.dst_type.clone() }).collect() }
},
step: Step::MapStruct { struct_repr, members: goals.into_iter().map(|(name,goal)| (name, GraphSearch::new(goal))).collect() },
step: Step::MapStruct {
struct_repr,
members: goals.into_iter().map(|(name,goal)| (name, GraphSearch::new(goal))).collect() },
ψ: self.read().unwrap().ψ.clone()
}))
}
@ -329,7 +335,10 @@ impl<M: Morphism+Clone> SearchNodeExt<M> for Arc<RwLock<SearchNode<M>>> {
fn map_enum(&self, goals: Vec<(String, MorphismType)>) -> Arc<RwLock<SearchNode<M>>> {
let enum_repr = match self.read().unwrap().ty.dst_type.get_floor_type().1 {
TypeTerm::Enum { enum_repr, variants } => {
enum_repr.unwrap().deref().clone()
match enum_repr.as_ref() {
Some(s) => s.deref().clone(),
None => TypeTerm::Id(0x59743) // <<= magic for native enum repr
}
}
_ => unreachable!()
};
@ -544,7 +553,7 @@ impl<M: Morphism+Clone> GraphSearch<M> {
Ok(_) => {
if ! node.is_ready() {
if ! node.creates_loop() {
// self.skip_preview = true;
self.skip_preview = true;
self.explore_queue.push(node);
}
return GraphSearchState::Continue;
@ -600,7 +609,7 @@ impl<M: Morphism+Clone> GraphSearch<M> {
}.set_sub(ψ.clone())
);
done.push((ψ, decomposition));
}else {
} else {
eprintln!("avoid duplicate decomposition");
}
}

View file

@ -243,5 +243,3 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

View file

@ -22,6 +22,7 @@ use {
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub trait Morphism : Sized {
fn ctx(&self) -> Arc<RwLock<Context>>;
fn get_type(&self) -> MorphismType;
fn weight(&self) -> u64 {
1

View file

@ -35,7 +35,7 @@ impl TypeTerm {
format!("{}", dict.get_typename(*id).unwrap_or("??".bright_red())).blue().bold()
}
TypeTerm::Var(id) => {
format!("{}", dict.get_typename(*id).unwrap_or("??".bright_red())).bright_magenta()
format!("{}", dict.get_varname(*id).unwrap_or("??".bright_red())).bright_magenta()
},
TypeTerm::Num(n) => {

View file

@ -1,8 +1,7 @@
use {
crate::{dict::*, morphism::*, parser::*,
HashMapSubst, TypeTerm
crate::{dict::*, morphism::*, parser::*, ConstraintError, ConstraintPair, ConstraintSystem, Context, HashMapSubst, LayeredContext, TypeKind, TypeTerm
},
std::collections::HashMap
std::{collections::HashMap, sync::{Arc, RwLock}}
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@ -10,6 +9,10 @@ use {
#[derive(Clone, Debug, PartialEq, Eq)]
struct DummyMorphism(MorphismType);
impl Morphism for DummyMorphism {
fn ctx(&self) -> Arc<RwLock<Context>> {
Context::new()
}
fn get_type(&self) -> MorphismType {
self.0.clone()
}
@ -79,6 +82,54 @@ fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
}
#[test]
fn test_morphism_compat() {
let ctx = Context::new();
let mut c1 = ctx.scope();
c1.add_variable("T1", TypeKind::Type);
c1.add_variable("T2", TypeKind::Type);
let t1 = MorphismType {
bounds: Vec::new(),
src_type: c1.parse("<Seq T1>~<A T1 T2>").unwrap(),
dst_type: c1.parse("<Seq T1>~<B T2 T2>").unwrap()
};
let mut c2 = ctx.scope();
c2.add_variable("S1", TypeKind::Type);
c2.add_variable("T1", TypeKind::Type); //< this variable name is scoped thus a *different* variable than T1 from t1
let t2 = MorphismType {
bounds: Vec::new(),
src_type: c2.parse("<Seq NotT>~<B S1 T1>").unwrap(),
dst_type: c2.parse("<Seq NotT>~<C T1>").unwrap()
};
// pull t1 & t2 into root ctx
let t1 = ctx.shift_variables(&c1, t1.dst_type.clone());
let t2 = ctx.shift_variables(&c2, t2.src_type.clone());
let csp = ConstraintSystem::new_sub(vec![
ConstraintPair {
lhs: t1.clone(),
rhs: t2.clone(),
addr: vec![]
}
]);
eprintln!("t1 = {:?} = {}", t1, t1.pretty(&mut ctx.clone(), 0));
eprintln!("t2 = {:?} = {}", t2, t2.pretty(&mut ctx.clone(), 0));
match csp.solve() {
Ok((Ψ,σ)) => {
eprintln!("σ = {:?}", σ);
assert!(true);
}
Err(err) => {
assert!(false);
}
}
}
#[test]
fn test_morphgraph_id() {
let (mut dict, mut base) = morphism_test_setup();