From 278296cfbb8e59076ee8ab2697e12b2690805f2a Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 5 Jan 2025 03:53:59 +0100 Subject: [PATCH] fix morphisms for Digit & PosInt editors --- examples/tty-04-posint/src/main.rs | 20 ++-- examples/tty-05-dictionary/src/main.rs | 29 +++--- lib-nested-core/src/editors/char/ctx.rs | 2 - lib-nested-core/src/editors/digit/ctx.rs | 92 ++++++++++++------ lib-nested-core/src/editors/integer/ctx.rs | 104 +++++++++++---------- lib-nested-core/src/editors/integer/mod.rs | 6 +- lib-nested-core/src/editors/list/ctx.rs | 91 +++++++++++++++++- lib-nested-core/src/editors/list/editor.rs | 11 ++- lib-nested-core/src/repr_tree/builder.rs | 13 ++- 9 files changed, 254 insertions(+), 114 deletions(-) diff --git a/examples/tty-04-posint/src/main.rs b/examples/tty-04-posint/src/main.rs index ee7419e..5f9e032 100644 --- a/examples/tty-04-posint/src/main.rs +++ b/examples/tty-04-posint/src/main.rs @@ -49,20 +49,18 @@ async fn main() { */ let int_builder = ReprTreeBuilder::new( ctx.clone() ) .require(Context::parse(&ctx, - "ℕ ~ ~ ~Char> ~ EditTree")) + "ℕ ~ ~ EditTree")) .require(Context::parse(&ctx, - "ℕ ~ ~ ~Char> ~ EditTree")) - /* + "ℕ ~ ~ EditTree")) .require(Context::parse(&ctx, "ℕ ~ ~ EditTree")) .require(Context::parse(&ctx, "ℕ ~ ~ EditTree")) - */ ; - let mut rt_int = nested::repr_tree::ReprTree::from_str("f"); + let mut rt_int = nested::repr_tree::ReprTree::from_str("3"); rt_int.write().unwrap().set_halo( - /* HALO TYPE */ + /* HALO TYPE (append to top of type ladder) */ Context::parse(&ctx, " ℕ ~ @@ -78,7 +76,11 @@ async fn main() { /* list of editors */ - let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "")); + let mut list_editor = nested::editors::list::ListEditor::new( + ctx.clone(), + Context::parse(&ctx, "EditTree"), + ReprTreeBuilder::new(ctx.clone()) + ); // add all desired editors to the list for edit_leaf in int_builder.required_leaves.iter() { @@ -97,7 +99,7 @@ async fn main() { leaf_rt.edittree(&ctx).get_mut().goto(TreeCursor::none()); } - let first_idx : usize = 1; + let first_idx : usize = 0; int_builder.update( &rt_int, int_builder.required_leaves[first_idx].clone() ); edittree.goto(TreeCursor{ @@ -124,9 +126,7 @@ async fn main() { let ci = cur.tree_addr[0]; if *li != ci as usize { - eprintln!("--------\nCHANGE MASTER EDITOR\n--------------------"); int_builder.update( &rt_int, int_builder.required_leaves[ci as usize].clone() ); - eprintln!("-----\nDone\n----"); *li = ci as usize; } } diff --git a/examples/tty-05-dictionary/src/main.rs b/examples/tty-05-dictionary/src/main.rs index 8536c11..c3e43b3 100644 --- a/examples/tty-05-dictionary/src/main.rs +++ b/examples/tty-05-dictionary/src/main.rs @@ -166,18 +166,23 @@ async fn main() { ")); let symbol_builder = ReprTreeBuilder::new( ctx.clone() ) - //.require(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ~ EditTree")) .require(Context::parse(&ctx, "Instruction ~ Mnemonic ~ ~ EditTree")) + .require(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ~ EditTree")) + .require(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ~ EditTree")) ; symbol_rt = symbol_builder.build_from(symbol_rt).expect("failed to build symbol repr-tree"); - let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "")); + let mut list_editor = nested::editors::list::ListEditor::new( + ctx.clone(), + Context::parse(&ctx, ""), + ReprTreeBuilder::new(ctx.clone()), + ); // add all desired editors to the list - for edit_leaf in symbol_builder.required_leaves { + for edit_leaf in symbol_builder.required_leaves.iter() { let leaf_rt = symbol_rt.descend(edit_leaf.clone()).unwrap(); - list_editor.data.push(leaf_rt); + list_editor.insert(leaf_rt); } let mut edittree = list_editor.into_node(SingletonBuffer::new(0).get_port()); @@ -195,17 +200,17 @@ async fn main() { /* event handler */ let ctx = ctx.clone(); - let symbol_rt = symbol_rt.clone(); - let last_idx = RwLock::new(0); + let symbol_rt = symbol_rt.clone(); //let symbol_builder = symbol_builder.clone(); + let last_idx = RwLock::new(99999); move |ev| { let cur = edittree.read().unwrap().get_cursor(); if cur.tree_addr.len() > 0 { let mut li = last_idx.write().unwrap(); let ci = cur.tree_addr[0]; - if *li != ci { - // symbol_builder.update() - *li = ci; + if *li != ci as usize { + symbol_builder.update( &symbol_rt, symbol_builder.required_leaves[ci as usize].clone() ); + *li = ci as usize; } } @@ -232,7 +237,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().read().unwrap().clone(); + let edittree = rt_edittree.edittree(&ctx).get(); 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)))) @@ -246,8 +251,8 @@ async fn main() { } show_edit_tree( &ctx, &mut comp, &symbol_rt.descend(Context::parse(&ctx, "Instruction ~ Mnemonic ~ ")).unwrap(), 1 ); - //show_edit_tree( &ctx, &mut comp, &symbol_rt.descend(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ")).unwrap(), 3 ); - //show_edit_tree( &ctx, &mut comp, &symbol_rt.descend(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ")).unwrap(), 5 ); + show_edit_tree( &ctx, &mut comp, &symbol_rt.descend(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ")).unwrap(), 3 ); + show_edit_tree( &ctx, &mut comp, &symbol_rt.descend(Context::parse(&ctx, "Instruction ~ Opcode ~ ℕ ~ ")).unwrap(), 5 ); } /* write the changes in the view of `term_port` to the terminal diff --git a/lib-nested-core/src/editors/char/ctx.rs b/lib-nested-core/src/editors/char/ctx.rs index a4dd6db..e689512 100644 --- a/lib-nested-core/src/editors/char/ctx.rs +++ b/lib-nested-core/src/editors/char/ctx.rs @@ -33,7 +33,6 @@ pub fn init_ctx( ctx: Arc> ) { if let Some(buf) = b { // buffer already exists } else { - eprintln!("create char buffer"); // create char buffer rt.write().unwrap().insert_leaf( vec![].into_iter(), @@ -73,7 +72,6 @@ pub fn init_ctx( ctx: Arc> ) { .singleton_buffer::(); if rt.write().unwrap().singleton_buffer::().is_none() { - eprintln!("insert singleton buffer"); rt.insert_leaf( Context::parse(&ctx, "Char"), ReprLeaf::from_singleton_buffer( diff --git a/lib-nested-core/src/editors/digit/ctx.rs b/lib-nested-core/src/editors/digit/ctx.rs index c2250cd..692cbf5 100644 --- a/lib-nested-core/src/editors/digit/ctx.rs +++ b/lib-nested-core/src/editors/digit/ctx.rs @@ -31,31 +31,68 @@ pub fn init_ctx( ctx: Arc> ) { _ => 0 }; - let char_buf = SingletonBuffer::::new('?'); + let char_rt = src_rt.descend_create(Context::parse(&ctx, "Char")).unwrap(); + let char_buf = { + let mut b = char_rt.write().unwrap().singleton_buffer::(); + if let Some(buf) = b { + // buffer already exists + eprintln!("take existing char buffer"); + buf + } else { + // create char buffer + eprintln!("create char buffer"); + let char_buf = SingletonBuffer::::new('?'); + src_rt.insert_leaf( + Context::parse(&ctx, "Char"), + ReprLeaf::from_singleton_buffer(char_buf.clone()) + ); + char_buf + } + }; /* Create EditTree object */ - let mut edittree = DigitEditor::new( - ctx.clone(), - radix, - char_buf - ).into_node( - r3vi::buffer::singleton::SingletonBuffer::::new(0).get_port() - ); - - src_rt.write().unwrap() - .insert_branch( - ReprTree::from_singleton_buffer( - Context::parse(&ctx, "EditTree"), - SingletonBuffer::new(edittree) - ) + //if src_rt.descend(Context::parse(&ctx, "EditTree")).is_none() { + eprintln!("create Digit-Editor"); + let mut edittree = DigitEditor::new( + ctx.clone(), + radix, + char_buf + ).into_node( + r3vi::buffer::singleton::SingletonBuffer::::new(0).get_port() ); - ctx.read().unwrap().setup_edittree( src_rt ); + src_rt.write().unwrap() + .insert_branch( + ReprTree::from_singleton_buffer( + Context::parse(&ctx, "EditTree"), + SingletonBuffer::new(edittree) + ) + ); + + ctx.read().unwrap().setup_edittree( src_rt ); + //} } } ); +/* + let digit_morph_char_to_digit = GenericReprTreeMorphism::new( + Context::parse(&ctx, "Char"), + Context::parse(&ctx, "~Char"), + { + let ctx = ctx.clone(); + move |src_rt, σ| { + src_rt.write().unwrap().set_halo( + Context::parse(&ctx, "") + .apply_substitution(&|k|σ.get(k).cloned()) + .clone() + ); + } + } + ); + */ + let digit_morph_char_to_edittree = GenericReprTreeMorphism::new( Context::parse(&ctx, "~Char"), Context::parse(&ctx, "~EditTree"), @@ -85,6 +122,7 @@ pub fn init_ctx( ctx: Arc> ) { .insert_branch( ReprTree::from_singleton_buffer( Context::parse(&ctx, "EditTree"), + SingletonBuffer::new(edittree) ) ); @@ -101,18 +139,20 @@ pub fn init_ctx( ctx: Arc> ) { { let ctx = ctx.clone(); move |src_rt, σ| { - let edittree = src_rt.edittree( &ctx ); - let port = - edittree - .get() - .get_edit::().unwrap() - .read().unwrap() - .get_char_port(); - src_rt.insert_leaf( + src_rt.attach_leaf_to( Context::parse(&ctx, "Char"), - ReprLeaf::from_view( port ) - ) + src_rt.edittree(&ctx) + .get_port() + .map( + |edit| { + edit.get_edit::().unwrap() + .read().unwrap() + .get_char_port() + .get_view().get() + } + ) + ); } } ); diff --git a/lib-nested-core/src/editors/integer/ctx.rs b/lib-nested-core/src/editors/integer/ctx.rs index 09552ad..78e3a6a 100644 --- a/lib-nested-core/src/editors/integer/ctx.rs +++ b/lib-nested-core/src/editors/integer/ctx.rs @@ -218,33 +218,37 @@ pub fn init_ctx(ctx: Arc>) { { let ctx = ctx.clone(); move |src_rt, σ| { - let mut list_edittree = src_rt.descend( - Context::parse(&ctx, "ℕ ~ ~ >") + if src_rt.descend( + Context::parse(&ctx, "ℕ ~ ~ EditTree") .apply_substitution(&|x| σ.get(x).cloned()).clone() - ) - .unwrap() - .edittree( &ctx ) - .get(); - - // clear display - list_edittree.disp.view = ReprTree::new_arc(Context::parse(&ctx, "Display")); -/* - src_rt.insert_leaf( - Context::parse(&ctx, " ~ EditTree") - .apply_substitution(&|x| σ.get(x).cloned()).clone(), - ReprLeaf::from_singleton_buffer( - SingletonBuffer::new( - list_edittree - ) - ) - ); -*/ - ctx.read().unwrap().setup_edittree( - &src_rt.descend( - Context::parse(&ctx, "") + ).is_none() { + let mut list_edittree = src_rt.descend( + Context::parse(&ctx, "ℕ ~ ~ >") .apply_substitution(&|x| σ.get(x).cloned()).clone() - ).unwrap() - ); + ) + .unwrap() + .edittree( &ctx ) + .get().clone(); + + // clear display + list_edittree.disp.view = ReprTree::new_arc(Context::parse(&ctx, "Display")); + src_rt.insert_leaf( + Context::parse(&ctx, " ~ EditTree") + .apply_substitution(&|x| σ.get(x).cloned()).clone(), + ReprLeaf::from_singleton_buffer( + SingletonBuffer::new( + list_edittree + ) + ) + ); + + ctx.read().unwrap().setup_edittree( + &src_rt.descend( + Context::parse(&ctx, "") + .apply_substitution(&|x| σ.get(x).cloned()).clone() + ).unwrap() + ); + } } } ); @@ -255,31 +259,35 @@ pub fn init_ctx(ctx: Arc>) { { let ctx = ctx.clone(); move |src_rt, σ| { - let mut list_edittree = src_rt.descend( - Context::parse(&ctx, "ℕ ~ ") - .apply_substitution(&|x| σ.get(x).cloned()).clone()) - .unwrap() - .edittree( &ctx ) - .get_mut(); + if src_rt.descend( + Context::parse(&ctx, "ℕ ~ ~> ~ EditTree") + .apply_substitution(&|x| σ.get(x).cloned()).clone() + ).is_none() { + let mut list_edittree = src_rt.descend( + Context::parse(&ctx, "ℕ ~ ~ EditTree") + .apply_substitution(&|x| σ.get(x).cloned()).clone()) + .unwrap() + .edittree( &ctx ) + .get().clone(); - // clear display - list_edittree.disp.view = ReprTree::new_arc(Context::parse(&ctx, "Display")); -/* - src_rt.insert_leaf( - Context::parse(&ctx, " ~ >~EditTree") - .apply_substitution(&|x| σ.get(x).cloned()).clone(), - ReprLeaf::from_singleton_buffer( - SingletonBuffer::new(list_edittree) - ) - ); -*/ + // clear display + list_edittree.disp.view = ReprTree::new_arc(Context::parse(&ctx, "Display")); - ctx.read().unwrap().setup_edittree( - &src_rt.descend( - Context::parse(&ctx, " ~ >") - .apply_substitution(&|x| σ.get(x).cloned()).clone() - ).unwrap() - ); + src_rt.insert_leaf( + Context::parse(&ctx, " ~ >~EditTree") + .apply_substitution(&|x| σ.get(x).cloned()).clone(), + ReprLeaf::from_singleton_buffer( + SingletonBuffer::new(list_edittree) + ) + ); + + ctx.read().unwrap().setup_edittree( + &src_rt.descend( + Context::parse(&ctx, " ~ >") + .apply_substitution(&|x| σ.get(x).cloned()).clone() + ).unwrap() + ); + } } } ); diff --git a/lib-nested-core/src/editors/integer/mod.rs b/lib-nested-core/src/editors/integer/mod.rs index c0d59d4..4eaabb8 100644 --- a/lib-nested-core/src/editors/integer/mod.rs +++ b/lib-nested-core/src/editors/integer/mod.rs @@ -5,7 +5,7 @@ pub mod ctx; pub use { add::Add, - editor::PosIntEditor, + //editor::PosIntEditor, radix::RadixProjection, ctx::init_ctx }; @@ -41,7 +41,7 @@ pub trait PositionalUInt : SequenceView { } } - val + val } } @@ -146,5 +146,3 @@ impl Observer for PosUIntToDigits { self.cast.notify(idx); } } - - diff --git a/lib-nested-core/src/editors/list/ctx.rs b/lib-nested-core/src/editors/list/ctx.rs index 098c6b2..1d00b34 100644 --- a/lib-nested-core/src/editors/list/ctx.rs +++ b/lib-nested-core/src/editors/list/ctx.rs @@ -3,7 +3,7 @@ use { edit_tree::EditTree, editors::{ char::CharEditor, list::ListEditor - }, repr_tree::{context::TYPEID_char, Context, GenericReprTreeMorphism, ReprLeaf, ReprTree, ReprTreeArc, ReprTreeExt} + }, repr_tree::{context::TYPEID_char, Context, GenericReprTreeMorphism, ReprLeaf, ReprTree, ReprTreeArc, ReprTreeBuilder, ReprTreeExt} }, laddertypes::TypeTerm, r3vi::{ buffer::{singleton::*, vec::*}, view::{ list::*, port::UpdateTask, singleton::*, Observer, OuterViewPort, ViewPort @@ -166,7 +166,34 @@ pub fn init_ctx__unpack_reprtree( ctx: &Arc> ) { } ); + /* + * note: this requires ReprTree to contain Char repr. + * todo: how to formally require and enforce this? + */ + let list_morph_rt_to_digit_char = GenericReprTreeMorphism::new( + Context::parse(&ctx, "> ~ "), + Context::parse(&ctx, "> ~ "), + { + let ctx = ctx.clone(); + move |src_rt, σ| { + src_rt.attach_leaf_to( + Context::parse(&ctx, ""), + src_rt.descend(Context::parse(&ctx, "")).expect("cant descend") + .view_list::() + .map({ let ctx = ctx.clone(); + move |rt| { + rt.descend(Context::parse(&ctx, "Char")).expect("cant descend to char") + .view_singleton::() + .get_view() + .get() + }}) + ); + } + } + ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_rt_to_char ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_rt_to_digit_char ); } pub fn init_ctx__pack_reprtree( ctx: &Arc> ) { @@ -177,7 +204,7 @@ pub fn init_ctx__pack_reprtree( ctx: &Arc> ) { let ctx = ctx.clone(); move |src_rt, σ| { src_rt.attach_leaf_to( - Context::parse(&ctx, "~"), + Context::parse(&ctx, " ~ "), src_rt.view_list::() .map(|c| { ReprTree::from_singleton_buffer( @@ -189,7 +216,45 @@ pub fn init_ctx__pack_reprtree( ctx: &Arc> ) { } } ); + + let list_morph_digit_rt_from_char_rt = GenericReprTreeMorphism::new( + Context::parse(&ctx, "> ~ ~ "), + Context::parse(&ctx, "> ~ "), + { + let ctx = ctx.clone(); + move |src_rt, σ| { + let ty_digit = Context::parse(&ctx, "") + .apply_substitution(&|k|σ.get(k).cloned()) + .clone(); + let ty_digit_as_char = Context::parse(&ctx, " ~ Char") + .apply_substitution(&|k|σ.get(k).cloned()) + .clone(); + + // list item builder + let item_builder = ReprTreeBuilder::new(ctx.clone()) + .require(ty_digit_as_char.clone()) + ; + + src_rt.attach_leaf_to( + Context::parse(&ctx, ""), + src_rt.descend(Context::parse(&ctx, "")).expect("cant descend to ") + .view_list::() + .map({ let ctx = ctx.clone(); + let σ = σ.clone(); + move |rt| { + rt.write().unwrap().set_halo(ty_digit.clone()); + let new_rt = item_builder.build_from(rt.clone()).expect("cant build item repr tree"); + eprintln!("morph ~Char> to :: new_rt = \n{}\n", new_rt.read().unwrap().fmt(&ctx, 0)); + new_rt + } + }) + ); + } + } + ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_rt_from_char ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_digit_rt_from_char_rt ); } pub fn init_ctx(ctx: Arc>) { @@ -221,8 +286,26 @@ pub fn init_ctx(ctx: Arc>) { list_editor.data = item_vec_buffer; list_editor.update_item_reprtrees(&item_type); } else { - let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer); - list_editor.update_item_reprtrees(&item_type); + let mut item_builder = ReprTreeBuilder::new(ctx.clone()); + let mut item_type = item_type.clone(); +/* + if item_type == &Context::parse(&ctx, "Char") { + item_builder = item_builder.require( + Context::parse(&ctx, "Char") + ); + } + if item_type == &Context::parse(&ctx, "") { + item_builder = item_builder.require( + Context::parse(&ctx, "~Char") + ); + } + if item_type == &Context::parse(&ctx, "") { + item_builder = item_builder.require( + Context::parse(&ctx, "~Char") + ); + } +*/ + let mut list_editor = ListEditor::with_data(ctx.clone(), item_type, item_builder, item_vec_buffer); let mut edittree_list = list_editor.into_node( SingletonBuffer::::new(0).get_port() ); diff --git a/lib-nested-core/src/editors/list/editor.rs b/lib-nested-core/src/editors/list/editor.rs index 1a76e84..9846026 100644 --- a/lib-nested-core/src/editors/list/editor.rs +++ b/lib-nested-core/src/editors/list/editor.rs @@ -34,11 +34,13 @@ pub struct ListEditor { impl ListEditor { pub fn new( ctx: Arc>, - typ: TypeTerm + typ: TypeTerm, + item_builder: ReprTreeBuilder ) -> Self { Self::with_data( ctx, typ, + item_builder, VecBuffer::new() ) } @@ -46,9 +48,11 @@ impl ListEditor { pub fn with_data( ctx: Arc>, typ: TypeTerm, + item_builder: ReprTreeBuilder, data: VecBuffer< ReprTreeArc > ) -> Self { let cursor = SingletonBuffer::new(ListCursor::default()); + eprintln!("make list editor of type {}\n", ctx.read().unwrap().type_term_to_str(&typ) ); let mut le = ListEditor { mode_port: cursor @@ -109,8 +113,8 @@ impl ListEditor { cursor, data, spillbuf: Arc::new(RwLock::new(Vec::new())), - item_builder: ReprTreeBuilder::new(ctx.clone()) - .require( typ.clone() ) + item_builder: item_builder + //.require( typ.clone() ) .require( TypeTerm::Ladder(vec![ typ.clone(), TypeTerm::TypeID(TYPEID_edittree) @@ -292,6 +296,7 @@ impl ListEditor { /// insert a new element pub fn insert(&mut self, item: ReprTreeArc) { + eprintln!("List: insert {}", item.read().unwrap().fmt(&self.ctx, 0)); self.item_builder.update( &item, self.master_repr.read().unwrap().clone() ); let mut item_edit = item.edittree(&self.ctx).get_mut(); diff --git a/lib-nested-core/src/repr_tree/builder.rs b/lib-nested-core/src/repr_tree/builder.rs index bb8f763..47002f6 100644 --- a/lib-nested-core/src/repr_tree/builder.rs +++ b/lib-nested-core/src/repr_tree/builder.rs @@ -44,8 +44,11 @@ impl ReprTreeBuilder { } /// Add a type to the set of required representations. - pub fn require(mut self, t: TypeTerm) -> Self { - self.required_leaves.push(t.normalize()); + pub fn require(mut self, mut t: TypeTerm) -> Self { + t = t.normalize(); + if !self.required_leaves.contains(&t) { + self.required_leaves.push(t); + } self } @@ -68,14 +71,14 @@ impl ReprTreeBuilder { leaves.retain(|t| t != &mt); let mut st_problem = laddertypes::steiner_tree::PathApproxSteinerTreeSolver::new( - mt, + mt.clone(), leaves ); if let Some( steiner_tree ) = st_problem.solve( &morphism_base ) { + eprintln!("--> from {}", self.ctx.read().unwrap().type_term_to_str(&mt)); for morphism_type in steiner_tree.into_edges() { - eprintln!("--> morph {} to {}", - self.ctx.read().unwrap().type_term_to_str(&morphism_type.src_type), + eprintln!("--> morph to {}", self.ctx.read().unwrap().type_term_to_str(&morphism_type.dst_type)); if let Some(( morphism, mut τ, σ )) =