Compare commits
3 commits
3e1fee2ee4
...
93634c2656
Author | SHA1 | Date | |
---|---|---|---|
93634c2656 | |||
5af2b59278 | |||
1e29653c61 |
6 changed files with 106 additions and 18 deletions
src
|
@ -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)
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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");
|
||||
}
|
||||
}
|
||||
|
|
|
@ -243,5 +243,3 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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) => {
|
||||
|
|
|
@ -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();
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue