morphisms to copy edittree from <List Digit> to <PosInt ..>
This commit is contained in:
parent
38c772389f
commit
4b7d929abc
1 changed files with 82 additions and 1 deletions
|
@ -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<RwLock<Context>>) {
|
|||
}
|
||||
);
|
||||
|
||||
let posint_make_edittree = GenericReprTreeMorphism::new(
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq~List <Digit Radix>> ~ EditTree"),
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ EditTree"),
|
||||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let mut list_edittree = src_rt.descend(
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq~List <Digit Radix>>")
|
||||
.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, "<PosInt Radix BigEndian> ~ 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, "<PosInt Radix BigEndian>")
|
||||
.apply_substitution(&|x| σ.get(x).cloned()).clone()
|
||||
).unwrap()
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
let posint_edittree_to_list = GenericReprTreeMorphism::new(
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ EditTree"),
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq~List <Digit Radix>> ~ EditTree"),
|
||||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let mut list_edittree = src_rt.descend(
|
||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian>")
|
||||
.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, "<PosInt Radix BigEndian> ~ <Seq~List <Digit Radix>>~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, "<PosInt Radix BigEndian> ~ <Seq~List <Digit Radix>>")
|
||||
.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 );
|
||||
|
|
Loading…
Reference in a new issue