improve morphisms for integer example
This commit is contained in:
parent
d02f33ee17
commit
cdf03c9aae
6 changed files with 543 additions and 100 deletions
|
@ -17,7 +17,7 @@ use {
|
|||
ObjCommander
|
||||
},
|
||||
repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf},
|
||||
edit_tree::{EditTree}
|
||||
edit_tree::{EditTree, TreeNav, TreeCursor}
|
||||
},
|
||||
nested_tty::{
|
||||
DisplaySegment, TTYApplication,
|
||||
|
@ -26,7 +26,7 @@ use {
|
|||
},
|
||||
r3vi::{
|
||||
buffer::{singleton::*, vec::*},
|
||||
view::{port::UpdateTask, list::*, sequence::*},
|
||||
view::{port::UpdateTask, singleton::*, list::*, sequence::*},
|
||||
projection::*
|
||||
},
|
||||
std::sync::{Arc, RwLock},
|
||||
|
@ -43,7 +43,6 @@ async fn main() {
|
|||
nested::editors::list::init_ctx( ctx.clone() );
|
||||
nested_tty::setup_edittree_hook(&ctx);
|
||||
|
||||
|
||||
/* Create a Representation-Tree of type `ℕ`
|
||||
*/
|
||||
let mut rt_int = ReprTree::new_arc( Context::parse(&ctx, "ℕ") );
|
||||
|
@ -51,39 +50,157 @@ async fn main() {
|
|||
/* Add a specific Representation-Path (big-endian hexadecimal)
|
||||
*/
|
||||
rt_int.create_branch(
|
||||
Context::parse(&ctx, "<PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16>>")
|
||||
Context::parse(&ctx, "<PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16>~Char>")
|
||||
);
|
||||
rt_int.create_branch(
|
||||
Context::parse(&ctx, "<PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16>~Char>")
|
||||
);
|
||||
rt_int.create_branch(
|
||||
Context::parse(&ctx, "<PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10>~Char>")
|
||||
);
|
||||
|
||||
eprintln!("make big endian hex repr");
|
||||
let mut b = VecBuffer::with_data(vec![ 'c', 'f', 'f' ]);
|
||||
rt_int.insert_leaf(
|
||||
Context::parse(&ctx, "<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>>~<List Char>"),
|
||||
nested::repr_tree::ReprLeaf::from_view( b.get_port().to_list() )
|
||||
);
|
||||
|
||||
let mut b_le = VecBuffer::with_data(vec!['3', '2', '1']);
|
||||
rt_int.insert_leaf(
|
||||
Context::parse(&ctx, "<PosInt 16 LittleEndian>~<Seq <Digit 16>>~<List <Digit 16>>~<List Char>"),
|
||||
nested::repr_tree::ReprLeaf::from_view( b_le.get_port().to_list() )
|
||||
);
|
||||
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>"),
|
||||
&Context::parse(&ctx, "<List Char~EditTree>")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16> >
|
||||
~ <List <Digit 16>~Char~EditTree >
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List EditTree>"),
|
||||
&Context::parse(&ctx, "<List EditTree>~<Vec EditTree>")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>~Char>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>~<List EditTree>~<Vec EditTree>"),
|
||||
&Context::parse(&ctx, "<List Char>~EditTree")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>~Char >
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>~EditTree"),
|
||||
&Context::parse(&ctx, "<List Char>")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.clone(),
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
"),
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 BigEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.clone(),
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 BigEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
"),
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
")
|
||||
);
|
||||
|
||||
let edittree_hex_le_list = ctx.read().unwrap()
|
||||
.setup_edittree(
|
||||
rt_int.descend(Context::parse(&ctx,"
|
||||
<PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>~Char >
|
||||
")).expect("descend"),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
);
|
||||
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>~Char>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>"),
|
||||
&Context::parse(&ctx, "<List Char~EditTree>")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>~Char~EditTree>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List EditTree>"),
|
||||
&Context::parse(&ctx, "<List EditTree>~<Vec EditTree>")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>~Char>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>~<List EditTree>~<Vec EditTree>"),
|
||||
&Context::parse(&ctx, "<List Char>~EditTree")
|
||||
);
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>~Char>
|
||||
")).expect("descend"),
|
||||
&Context::parse(&ctx, "<List Char>~EditTree"),
|
||||
&Context::parse(&ctx, "<List Char>")
|
||||
);
|
||||
|
||||
/* Setup an Editor for the big-endian hexadecimal representation
|
||||
* (this will add the representation `<List <Digit 16>>~EditTree` to the ReprTree)
|
||||
*/
|
||||
let rt_edittree_list = ctx.read().unwrap()
|
||||
let edittree_hex_be_list = ctx.read().unwrap()
|
||||
.setup_edittree(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
~ <List Char>
|
||||
")).expect("cant descend reprtree"),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
);
|
||||
|
||||
/* Setup a morphism to extract Char values from the list-editor
|
||||
*/
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.descend(Context::parse(&ctx, "
|
||||
<PosInt 16 BigEndian>
|
||||
~ <Seq <Digit 16>>
|
||||
~ <List <Digit 16>>
|
||||
")).expect("cant descend reprtree"),
|
||||
&Context::parse(&ctx, "<List <Digit 16>>~EditTree"),
|
||||
&Context::parse(&ctx, "<List <Digit 16>~Char>")
|
||||
);
|
||||
|
||||
/*
|
||||
* 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, "
|
||||
|
@ -119,13 +236,24 @@ async fn main() {
|
|||
//ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ
|
||||
//
|
||||
|
||||
|
||||
/* convert to little endian
|
||||
*/
|
||||
ctx.read().unwrap().morphisms.apply_morphism(
|
||||
rt_int.clone(),
|
||||
&Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>~ℤ_2^64~machine.UInt64>"),
|
||||
&Context::parse(&ctx, "ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>~ℤ_2^64~machine.UInt64>")
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 BigEndian>
|
||||
~ <Seq <Digit 16>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >
|
||||
"),
|
||||
&Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt 16 LittleEndian>
|
||||
~ <Seq <Digit 16>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >
|
||||
")
|
||||
);
|
||||
|
||||
/* convert to decimal
|
||||
|
@ -144,6 +272,7 @@ async fn main() {
|
|||
&Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>~ℤ_2^64~machine.UInt64>")
|
||||
);
|
||||
|
||||
|
||||
/* map seq of u64 digits to seq of chars
|
||||
* and add this projection to the ReprTree
|
||||
*/
|
||||
|
@ -178,18 +307,32 @@ async fn main() {
|
|||
//ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ
|
||||
//
|
||||
|
||||
/* list of both editors
|
||||
*/
|
||||
let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "<Seq Char>"));
|
||||
list_editor.data.push( edittree_hex_be_list.value.clone() );
|
||||
list_editor.data.push( edittree_hex_le_list.value.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.goto(TreeCursor{
|
||||
leaf_mode: nested::editors::list::ListCursorMode::Insert,
|
||||
tree_addr: vec![0,0]
|
||||
});
|
||||
let edittree = Arc::new(RwLock::new(edittree));
|
||||
|
||||
/* setup terminal
|
||||
*/
|
||||
let app = TTYApplication::new({
|
||||
let edittree_list = rt_edittree_list.clone();
|
||||
|
||||
/* event handler
|
||||
*/
|
||||
let ctx = ctx.clone();
|
||||
move |ev| {
|
||||
edittree_list.get().send_cmd_obj(ev.to_repr_tree(&ctx));
|
||||
edittree.write().unwrap().send_cmd_obj(ev.to_repr_tree(&ctx));
|
||||
}
|
||||
});
|
||||
|
||||
|
@ -204,23 +347,32 @@ async fn main() {
|
|||
{
|
||||
let mut comp = compositor.write().unwrap();
|
||||
|
||||
let label_str = ctx.read().unwrap().type_term_to_str(&rt_int.read().unwrap().get_type());
|
||||
comp.push(
|
||||
nested_tty::make_label(&label_str)
|
||||
fn show_edit_tree( ctx: &Arc<RwLock<Context>>, comp: &mut TerminalCompositor, rt: &Arc<RwLock<ReprTree>>, y: i16 )
|
||||
{
|
||||
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::<dyn r3vi::view::singleton::SingletonView<Item = EditTree>>().unwrap().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))))
|
||||
.offset(Vector2::new(1,1)));
|
||||
.offset(Vector2::new(1,y)));
|
||||
|
||||
comp.push(rt_edittree_list.get()
|
||||
.display_view()
|
||||
.offset(Vector2::new(3,2)));
|
||||
comp.push( edittree.display_view()
|
||||
.offset(Vector2::new(1,y+1)));
|
||||
}
|
||||
|
||||
comp.push(nested_tty::make_label("dec: ").offset(Vector2::new(3,4)));
|
||||
comp.push(dec_digits_view.offset(Vector2::new(8,4)).map_item(|_,a| {
|
||||
show_edit_tree(&ctx, &mut comp, &rt_int.descend(Context::parse(&ctx, "<PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>")).expect(""), 1);
|
||||
show_edit_tree(&ctx, &mut comp, &rt_int.descend(Context::parse(&ctx, "<PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16>~Char>")).expect(""), 4);
|
||||
|
||||
/* 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,5)));
|
||||
comp.push(hex_digits_view.offset(Vector2::new(8,5)).map_item(|_,a| {
|
||||
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)))
|
||||
}));
|
||||
}
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
|
||||
use {
|
||||
r3vi::{
|
||||
view::{OuterViewPort, singleton::*}
|
||||
view::{OuterViewPort, singleton::*, list::*}
|
||||
},
|
||||
laddertypes::{TypeTerm},
|
||||
crate::{
|
||||
repr_tree::{ReprTree, ReprLeaf, Context, MorphismType},
|
||||
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf, Context, MorphismType},
|
||||
editors::{
|
||||
list::*,
|
||||
integer::*
|
||||
|
@ -16,13 +16,71 @@ use {
|
|||
|
||||
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||
// TODO: proper scoping
|
||||
// ctx.write().unwrap().add_varname("Radix");
|
||||
ctx.write().unwrap().add_varname("Radix");
|
||||
ctx.write().unwrap().add_varname("SrcRadix");
|
||||
ctx.write().unwrap().add_varname("DstRadix");
|
||||
|
||||
let morphism_type =
|
||||
MorphismType {
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
morphism_type, {
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let src_digits = src_rt.descend(
|
||||
Context::parse(&ctx, "
|
||||
<PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >
|
||||
")
|
||||
.apply_substitution(&|k|σ.get(k).cloned())
|
||||
.clone()
|
||||
).expect("cant descend")
|
||||
.read().unwrap()
|
||||
.view_seq::< u64 >();
|
||||
|
||||
src_rt.insert_leaf(Context::parse(&ctx, "
|
||||
<PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >
|
||||
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||
ReprLeaf::from_view( src_digits.reverse() )
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
let morphism_type = MorphismType {
|
||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>"),
|
||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>")
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List ℤ_2^64>
|
||||
~ <List machine.UInt64>
|
||||
"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List ℤ_2^64>
|
||||
~ <List machine.UInt64>
|
||||
")
|
||||
};
|
||||
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
|
@ -30,27 +88,65 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let src_digits = ReprTree::descend(
|
||||
&src_rt,
|
||||
Context::parse(&ctx, "
|
||||
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||
<PosInt Radix BigEndian>
|
||||
~<Seq <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
||||
")
|
||||
.apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||
).expect("cant descend")
|
||||
.read().unwrap()
|
||||
.view_seq::< u64 >();
|
||||
.get_port::< dyn ListView<u64> >().unwrap();
|
||||
|
||||
src_rt.write().unwrap().insert_leaf(
|
||||
vec![
|
||||
Context::parse(&ctx, "<PosInt Radix LittleEndian>")
|
||||
.apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||
Context::parse(&ctx, "<Seq <Digit Radix>>")
|
||||
.apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||
Context::parse(&ctx, "<Seq ℤ_2^64>"),
|
||||
Context::parse(&ctx, "<Seq machine.UInt64>")
|
||||
].into_iter(),
|
||||
src_rt.insert_leaf(
|
||||
Context::parse(&ctx, "
|
||||
<PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>
|
||||
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||
ReprLeaf::from_view( src_digits.reverse() )
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
|
||||
let mt = MorphismType {
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List Char>
|
||||
"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List Char>
|
||||
")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
mt,
|
||||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||
<PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>~Char >
|
||||
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||
).expect("cant descend")
|
||||
.read().unwrap()
|
||||
.get_port::< dyn ListView<char> >().unwrap();
|
||||
|
||||
src_rt.insert_leaf(
|
||||
Context::parse(&ctx, "
|
||||
< PosInt Radix LittleEndian >
|
||||
~ < Seq <Digit Radix> >
|
||||
~ < List <Digit Radix>~Char >
|
||||
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||
ReprLeaf::from_view( src_digits.reverse() )
|
||||
);
|
||||
}
|
||||
|
@ -63,8 +159,8 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
|
||||
|
||||
let morphism_type = MorphismType {
|
||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>"),
|
||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>")
|
||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>"),
|
||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>")
|
||||
};
|
||||
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
|
@ -99,12 +195,117 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
}
|
||||
);
|
||||
|
||||
let morphism_type =
|
||||
MorphismType {
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List ℤ_2^64>
|
||||
~ <List machine.UInt64>
|
||||
"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List ℤ_2^64>
|
||||
~ <List machine.UInt64>
|
||||
")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
morphism_type, {
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ|
|
||||
{
|
||||
let src_digits = ReprTree::descend(
|
||||
&src_rt,
|
||||
Context::parse(&ctx, "
|
||||
<PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||
")
|
||||
.apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||
).expect("cant descend")
|
||||
.read().unwrap()
|
||||
.get_port::< dyn ListView<u64> >().unwrap();
|
||||
|
||||
src_rt.insert_leaf(
|
||||
Context::parse(&ctx, "
|
||||
<PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||
"),
|
||||
ReprLeaf::from_view( src_digits.reverse() )
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
|
||||
|
||||
let mt = MorphismType {
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List Char>
|
||||
"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>>
|
||||
~ <List Char>
|
||||
")
|
||||
};
|
||||
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
mt,
|
||||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||
<PosInt Radix LittleEndian>
|
||||
~ <Seq <Digit Radix>>
|
||||
~ <List <Digit Radix>~Char >
|
||||
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||
).expect("cant descend")
|
||||
.read().unwrap()
|
||||
.get_port::< dyn ListView<char> >().unwrap();
|
||||
|
||||
src_rt.insert_leaf(
|
||||
Context::parse(&ctx, "
|
||||
< PosInt Radix BigEndian >
|
||||
~ < Seq <Digit Radix> >
|
||||
~ < List <Digit Radix>~Char >
|
||||
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||
ReprLeaf::from_view( src_digits.reverse() )
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
|
||||
|
||||
|
||||
|
||||
let morphism_type = MorphismType {
|
||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>"),
|
||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>")
|
||||
src_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt SrcRadix LittleEndian>
|
||||
~ <Seq <Digit SrcRadix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64>
|
||||
"),
|
||||
dst_type: Context::parse(&ctx, "
|
||||
ℕ
|
||||
~ <PosInt DstRadix LittleEndian>
|
||||
~ <Seq <Digit DstRadix>
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64 >
|
||||
")
|
||||
};
|
||||
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
|
@ -138,8 +339,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
src_digits_rt.read().unwrap()
|
||||
.view_seq::<u64>()
|
||||
.to_positional_uint( src_radix )
|
||||
.transform_radix( dst_radix )
|
||||
;
|
||||
.transform_radix( dst_radix );
|
||||
|
||||
src_rt.write().unwrap()
|
||||
.insert_leaf(
|
||||
|
|
|
@ -23,28 +23,88 @@ use {
|
|||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||
ctx.write().unwrap().add_list_typename("List".into());
|
||||
ctx.write().unwrap().add_varname("Item");
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Item>"),
|
||||
src_type: Context::parse(&ctx, "<List Char>"),
|
||||
dst_type: Context::parse(&ctx, "<List Char~EditTree>")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(mt, {
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let list_port = src_rt.read().unwrap().get_port::<dyn ListView<char>>().clone();
|
||||
if let Some(list_port) = list_port {
|
||||
let edit_tree_list =
|
||||
list_port
|
||||
// for each char, create and EditTree
|
||||
.map({
|
||||
let ctx = ctx.clone();
|
||||
move |c| {
|
||||
let item_rt = ReprTree::from_char(&ctx, *c);
|
||||
ctx.read().unwrap().setup_edittree(
|
||||
item_rt.clone(),
|
||||
SingletonBuffer::new(0).get_port()
|
||||
);
|
||||
let et = item_rt
|
||||
.descend(Context::parse(&ctx, "EditTree")).unwrap()
|
||||
.read().unwrap()
|
||||
.get_port::< dyn SingletonView<Item = EditTree> >()
|
||||
.expect("cant get view port (EditTree)")
|
||||
.get_view().unwrap()
|
||||
.get();
|
||||
Arc::new(RwLock::new(et))
|
||||
}
|
||||
});
|
||||
|
||||
src_rt.write().unwrap().insert_leaf(
|
||||
Context::parse(&ctx, "<List EditTree>").get_lnf_vec().into_iter(),
|
||||
ReprLeaf::from_view( edit_tree_list )
|
||||
);
|
||||
} else {
|
||||
eprintln!("morphism missing view port");
|
||||
}
|
||||
}
|
||||
});
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Item>~<List EditTree>~<Vec EditTree>"),
|
||||
dst_type: Context::parse(&ctx, "<List Item>~EditTree")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
mt,
|
||||
{
|
||||
ctx.write().unwrap().morphisms.add_morphism(mt, {
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let item_id = laddertypes::TypeID::Var( ctx.read().unwrap().get_var_typeid("Item").unwrap() );
|
||||
if let Some( item_type ) = σ.get( &item_id ) {
|
||||
/*
|
||||
let mut item_vec_buffer = VecBuffer::new();
|
||||
|
||||
let mut edittree_list = ListEditor::new(
|
||||
ctx.clone(),
|
||||
item_type.clone()
|
||||
).into_node(
|
||||
eprintln!("try attach to data port");
|
||||
if let Some( list_port ) =
|
||||
src_rt
|
||||
.descend(Context::parse(&ctx, "<List EditTree>")).expect("")
|
||||
.read().unwrap()
|
||||
.get_port::< dyn ListView< Arc<RwLock<EditTree>> > >()
|
||||
{
|
||||
eprintln!("get list<edittree> port");
|
||||
item_vec_buffer.attach_to( list_port );
|
||||
}*/
|
||||
|
||||
let mut item_vec_rt = src_rt
|
||||
.descend(Context::parse(&ctx, "<List EditTree>~<Vec EditTree>"))
|
||||
.expect("cant descend src repr");
|
||||
|
||||
let item_vec_buffer = item_vec_rt
|
||||
.write().unwrap()
|
||||
.vec_buffer::< Arc<RwLock<EditTree>> >().expect("cant get vec buffer");
|
||||
|
||||
// eprintln!("create ListEditor");
|
||||
let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer);
|
||||
|
||||
let edittree_list = list_editor.into_node(
|
||||
SingletonBuffer::<usize>::new(0).get_port()
|
||||
);
|
||||
|
||||
// eprintln!("make edittree");
|
||||
src_rt.write().unwrap().insert_branch(
|
||||
ReprTree::from_singleton_buffer(
|
||||
Context::parse(&ctx, "EditTree"),
|
||||
|
@ -55,8 +115,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
eprintln!("no item type");
|
||||
}
|
||||
}
|
||||
}
|
||||
);
|
||||
});
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Char>~EditTree"),
|
||||
|
@ -93,8 +152,8 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
);
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List <Digit 16>>~EditTree"),
|
||||
dst_type: Context::parse(&ctx, "<List <Digit 16>~Char>")
|
||||
src_type: Context::parse(&ctx, "<List <Digit Radix>>~EditTree"),
|
||||
dst_type: Context::parse(&ctx, "<List <Digit Radix>~Char>")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
mt,
|
||||
|
@ -127,7 +186,6 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
);
|
||||
|
||||
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List Char>"),
|
||||
dst_type: Context::parse(&ctx, "<List Char>~<Vec Char>")
|
||||
|
@ -151,5 +209,29 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
|||
}
|
||||
}
|
||||
);
|
||||
|
||||
let mt = crate::repr_tree::MorphismType {
|
||||
src_type: Context::parse(&ctx, "<List EditTree>"),
|
||||
dst_type: Context::parse(&ctx, "<List EditTree>~<Vec EditTree>")
|
||||
};
|
||||
ctx.write().unwrap().morphisms.add_morphism(
|
||||
mt,
|
||||
{
|
||||
let ctx = ctx.clone();
|
||||
move |src_rt, σ| {
|
||||
let buf = VecBuffer::<Arc<RwLock<EditTree>>>::new();
|
||||
let mut leaf = ReprLeaf::from_vec_buffer(buf);
|
||||
leaf.attach_to(
|
||||
src_rt.read().unwrap()
|
||||
.get_port::<dyn ListView< Arc<RwLock<EditTree>> >>()
|
||||
.unwrap()
|
||||
);
|
||||
src_rt.write().unwrap().insert_leaf(
|
||||
vec![ Context::parse(&ctx, "<Vec EditTree>") ].into_iter(),
|
||||
leaf
|
||||
);
|
||||
}
|
||||
}
|
||||
);
|
||||
}
|
||||
|
||||
|
|
|
@ -35,11 +35,22 @@ pub struct ListEditor {
|
|||
|
||||
impl ListEditor {
|
||||
pub fn new(
|
||||
ctx: Arc<RwLock<Context>>,
|
||||
typ: TypeTerm
|
||||
) -> Self {
|
||||
Self::with_data(
|
||||
ctx,
|
||||
typ,
|
||||
VecBuffer::new()
|
||||
)
|
||||
}
|
||||
|
||||
pub fn with_data(
|
||||
ctx: Arc<RwLock<Context>>,
|
||||
typ: TypeTerm,
|
||||
data: VecBuffer<Arc<RwLock<EditTree>>>
|
||||
) -> Self {
|
||||
let cursor = SingletonBuffer::new(ListCursor::default());
|
||||
let data : VecBuffer<Arc<RwLock<EditTree>>> = VecBuffer::new();
|
||||
|
||||
ListEditor {
|
||||
mode_port: cursor
|
||||
|
|
|
@ -55,7 +55,6 @@ impl Context {
|
|||
None => Vec::new()
|
||||
},
|
||||
parent,
|
||||
|
||||
edittree_hook: Arc::new(|_et, _t| {})
|
||||
}
|
||||
}
|
||||
|
|
|
@ -21,7 +21,6 @@ use {
|
|||
pub fn edittree_make_char_view(
|
||||
node: EditTree
|
||||
) -> EditTree {
|
||||
eprintln!("nested-tty: EditTree make char-view");
|
||||
node.disp.view
|
||||
.write().unwrap()
|
||||
.insert_branch(ReprTree::from_view(
|
||||
|
|
Loading…
Reference in a new issue