From 6e8bb0aeb5c74cb70ef3215c9b11061b2042babf Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 1 Aug 2024 18:35:57 +0200 Subject: [PATCH] apply_list_map_morphism --- examples/tty-04-posint/src/main.rs | 177 +++++++++++---------- lib-nested-core/src/editors/digit/ctx.rs | 9 +- lib-nested-core/src/editors/integer/ctx.rs | 69 ++++++-- lib-nested-core/src/repr_tree/mod.rs | 9 ++ lib-nested-core/src/repr_tree/morphism.rs | 84 ++++++++-- 5 files changed, 237 insertions(+), 111 deletions(-) diff --git a/examples/tty-04-posint/src/main.rs b/examples/tty-04-posint/src/main.rs index b48d112..2c12c17 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(), @@ -48,6 +48,8 @@ fn rebuild_projections( } fn setup_le_master(ctx: &Arc>, rt_int: &Arc>) { + rt_int.write().unwrap().detach(&ctx); + rebuild_projections( ctx.clone(), rt_int.clone(), @@ -81,51 +83,38 @@ fn setup_le_master(ctx: &Arc>, rt_int: &Arc>) { .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) .collect() ); -/* - /* - * map seq of chars to seq of u64 digits - * and add this projection to the ReprTree - */ - // - //VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV - let mut chars_view = rt_int.descend(Context::parse(&ctx, " - - ~ > - ~ ~Char> - ")).expect("cant descend") - .read().unwrap() - .get_port::>() - .unwrap(); - - let mut digits_view = chars_view - .to_sequence() - .filter_map( - |digit_char| - - /* TODO: call morphism for each item - */ - match digit_char.to_digit(16) { - Some(d) => Some(d as u64), - None => None - } + 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 ); - rt_int.attach_leaf_to(Context::parse(&ctx, " - - ~ - ~ ℤ_2^64 - ~ machine.UInt64 > - "), - digits_view.clone() + rebuild_projections( + ctx.clone(), + rt_int.clone(), + vec![ + // Radix Convert + ( + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" + ) + ].into_iter() + .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) + .collect() ); - - //ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ - // - */ } fn setup_be_master(ctx: &Arc>, rt_int: &Arc>) { + rt_int.write().unwrap().detach(&ctx); + rebuild_projections( ctx.clone(), rt_int.clone(), @@ -142,7 +131,7 @@ fn setup_be_master(ctx: &Arc>, rt_int: &Arc>) { "ℕ ~ ~ > ~ ~ Char>" ), - // Big Endian Editor + // Little Endian Editor ( "ℕ ~ ~ > ~ ~ Char>", "ℕ ~ ~ > ~ ~ Char ~ EditTree>" @@ -160,47 +149,33 @@ fn setup_be_master(ctx: &Arc>, rt_int: &Arc>) { .collect() ); - /* - /* - * map seq of chars to seq of u64 digits - * and add this projection to the ReprTree - */ - // - //VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV - let mut chars_view = rt_int.descend(Context::parse(&ctx, " - - ~ > - ~ ~Char> - ")).expect("cant descend") - .read().unwrap() - .get_port::>() - .unwrap(); - - let mut digits_view = chars_view - .to_sequence() - .filter_map( - |digit_char| - - /* TODO: call morphism for each item - */ - match digit_char.to_digit(16) { - Some(d) => Some(d as u64), - None => None - } + + 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 ); - rt_int.attach_leaf_to(Context::parse(&ctx, " - - ~ - ~ ℤ_2^64 - ~ machine.UInt64 > - "), - digits_view.clone() + rebuild_projections( + ctx.clone(), + rt_int.clone(), + vec![ + // Little Endian Editor + ( + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", + "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" + ), + ].into_iter() + .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) + .collect() ); - - //ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ - // - */ } #[async_std::main] @@ -309,6 +284,47 @@ async fn main() { SingletonBuffer::new(0).get_port() ).unwrap(); + + + 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, " + + ~ > + ~ + ~ ℤ_2^64 + ~ machine.UInt64 > + ")).expect("descend") + .view_list::() + .map(|v| TerminalAtom::from(char::from_digit(*v as u32, 16))) + .to_sequence() + .to_grid_horizontal() + ; + + let dec_digits_view = rt_int.descend(Context::parse(&ctx, " + + ~ > + ~ + ~ ℤ_2^64 + ~ machine.UInt64 > + ")).expect("descend") + .view_list::() + .map(|v| TerminalAtom::from(char::from_digit(*v as u32, 10))) + .to_sequence() + .to_grid_horizontal() + ; + /* list of both editors */ let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "")); @@ -392,18 +408,15 @@ async fn main() { /* project the seq of u64 representations to a view */ - /* comp.push(nested_tty::make_label("dec: ").offset(Vector2::new(3,7))); comp.push(dec_digits_view.offset(Vector2::new(8,7)).map_item(|_,a| { a.add_style_back(TerminalStyle::fg_color((30,90,200))) })); - */ - /* + comp.push(nested_tty::make_label("hex: ").offset(Vector2::new(3,8))); comp.push(hex_digits_view.offset(Vector2::new(8,8)).map_item(|_,a| { a.add_style_back(TerminalStyle::fg_color((200, 200, 30))) })); - */ } /* write the changes in the view of `term_port` to the terminal diff --git a/lib-nested-core/src/editors/digit/ctx.rs b/lib-nested-core/src/editors/digit/ctx.rs index b87e5ec..ea5b8d6 100644 --- a/lib-nested-core/src/editors/digit/ctx.rs +++ b/lib-nested-core/src/editors/digit/ctx.rs @@ -92,14 +92,17 @@ pub fn init_ctx( ctx: Arc> ) { move |rt: &mut Arc>, σ: &std::collections::HashMap| { /* infer radix from type */ + let radix_typeid = ctx.read().unwrap().get_var_typeid("Radix").unwrap(); let radix = - match σ.get( &laddertypes::TypeID::Var(ctx.read().unwrap().get_var_typeid("Radix").unwrap()) ) { + match σ.get( &laddertypes::TypeID::Var(radix_typeid) ) { Some(TypeTerm::Num(n)) => (*n) as u32, - _ => 0 + x => { + eprintln!("invalid radix {:?}", x); + 0 + } }; if radix <= 16 { - if let Some(src_rt) = rt.descend(Context::parse(&ctx, "Char")) { /* insert projected view into ReprTree */ diff --git a/lib-nested-core/src/editors/integer/ctx.rs b/lib-nested-core/src/editors/integer/ctx.rs index 683dc61..868acec 100644 --- a/lib-nested-core/src/editors/integer/ctx.rs +++ b/lib-nested-core/src/editors/integer/ctx.rs @@ -16,7 +16,6 @@ use { pub fn init_ctx(ctx: Arc>) { // TODO: proper scoping - ctx.write().unwrap().add_varname("Radix"); ctx.write().unwrap().add_varname("SrcRadix"); ctx.write().unwrap().add_varname("DstRadix"); @@ -281,24 +280,66 @@ pub fn init_ctx(ctx: Arc>) { } } ); +/* + let mt = MorphismType { + src_type: Context::parse(&ctx, " + ℕ + ~ + ~ > + ~ > + ~ + "), + dst_type: Context::parse(&ctx, " + ℕ + ~ + ~ > + ~ > + ~ + ") + }; + ctx.write().unwrap().morphisms.add_morphism( + mt, + { + let ctx = ctx.clone(); + move |src_rt, σ| { + let src_digits = src_rt.descend(Context::parse(&ctx, " + + ~ > + ~ ~Char > + ").apply_substitution(&|k|σ.get(k).cloned()).clone() + ).expect("cant descend") + .view_list::(); - + src_rt.attach_leaf_to( + Context::parse(&ctx, " + < PosInt Radix LittleEndian > + ~ < Seq > + ~ < List ~Char > + ").apply_substitution(&|k| σ.get(k).cloned()).clone(), + src_digits.reverse() + ); + } + } + ); +*/ let morphism_type = MorphismType { src_type: Context::parse(&ctx, " ℕ ~ - ~ + ~ > + ~ ~ ℤ_2^64 ~ machine.UInt64> "), dst_type: Context::parse(&ctx, " ℕ ~ - ~ + ~ > + ~ ~ ℤ_2^64 - ~ machine.UInt64 > + ~ machine.UInt64> ") }; @@ -323,19 +364,27 @@ pub fn init_ctx(ctx: Arc>) { let src_digits_rt = src_rt.descend(Context::parse(&ctx, " - ~ ~ ℤ_2^64 ~ machine.UInt64 > + ~ > + ~ + ~ ℤ_2^64 + ~ machine.UInt64 > ").apply_substitution(&|k|σ.get(k).cloned()).clone() ).expect("cant descend repr tree"); let dst_digits_port = - src_digits_rt.view_seq::() + src_digits_rt.view_list::() + .to_sequence() .to_positional_uint( src_radix ) - .transform_radix( dst_radix ); + .transform_radix( dst_radix ) + .to_list(); src_rt.attach_leaf_to( Context::parse(&ctx, " - - ~ ~ ℤ_2^64 ~ machine.UInt64> + + ~ > + ~ + ~ ℤ_2^64 + ~ machine.UInt64 > ").apply_substitution(&|k|σ.get(k).cloned()).clone(), dst_digits_port ); diff --git a/lib-nested-core/src/repr_tree/mod.rs b/lib-nested-core/src/repr_tree/mod.rs index 072424f..bad1396 100644 --- a/lib-nested-core/src/repr_tree/mod.rs +++ b/lib-nested-core/src/repr_tree/mod.rs @@ -515,6 +515,10 @@ impl ReprTree { //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + pub fn view_singleton(&self) -> OuterViewPort> { + self.get_port::>().expect("no singleton-view available") + } + pub fn view_seq(&self) -> OuterViewPort> { self.get_port::>().expect("no sequence-view available") } @@ -560,6 +564,7 @@ pub trait ReprTreeExt { fn view_u64(&self) -> OuterViewPort>; fn view_usize(&self) -> OuterViewPort>; + fn view_singleton(&self) -> OuterViewPort>; fn view_seq(&self) -> OuterViewPort>; fn view_list(&self) -> OuterViewPort>; @@ -622,6 +627,10 @@ impl ReprTreeExt for Arc> { self.read().unwrap().view_usize() } + fn view_singleton(&self) -> OuterViewPort> { + self.read().unwrap().view_singleton::() + } + fn view_seq(&self) -> OuterViewPort> { self.read().unwrap().view_seq::() } diff --git a/lib-nested-core/src/repr_tree/morphism.rs b/lib-nested-core/src/repr_tree/morphism.rs index 65eb5bb..d78f2c5 100644 --- a/lib-nested-core/src/repr_tree/morphism.rs +++ b/lib-nested-core/src/repr_tree/morphism.rs @@ -1,6 +1,6 @@ use { laddertypes::{TypeTerm, TypeID}, - r3vi::view::AnyOuterViewPort, + r3vi::view::{AnyOuterViewPort, port::UpdateTask}, crate::{ repr_tree::{ReprTree, ReprTreeExt, ReprLeaf}, }, @@ -128,26 +128,78 @@ impl MorphismBase { eprintln!("could not find morphism\n {:?}\n ====>\n {:?}", src_type, dst_type); } } -/* - pub fn apply_seq_map_morphism( - &self, - mut repr_tree: Arc>, - src_item_type: &TypeTerm, - dst_item_type: &TypeTerm - ) { - if let Some((item_morphism, σ)) = self.find_morphism( &src_item_type, dst_item_type ) { - let src_port = repr_tree.read().unwrap().get_port::> >>().unwrap(); - src_port.map( - m.setup_projection - ) - - (m.setup_projection)( &mut repr_tree, &σ ); + pub fn apply_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; + (&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 */)), + src_item_type.clone() + ]); + let dst_lst_type = + TypeTerm::App(vec![ + TypeTerm::TypeID(TypeID::Fun(10 /* FIXME: remove magic */)), + dst_item_type.clone() + ]); + + let src_port = repr_tree.descend( src_lst_type ).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()) + ); + 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 > + ); } else { eprintln!("could not find item morphism"); } } - */ } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>