automatically generate list-map morphisms in find_morphism()
this allows us to now to create <List EditTree> from <List Char> with apply_morphism()
This commit is contained in:
parent
6e8bb0aeb5
commit
a3c701ce88
8 changed files with 150 additions and 148 deletions
|
@ -37,7 +37,7 @@ fn rebuild_projections(
|
|||
repr_tree: Arc<RwLock<ReprTree>>,
|
||||
morph_types: Vec< (laddertypes::TypeTerm, laddertypes::TypeTerm) >
|
||||
) {
|
||||
// repr_tree.write().unwrap().detach(&ctx);
|
||||
repr_tree.write().unwrap().detach(&ctx);
|
||||
for (src_type, dst_type) in morph_types.iter() {
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
repr_tree.clone(),
|
||||
|
@ -47,9 +47,7 @@ fn rebuild_projections(
|
|||
}
|
||||
}
|
||||
|
||||
fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||
rt_int.write().unwrap().detach(&ctx);
|
||||
|
||||
fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||
rebuild_projections(
|
||||
ctx.clone(),
|
||||
rt_int.clone(),
|
||||
|
@ -79,33 +77,17 @@ fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
|||
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree> ~ <Vec EditTree>",
|
||||
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree"
|
||||
),
|
||||
].into_iter()
|
||||
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||
.collect()
|
||||
);
|
||||
|
||||
let rt_digitseq =
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
")).expect("test");
|
||||
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||
ctx.read().unwrap().morphisms
|
||||
.apply_list_map_morphism::<char, u64>(
|
||||
rt_digitseq, src_type, dst_type
|
||||
);
|
||||
|
||||
rebuild_projections(
|
||||
ctx.clone(),
|
||||
rt_int.clone(),
|
||||
vec![
|
||||
// convert to different digit-representation
|
||||
(
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||
),
|
||||
// Radix Convert
|
||||
(
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||
)
|
||||
),
|
||||
].into_iter()
|
||||
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||
.collect()
|
||||
|
@ -113,8 +95,6 @@ fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
|||
}
|
||||
|
||||
fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||
rt_int.write().unwrap().detach(&ctx);
|
||||
|
||||
rebuild_projections(
|
||||
ctx.clone(),
|
||||
rt_int.clone(),
|
||||
|
@ -144,35 +124,19 @@ fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
|||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree> ~ <Vec EditTree>",
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree"
|
||||
),
|
||||
].into_iter()
|
||||
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||
.collect()
|
||||
);
|
||||
|
||||
|
||||
let rt_digitseq =
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
")).expect("test");
|
||||
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||
ctx.read().unwrap().morphisms
|
||||
.apply_list_map_morphism::<char, u64>(
|
||||
rt_digitseq, src_type, dst_type
|
||||
);
|
||||
|
||||
rebuild_projections(
|
||||
ctx.clone(),
|
||||
rt_int.clone(),
|
||||
vec![
|
||||
// Little Endian Editor
|
||||
// convert to different digit-representation
|
||||
(
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||
),
|
||||
// Radix Convert
|
||||
(
|
||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||
),
|
||||
].into_iter()
|
||||
)
|
||||
].into_iter()
|
||||
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||
.collect()
|
||||
);
|
||||
|
@ -272,7 +236,8 @@ async fn main() {
|
|||
~ <List Char>
|
||||
")).expect("descend"),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
).unwrap();
|
||||
).unwrap().get();
|
||||
|
||||
let edittree_hex_be_list = ctx.read().unwrap()
|
||||
.setup_edittree(
|
||||
rt_int.descend(Context::parse(&ctx,"
|
||||
|
@ -282,23 +247,9 @@ async fn main() {
|
|||
~ <List Char>
|
||||
")).expect("descend"),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
).unwrap();
|
||||
).unwrap().get();
|
||||
|
||||
|
||||
|
||||
let rt_digitseq =
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
")).expect("test");
|
||||
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||
ctx.read().unwrap().morphisms
|
||||
.apply_list_map_morphism::<char, u64>(
|
||||
rt_digitseq, src_type, dst_type
|
||||
);
|
||||
|
||||
let hex_digits_view = rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16> >
|
||||
|
@ -328,15 +279,15 @@ async fn main() {
|
|||
/* list of both editors
|
||||
*/
|
||||
let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "<Seq Char>"));
|
||||
list_editor.data.push( edittree_hex_be_list.value.clone() );
|
||||
list_editor.data.push( edittree_hex_le_list.value.clone() );
|
||||
list_editor.data.push( edittree_hex_be_list.clone() );
|
||||
list_editor.data.push( edittree_hex_le_list.clone() );
|
||||
let mut edittree = list_editor.into_node(SingletonBuffer::new(0).get_port());
|
||||
|
||||
/* cursors are a bit screwed initially so fix them up
|
||||
* TODO: how to fix this generally?
|
||||
*/
|
||||
edittree_hex_be_list.get().goto(TreeCursor::none());
|
||||
edittree_hex_le_list.get().goto(TreeCursor::none());
|
||||
edittree_hex_be_list.write().unwrap().goto(TreeCursor::none());
|
||||
edittree_hex_le_list.write().unwrap().goto(TreeCursor::none());
|
||||
edittree.goto(TreeCursor{
|
||||
leaf_mode: nested::editors::list::ListCursorMode::Insert,
|
||||
tree_addr: vec![1,0]
|
||||
|
@ -393,7 +344,7 @@ async fn main() {
|
|||
{
|
||||
let rt_edittree = rt.descend(Context::parse(&ctx, "EditTree")).expect("descend");
|
||||
let halo_type = rt_edittree.read().unwrap().get_halo_type().clone();
|
||||
let edittree = rt_edittree.read().unwrap().get_view::<dyn r3vi::view::singleton::SingletonView<Item = EditTree>>().unwrap().get();
|
||||
let edittree = rt_edittree.read().unwrap().get_view::<dyn r3vi::view::singleton::SingletonView<Item = Arc<RwLock<EditTree>>>>().unwrap().get().read().unwrap().clone();
|
||||
|
||||
comp.push( nested_tty::make_label( &ctx.read().unwrap().type_term_to_str(&halo_type) )
|
||||
.map_item(|_pt, atom| atom.add_style_front(TerminalStyle::fg_color((90,90,90))))
|
||||
|
|
|
@ -56,7 +56,12 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
|||
|
||||
rt.insert_leaf(
|
||||
Context::parse(&ctx, "EditTree"),
|
||||
ReprLeaf::from_singleton_buffer(SingletonBuffer::new(edittree))
|
||||
ReprLeaf::from_singleton_buffer(SingletonBuffer::new(Arc::new(RwLock::new(edittree))))
|
||||
);
|
||||
|
||||
ctx.read().unwrap().setup_edittree(
|
||||
rt.clone(),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -19,7 +19,7 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
|||
|
||||
// todo: proper scoping of Radix variable
|
||||
ctx.write().unwrap().add_varname("Radix");
|
||||
|
||||
/*
|
||||
let morphtype =
|
||||
crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<Digit Radix>"),
|
||||
|
@ -76,7 +76,7 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
|||
}
|
||||
}
|
||||
);
|
||||
|
||||
*/
|
||||
let morphtype =
|
||||
crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<Digit Radix>~Char"),
|
||||
|
|
|
@ -24,7 +24,7 @@ use {
|
|||
|
||||
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||
ctx.write().unwrap().add_varname("Item");
|
||||
|
||||
/*
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Char>"),
|
||||
dst_type: Context::parse(&ctx, "<List Char~EditTree>")
|
||||
|
@ -66,7 +66,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
}
|
||||
}
|
||||
});
|
||||
|
||||
*/
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Item>~<List EditTree>~<Vec EditTree>"),
|
||||
dst_type: Context::parse(&ctx, "<List Item>~EditTree")
|
||||
|
@ -94,7 +94,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
Context::parse(&ctx, "<List Item> ~ EditTree")
|
||||
.apply_substitution(&|id| σ.get(id).cloned()).clone(),
|
||||
ReprLeaf::from_singleton_buffer(
|
||||
SingletonBuffer::new(edittree_list)
|
||||
SingletonBuffer::new(Arc::new(RwLock::new(edittree_list)))
|
||||
)
|
||||
);
|
||||
} else {
|
||||
|
@ -115,9 +115,9 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
let edittree =
|
||||
src_rt
|
||||
.descend(Context::parse(&ctx, "<List Char>~EditTree")).unwrap()
|
||||
.singleton_buffer::<EditTree>();
|
||||
.singleton_buffer::<Arc<RwLock<EditTree>>>();
|
||||
|
||||
let list_edit = edittree.get().get_edit::< ListEditor >().unwrap();
|
||||
let list_edit = edittree.get().read().unwrap().get_edit::< ListEditor >().unwrap();
|
||||
let edittree_items = list_edit.read().unwrap().data.get_port().to_list();
|
||||
|
||||
src_rt.insert_leaf(
|
||||
|
|
|
@ -327,7 +327,8 @@ impl ListEditor {
|
|||
|
||||
if let Some(edittree) = et.as_mut(){
|
||||
|
||||
let mut tail_node = edittree.get_mut();
|
||||
let mut tail_node = edittree.get();
|
||||
let mut tail_node = tail_node.write().unwrap();
|
||||
tail_node.goto(TreeCursor::home());
|
||||
|
||||
for node in b.iter() {
|
||||
|
@ -353,7 +354,7 @@ impl ListEditor {
|
|||
drop(tail_node);
|
||||
|
||||
self.insert(
|
||||
edittree.value.clone()
|
||||
edittree.value.read().unwrap().clone()
|
||||
);
|
||||
|
||||
}
|
||||
|
|
|
@ -179,25 +179,14 @@ impl Context {
|
|||
&self,
|
||||
rt: Arc<RwLock<ReprTree>>,
|
||||
depth: OuterViewPort<dyn SingletonView<Item = usize>>
|
||||
) -> Option<SingletonBuffer<EditTree>> {
|
||||
let ladder = TypeTerm::Ladder(vec![
|
||||
rt.read().unwrap().get_type().clone(),
|
||||
self.type_term_from_str("EditTree").expect("")
|
||||
]);
|
||||
|
||||
self.morphisms.apply_morphism(
|
||||
rt.clone(),
|
||||
&rt.get_type(),
|
||||
&ladder
|
||||
);
|
||||
|
||||
) -> Option<SingletonBuffer<Arc<RwLock<EditTree>>>> {
|
||||
if let Some(new_edittree) =
|
||||
rt.descend(self.type_term_from_str("EditTree").unwrap())
|
||||
{
|
||||
let typ = rt.read().unwrap().get_type().clone();
|
||||
let buf = new_edittree.singleton_buffer::<EditTree>();
|
||||
let buf = new_edittree.singleton_buffer::<Arc<RwLock<EditTree>>>();
|
||||
(*self.edittree_hook)(
|
||||
&mut *buf.get_mut(),
|
||||
&mut *buf.get().write().unwrap(),
|
||||
typ
|
||||
);
|
||||
Some(buf)
|
||||
|
|
|
@ -65,9 +65,48 @@ impl MorphismBase {
|
|||
&self,
|
||||
src_type: &TypeTerm,
|
||||
dst_type: &TypeTerm
|
||||
) -> Option<(&GenericReprTreeMorphism, HashMap<TypeID, TypeTerm>)> {
|
||||
for m in self.morphisms.iter() {
|
||||
) -> Option<(GenericReprTreeMorphism, HashMap<TypeID, TypeTerm>)> {
|
||||
|
||||
// try list-map morphism
|
||||
if let Ok(σ) = laddertypes::UnificationProblem::new(vec![
|
||||
(src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(TypeID::Fun(10)), TypeTerm::TypeID(TypeID::Var(100)) ])),
|
||||
(dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(TypeID::Fun(10)), TypeTerm::TypeID(TypeID::Var(101)) ])),
|
||||
]).solve() {
|
||||
let src_item_type = σ.get(&TypeID::Var(100)).unwrap().clone();
|
||||
let dst_item_type = σ.get(&TypeID::Var(101)).unwrap().clone();
|
||||
/*
|
||||
eprintln!("Got a List- Type, check if we find a list-map morphism");
|
||||
eprintln!("src-item-type : {:?}", src_item_type);
|
||||
eprintln!("dst-item-type : {:?}", dst_item_type);
|
||||
*/
|
||||
let src_item_type_lnf = src_item_type.clone().get_lnf_vec();
|
||||
let dst_item_type_lnf = dst_item_type.clone().get_lnf_vec();
|
||||
|
||||
/* if src_item_type ~== "Char",
|
||||
dst_item_type ~== "machine.UInt64"
|
||||
*/
|
||||
if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(0))) &&
|
||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(4)))
|
||||
{
|
||||
if let Some((m, σ)) = self.find_list_map_morphism::< char, u64 >( src_item_type, dst_item_type ) {
|
||||
return Some((m, σ));
|
||||
}
|
||||
}
|
||||
|
||||
/* if src_item_type ~== "Char"
|
||||
dst_item_type ~== "EditTree"
|
||||
*/
|
||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(0))) &&
|
||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(1)))
|
||||
{
|
||||
if let Some((m, σ)) = self.find_list_map_morphism::< char, Arc<RwLock<crate::edit_tree::EditTree>> >( src_item_type, dst_item_type ) {
|
||||
return Some((m, σ));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// otherwise
|
||||
for m in self.morphisms.iter() {
|
||||
let unification_problem = laddertypes::UnificationProblem::new(
|
||||
vec![
|
||||
( src_type.clone().normalize(), m.morph_type.src_type.clone() ),
|
||||
|
@ -77,7 +116,7 @@ impl MorphismBase {
|
|||
|
||||
let unification_result = unification_problem.solve();
|
||||
if let Ok(σ) = unification_result {
|
||||
return Some((m, σ));
|
||||
return Some((m.clone(), σ));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -90,7 +129,7 @@ impl MorphismBase {
|
|||
src_type: &TypeTerm,
|
||||
dst_type: &TypeTerm,
|
||||
) -> Option<(
|
||||
&GenericReprTreeMorphism,
|
||||
GenericReprTreeMorphism,
|
||||
TypeTerm,
|
||||
HashMap<TypeID, TypeTerm>
|
||||
)> {
|
||||
|
@ -129,33 +168,21 @@ impl MorphismBase {
|
|||
}
|
||||
}
|
||||
|
||||
pub fn apply_list_map_morphism<
|
||||
pub fn find_list_map_morphism<
|
||||
SrcItem: Clone + Send + Sync + 'static,
|
||||
DstItem: Clone + Send + Sync + 'static
|
||||
>(
|
||||
&self,
|
||||
repr_tree: Arc<RwLock<ReprTree>>,
|
||||
mut src_item_type: TypeTerm,
|
||||
mut dst_item_type: TypeTerm
|
||||
) {
|
||||
if let Some((item_morphism, s, σ)) = self.find_morphism_ladder( &src_item_type, &dst_item_type ) {
|
||||
let sl = s.get_lnf_vec().len()+1;
|
||||
) -> Option<
|
||||
( GenericReprTreeMorphism, HashMap< TypeID, TypeTerm > )
|
||||
>
|
||||
{
|
||||
if let Some((item_morphism, σ)) = self.find_morphism( &src_item_type, &dst_item_type ) {
|
||||
(&mut src_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||
(&mut dst_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||
|
||||
let src_item_type =
|
||||
TypeTerm::Ladder({
|
||||
let mut l = src_item_type.clone().get_lnf_vec();
|
||||
for i in 0..sl { l.remove(0); }
|
||||
l
|
||||
});
|
||||
let dst_item_type =
|
||||
TypeTerm::Ladder({
|
||||
let mut l = dst_item_type.clone().get_lnf_vec();
|
||||
for i in 0..sl { l.remove(0); }
|
||||
l
|
||||
});
|
||||
|
||||
|
||||
let src_lst_type =
|
||||
TypeTerm::App(vec![
|
||||
TypeTerm::TypeID(TypeID::Fun(10 /* FIXME: remove magic */)),
|
||||
|
@ -167,37 +194,54 @@ impl MorphismBase {
|
|||
dst_item_type.clone()
|
||||
]);
|
||||
|
||||
let src_port = repr_tree.descend( src_lst_type ).expect("descend src seq")
|
||||
.view_list::<SrcItem>();
|
||||
let sigmalol = σ.clone();
|
||||
let m = GenericReprTreeMorphism{
|
||||
morph_type: MorphismType {
|
||||
src_type: src_lst_type.clone(),
|
||||
dst_type: dst_lst_type.clone(),
|
||||
},
|
||||
setup_projection: Arc::new(move |repr_tree, subst| {
|
||||
let src_port = repr_tree.descend( src_lst_type.clone() ).expect("descend src seq")
|
||||
.view_list::<SrcItem>();
|
||||
|
||||
let dst_view = src_port.map({
|
||||
let dst_item_type = dst_item_type.clone();
|
||||
let item_morphism = item_morphism.clone();
|
||||
move |x| {
|
||||
let mut item_ladder = src_item_type.clone().get_lnf_vec();
|
||||
let mut item_rt = ReprTree::from_singleton_buffer(
|
||||
item_ladder.remove( item_ladder.len() - 1 ),
|
||||
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
||||
let src_item_type = src_item_type.clone();
|
||||
let dst_item_type = dst_item_type.clone();
|
||||
let item_morphism = item_morphism.clone();
|
||||
let subst = subst.clone();
|
||||
|
||||
let dst_view = src_port.map(
|
||||
move |x| {
|
||||
let mut item_ladder = src_item_type.clone().get_lnf_vec();
|
||||
let mut item_rt = ReprTree::from_singleton_buffer(
|
||||
item_ladder.remove( item_ladder.len() - 1 ),
|
||||
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
||||
);
|
||||
|
||||
while item_ladder.len() > 0 {
|
||||
let mut n = ReprTree::new_arc( item_ladder.remove( item_ladder.len() - 1) );
|
||||
n.insert_branch( item_rt );
|
||||
item_rt = n;
|
||||
}
|
||||
|
||||
(item_morphism.setup_projection)( &mut item_rt, &subst );
|
||||
item_rt.descend( dst_item_type.clone() ).expect("descend to item rt")
|
||||
.view_singleton::< DstItem >()
|
||||
.get_view().unwrap()
|
||||
.get()
|
||||
}
|
||||
);
|
||||
while item_ladder.len() > 0 {
|
||||
let mut n = ReprTree::new_arc( item_ladder.remove( item_ladder.len() - 1) );
|
||||
n.insert_branch( item_rt );
|
||||
item_rt = n;
|
||||
}
|
||||
(item_morphism.setup_projection)( &mut item_rt, &σ );
|
||||
item_rt.descend( dst_item_type.clone() ).expect("descend to item rt")
|
||||
.view_singleton::< DstItem >()
|
||||
.get_view().unwrap()
|
||||
.get()
|
||||
}
|
||||
});
|
||||
|
||||
repr_tree.attach_leaf_to(
|
||||
dst_lst_type,
|
||||
dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView<DstItem> >
|
||||
);
|
||||
repr_tree.attach_leaf_to(
|
||||
dst_lst_type.clone(),
|
||||
dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView<DstItem> >
|
||||
);
|
||||
})
|
||||
};
|
||||
|
||||
Some((m, σ))
|
||||
} else {
|
||||
eprintln!("could not find item morphism");
|
||||
eprintln!("could not find item morphism\n");
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -223,6 +223,17 @@ impl PTYListController {
|
|||
match cur.mode {
|
||||
ListCursorMode::Insert => {
|
||||
let rt = ReprTree::new_arc(e.typ.clone());
|
||||
|
||||
let ladder = laddertypes::TypeTerm::Ladder(vec![
|
||||
rt.read().unwrap().get_type().clone(),
|
||||
ctx.type_term_from_str("EditTree").expect("")
|
||||
]);
|
||||
ctx.morphisms.apply_morphism(
|
||||
rt.clone(),
|
||||
&rt.get_type(),
|
||||
&ladder
|
||||
);
|
||||
|
||||
let new_edittree = ctx.setup_edittree(
|
||||
rt,
|
||||
self.depth.map(|d| d+1)
|
||||
|
@ -231,10 +242,11 @@ impl PTYListController {
|
|||
if let Some(new_edittree) = new_edittree {
|
||||
|
||||
let mut ne = new_edittree.get();
|
||||
let mut ne = ne.write().unwrap();
|
||||
match ne.send_cmd_obj(cmd_obj.clone()) {
|
||||
TreeNavResult::Continue => {
|
||||
drop(ne);
|
||||
e.insert(new_edittree.value.clone());
|
||||
e.insert(new_edittree.value.read().unwrap().clone());
|
||||
TreeNavResult::Continue
|
||||
}
|
||||
TreeNavResult::Exit => {
|
||||
|
|
Loading…
Reference in a new issue