apply_list_map_morphism
This commit is contained in:
parent
e86070da50
commit
6e8bb0aeb5
5 changed files with 237 additions and 111 deletions
|
@ -37,7 +37,7 @@ fn rebuild_projections(
|
||||||
repr_tree: Arc<RwLock<ReprTree>>,
|
repr_tree: Arc<RwLock<ReprTree>>,
|
||||||
morph_types: Vec< (laddertypes::TypeTerm, laddertypes::TypeTerm) >
|
morph_types: Vec< (laddertypes::TypeTerm, laddertypes::TypeTerm) >
|
||||||
) {
|
) {
|
||||||
repr_tree.write().unwrap().detach(&ctx);
|
// repr_tree.write().unwrap().detach(&ctx);
|
||||||
for (src_type, dst_type) in morph_types.iter() {
|
for (src_type, dst_type) in morph_types.iter() {
|
||||||
ctx.read().unwrap().morphisms.apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
repr_tree.clone(),
|
repr_tree.clone(),
|
||||||
|
@ -48,6 +48,8 @@ fn rebuild_projections(
|
||||||
}
|
}
|
||||||
|
|
||||||
fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
|
rt_int.write().unwrap().detach(&ctx);
|
||||||
|
|
||||||
rebuild_projections(
|
rebuild_projections(
|
||||||
ctx.clone(),
|
ctx.clone(),
|
||||||
rt_int.clone(),
|
rt_int.clone(),
|
||||||
|
@ -81,51 +83,38 @@ fn setup_le_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
.collect()
|
.collect()
|
||||||
);
|
);
|
||||||
/*
|
|
||||||
|
|
||||||
/*
|
let rt_digitseq =
|
||||||
* map seq of chars to seq of u64 digits
|
rt_int.descend(Context::parse(&ctx, "
|
||||||
* and add this projection to the ReprTree
|
<PosInt 16 LittleEndian>
|
||||||
*/
|
~ <Seq <Digit 16>>
|
||||||
//
|
~ <List <Digit 16>>
|
||||||
//VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV
|
")).expect("test");
|
||||||
let mut chars_view = rt_int.descend(Context::parse(&ctx, "
|
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||||
<PosInt 16 BigEndian>
|
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||||
~ <Seq <Digit 16>>
|
ctx.read().unwrap().morphisms
|
||||||
~ <List <Digit 16>~Char>
|
.apply_list_map_morphism::<char, u64>(
|
||||||
")).expect("cant descend")
|
rt_digitseq, src_type, dst_type
|
||||||
.read().unwrap()
|
|
||||||
.get_port::<dyn ListView<char>>()
|
|
||||||
.unwrap();
|
|
||||||
|
|
||||||
let mut digits_view = chars_view
|
|
||||||
.to_sequence()
|
|
||||||
.filter_map(
|
|
||||||
|digit_char|
|
|
||||||
|
|
||||||
/* TODO: call morphism for each item
|
|
||||||
*/
|
|
||||||
match digit_char.to_digit(16) {
|
|
||||||
Some(d) => Some(d as u64),
|
|
||||||
None => None
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
rt_int.attach_leaf_to(Context::parse(&ctx, "
|
rebuild_projections(
|
||||||
<PosInt 16 BigEndian>
|
ctx.clone(),
|
||||||
~ <Seq <Digit 16>
|
rt_int.clone(),
|
||||||
~ ℤ_2^64
|
vec![
|
||||||
~ machine.UInt64 >
|
// Radix Convert
|
||||||
"),
|
(
|
||||||
digits_view.clone()
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||||
|
)
|
||||||
|
].into_iter()
|
||||||
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
|
.collect()
|
||||||
);
|
);
|
||||||
|
|
||||||
//ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ
|
|
||||||
//
|
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
|
rt_int.write().unwrap().detach(&ctx);
|
||||||
|
|
||||||
rebuild_projections(
|
rebuild_projections(
|
||||||
ctx.clone(),
|
ctx.clone(),
|
||||||
rt_int.clone(),
|
rt_int.clone(),
|
||||||
|
@ -142,7 +131,7 @@ fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
),
|
),
|
||||||
|
|
||||||
// Big Endian Editor
|
// Little Endian Editor
|
||||||
(
|
(
|
||||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree>"
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree>"
|
||||||
|
@ -160,47 +149,33 @@ fn setup_be_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
.collect()
|
.collect()
|
||||||
);
|
);
|
||||||
|
|
||||||
/*
|
|
||||||
/*
|
let rt_digitseq =
|
||||||
* map seq of chars to seq of u64 digits
|
rt_int.descend(Context::parse(&ctx, "
|
||||||
* and add this projection to the ReprTree
|
<PosInt 16 LittleEndian>
|
||||||
*/
|
~ <Seq <Digit 16>>
|
||||||
//
|
~ <List <Digit 16>>
|
||||||
//VVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVV
|
")).expect("test");
|
||||||
let mut chars_view = rt_int.descend(Context::parse(&ctx, "
|
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||||
<PosInt 16 BigEndian>
|
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||||
~ <Seq <Digit 16>>
|
ctx.read().unwrap().morphisms
|
||||||
~ <List <Digit 16>~Char>
|
.apply_list_map_morphism::<char, u64>(
|
||||||
")).expect("cant descend")
|
rt_digitseq, src_type, dst_type
|
||||||
.read().unwrap()
|
|
||||||
.get_port::<dyn ListView<char>>()
|
|
||||||
.unwrap();
|
|
||||||
|
|
||||||
let mut digits_view = chars_view
|
|
||||||
.to_sequence()
|
|
||||||
.filter_map(
|
|
||||||
|digit_char|
|
|
||||||
|
|
||||||
/* TODO: call morphism for each item
|
|
||||||
*/
|
|
||||||
match digit_char.to_digit(16) {
|
|
||||||
Some(d) => Some(d as u64),
|
|
||||||
None => None
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
rt_int.attach_leaf_to(Context::parse(&ctx, "
|
rebuild_projections(
|
||||||
<PosInt 16 BigEndian>
|
ctx.clone(),
|
||||||
~ <Seq <Digit 16>
|
rt_int.clone(),
|
||||||
~ ℤ_2^64
|
vec![
|
||||||
~ machine.UInt64 >
|
// Little Endian Editor
|
||||||
"),
|
(
|
||||||
digits_view.clone()
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||||
|
),
|
||||||
|
].into_iter()
|
||||||
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
|
.collect()
|
||||||
);
|
);
|
||||||
|
|
||||||
//ΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛΛ
|
|
||||||
//
|
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[async_std::main]
|
#[async_std::main]
|
||||||
|
@ -309,6 +284,47 @@ async fn main() {
|
||||||
SingletonBuffer::new(0).get_port()
|
SingletonBuffer::new(0).get_port()
|
||||||
).unwrap();
|
).unwrap();
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
let rt_digitseq =
|
||||||
|
rt_int.descend(Context::parse(&ctx, "
|
||||||
|
<PosInt 16 LittleEndian>
|
||||||
|
~ <Seq <Digit 16>>
|
||||||
|
~ <List <Digit 16>>
|
||||||
|
")).expect("test");
|
||||||
|
let src_type = Context::parse(&ctx, "<Digit 16> ~ Char");
|
||||||
|
let dst_type = Context::parse(&ctx, "<Digit 16> ~ ℤ_2^64 ~ machine.UInt64");
|
||||||
|
ctx.read().unwrap().morphisms
|
||||||
|
.apply_list_map_morphism::<char, u64>(
|
||||||
|
rt_digitseq, src_type, dst_type
|
||||||
|
);
|
||||||
|
|
||||||
|
let hex_digits_view = rt_int.descend(Context::parse(&ctx, "
|
||||||
|
<PosInt 16 LittleEndian>
|
||||||
|
~ <Seq <Digit 16> >
|
||||||
|
~ <List <Digit 16>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
|
")).expect("descend")
|
||||||
|
.view_list::<u64>()
|
||||||
|
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 16)))
|
||||||
|
.to_sequence()
|
||||||
|
.to_grid_horizontal()
|
||||||
|
;
|
||||||
|
|
||||||
|
let dec_digits_view = rt_int.descend(Context::parse(&ctx, "
|
||||||
|
<PosInt 10 LittleEndian>
|
||||||
|
~ <Seq <Digit 10>>
|
||||||
|
~ <List <Digit 10>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
|
")).expect("descend")
|
||||||
|
.view_list::<u64>()
|
||||||
|
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 10)))
|
||||||
|
.to_sequence()
|
||||||
|
.to_grid_horizontal()
|
||||||
|
;
|
||||||
|
|
||||||
/* list of both editors
|
/* list of both editors
|
||||||
*/
|
*/
|
||||||
let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "<Seq Char>"));
|
let mut list_editor = nested::editors::list::ListEditor::new(ctx.clone(), Context::parse(&ctx, "<Seq Char>"));
|
||||||
|
@ -392,18 +408,15 @@ async fn main() {
|
||||||
|
|
||||||
/* project the seq of u64 representations to a view
|
/* project the seq of u64 representations to a view
|
||||||
*/
|
*/
|
||||||
/*
|
|
||||||
comp.push(nested_tty::make_label("dec: ").offset(Vector2::new(3,7)));
|
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| {
|
comp.push(dec_digits_view.offset(Vector2::new(8,7)).map_item(|_,a| {
|
||||||
a.add_style_back(TerminalStyle::fg_color((30,90,200)))
|
a.add_style_back(TerminalStyle::fg_color((30,90,200)))
|
||||||
}));
|
}));
|
||||||
*/
|
|
||||||
/*
|
|
||||||
comp.push(nested_tty::make_label("hex: ").offset(Vector2::new(3,8)));
|
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| {
|
comp.push(hex_digits_view.offset(Vector2::new(8,8)).map_item(|_,a| {
|
||||||
a.add_style_back(TerminalStyle::fg_color((200, 200, 30)))
|
a.add_style_back(TerminalStyle::fg_color((200, 200, 30)))
|
||||||
}));
|
}));
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/* write the changes in the view of `term_port` to the terminal
|
/* write the changes in the view of `term_port` to the terminal
|
||||||
|
|
|
@ -92,14 +92,17 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
move |rt: &mut Arc<RwLock<ReprTree>>, σ: &std::collections::HashMap<laddertypes::TypeID, TypeTerm>| {
|
move |rt: &mut Arc<RwLock<ReprTree>>, σ: &std::collections::HashMap<laddertypes::TypeID, TypeTerm>| {
|
||||||
/* infer radix from type
|
/* infer radix from type
|
||||||
*/
|
*/
|
||||||
|
let radix_typeid = ctx.read().unwrap().get_var_typeid("Radix").unwrap();
|
||||||
let radix =
|
let radix =
|
||||||
match σ.get( &laddertypes::TypeID::Var(ctx.read().unwrap().get_var_typeid("Radix").unwrap()) ) {
|
match σ.get( &laddertypes::TypeID::Var(radix_typeid) ) {
|
||||||
Some(TypeTerm::Num(n)) => (*n) as u32,
|
Some(TypeTerm::Num(n)) => (*n) as u32,
|
||||||
_ => 0
|
x => {
|
||||||
|
eprintln!("invalid radix {:?}", x);
|
||||||
|
0
|
||||||
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
if radix <= 16 {
|
if radix <= 16 {
|
||||||
|
|
||||||
if let Some(src_rt) = rt.descend(Context::parse(&ctx, "Char")) {
|
if let Some(src_rt) = rt.descend(Context::parse(&ctx, "Char")) {
|
||||||
/* insert projected view into ReprTree
|
/* insert projected view into ReprTree
|
||||||
*/
|
*/
|
||||||
|
|
|
@ -16,7 +16,6 @@ use {
|
||||||
|
|
||||||
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
// TODO: proper scoping
|
// TODO: proper scoping
|
||||||
ctx.write().unwrap().add_varname("Radix");
|
|
||||||
ctx.write().unwrap().add_varname("SrcRadix");
|
ctx.write().unwrap().add_varname("SrcRadix");
|
||||||
ctx.write().unwrap().add_varname("DstRadix");
|
ctx.write().unwrap().add_varname("DstRadix");
|
||||||
|
|
||||||
|
@ -281,24 +280,66 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
/*
|
||||||
|
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")
|
||||||
|
.view_list::<char>();
|
||||||
|
|
||||||
|
src_rt.attach_leaf_to(
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
< PosInt Radix LittleEndian >
|
||||||
|
~ < Seq <Digit Radix> >
|
||||||
|
~ < List <Digit Radix>~Char >
|
||||||
|
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||||
|
src_digits.reverse()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
);
|
||||||
|
*/
|
||||||
|
|
||||||
let morphism_type = MorphismType {
|
let morphism_type = MorphismType {
|
||||||
src_type: Context::parse(&ctx, "
|
src_type: Context::parse(&ctx, "
|
||||||
ℕ
|
ℕ
|
||||||
~ <PosInt SrcRadix LittleEndian>
|
~ <PosInt SrcRadix LittleEndian>
|
||||||
~ <Seq <Digit SrcRadix>
|
~ <Seq <Digit SrcRadix>>
|
||||||
|
~ <List <Digit SrcRadix>
|
||||||
~ ℤ_2^64
|
~ ℤ_2^64
|
||||||
~ machine.UInt64>
|
~ machine.UInt64>
|
||||||
"),
|
"),
|
||||||
dst_type: Context::parse(&ctx, "
|
dst_type: Context::parse(&ctx, "
|
||||||
ℕ
|
ℕ
|
||||||
~ <PosInt DstRadix LittleEndian>
|
~ <PosInt DstRadix LittleEndian>
|
||||||
~ <Seq <Digit DstRadix>
|
~ <Seq <Digit DstRadix>>
|
||||||
|
~ <List <Digit DstRadix>
|
||||||
~ ℤ_2^64
|
~ ℤ_2^64
|
||||||
~ machine.UInt64 >
|
~ machine.UInt64>
|
||||||
")
|
")
|
||||||
};
|
};
|
||||||
|
|
||||||
|
@ -323,19 +364,27 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
|
|
||||||
let src_digits_rt = src_rt.descend(Context::parse(&ctx, "
|
let src_digits_rt = src_rt.descend(Context::parse(&ctx, "
|
||||||
<PosInt SrcRadix LittleEndian>
|
<PosInt SrcRadix LittleEndian>
|
||||||
~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64 >
|
~ <Seq <Digit SrcRadix>>
|
||||||
|
~ <List <Digit SrcRadix>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
).expect("cant descend repr tree");
|
).expect("cant descend repr tree");
|
||||||
|
|
||||||
let dst_digits_port =
|
let dst_digits_port =
|
||||||
src_digits_rt.view_seq::<u64>()
|
src_digits_rt.view_list::<u64>()
|
||||||
|
.to_sequence()
|
||||||
.to_positional_uint( src_radix )
|
.to_positional_uint( src_radix )
|
||||||
.transform_radix( dst_radix );
|
.transform_radix( dst_radix )
|
||||||
|
.to_list();
|
||||||
|
|
||||||
src_rt.attach_leaf_to(
|
src_rt.attach_leaf_to(
|
||||||
Context::parse(&ctx, "
|
Context::parse(&ctx, "
|
||||||
<PosInt DstRadix LittleEndian>
|
<PosInt DstRadix LittleEndian>
|
||||||
~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>
|
~ <Seq <Digit DstRadix> >
|
||||||
|
~ <List <Digit DstRadix>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||||
dst_digits_port
|
dst_digits_port
|
||||||
);
|
);
|
||||||
|
|
|
@ -515,6 +515,10 @@ impl ReprTree {
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
pub fn view_singleton<T: 'static>(&self) -> OuterViewPort<dyn SingletonView<Item = T>> {
|
||||||
|
self.get_port::<dyn SingletonView<Item = T>>().expect("no singleton-view available")
|
||||||
|
}
|
||||||
|
|
||||||
pub fn view_seq<T: 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>> {
|
pub fn view_seq<T: 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>> {
|
||||||
self.get_port::<dyn SequenceView<Item = T>>().expect("no sequence-view available")
|
self.get_port::<dyn SequenceView<Item = T>>().expect("no sequence-view available")
|
||||||
}
|
}
|
||||||
|
@ -560,6 +564,7 @@ pub trait ReprTreeExt {
|
||||||
fn view_u64(&self) -> OuterViewPort<dyn SingletonView<Item = u64>>;
|
fn view_u64(&self) -> OuterViewPort<dyn SingletonView<Item = u64>>;
|
||||||
fn view_usize(&self) -> OuterViewPort<dyn SingletonView<Item = usize>>;
|
fn view_usize(&self) -> OuterViewPort<dyn SingletonView<Item = usize>>;
|
||||||
|
|
||||||
|
fn view_singleton<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SingletonView<Item = T>>;
|
||||||
fn view_seq<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>>;
|
fn view_seq<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>>;
|
||||||
fn view_list<T: Clone + Send + Sync + 'static>(&self) -> OuterViewPort<dyn ListView<T>>;
|
fn view_list<T: Clone + Send + Sync + 'static>(&self) -> OuterViewPort<dyn ListView<T>>;
|
||||||
|
|
||||||
|
@ -622,6 +627,10 @@ impl ReprTreeExt for Arc<RwLock<ReprTree>> {
|
||||||
self.read().unwrap().view_usize()
|
self.read().unwrap().view_usize()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn view_singleton<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SingletonView<Item = T>> {
|
||||||
|
self.read().unwrap().view_singleton::<T>()
|
||||||
|
}
|
||||||
|
|
||||||
fn view_seq<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>> {
|
fn view_seq<T: Send + Sync + 'static>(&self) -> OuterViewPort<dyn SequenceView<Item = T>> {
|
||||||
self.read().unwrap().view_seq::<T>()
|
self.read().unwrap().view_seq::<T>()
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
use {
|
use {
|
||||||
laddertypes::{TypeTerm, TypeID},
|
laddertypes::{TypeTerm, TypeID},
|
||||||
r3vi::view::AnyOuterViewPort,
|
r3vi::view::{AnyOuterViewPort, port::UpdateTask},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf},
|
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf},
|
||||||
},
|
},
|
||||||
|
@ -128,26 +128,78 @@ impl MorphismBase {
|
||||||
eprintln!("could not find morphism\n {:?}\n ====>\n {:?}", src_type, dst_type);
|
eprintln!("could not find morphism\n {:?}\n ====>\n {:?}", src_type, dst_type);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
/*
|
|
||||||
pub fn apply_seq_map_morphism<SrcItem, DstItem>(
|
|
||||||
&self,
|
|
||||||
mut repr_tree: Arc<RwLock<ReprTree>>,
|
|
||||||
src_item_type: &TypeTerm,
|
|
||||||
dst_item_type: &TypeTerm
|
|
||||||
) {
|
|
||||||
if let Some((item_morphism, σ)) = self.find_morphism( &src_item_type, dst_item_type ) {
|
|
||||||
|
|
||||||
let src_port = repr_tree.read().unwrap().get_port::<dyn SequenceView<Item = Arc<RwLock<ReprTree>> >>().unwrap();
|
pub fn apply_list_map_morphism<
|
||||||
src_port.map(
|
SrcItem: Clone + Send + Sync + 'static,
|
||||||
m.setup_projection
|
DstItem: Clone + Send + Sync + 'static
|
||||||
)
|
>(
|
||||||
|
&self,
|
||||||
(m.setup_projection)( &mut repr_tree, &σ );
|
repr_tree: Arc<RwLock<ReprTree>>,
|
||||||
|
mut src_item_type: TypeTerm,
|
||||||
|
mut dst_item_type: TypeTerm
|
||||||
|
) {
|
||||||
|
if let Some((item_morphism, s, σ)) = self.find_morphism_ladder( &src_item_type, &dst_item_type ) {
|
||||||
|
let sl = s.get_lnf_vec().len()+1;
|
||||||
|
(&mut src_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||||
|
(&mut dst_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||||
|
|
||||||
|
let src_item_type =
|
||||||
|
TypeTerm::Ladder({
|
||||||
|
let mut l = src_item_type.clone().get_lnf_vec();
|
||||||
|
for i in 0..sl { l.remove(0); }
|
||||||
|
l
|
||||||
|
});
|
||||||
|
let dst_item_type =
|
||||||
|
TypeTerm::Ladder({
|
||||||
|
let mut l = dst_item_type.clone().get_lnf_vec();
|
||||||
|
for i in 0..sl { l.remove(0); }
|
||||||
|
l
|
||||||
|
});
|
||||||
|
|
||||||
|
let src_lst_type =
|
||||||
|
TypeTerm::App(vec![
|
||||||
|
TypeTerm::TypeID(TypeID::Fun(10 /* FIXME: remove magic */)),
|
||||||
|
src_item_type.clone()
|
||||||
|
]);
|
||||||
|
let dst_lst_type =
|
||||||
|
TypeTerm::App(vec![
|
||||||
|
TypeTerm::TypeID(TypeID::Fun(10 /* FIXME: remove magic */)),
|
||||||
|
dst_item_type.clone()
|
||||||
|
]);
|
||||||
|
|
||||||
|
let src_port = repr_tree.descend( src_lst_type ).expect("descend src seq")
|
||||||
|
.view_list::<SrcItem>();
|
||||||
|
|
||||||
|
let dst_view = src_port.map({
|
||||||
|
let dst_item_type = dst_item_type.clone();
|
||||||
|
let item_morphism = item_morphism.clone();
|
||||||
|
move |x| {
|
||||||
|
let mut item_ladder = src_item_type.clone().get_lnf_vec();
|
||||||
|
let mut item_rt = ReprTree::from_singleton_buffer(
|
||||||
|
item_ladder.remove( item_ladder.len() - 1 ),
|
||||||
|
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
||||||
|
);
|
||||||
|
while item_ladder.len() > 0 {
|
||||||
|
let mut n = ReprTree::new_arc( item_ladder.remove( item_ladder.len() - 1) );
|
||||||
|
n.insert_branch( item_rt );
|
||||||
|
item_rt = n;
|
||||||
|
}
|
||||||
|
(item_morphism.setup_projection)( &mut item_rt, &σ );
|
||||||
|
item_rt.descend( dst_item_type.clone() ).expect("descend to item rt")
|
||||||
|
.view_singleton::< DstItem >()
|
||||||
|
.get_view().unwrap()
|
||||||
|
.get()
|
||||||
|
}
|
||||||
|
});
|
||||||
|
|
||||||
|
repr_tree.attach_leaf_to(
|
||||||
|
dst_lst_type,
|
||||||
|
dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView<DstItem> >
|
||||||
|
);
|
||||||
} else {
|
} else {
|
||||||
eprintln!("could not find item morphism");
|
eprintln!("could not find item morphism");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
Loading…
Reference in a new issue