From 7268ed9bc9b98543e3c27e0bd66388e7b55ee057 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 2 Sep 2024 00:01:25 +0200 Subject: [PATCH] morphisms to copy edittree from to --- lib-nested-core/src/editors/integer/ctx.rs | 83 +++++++++++++++++++++- 1 file changed, 82 insertions(+), 1 deletion(-) diff --git a/lib-nested-core/src/editors/integer/ctx.rs b/lib-nested-core/src/editors/integer/ctx.rs index d7df660..1165543 100644 --- a/lib-nested-core/src/editors/integer/ctx.rs +++ b/lib-nested-core/src/editors/integer/ctx.rs @@ -1,7 +1,8 @@ use { r3vi::{ - view::{OuterViewPort, singleton::*, list::*} + view::{OuterViewPort, singleton::*, list::*}, + buffer::singleton::SingletonBuffer }, laddertypes::{TypeTerm, MorphismType}, crate::{ @@ -211,6 +212,86 @@ pub fn init_ctx(ctx: Arc>) { } ); + let posint_make_edittree = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ ~ > ~ EditTree"), + Context::parse(&ctx, "ℕ ~ ~ EditTree"), + { + 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().clone() + .read().unwrap() + .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( + Arc::new(RwLock::new(list_edittree)) + ) + ) + ); + + ctx.read().unwrap().setup_edittree( + &src_rt.descend( + Context::parse(&ctx, "") + .apply_substitution(&|x| σ.get(x).cloned()).clone() + ).unwrap() + ); + } + } + ); + + let posint_edittree_to_list = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ ~ EditTree"), + Context::parse(&ctx, "ℕ ~ ~ > ~ EditTree"), + { + 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().clone() + .read().unwrap() + .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( + Arc::new(RwLock::new(list_edittree)) + ) + ) + ); + + ctx.read().unwrap().setup_edittree( + &src_rt.descend( + Context::parse(&ctx, " ~ >") + .apply_substitution(&|x| σ.get(x).cloned()).clone() + ).unwrap() + ); + } + } + ); + + ctx.write().unwrap().morphisms.add_morphism( posint_make_edittree ); + ctx.write().unwrap().morphisms.add_morphism( posint_edittree_to_list ); + ctx.write().unwrap().morphisms.add_morphism( posint_seq_morph_big_to_little ); ctx.write().unwrap().morphisms.add_morphism( posint_list_morph_big_to_little ); ctx.write().unwrap().morphisms.add_morphism( posint_list_morph_little_to_big );