wip
This commit is contained in:
parent
bbcf97d00b
commit
894e19b84b
9 changed files with 139 additions and 216 deletions
|
@ -12,4 +12,5 @@ members = [
|
||||||
"examples/tty-04-posint",
|
"examples/tty-04-posint",
|
||||||
"examples/tty-05-dictionary",
|
"examples/tty-05-dictionary",
|
||||||
"examples/tty-06-lines",
|
"examples/tty-06-lines",
|
||||||
|
"examples/tty-07-color",
|
||||||
]
|
]
|
||||||
|
|
|
@ -39,8 +39,8 @@ async fn main() {
|
||||||
*/
|
*/
|
||||||
let ctx = Arc::new(RwLock::new(Context::new()));
|
let ctx = Arc::new(RwLock::new(Context::new()));
|
||||||
nested::editors::char::init_ctx( ctx.clone() );
|
nested::editors::char::init_ctx( ctx.clone() );
|
||||||
nested::editors::digit::init_ctx( ctx.clone() );
|
//nested::editors::digit::init_ctx( ctx.clone() );
|
||||||
nested::editors::integer::init_ctx( ctx.clone() );
|
//nested::editors::integer::init_ctx( ctx.clone() );
|
||||||
nested::editors::list::init_ctx( ctx.clone() );
|
nested::editors::list::init_ctx( ctx.clone() );
|
||||||
nested_tty::setup_edittree_hook(&ctx);
|
nested_tty::setup_edittree_hook(&ctx);
|
||||||
|
|
||||||
|
@ -49,23 +49,28 @@ async fn main() {
|
||||||
*/
|
*/
|
||||||
let int_builder = ReprTreeBuilder::new( ctx.clone() )
|
let int_builder = ReprTreeBuilder::new( ctx.clone() )
|
||||||
.require(Context::parse(&ctx,
|
.require(Context::parse(&ctx,
|
||||||
"ℕ ~ <PosInt 16 BigEndian> ~ EditTree"))
|
//"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16>> ~
|
||||||
|
"<List <Digit 16>> ~ <List Char> ~ EditTree"))
|
||||||
|
/*
|
||||||
.require(Context::parse(&ctx,
|
.require(Context::parse(&ctx,
|
||||||
"ℕ ~ <PosInt 10 BigEndian> ~ EditTree"))
|
"ℕ ~ <PosInt 10 BigEndian> ~ EditTree"))
|
||||||
.require(Context::parse(&ctx,
|
.require(Context::parse(&ctx,
|
||||||
"ℕ ~ <PosInt 8 BigEndian> ~ EditTree"))
|
"ℕ ~ <PosInt 8 BigEndian> ~ EditTree"))
|
||||||
.require(Context::parse(&ctx,
|
.require(Context::parse(&ctx,
|
||||||
"ℕ ~ <PosInt 2 BigEndian> ~ EditTree"))
|
"ℕ ~ <PosInt 2 BigEndian> ~ EditTree"))
|
||||||
|
*/
|
||||||
;
|
;
|
||||||
|
|
||||||
let mut rt_int = nested::repr_tree::ReprTree::from_str("3");
|
let mut rt_int = nested::repr_tree::ReprTree::from_str("3");
|
||||||
rt_int.write().unwrap().set_halo(
|
rt_int.write().unwrap().set_halo(
|
||||||
/* HALO TYPE (append to top of type ladder) */
|
/* HALO TYPE (append to top of type ladder) */
|
||||||
Context::parse(&ctx, "
|
Context::parse(&ctx, /*"
|
||||||
ℕ
|
ℕ
|
||||||
~ <PosInt 16 BigEndian>
|
~ <PosInt 16 BigEndian>
|
||||||
~ <Seq <Digit 16>>
|
~ <Seq <Digit 16>>
|
||||||
~ <List <Digit 16>>
|
~ <List <Digit 16>>
|
||||||
|
*/
|
||||||
|
" <List <Digit 16>>
|
||||||
~ <List Char>
|
~ <List Char>
|
||||||
")
|
")
|
||||||
);
|
);
|
||||||
|
@ -102,7 +107,7 @@ async fn main() {
|
||||||
let first_idx : usize = 0;
|
let first_idx : usize = 0;
|
||||||
int_builder.update( &rt_int, int_builder.required_leaves[first_idx].clone() );
|
int_builder.update( &rt_int, int_builder.required_leaves[first_idx].clone() );
|
||||||
|
|
||||||
edittree.goto(TreeCursor{
|
edittree.goto(TreeCursor {
|
||||||
leaf_mode: nested::editors::list::ListCursorMode::Insert,
|
leaf_mode: nested::editors::list::ListCursorMode::Insert,
|
||||||
tree_addr: vec![first_idx as isize, 0]
|
tree_addr: vec![first_idx as isize, 0]
|
||||||
});
|
});
|
||||||
|
@ -155,7 +160,6 @@ async fn main() {
|
||||||
let halo_type = rt_edittree.read().unwrap().get_halo_type().clone();
|
let halo_type = rt_edittree.read().unwrap().get_halo_type().clone();
|
||||||
let edittree = rt_edittree.edittree( &ctx );
|
let edittree = rt_edittree.edittree( &ctx );
|
||||||
|
|
||||||
|
|
||||||
let box_port = ViewPort::new();
|
let box_port = ViewPort::new();
|
||||||
let ascii_box = nested_tty::widgets::ascii_box::AsciiBox::new(
|
let ascii_box = nested_tty::widgets::ascii_box::AsciiBox::new(
|
||||||
Vector2::new(30, 1),
|
Vector2::new(30, 1),
|
||||||
|
|
|
@ -85,6 +85,7 @@ impl LinesEditor {
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write()
|
ctx.write()
|
||||||
.unwrap()
|
.unwrap()
|
||||||
.morphisms
|
.morphisms
|
||||||
|
@ -120,7 +121,9 @@ impl LinesEditor {
|
||||||
.flatten();
|
.flatten();
|
||||||
|
|
||||||
let mut list_edit = list_edit.into_node(depth_port);
|
let mut list_edit = list_edit.into_node(depth_port);
|
||||||
nested_tty::editors::list::PTYListController::for_node(&mut list_edit, Some('\n'), None);
|
{
|
||||||
|
nested_tty::editors::list::PTYListController::for_node(&mut list_edit, Some('\n'), None);
|
||||||
|
}
|
||||||
list_edit
|
list_edit
|
||||||
.disp
|
.disp
|
||||||
.view
|
.view
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
[package]
|
[package]
|
||||||
name = "tty-06-color"
|
name = "tty-07-color"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2021"
|
edition = "2021"
|
||||||
|
|
||||||
|
@ -16,4 +16,3 @@ cgmath = "*"
|
||||||
[dependencies.async-std]
|
[dependencies.async-std]
|
||||||
version = "1.9.0"
|
version = "1.9.0"
|
||||||
features = ["unstable", "attributes"]
|
features = ["unstable", "attributes"]
|
||||||
|
|
||||||
|
|
|
@ -10,7 +10,7 @@ use {
|
||||||
editors::{
|
editors::{
|
||||||
ObjCommander
|
ObjCommander
|
||||||
},
|
},
|
||||||
repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf},
|
repr_tree::{Context, ReprTree, ReprTreeBuilder, ReprTreeExt, ReprTreeArc, ReprLeaf},
|
||||||
edit_tree::{EditTree, TreeNav, TreeCursor}
|
edit_tree::{EditTree, TreeNav, TreeCursor}
|
||||||
},
|
},
|
||||||
nested_tty::{
|
nested_tty::{
|
||||||
|
@ -46,139 +46,57 @@ async fn main() {
|
||||||
Context::parse(&ctx, "<Vec EditTree>")
|
Context::parse(&ctx, "<Vec EditTree>")
|
||||||
);
|
);
|
||||||
|
|
||||||
let mut red = nested::repr_tree::ReprTree::from_str(Context::parse(&ctx, "
|
let channel_builder = ReprTreeBuilder::new(ctx.clone())
|
||||||
ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ <Vec Char>
|
.require(Context::parse(&ctx, "
|
||||||
"),
|
ℕ ~ <PosInt 10 BigEndian> ~ EditTree
|
||||||
"221"
|
"))
|
||||||
);
|
.require(Context::parse(&ctx, "
|
||||||
ctx.read().unwrap().apply_morphism( &red,
|
ℕ ~ <PosInt 16 BigEndian> ~ EditTree
|
||||||
&laddertypes::MorphismType {
|
"));
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10> ~ Char > ~ <Vec Char>"),
|
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > ~ EditTree")
|
|
||||||
});
|
|
||||||
let red_edit = ctx.read().unwrap().setup_edittree(
|
|
||||||
red.descend(Context::parse(&ctx, "
|
|
||||||
ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>
|
|
||||||
")).unwrap(),
|
|
||||||
SingletonBuffer::new(0).get_port()
|
|
||||||
).unwrap();
|
|
||||||
|
|
||||||
let mut green = nested::repr_tree::ReprTree::from_str(Context::parse(&ctx, "
|
let mut red = nested::repr_tree::ReprTree::from_str("221");
|
||||||
ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ <Vec Char>
|
red.write().unwrap().set_halo(Context::parse(&ctx, "
|
||||||
"),
|
ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10>~Char>
|
||||||
"220"
|
"));
|
||||||
);
|
red = channel_builder.build_from(red).expect("");
|
||||||
ctx.read().unwrap().apply_morphism( &green,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10> ~ Char > ~ <Vec Char>"),
|
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > ~ EditTree")
|
|
||||||
});
|
|
||||||
let green_edit = ctx.read().unwrap().setup_edittree(green.descend(Context::parse(&ctx, "
|
|
||||||
ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>
|
|
||||||
")).unwrap(),
|
|
||||||
SingletonBuffer::new(0).get_port()
|
|
||||||
).unwrap();
|
|
||||||
|
|
||||||
|
let mut green = nested::repr_tree::ReprTree::from_str("220");
|
||||||
let mut blue = nested::repr_tree::ReprTree::from_str(Context::parse(&ctx, "
|
green.write().unwrap().set_halo(Context::parse(&ctx, "
|
||||||
ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ <Vec Char>
|
ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10>~Char>
|
||||||
"),
|
"));
|
||||||
"5"
|
green = channel_builder.build_from(green).expect("");
|
||||||
);
|
|
||||||
ctx.read().unwrap().apply_morphism( &blue,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10> ~ Char > ~ <Vec Char>"),
|
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > ~ EditTree")
|
|
||||||
});
|
|
||||||
let blue_edit = ctx.read().unwrap().setup_edittree(
|
|
||||||
blue.descend(Context::parse(&ctx, "
|
|
||||||
ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>
|
|
||||||
")).unwrap(),
|
|
||||||
SingletonBuffer::new(0).get_port()
|
|
||||||
).unwrap();
|
|
||||||
|
|
||||||
|
let mut blue = nested::repr_tree::ReprTree::from_str("150");
|
||||||
|
blue.write().unwrap().set_halo(Context::parse(&ctx, "
|
||||||
|
ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10>~Char>
|
||||||
|
"));
|
||||||
|
blue = channel_builder.build_from(blue).expect("");
|
||||||
|
|
||||||
|
let mut color_builder = ReprTreeBuilder::new(ctx.clone())
|
||||||
|
.require(Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian>> ~ EditTree"))
|
||||||
|
.require(Context::parse(&ctx, "<List ℕ ~ <PosInt 10 BigEndian>> ~ EditTree"))
|
||||||
|
;
|
||||||
|
|
||||||
eprintln!("======\n M A K E L I S T E D I T O R\n======\n");
|
|
||||||
|
|
||||||
let mut color = nested::repr_tree::ReprTree::new_arc(
|
let mut color = nested::repr_tree::ReprTree::new_arc(
|
||||||
Context::parse(&ctx, "<List ℕ>")
|
Context::parse(&ctx, "<List ℕ>")
|
||||||
);
|
);
|
||||||
|
|
||||||
color.insert_leaf(
|
color.insert_leaf(
|
||||||
Context::parse(&ctx, "
|
Context::parse(&ctx, "
|
||||||
<List ℕ
|
< List ℕ ~ ReprTree >
|
||||||
~ <PosInt 16 BigEndian>
|
~ < Vec ReprTree >
|
||||||
~ <Seq <Digit 16>>
|
|
||||||
~ <List <Digit 16>
|
|
||||||
~ Char >
|
|
||||||
>
|
|
||||||
~ <List EditTree>
|
|
||||||
~ <Vec EditTree>
|
|
||||||
"),
|
"),
|
||||||
|
ReprLeaf::from_vec_buffer(VecBuffer::<ReprTreeArc>::with_data(
|
||||||
ReprLeaf::from_vec_buffer(VecBuffer::<
|
vec![ red, green, blue ])
|
||||||
Arc<RwLock< EditTree >>
|
)
|
||||||
>::with_data(vec![
|
);
|
||||||
red_edit.get(),
|
/*
|
||||||
green_edit.get(),
|
color.attach_leaf_to(
|
||||||
blue_edit.get()
|
Context::parse(&ctx, "< List ℕ ~ <PosInt 10 BigEndian> ~ EditTre >"),
|
||||||
]))
|
color.descend(Context::parse(&ctx, "<List ℕ ~ ReprTree> ~ <Vec ReprTree>"))
|
||||||
|
.expect("descend")
|
||||||
|
.
|
||||||
);
|
);
|
||||||
ctx.read().unwrap().apply_morphism(
|
|
||||||
&color,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > ~ EditTree > ~ <Vec EditTree>"),
|
|
||||||
dst_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > > ~ EditTree")
|
|
||||||
});
|
|
||||||
let edit = ctx.read().unwrap().setup_edittree(
|
|
||||||
color.descend(Context::parse(&ctx, "
|
|
||||||
<List ℕ
|
|
||||||
~ < PosInt 16 BigEndian >
|
|
||||||
~ < Seq~List <Digit 16>
|
|
||||||
~ Char >
|
|
||||||
>
|
|
||||||
")).unwrap(),
|
|
||||||
SingletonBuffer::new(0).get_port()
|
|
||||||
).unwrap();
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
eprintln!(" edittree => list list char ");
|
|
||||||
ctx.read().unwrap().apply_morphism(
|
|
||||||
&color,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > > ~ EditTree"),
|
|
||||||
dst_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char > >")
|
|
||||||
});
|
|
||||||
|
|
||||||
eprintln!("list char ==> list u64");
|
|
||||||
ctx.read().unwrap().apply_morphism(
|
|
||||||
&color,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ Char>>"),
|
|
||||||
dst_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>>")
|
|
||||||
});
|
|
||||||
return;
|
|
||||||
|
|
||||||
ctx.read().unwrap().apply_morphism(
|
|
||||||
&color,
|
|
||||||
&laddertypes::MorphismType {
|
|
||||||
src_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64 > >"),
|
|
||||||
dst_type: Context::parse(&ctx, "<List ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10> ~ Char > >")
|
|
||||||
});
|
|
||||||
/*
|
|
||||||
let edit2 = ctx.read().unwrap().setup_edittree(
|
|
||||||
color.descend(Context::parse(&ctx, "
|
|
||||||
<List ℕ
|
|
||||||
~ < PosInt 10 BigEndian >
|
|
||||||
~ < Seq~List <Digit 10>
|
|
||||||
~ Char >
|
|
||||||
>
|
|
||||||
")).unwrap(),
|
|
||||||
SingletonBuffer::new(0).get_port()
|
|
||||||
).unwrap();
|
|
||||||
*/
|
*/
|
||||||
|
|
||||||
return;
|
return;
|
||||||
|
|
||||||
/* setup terminal
|
/* setup terminal
|
||||||
|
@ -187,12 +105,12 @@ return;
|
||||||
/* event handler
|
/* event handler
|
||||||
*/
|
*/
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
let edit = edit.get().clone();
|
//let edit = edit.get().clone();
|
||||||
|
|
||||||
|
// edit.write().unwrap().goto(TreeCursor::home());
|
||||||
|
|
||||||
edit.write().unwrap().goto(TreeCursor::home());
|
|
||||||
|
|
||||||
move |ev| {
|
move |ev| {
|
||||||
edit.write().unwrap().send_cmd_obj( ev.to_repr_tree(&ctx) );
|
// edit.write().unwrap().send_cmd_obj( ev.to_repr_tree(&ctx) );
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
|
||||||
|
@ -213,7 +131,7 @@ return;
|
||||||
let halo_type = rt_edittree.read().unwrap().get_halo_type().clone();
|
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 = Arc<RwLock<EditTree>>>>().unwrap().get().read().unwrap().clone();
|
let edittree = rt_edittree.read().unwrap().get_view::<dyn r3vi::view::singleton::SingletonView<Item = Arc<RwLock<EditTree>>>>().unwrap().get().read().unwrap().clone();
|
||||||
|
|
||||||
comp.push( nested_tty::make_label( &ctx.read().unwrap().type_term_to_str(&halo_type) )
|
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))))
|
.map_item(|_pt, atom| atom.add_style_front(TerminalStyle::fg_color((90,90,90))))
|
||||||
.offset(Vector2::new(1,y)));
|
.offset(Vector2::new(1,y)));
|
||||||
|
|
||||||
|
@ -221,12 +139,11 @@ return;
|
||||||
.offset(Vector2::new(1,y+1)));
|
.offset(Vector2::new(1,y+1)));
|
||||||
}
|
}
|
||||||
|
|
||||||
show_edit_tree( &ctx, &mut comp, &color.descend(Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>>")).unwrap(), 1 );
|
// show_edit_tree( &ctx, &mut comp, &color.descend(Context::parse(&ctx, "<List ℕ ~ <PosInt 16 BigEndian> ~ <Seq~List <Digit 16>~Char>>")).unwrap(), 1 );
|
||||||
show_edit_tree( &ctx, &mut comp, &color.descend(Context::parse(&ctx, "<List ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10>~Char>>")).unwrap(), 3 );
|
// show_edit_tree( &ctx, &mut comp, &color.descend(Context::parse(&ctx, "<List ℕ ~ <PosInt 10 BigEndian> ~ <Seq~List <Digit 10>~Char>>")).unwrap(), 3 );
|
||||||
}
|
}
|
||||||
|
|
||||||
/* write the changes in the view of `term_port` to the terminal
|
/* write the changes in the view of `term_port` to the terminal
|
||||||
*/
|
*/
|
||||||
app.show().await.expect("output error!");
|
app.show().await.expect("output error!");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -261,7 +261,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
ctx.write().unwrap().add_varname("Item");
|
ctx.write().unwrap().add_varname("Item");
|
||||||
|
|
||||||
let list_morph_editsetup1 = GenericReprTreeMorphism::new(
|
let list_morph_editsetup1 = GenericReprTreeMorphism::new(
|
||||||
Context::parse(&ctx, "<List Item>~<List ReprTree>~<Vec ReprTree>"),
|
Context::parse(&ctx, "<List~Vec Item~ReprTree>"),
|
||||||
Context::parse(&ctx, "<List Item>~EditTree"),
|
Context::parse(&ctx, "<List Item>~EditTree"),
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
|
|
|
@ -1,23 +1,11 @@
|
||||||
use {
|
use {
|
||||||
r3vi::{
|
super::{context::{TYPEID_char, TYPEID_edittree, TYPEID_list, TYPEID_u64, TYPEID_vec}, Context, ReprLeaf, ReprTree, ReprTreeExt}, laddertypes::{steiner_tree, sugar::*, unparser::UnparseLadderType as _, TypeID, TypeTerm}, r3vi::{
|
||||||
view::{
|
buffer::{singleton::*, vec::*}, view::{
|
||||||
ViewPort, OuterViewPort,
|
list::*, port::UpdateTask, sequence::*, singleton::*, AnyInnerViewPort, AnyOuterViewPort, AnyViewPort, Observer, OuterViewPort, View, ViewPort
|
||||||
AnyViewPort, AnyInnerViewPort, AnyOuterViewPort,
|
}
|
||||||
port::UpdateTask,
|
}, std::{
|
||||||
View, Observer,
|
any::Any, collections::HashMap, sync::{Arc, RwLock}
|
||||||
singleton::*,
|
}
|
||||||
sequence::*,
|
|
||||||
list::*
|
|
||||||
},
|
|
||||||
buffer::{singleton::*, vec::*}
|
|
||||||
},
|
|
||||||
laddertypes::{TypeTerm, TypeID, sugar::*},
|
|
||||||
std::{
|
|
||||||
collections::HashMap,
|
|
||||||
sync::{Arc, RwLock},
|
|
||||||
any::Any
|
|
||||||
},
|
|
||||||
super::{Context, ReprLeaf, ReprTree, ReprTreeExt, context::{TYPEID_list, TYPEID_vec, TYPEID_char, TYPEID_u64, TYPEID_edittree}}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
@ -65,8 +53,8 @@ impl ReprTreeBuilder {
|
||||||
|
|
||||||
let morphism_base = &self.ctx.read().unwrap().morphisms;
|
let morphism_base = &self.ctx.read().unwrap().morphisms;
|
||||||
|
|
||||||
let mt = master_leaf_type.into();
|
let mt = master_leaf_type.into().normalize().param_normalize();
|
||||||
//eprintln!("REBUILD repr tree from {}", self.ctx.read().unwrap().type_term_to_str(&mt));
|
eprintln!("REBUILD repr tree from {}", self.ctx.read().unwrap().type_term_to_str(&mt));
|
||||||
let mut leaves = self.required_leaves.clone();
|
let mut leaves = self.required_leaves.clone();
|
||||||
leaves.retain(|t| t != &mt);
|
leaves.retain(|t| t != &mt);
|
||||||
|
|
||||||
|
@ -77,18 +65,32 @@ impl ReprTreeBuilder {
|
||||||
|
|
||||||
if let Some( steiner_tree ) = st_problem.solve( &morphism_base ) {
|
if let Some( steiner_tree ) = st_problem.solve( &morphism_base ) {
|
||||||
eprintln!("--> from {}", self.ctx.read().unwrap().type_term_to_str(&mt));
|
eprintln!("--> from {}", self.ctx.read().unwrap().type_term_to_str(&mt));
|
||||||
for morphism_type in steiner_tree.into_edges() {
|
|
||||||
|
let edges = steiner_tree.into_edges();
|
||||||
|
eprintln!("steiner tree has {} edges", edges.len());
|
||||||
|
for morphism_type in edges {
|
||||||
eprintln!("--> morph to {}",
|
eprintln!("--> morph to {}",
|
||||||
self.ctx.read().unwrap().type_term_to_str(&morphism_type.dst_type));
|
self.ctx.read().unwrap().type_term_to_str(&morphism_type.dst_type));
|
||||||
|
|
||||||
if let Some(( morphism, mut τ, σ )) =
|
let mut dict = self.ctx.read().unwrap().type_dict.clone();
|
||||||
morphism_base.find_morphism_with_subtyping( &morphism_type )
|
|
||||||
|
if let Some(morph_inst) =
|
||||||
|
morphism_base.find_morphism( &morphism_type, &mut dict )
|
||||||
{
|
{
|
||||||
let mut rt = rt.descend_create( τ ).expect("descend src repr");
|
eprintln!("setup morph");
|
||||||
(morphism.setup_projection)( &mut rt, &σ );
|
|
||||||
|
let halo = laddertypes::common_halo(
|
||||||
|
&morphism_type.src_type,
|
||||||
|
&morphism_type.dst_type
|
||||||
|
).unwrap_or(TypeTerm::unit());
|
||||||
|
eprintln!("halo = {}", dict.read().unwrap().unparse(&halo));
|
||||||
|
|
||||||
|
let mut rt = rt.descend_create( halo ).expect("descend src repr");
|
||||||
|
eprintln!("{}", rt.read().unwrap().fmt(&self.ctx, 0));
|
||||||
|
(morph_inst.m.setup_projection)( &mut rt, &morph_inst.σ );
|
||||||
} else {
|
} else {
|
||||||
eprintln!("failed to get morphism");
|
eprintln!("failed to get morphism");
|
||||||
//return Err(ReprTreeError::MissingMorphism);
|
return Err(ReprTreeError::MissingMorphism);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -53,22 +53,28 @@ pub struct Context {
|
||||||
|
|
||||||
impl Context {
|
impl Context {
|
||||||
pub fn with_parent(parent: Option<Arc<RwLock<Context>>>) -> Self {
|
pub fn with_parent(parent: Option<Arc<RwLock<Context>>>) -> Self {
|
||||||
Context {
|
|
||||||
type_dict: match parent.as_ref() {
|
|
||||||
Some(p) => p.read().unwrap().type_dict.clone(),
|
|
||||||
None => {
|
|
||||||
let mut dict = BimapTypeDict::new();
|
|
||||||
assert_eq!(TYPEID_reprtree, dict.add_typename("ReprTree".into()));
|
|
||||||
assert_eq!(TYPEID_edittree, dict.add_typename("EditTree".into()));
|
|
||||||
assert_eq!(TYPEID_char, dict.add_typename("Char".into()));
|
|
||||||
assert_eq!(TYPEID_u64, dict.add_typename("machine.UInt64".into()));
|
|
||||||
assert_eq!(TYPEID_list, dict.add_typename("List".into()));
|
|
||||||
assert_eq!(TYPEID_vec, dict.add_typename("Vec".into()));
|
|
||||||
|
|
||||||
Arc::new(RwLock::new(dict))
|
let mut dict = match parent.as_ref() {
|
||||||
}
|
Some(p) => p.read().unwrap().type_dict.clone(),
|
||||||
},
|
None => {
|
||||||
morphisms: MorphismBase::new(TYPEID_list),
|
let mut dict = BimapTypeDict::new();
|
||||||
|
assert_eq!(TYPEID_reprtree, dict.add_typename("ReprTree".into()));
|
||||||
|
assert_eq!(TYPEID_edittree, dict.add_typename("EditTree".into()));
|
||||||
|
assert_eq!(TYPEID_char, dict.add_typename("Char".into()));
|
||||||
|
assert_eq!(TYPEID_u64, dict.add_typename("machine.UInt64".into()));
|
||||||
|
assert_eq!(TYPEID_list, dict.add_typename("List".into()));
|
||||||
|
assert_eq!(TYPEID_vec, dict.add_typename("Vec".into()));
|
||||||
|
|
||||||
|
Arc::new(RwLock::new(dict))
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
Context {
|
||||||
|
type_dict: dict.clone(),
|
||||||
|
morphisms: MorphismBase::new(vec![
|
||||||
|
dict.parse("List").expect(""),
|
||||||
|
//dict.parse("Vec").expect("")
|
||||||
|
]),
|
||||||
nodes: HashMap::new(),
|
nodes: HashMap::new(),
|
||||||
list_types: match parent.as_ref() {
|
list_types: match parent.as_ref() {
|
||||||
Some(p) => p.read().unwrap().list_types.clone(),
|
Some(p) => p.read().unwrap().list_types.clone(),
|
||||||
|
@ -104,22 +110,9 @@ impl Context {
|
||||||
|
|
||||||
pub fn apply_morphism(&self, rt: &Arc<RwLock<ReprTree>>, ty: &MorphismType) {
|
pub fn apply_morphism(&self, rt: &Arc<RwLock<ReprTree>>, ty: &MorphismType) {
|
||||||
if let Some(path) = self.morphisms.find_morphism_path(ty.clone().normalize()) {
|
if let Some(path) = self.morphisms.find_morphism_path(ty.clone().normalize()) {
|
||||||
let mut path = path.into_iter();
|
for morph_inst in path {
|
||||||
if let Some(mut src_type) = path.next() {
|
let mut rt = rt.descend(morph_inst.halo).expect("descend src repr");
|
||||||
for dst_type in path {
|
(morph_inst.m.setup_projection)(&mut rt, &morph_inst.σ);
|
||||||
if let Some((m, mut τ, σ)) =
|
|
||||||
self.morphisms
|
|
||||||
.find_morphism_with_subtyping(&laddertypes::MorphismType {
|
|
||||||
src_type: src_type.clone(),
|
|
||||||
dst_type: dst_type.clone(),
|
|
||||||
})
|
|
||||||
{
|
|
||||||
let mut rt = rt.descend(τ).expect("descend src repr");
|
|
||||||
(m.setup_projection)(&mut rt, &σ);
|
|
||||||
}
|
|
||||||
|
|
||||||
src_type = dst_type;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
eprintln!("no path found");
|
eprintln!("no path found");
|
||||||
|
|
|
@ -27,13 +27,19 @@ pub struct GenericReprTreeMorphism {
|
||||||
>
|
>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl PartialEq for GenericReprTreeMorphism {
|
||||||
|
fn eq(&self, other: &Self) -> bool {
|
||||||
|
self.morph_type == other.morph_type
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
impl Morphism for GenericReprTreeMorphism {
|
impl Morphism for GenericReprTreeMorphism {
|
||||||
fn get_type(&self) -> MorphismType {
|
fn get_type(&self) -> MorphismType {
|
||||||
self.morph_type.clone()
|
self.morph_type.clone()
|
||||||
}
|
}
|
||||||
|
|
||||||
fn list_map_morphism(&self, list_typeid: TypeID) -> Option< GenericReprTreeMorphism > {
|
fn map_morphism(&self, seq_type: TypeTerm) -> Option< GenericReprTreeMorphism > {
|
||||||
self.into_list_map_dyn(list_typeid)
|
self.into_list_map_dyn(seq_type)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -54,7 +60,7 @@ impl GenericReprTreeMorphism {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn into_list_map< SrcItem, DstItem >(&self, list_typeid: TypeID)
|
pub fn into_list_map< SrcItem, DstItem >(&self, seq_type: TypeTerm)
|
||||||
-> GenericReprTreeMorphism
|
-> GenericReprTreeMorphism
|
||||||
where
|
where
|
||||||
SrcItem: Clone + Send + Sync + 'static,
|
SrcItem: Clone + Send + Sync + 'static,
|
||||||
|
@ -62,11 +68,11 @@ impl GenericReprTreeMorphism {
|
||||||
{
|
{
|
||||||
let mut lst_map_type = MorphismType {
|
let mut lst_map_type = MorphismType {
|
||||||
src_type: TypeTerm::App(vec![
|
src_type: TypeTerm::App(vec![
|
||||||
TypeTerm::TypeID(list_typeid),
|
seq_type.clone(),
|
||||||
self.morph_type.src_type.clone()
|
self.morph_type.src_type.clone()
|
||||||
]),
|
]),
|
||||||
dst_type: TypeTerm::App(vec![
|
dst_type: TypeTerm::App(vec![
|
||||||
TypeTerm::TypeID(list_typeid),
|
seq_type.clone(),
|
||||||
self.morph_type.dst_type.clone()
|
self.morph_type.dst_type.clone()
|
||||||
])
|
])
|
||||||
}.normalize();
|
}.normalize();
|
||||||
|
@ -86,14 +92,13 @@ impl GenericReprTreeMorphism {
|
||||||
"lst map type ::\n {:?}\n===> {:?}\n\n", lst_map_type.src_type, lst_map_type.dst_type
|
"lst map type ::\n {:?}\n===> {:?}\n\n", lst_map_type.src_type, lst_map_type.dst_type
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
||||||
let mut item_ladder = item_morph.morph_type.src_type.clone().get_lnf_vec();
|
let mut item_ladder = item_morph.morph_type.src_type.clone().get_lnf_vec();
|
||||||
let top_type = item_ladder.remove( item_ladder.len() - 1 );
|
let top_type = item_ladder.remove( item_ladder.len() - 1 );
|
||||||
|
|
||||||
if let Ok(item_sigma) = laddertypes::unify(
|
if let Ok(item_sigma) = laddertypes::unify(
|
||||||
&top_type,
|
&top_type,
|
||||||
&TypeTerm::App(vec![
|
&TypeTerm::App(vec![
|
||||||
TypeTerm::TypeID( list_typeid ),
|
seq_type.clone(),
|
||||||
TypeTerm::TypeID( TypeID::Var( 200 ) )
|
TypeTerm::TypeID( TypeID::Var( 200 ) )
|
||||||
])
|
])
|
||||||
) {
|
) {
|
||||||
|
@ -113,7 +118,7 @@ impl GenericReprTreeMorphism {
|
||||||
top_type.clone(),
|
top_type.clone(),
|
||||||
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
||||||
// TODO: required?
|
// TODO: required?
|
||||||
for t in item_ladder.iter().rev() {
|
for t in item_ladder.iter().rev() {
|
||||||
|
@ -139,43 +144,43 @@ impl GenericReprTreeMorphism {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn into_list_map_dyn(&self, typeid_list: TypeID)
|
pub fn into_list_map_dyn(&self, seq_type: TypeTerm)
|
||||||
-> Option< GenericReprTreeMorphism >
|
-> Option< GenericReprTreeMorphism >
|
||||||
{
|
{
|
||||||
let src_item_type_lnf = self.morph_type.src_type.clone().get_lnf_vec();
|
let src_item_type_lnf = self.morph_type.src_type.clone().get_lnf_vec();
|
||||||
let dst_item_type_lnf = self.morph_type.dst_type.clone().get_lnf_vec();
|
let dst_item_type_lnf = self.morph_type.dst_type.clone().get_lnf_vec();
|
||||||
|
|
||||||
eprintln!("into list map dyn");
|
eprintln!("into list map dyn:\n src {:?}\n dst {:?}", src_item_type_lnf, dst_item_type_lnf);
|
||||||
|
|
||||||
if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< char, char >(TYPEID_list) )
|
Some( self.into_list_map::< char, char >( seq_type ) )
|
||||||
}
|
}
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64)) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< u64, u64 >(TYPEID_list) )
|
Some( self.into_list_map::< u64, u64 >( seq_type ) )
|
||||||
}
|
}
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< char, u64 >(TYPEID_list) )
|
Some( self.into_list_map::< char, u64 >( seq_type ) )
|
||||||
}
|
}
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64)) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_u64)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< u64, char >(TYPEID_list) )
|
Some( self.into_list_map::< u64, char >( seq_type ) )
|
||||||
}
|
}
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_edittree))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_edittree))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< char, Arc<RwLock<crate::edit_tree::EditTree>> >(TYPEID_list) )
|
Some( self.into_list_map::< char, Arc<RwLock<crate::edit_tree::EditTree>> >(seq_type) )
|
||||||
}
|
}
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_edittree)) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_edittree)) &&
|
||||||
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TYPEID_char))
|
||||||
{
|
{
|
||||||
Some( self.into_list_map::< Arc<RwLock<crate::edit_tree::EditTree>>, char >(TYPEID_list) )
|
Some( self.into_list_map::< Arc<RwLock<crate::edit_tree::EditTree>>, char >(seq_type) )
|
||||||
}
|
}
|
||||||
/*
|
/*
|
||||||
else if src_item_type_lnf.last() == Some(&TypeTerm::App(vec![ TypeTerm::TypeID(typeid_list), TypeTerm::TypeID(typeid_char) ])) &&
|
else if src_item_type_lnf.last() == Some(&TypeTerm::App(vec![ TypeTerm::TypeID(typeid_list), TypeTerm::TypeID(typeid_char) ])) &&
|
||||||
|
@ -208,4 +213,3 @@ impl GenericReprTreeMorphism {
|
||||||
}
|
}
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue