From a3c701ce88097411860ab2500e81d9aa3f521945 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Fri, 2 Aug 2024 21:58:07 +0200 Subject: [PATCH] automatically generate list-map morphisms in find_morphism() this allows us to now to create from with apply_morphism() --- examples/tty-04-posint/src/main.rs | 97 ++++---------- lib-nested-core/src/editors/char/mod.rs | 7 +- lib-nested-core/src/editors/digit/ctx.rs | 4 +- lib-nested-core/src/editors/list/ctx.rs | 10 +- lib-nested-core/src/editors/list/editor.rs | 5 +- lib-nested-core/src/repr_tree/context.rs | 17 +-- lib-nested-core/src/repr_tree/morphism.rs | 144 ++++++++++++++------- lib-nested-tty/src/editors/list.rs | 14 +- 8 files changed, 150 insertions(+), 148 deletions(-) diff --git a/examples/tty-04-posint/src/main.rs b/examples/tty-04-posint/src/main.rs index 2c12c17..67385eb 100644 --- a/examples/tty-04-posint/src/main.rs +++ b/examples/tty-04-posint/src/main.rs @@ -37,7 +37,7 @@ fn rebuild_projections( repr_tree: Arc>, 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>, rt_int: &Arc>) { - rt_int.write().unwrap().detach(&ctx); - +fn setup_le_master(ctx: &Arc>, rt_int: &Arc>) { rebuild_projections( ctx.clone(), rt_int.clone(), @@ -79,33 +77,17 @@ fn setup_le_master(ctx: &Arc>, rt_int: &Arc>) { "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ ", "ℕ ~ ~ > ~ ~ 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, " - - ~ > - ~ > - ")).expect("test"); - let src_type = Context::parse(&ctx, " ~ Char"); - let dst_type = Context::parse(&ctx, " ~ ℤ_2^64 ~ machine.UInt64"); - ctx.read().unwrap().morphisms - .apply_list_map_morphism::( - rt_digitseq, src_type, dst_type - ); - rebuild_projections( - ctx.clone(), - rt_int.clone(), - vec![ + // convert to different digit-representation + ( + "ℕ ~ ~ > ~ ~ Char>", + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" + ), // Radix Convert ( "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", "ℕ ~ ~ > ~ ~ ℤ_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>, rt_int: &Arc>) { } fn setup_be_master(ctx: &Arc>, rt_int: &Arc>) { - rt_int.write().unwrap().detach(&ctx); - rebuild_projections( ctx.clone(), rt_int.clone(), @@ -144,35 +124,19 @@ fn setup_be_master(ctx: &Arc>, rt_int: &Arc>) { "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ ", "ℕ ~ ~ > ~ ~ 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, " - - ~ > - ~ > - ")).expect("test"); - let src_type = Context::parse(&ctx, " ~ Char"); - let dst_type = Context::parse(&ctx, " ~ ℤ_2^64 ~ machine.UInt64"); - ctx.read().unwrap().morphisms - .apply_list_map_morphism::( - rt_digitseq, src_type, dst_type - ); - rebuild_projections( - ctx.clone(), - rt_int.clone(), - vec![ - // Little Endian Editor + // convert to different digit-representation + ( + "ℕ ~ ~ > ~ ~ Char>", + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" + ), + // Radix Convert ( "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", "ℕ ~ ~ > ~ ~ ℤ_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() { ~ ")).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() { ~ ")).expect("descend"), SingletonBuffer::new(0).get_port() - ).unwrap(); + ).unwrap().get(); - - let rt_digitseq = - rt_int.descend(Context::parse(&ctx, " - - ~ > - ~ > - ")).expect("test"); - let src_type = Context::parse(&ctx, " ~ Char"); - let dst_type = Context::parse(&ctx, " ~ ℤ_2^64 ~ machine.UInt64"); - ctx.read().unwrap().morphisms - .apply_list_map_morphism::( - rt_digitseq, src_type, dst_type - ); - let hex_digits_view = rt_int.descend(Context::parse(&ctx, " ~ > @@ -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, "")); - 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::>().unwrap().get(); + let edittree = rt_edittree.read().unwrap().get_view::>>>().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)))) diff --git a/lib-nested-core/src/editors/char/mod.rs b/lib-nested-core/src/editors/char/mod.rs index 5d37008..fb9abae 100644 --- a/lib-nested-core/src/editors/char/mod.rs +++ b/lib-nested-core/src/editors/char/mod.rs @@ -56,7 +56,12 @@ pub fn init_ctx( ctx: Arc> ) { 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() ); } } diff --git a/lib-nested-core/src/editors/digit/ctx.rs b/lib-nested-core/src/editors/digit/ctx.rs index ea5b8d6..538780c 100644 --- a/lib-nested-core/src/editors/digit/ctx.rs +++ b/lib-nested-core/src/editors/digit/ctx.rs @@ -19,7 +19,7 @@ pub fn init_ctx( ctx: Arc> ) { // todo: proper scoping of Radix variable ctx.write().unwrap().add_varname("Radix"); - +/* let morphtype = crate::repr_tree::MorphismType { src_type: Context::parse(&ctx, ""), @@ -76,7 +76,7 @@ pub fn init_ctx( ctx: Arc> ) { } } ); - +*/ let morphtype = crate::repr_tree::MorphismType { src_type: Context::parse(&ctx, "~Char"), diff --git a/lib-nested-core/src/editors/list/ctx.rs b/lib-nested-core/src/editors/list/ctx.rs index 839110d..d35ec7a 100644 --- a/lib-nested-core/src/editors/list/ctx.rs +++ b/lib-nested-core/src/editors/list/ctx.rs @@ -24,7 +24,7 @@ use { pub fn init_ctx(ctx: Arc>) { ctx.write().unwrap().add_varname("Item"); - +/* let mt = crate::repr_tree::MorphismType { src_type: Context::parse(&ctx, ""), dst_type: Context::parse(&ctx, "") @@ -66,7 +66,7 @@ pub fn init_ctx(ctx: Arc>) { } } }); - +*/ let mt = crate::repr_tree::MorphismType { src_type: Context::parse(&ctx, "~~"), dst_type: Context::parse(&ctx, "~EditTree") @@ -94,7 +94,7 @@ pub fn init_ctx(ctx: Arc>) { Context::parse(&ctx, " ~ 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>) { let edittree = src_rt .descend(Context::parse(&ctx, "~EditTree")).unwrap() - .singleton_buffer::(); + .singleton_buffer::>>(); - 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( diff --git a/lib-nested-core/src/editors/list/editor.rs b/lib-nested-core/src/editors/list/editor.rs index b9fa64e..04cc63b 100644 --- a/lib-nested-core/src/editors/list/editor.rs +++ b/lib-nested-core/src/editors/list/editor.rs @@ -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() ); } diff --git a/lib-nested-core/src/repr_tree/context.rs b/lib-nested-core/src/repr_tree/context.rs index 78f2ed7..71add2a 100644 --- a/lib-nested-core/src/repr_tree/context.rs +++ b/lib-nested-core/src/repr_tree/context.rs @@ -179,25 +179,14 @@ impl Context { &self, rt: Arc>, depth: OuterViewPort> - ) -> Option> { - 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>>> { 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::(); + let buf = new_edittree.singleton_buffer::>>(); (*self.edittree_hook)( - &mut *buf.get_mut(), + &mut *buf.get().write().unwrap(), typ ); Some(buf) diff --git a/lib-nested-core/src/repr_tree/morphism.rs b/lib-nested-core/src/repr_tree/morphism.rs index d78f2c5..68e837c 100644 --- a/lib-nested-core/src/repr_tree/morphism.rs +++ b/lib-nested-core/src/repr_tree/morphism.rs @@ -65,9 +65,48 @@ impl MorphismBase { &self, src_type: &TypeTerm, dst_type: &TypeTerm - ) -> Option<(&GenericReprTreeMorphism, HashMap)> { - for m in self.morphisms.iter() { + ) -> Option<(GenericReprTreeMorphism, HashMap)> { + // 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> >( 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 )> { @@ -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>, 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::(); + 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::(); - 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 > - ); + repr_tree.attach_leaf_to( + dst_lst_type.clone(), + dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView > + ); + }) + }; + + Some((m, σ)) } else { - eprintln!("could not find item morphism"); + eprintln!("could not find item morphism\n"); + None } } } diff --git a/lib-nested-tty/src/editors/list.rs b/lib-nested-tty/src/editors/list.rs index 4584e9c..f3ae4ee 100644 --- a/lib-nested-tty/src/editors/list.rs +++ b/lib-nested-tty/src/editors/list.rs @@ -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 => {