From 6e2b82585ebfb8dd7e947de837ba2aaa49a3559e Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Tue, 6 Aug 2024 16:20:02 +0200 Subject: [PATCH] in context.apply_morphism() now use find_morphism_path() to automatically find chained morphisms to create projections in ReprTree --- examples/tty-02-digit/src/main.rs | 21 +- examples/tty-03-string/src/main.rs | 41 ++- examples/tty-04-posint/src/main.rs | 212 ++----------- lib-nested-core/src/editors/char/mod.rs | 38 +-- lib-nested-core/src/editors/digit/ctx.rs | 87 ++---- lib-nested-core/src/editors/integer/ctx.rs | 335 ++++----------------- lib-nested-core/src/editors/list/ctx.rs | 128 ++++---- lib-nested-core/src/repr_tree/context.rs | 41 ++- lib-nested-core/src/repr_tree/mod.rs | 2 +- lib-nested-core/src/repr_tree/morphism.rs | 302 ++++++------------- lib-nested-core/src/repr_tree/node.rs | 15 +- lib-nested-core/src/repr_tree/tests.rs | 24 +- lib-nested-tty/src/editors/list.rs | 10 +- 13 files changed, 395 insertions(+), 861 deletions(-) diff --git a/examples/tty-02-digit/src/main.rs b/examples/tty-02-digit/src/main.rs index c7df17e..60f6032 100644 --- a/examples/tty-02-digit/src/main.rs +++ b/examples/tty-02-digit/src/main.rs @@ -69,16 +69,19 @@ async fn main() { /* furthermore, setup projections to and from u8 value, * this synchronizes the buffers */ - ctx.read().unwrap().morphisms.apply_morphism( - rt_digit.clone(), - &Context::parse(&ctx, "~Char"), - &Context::parse(&ctx, "~ℤ_2^64~machine.UInt64") + ctx.read().unwrap().apply_morphism( + &rt_digit, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~Char"), + dst_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64") + } ); - - ctx.read().unwrap().morphisms.apply_morphism( - rt_digit.clone(), - &Context::parse(&ctx, "~Char"), - &Context::parse(&ctx, "~EditTree") + ctx.read().unwrap().apply_morphism( + &rt_digit, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~Char"), + dst_type: Context::parse(&ctx, "~EditTree") + } ); /* setup TTY-Display for DigitEditor diff --git a/examples/tty-03-string/src/main.rs b/examples/tty-03-string/src/main.rs index dfa84e1..c0b1bfc 100644 --- a/examples/tty-03-string/src/main.rs +++ b/examples/tty-03-string/src/main.rs @@ -45,21 +45,16 @@ async fn main() { */ let mut rt_string = ReprTree::new_arc( Context::parse(&ctx, "") ); - let vec = VecBuffer::>>::new(); rt_string.insert_leaf( - Context::parse(&ctx, " ~ "), - nested::repr_tree::ReprLeaf::from_vec_buffer( vec.clone() ) + Context::parse(&ctx, ""), + nested::repr_tree::ReprLeaf::from_vec_buffer( VecBuffer::>>::new() ) ); - - let v2 = VecBuffer::::new(); - rt_string.insert_leaf( - Context::parse(&ctx, ""), - nested::repr_tree::ReprLeaf::from_vec_buffer( v2.clone() ) - ); - ctx.read().unwrap().morphisms.apply_morphism( - rt_string.clone(), - &Context::parse(&ctx, " ~ "), - &Context::parse(&ctx, " ~ EditTree") + ctx.read().unwrap().apply_morphism( + &rt_string, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~"), + dst_type: Context::parse(&ctx, " ~ EditTree") + } ); /* Setup the Editor-View for this ReprTree @@ -74,10 +69,12 @@ async fn main() { * we apply a morphism that, given the List of Edit-Trees, extracts * the value from each EditTree and shows them in a ListView. */ - ctx.read().unwrap().morphisms.apply_morphism( - rt_string.clone(), - &Context::parse(&ctx, "~EditTree"), - &Context::parse(&ctx, "") + ctx.read().unwrap().apply_morphism( + &rt_string, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~EditTree"), + dst_type: Context::parse(&ctx, "") + } ); /* Now, get the ListView that serves our char-values. @@ -91,10 +88,12 @@ async fn main() { /* Lets add another morphism which will store the values * of the character-list in a `Vec` */ - ctx.read().unwrap().morphisms.apply_morphism( - rt_string.clone(), - &Context::parse(&ctx, ""), - &Context::parse(&ctx, "~") + ctx.read().unwrap().apply_morphism( + &rt_string, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, ""), + dst_type: Context::parse(&ctx, "~") + } ); /* Access the Vec object (wrapped behind a VecBuffer) diff --git a/examples/tty-04-posint/src/main.rs b/examples/tty-04-posint/src/main.rs index ed8311f..87ecfc1 100644 --- a/examples/tty-04-posint/src/main.rs +++ b/examples/tty-04-posint/src/main.rs @@ -32,131 +32,25 @@ use { std::sync::{Arc, RwLock}, }; -fn rebuild_projections( - ctx: Arc>, - repr_tree: Arc>, - morph_types: Vec< (laddertypes::TypeTerm, laddertypes::TypeTerm) > -) { - repr_tree.write().unwrap().detach(&ctx); - for (src_type, dst_type) in morph_types.iter() { - ctx.read().unwrap().morphisms.apply_morphism( - repr_tree.clone(), - &src_type, - &dst_type - ); - } -} - -fn setup_hex_master(ctx: &Arc>, rt_int: &Arc>) { - rebuild_projections( - ctx.clone(), - rt_int.clone(), - vec![ - // extract values from hex-editor - ( - "ℕ ~ ~ > ~ ~ Char> ~ EditTree", - "ℕ ~ ~ > ~ ~ Char>" - ), - - // convert to little-endian - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char>" - ), - // convert digit representation from char to u64 - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" - ), - // convert radix to decimal - ( - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" - ), - // convert decimal digit representation back to char - ( - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", - "ℕ ~ ~ > ~ ~ Char>" - ), - // convert to big-endian - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char>" - ), - - // decimal editor - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char ~ EditTree>" - ), - ( - "ℕ ~ ~ > ~ ~ Char ~ EditTree>", - "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ " - ), - ( - "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ ", - "ℕ ~ ~ > ~ ~ Char> ~ EditTree" - ), - - ].into_iter() - .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) - .collect() +fn setup_hex_master(ctx: &Arc>, rt_int: &Arc>) { + rt_int.write().unwrap().detach( ctx ); + ctx.read().unwrap().apply_morphism( + rt_int, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ EditTree"), + dst_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ EditTree") + } ); } fn setup_dec_master(ctx: &Arc>, rt_int: &Arc>) { - rebuild_projections( - ctx.clone(), - rt_int.clone(), - vec![ - // extract values from decimal-editor - ( - "ℕ ~ ~ > ~ ~ Char> ~ EditTree", - "ℕ ~ ~ > ~ ~ Char>" - ), - - // convert to little-endian - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char>" - ), - // convert digit representation to u64 - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" - ), - // convert radix to decimal - ( - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>" - ), - // convert back digit representation char - ( - "ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64>", - "ℕ ~ ~ > ~ ~ Char>" - ), - // convert back to big-endian - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char>" - ), - - // hex editor - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char ~ EditTree>" - ), - ( - "ℕ ~ ~ > ~ ~ Char ~ EditTree>", - "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ " - ), - ( - "ℕ ~ ~ > ~ ~ Char ~ EditTree> ~ ", - "ℕ ~ ~ > ~ ~ Char> ~ EditTree" - ), - ].into_iter() - .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) - .collect() + rt_int.write().unwrap().detach( ctx ); + ctx.read().unwrap().apply_morphism( + rt_int, + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ EditTree"), + dst_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ EditTree") + } ); } @@ -177,71 +71,20 @@ async fn main() { /* Add a specific Representation-Path (big-endian hexadecimal) */ - let mut digits_hex = VecBuffer::with_data(vec![ 'c', 'f', 'f' ]); rt_int.insert_leaf( Context::parse(&ctx, "~>~>~~"), - nested::repr_tree::ReprLeaf::from_vec_buffer( digits_hex.clone() ) - ); - - let mut digits_dec = VecBuffer::with_data(vec!['3', '2', '1']); - rt_int.insert_leaf( - Context::parse(&ctx, "~>~>~~"), - nested::repr_tree::ReprLeaf::from_vec_buffer( digits_dec.clone() ) - ); - - let mut digits_hex_editvec = VecBuffer::>>::new(); - rt_int.insert_leaf( - Context::parse(&ctx, " - - ~ > - ~ - ~ Char - ~ EditTree> - ~ - "), - nested::repr_tree::ReprLeaf::from_vec_buffer( digits_hex_editvec.clone() ) - ); - - let mut digits_dec_editvec = VecBuffer::>>::new(); - rt_int.insert_leaf( - Context::parse(&ctx, " - - ~ > - ~ - ~ Char - ~ EditTree> - ~ - "), - nested::repr_tree::ReprLeaf::from_vec_buffer( digits_dec_editvec.clone() ) - ); + nested::repr_tree::ReprLeaf::from_vec_buffer( + VecBuffer::with_data(vec![ 'c', 'f', 'f' ] + ))); /* initially copy values from Vec to EditTree... */ - rebuild_projections( - ctx.clone(), - rt_int.clone(), - // master representation - vec![ - ( - "ℕ ~ ~ > ~ ~ Char> ~ ", - "ℕ ~ ~ > ~ ~ Char>" - ), - ( - "ℕ ~ ~ > ~ ~ Char>", - "ℕ ~ ~ > ~ ~ Char ~ EditTree>" - ), - ( - "ℕ ~ ~ > ~ ~ Char> ~ ", - "ℕ ~ ~ > ~ ~ Char> ~ ~ " - ), - ( - "ℕ ~ ~ > ~ ~ Char> ~ ~ ", - "ℕ ~ ~ > ~ ~ Char> ~ EditTree" - ), - ].into_iter() - .map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d))) - .collect() - ); + ctx.read().unwrap().apply_morphism( + &rt_int, + &nested::repr_tree::morphism::MorphismType { + src_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ "), + dst_type: Context::parse(&ctx, "ℕ ~ ~ > ~ ~ Char> ~ EditTree") + }); setup_hex_master(&ctx, &rt_int); @@ -267,7 +110,6 @@ async fn main() { SingletonBuffer::new(0).get_port() ).unwrap().get(); - let hex_digits_view = rt_int.descend(Context::parse(&ctx, " ~ > @@ -278,8 +120,7 @@ async fn main() { .view_list::() .map(|v| TerminalAtom::from(char::from_digit(*v as u32, 16))) .to_sequence() - .to_grid_horizontal() - ; + .to_grid_horizontal(); let dec_digits_view = rt_int.descend(Context::parse(&ctx, " @@ -291,8 +132,7 @@ async fn main() { .view_list::() .map(|v| TerminalAtom::from(char::from_digit(*v as u32, 10))) .to_sequence() - .to_grid_horizontal() - ; + .to_grid_horizontal(); /* list of both editors */ diff --git a/lib-nested-core/src/editors/char/mod.rs b/lib-nested-core/src/editors/char/mod.rs index fb9abae..3d33efc 100644 --- a/lib-nested-core/src/editors/char/mod.rs +++ b/lib-nested-core/src/editors/char/mod.rs @@ -9,7 +9,7 @@ use { }, laddertypes::{TypeTerm}, crate::{ - repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt}, + repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt, GenericReprTreeMorphism}, edit_tree::{EditTree, TreeNavResult}, editors::ObjCommander, }, @@ -18,21 +18,16 @@ use { }; pub fn init_ctx( ctx: Arc> ) { - let morphtype = - crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "Char"), - dst_type: Context::parse(&ctx, "Char~EditTree") - }; - ctx.write().unwrap() - .morphisms - .add_morphism( - morphtype, - { - let ctx = ctx.clone(); - move |rt, σ| { - { - let mut b = rt.write().unwrap().singleton_buffer::(); + let char_morph_to_edittree = GenericReprTreeMorphism::new( + Context::parse(&ctx, "Char"), + Context::parse(&ctx, "Char~EditTree"), + { + let ctx = ctx.clone(); + move |rt, σ| { + + { + let mut b = rt.write().unwrap().singleton_buffer::(); if let Some(buf) = b { // buffer already exists } else { @@ -56,7 +51,11 @@ pub fn init_ctx( ctx: Arc> ) { rt.insert_leaf( Context::parse(&ctx, "EditTree"), - ReprLeaf::from_singleton_buffer(SingletonBuffer::new(Arc::new(RwLock::new(edittree)))) + ReprLeaf::from_singleton_buffer( + SingletonBuffer::new( + Arc::new(RwLock::new(edittree)) + ) + ) ); ctx.read().unwrap().setup_edittree( @@ -64,8 +63,11 @@ pub fn init_ctx( ctx: Arc> ) { SingletonBuffer::new(0).get_port() ); } - } - ); + + } + ); + + ctx.write().unwrap().morphisms.add_morphism( char_morph_to_edittree ); } pub struct CharEditor { diff --git a/lib-nested-core/src/editors/digit/ctx.rs b/lib-nested-core/src/editors/digit/ctx.rs index 40a7826..d2d22ae 100644 --- a/lib-nested-core/src/editors/digit/ctx.rs +++ b/lib-nested-core/src/editors/digit/ctx.rs @@ -9,28 +9,21 @@ use { } }, crate::{ - repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf}, + repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf, GenericReprTreeMorphism}, editors::digit::DigitEditor, }, std::sync::{Arc, RwLock} }; pub fn init_ctx( ctx: Arc> ) { - // todo: proper scoping of Radix variable ctx.write().unwrap().add_varname("Radix"); - let morphtype = - crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~Char"), - dst_type: Context::parse(&ctx, "~EditTree") - }; + let digit_morph_char_to_edittree = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~Char"), + Context::parse(&ctx, "~EditTree"), - ctx.write().unwrap() - .morphisms - .add_morphism( - morphtype, - { + { let ctx = ctx.clone(); move |src_rt, σ| { let radix = @@ -39,32 +32,14 @@ pub fn init_ctx( ctx: Arc> ) { _ => 0 }; - /* get char representation or create it if not available - */ - let char_rt = - if let Some(crt) = src_rt.descend(Context::parse(&ctx, "Char")) { - crt - } else { - /* TODO: replace this with some formal specification - * of "required representations" - */ - let crt = ReprTree::from_singleton_buffer( - Context::parse(&ctx, "Char"), - SingletonBuffer::new('\0') - ); - src_rt.insert_branch(crt.clone()); - crt - }; - /* Create EditTree object */ let mut edittree = DigitEditor::new( ctx.clone(), radix, - src_rt.descend( - Context::parse(&ctx, "Char") - ).unwrap() - .singleton_buffer::() + src_rt + .descend( Context::parse(&ctx, "Char") ).unwrap() + .singleton_buffer::() ).into_node( r3vi::buffer::singleton::SingletonBuffer::::new(0).get_port() ); @@ -77,22 +52,16 @@ pub fn init_ctx( ctx: Arc> ) { ) ); } - } - ); + } + ); - let morphtype = - crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~Char"), - dst_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64") - }; + let digit_morph_char_to_u64 = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~Char"), + Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), - ctx.write().unwrap() - .morphisms - .add_morphism( - morphtype, - { - let ctx = ctx.clone(); - move |rt: &mut Arc>, σ: &std::collections::HashMap| { + { + let ctx = ctx.clone(); + move |rt: &mut Arc>, σ: &std::collections::HashMap| { /* infer radix from type */ let radix_typeid = ctx.read().unwrap().get_var_typeid("Radix").unwrap(); @@ -123,19 +92,15 @@ pub fn init_ctx( ctx: Arc> ) { } else { eprintln!("radix too large ({})", radix); } - } } - ); + } + ); - let morphtype = - crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), - dst_type: Context::parse(&ctx, "~Char") - }; - - ctx.write().unwrap().morphisms - .add_morphism(morphtype, { + let digit_morph_u64_to_char = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), + Context::parse(&ctx, "~Char"), + { let ctx = ctx.clone(); move |rt: &mut Arc>, σ: &std::collections::HashMap| { /* infer radix from type @@ -163,7 +128,13 @@ pub fn init_ctx( ctx: Arc> ) { eprintln!("radix too large ({})", radix); } } - }); + } + ); + + + ctx.write().unwrap().morphisms.add_morphism( digit_morph_char_to_edittree ); + ctx.write().unwrap().morphisms.add_morphism( digit_morph_char_to_u64 ); + ctx.write().unwrap().morphisms.add_morphism( digit_morph_u64_to_char ); } diff --git a/lib-nested-core/src/editors/integer/ctx.rs b/lib-nested-core/src/editors/integer/ctx.rs index 868acec..dc6aa61 100644 --- a/lib-nested-core/src/editors/integer/ctx.rs +++ b/lib-nested-core/src/editors/integer/ctx.rs @@ -3,9 +3,9 @@ use { r3vi::{ view::{OuterViewPort, singleton::*, list::*} }, - laddertypes::{TypeTerm}, + laddertypes::{TypeTerm, MorphismType}, crate::{ - repr_tree::{ReprTree, ReprTreeExt, ReprLeaf, Context, MorphismType}, + repr_tree::{ReprTree, ReprTreeExt, ReprLeaf, Context, GenericReprTreeMorphism}, editors::{ list::*, integer::* @@ -20,312 +20,93 @@ pub fn init_ctx(ctx: Arc>) { ctx.write().unwrap().add_varname("DstRadix"); - /* - * MACHINE INT, SEQ - */ - let morphism_type = - MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ - ~ ℤ_2^64 - ~ machine.UInt64 >"), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ - ~ ℤ_2^64 - ~ machine.UInt64 >") - }; - ctx.write().unwrap().morphisms.add_morphism( - morphism_type, { + let posint_seq_morph_big_to_little = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), + { let ctx = ctx.clone(); move |src_rt, σ| { - let src_digits = src_rt.descend( - Context::parse(&ctx, " + let src_digits = src_rt + .descend(Context::parse(&ctx, " - ~ - ~ ℤ_2^64 - ~ machine.UInt64 > - ") + ~ ~ ℤ_2^64 ~ machine.UInt64 > + ") .apply_substitution(&|k|σ.get(k).cloned()) .clone() - ).expect("cant descend") - .view_seq::< u64 >(); + ).expect("cant descend") + .view_seq::< u64 >(); src_rt.attach_leaf_to(Context::parse(&ctx, " - ~ - ~ ℤ_2^64 - ~ machine.UInt64 > + ~ ~ ℤ_2^64 ~ machine.UInt64 > ").apply_substitution(&|k|σ.get(k).cloned()).clone(), src_digits.reverse() - ); + ); } } ); - /* MACHINE INT, LIST - */ - let morphism_type = MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ~ - "), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ~ - ") - }; - - ctx.write().unwrap().morphisms.add_morphism( - morphism_type, + let posint_list_morph_big_to_little = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), { let ctx = ctx.clone(); move |src_rt, σ| { - let src_digits = src_rt.descend(Context::parse(&ctx, " - - ~ > - ~ ~ ℤ_2^64 ~ machine.UInt64 > + let src_digits = src_rt + .descend(Context::parse(&ctx, " + + ~ ~ ℤ_2^64 ~ machine.UInt64 > ") - .apply_substitution(&|k|σ.get(k).cloned()).clone() - ).expect("cant descend") - .get_port::< dyn ListView >().unwrap(); + .apply_substitution(&|k|σ.get(k).cloned()) + .clone() + ).expect("cant descend") + .view_list::< u64 >(); - src_rt.attach_leaf_to( - Context::parse(&ctx, " - - ~ > - ~ ~ ℤ_2^64 ~ machine.UInt64> - ").apply_substitution(&|k| σ.get(k).cloned()).clone(), + src_rt.attach_leaf_to(Context::parse(&ctx, " + + ~ ~ ℤ_2^64 ~ machine.UInt64 > + ").apply_substitution(&|k|σ.get(k).cloned()).clone(), src_digits.reverse() - ); + ); } } ); - - let mt = MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - "), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ") - }; - ctx.write().unwrap().morphisms.add_morphism( - mt, + let posint_list_morph_little_to_big = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), + Context::parse(&ctx, "ℕ ~ + ~ ~ ℤ_2^64 ~ machine.UInt64 >"), { let ctx = ctx.clone(); move |src_rt, σ| { - let radix = σ.get( &laddertypes::TypeID::Var(ctx.read().unwrap().get_var_typeid("Radix").unwrap()) ); - let src_digits = src_rt.descend(Context::parse(&ctx, " - - ~ > - ~ ~Char > - ").apply_substitution(&|k|σ.get(k).cloned()).clone() - ).expect("cant descend") - .get_port::< dyn ListView >().unwrap(); - - let rev_port = src_digits.reverse(); - src_rt.attach_leaf_to( - Context::parse(&ctx, " - < PosInt Radix LittleEndian > - ~ < Seq > - ~ < List ~Char > - ").apply_substitution(&|k| σ.get(k).cloned()).clone(), - rev_port - ); - } - } - ); - - - - - - - let morphism_type = MorphismType { - src_type: Context::parse(&ctx, "ℕ ~ ~ ~ℤ_2^64~machine.UInt64>"), - dst_type: Context::parse(&ctx, "ℕ ~ ~ ~ℤ_2^64~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, " - - ~~ℤ_2^64~machine.UInt64 > + let src_digits = src_rt + .descend(Context::parse(&ctx, " + + ~ ~ ℤ_2^64 ~ machine.UInt64 > ") - .apply_substitution(&|k|σ.get(k).cloned()).clone() - ).expect("cant descend") - .view_seq::< u64 >(); + .apply_substitution(&|k|σ.get(k).cloned()) + .clone() + ).expect("cant descend") + .view_list::< u64 >(); src_rt.attach_leaf_to(Context::parse(&ctx, " - ~ ~ ℤ_2^64 ~ machine.UInt64> - ").apply_substitution(&|k|σ.get(k).cloned()).clone(), - src_digits.reverse() - ); - } - } - ); - - let morphism_type = - MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ~ - "), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ~ - ") - }; - ctx.write().unwrap().morphisms.add_morphism( - morphism_type, { - let ctx = ctx.clone(); - move |src_rt, σ| - { - let src_digits = src_rt.descend( - Context::parse(&ctx, " - - ~ > - ~ ~ℤ_2^64~machine.UInt64 > - ").apply_substitution(&|k|σ.get(k).cloned()).clone() - ) - .expect("cant descend") - .view_list::(); - - src_rt.attach_leaf_to( - Context::parse(&ctx, " - - ~ > - ~ ~ℤ_2^64~machine.UInt64 > + ~ ~ ℤ_2^64 ~ machine.UInt64 > ").apply_substitution(&|k|σ.get(k).cloned()).clone(), src_digits.reverse() - ); + ); } } ); - let mt = MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - "), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ") - }; - - ctx.write().unwrap().morphisms.add_morphism( - mt, - { - let ctx = ctx.clone(); - move |src_rt, σ| { - let src_digits = src_rt.descend(Context::parse(&ctx, " - - ~ > - ~ ~Char > - ").apply_substitution(&|k|σ.get(k).cloned()).clone() - ).expect("cant descend") - .view_list::(); - - src_rt.attach_leaf_to( - Context::parse(&ctx, " - < PosInt Radix BigEndian > - ~ < Seq > - ~ < List ~Char > - ").apply_substitution(&|k| σ.get(k).cloned()).clone(), - src_digits.reverse() - ); - } - } - ); -/* - let mt = MorphismType { - src_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - "), - dst_type: Context::parse(&ctx, " - ℕ - ~ - ~ > - ~ > - ~ - ") - }; - - ctx.write().unwrap().morphisms.add_morphism( - mt, - { - let ctx = ctx.clone(); - move |src_rt, σ| { - let src_digits = src_rt.descend(Context::parse(&ctx, " - - ~ > - ~ ~Char > - ").apply_substitution(&|k|σ.get(k).cloned()).clone() - ).expect("cant descend") - .view_list::(); - - src_rt.attach_leaf_to( - Context::parse(&ctx, " - < PosInt Radix LittleEndian > - ~ < Seq > - ~ < List ~Char > - ").apply_substitution(&|k| σ.get(k).cloned()).clone(), - src_digits.reverse() - ); - } - } - ); -*/ - - let morphism_type = MorphismType { - src_type: Context::parse(&ctx, " + let posint_list_morph_radix = GenericReprTreeMorphism::new( + Context::parse(&ctx, " ℕ ~ ~ > @@ -333,18 +114,14 @@ pub fn init_ctx(ctx: Arc>) { ~ ℤ_2^64 ~ machine.UInt64> "), - dst_type: Context::parse(&ctx, " + Context::parse(&ctx, " ℕ ~ ~ > ~ ~ ℤ_2^64 ~ machine.UInt64> - ") - }; - - ctx.write().unwrap().morphisms.add_morphism( - morphism_type, + "), { let ctx = ctx.clone(); move |src_rt, σ| { @@ -389,7 +166,13 @@ pub fn init_ctx(ctx: Arc>) { dst_digits_port ); } + } ); + + 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 ); + ctx.write().unwrap().morphisms.add_morphism( posint_list_morph_radix ); } diff --git a/lib-nested-core/src/editors/list/ctx.rs b/lib-nested-core/src/editors/list/ctx.rs index 93a47a5..56f0cf5 100644 --- a/lib-nested-core/src/editors/list/ctx.rs +++ b/lib-nested-core/src/editors/list/ctx.rs @@ -10,11 +10,11 @@ use { }, laddertypes::{TypeTerm}, crate::{ - repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt}, + repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt, GenericReprTreeMorphism}, edit_tree::{EditTree}, editors::{ char::{CharEditor}, - list::{ListEditor}//, PTYListController, PTYListStyle} + list::{ListEditor} } }, std::sync::{Arc, RwLock} @@ -25,49 +25,46 @@ use { pub fn init_ctx(ctx: Arc>) { ctx.write().unwrap().add_varname("Item"); - let mt = crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~~"), - dst_type: Context::parse(&ctx, "~EditTree") - }; + let list_morph_editsetup1 = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~~"), + Context::parse(&ctx, "~EditTree"), + { + 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_rt = src_rt + .descend( + Context::parse(&ctx, "~") + .apply_substitution(&|id| σ.get(id).cloned()).clone() + ) + .expect("cant descend src repr"); - 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_rt = src_rt - .descend( - Context::parse(&ctx, "~") - .apply_substitution(&|id| σ.get(id).cloned()).clone() - ) - .expect("cant descend src repr"); + let item_vec_buffer = item_vec_rt.vec_buffer::< Arc> >(); - let item_vec_buffer = item_vec_rt.vec_buffer::< Arc> >(); + let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer); + let edittree_list = list_editor.into_node( + SingletonBuffer::::new(0).get_port() + ); + src_rt.insert_leaf( + Context::parse(&ctx, " ~ EditTree") + .apply_substitution(&|id| σ.get(id).cloned()).clone(), - let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer); - let edittree_list = list_editor.into_node( - SingletonBuffer::::new(0).get_port() - ); - src_rt.insert_leaf( - Context::parse(&ctx, " ~ EditTree") - .apply_substitution(&|id| σ.get(id).cloned()).clone(), - - ReprLeaf::from_singleton_buffer( - SingletonBuffer::new(Arc::new(RwLock::new(edittree_list))) - ) - ); - } else { - eprintln!("no item type"); + ReprLeaf::from_singleton_buffer( + SingletonBuffer::new(Arc::new(RwLock::new(edittree_list))) + ) + ); + } else { + eprintln!("no item type"); + } } } - }); + ); - let mt = crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~EditTree"), - dst_type: Context::parse(&ctx, "") - }; - ctx.write().unwrap().morphisms.add_morphism( - mt, + + let list_morph_editsetup2 = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~EditTree"), + Context::parse(&ctx, ""), { let ctx = ctx.clone(); move |src_rt, σ| { @@ -93,54 +90,43 @@ pub fn init_ctx(ctx: Arc>) { ) ); } + } ); - - /* todo : unify the following two morphims with generic item parameter ? - */ - let mt = crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, ""), - dst_type: Context::parse(&ctx, "~") - }; - ctx.write().unwrap().morphisms.add_morphism( - mt, + let list_morph_to_vec_char = GenericReprTreeMorphism::new( + Context::parse(&ctx, ""), + Context::parse(&ctx, "~"), { let ctx = ctx.clone(); move |src_rt, σ| { - let list_view = src_rt.view_list::(); - - src_rt - .attach_leaf_to( - Context::parse(&ctx, ""), - list_view - ); + src_rt.attach_leaf_to( + Context::parse(&ctx, ""), + src_rt.view_list::() + ); } } ); - let mt = crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, "~"), - dst_type: Context::parse(&ctx, "") - }; - ctx.write().unwrap().morphisms.add_morphism( - mt, + let list_morph_from_vec_char = GenericReprTreeMorphism::new( + Context::parse(&ctx, "~"), + Context::parse(&ctx, ""), { let ctx = ctx.clone(); move |src_rt, σ| { let src_port = src_rt.descend(Context::parse(&ctx, "~")).expect("descend") .get_port::>>().unwrap(); - src_rt.attach_leaf_to( Context::parse(&ctx, ""), src_port.to_list() ); + + src_rt.attach_leaf_to( Context::parse(&ctx, ""), src_port.to_list() ); } } ); - let mt = crate::repr_tree::MorphismType { - src_type: Context::parse(&ctx, ""), - dst_type: Context::parse(&ctx, "~") - }; - ctx.write().unwrap().morphisms.add_morphism( - mt, + + let list_morph_to_vec_edittree = GenericReprTreeMorphism::new( + Context::parse(&ctx, ""), + Context::parse(&ctx, " ~ "), + { let ctx = ctx.clone(); move |src_rt, σ| { @@ -156,5 +142,11 @@ pub fn init_ctx(ctx: Arc>) { } } ); + + ctx.write().unwrap().morphisms.add_morphism( list_morph_editsetup1 ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_editsetup2 ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_from_vec_char ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_to_vec_char ); + ctx.write().unwrap().morphisms.add_morphism( list_morph_to_vec_edittree ); } diff --git a/lib-nested-core/src/repr_tree/context.rs b/lib-nested-core/src/repr_tree/context.rs index 71add2a..6bbff0b 100644 --- a/lib-nested-core/src/repr_tree/context.rs +++ b/lib-nested-core/src/repr_tree/context.rs @@ -1,8 +1,8 @@ use { r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}}, - laddertypes::{TypeDict, TypeTerm, TypeID}, + laddertypes::{TypeDict, TypeTerm, TypeID, MorphismType, MorphismBase, Morphism}, crate::{ - repr_tree::{ReprTree, ReprTreeExt, MorphismType, GenericReprTreeMorphism, MorphismBase}, + repr_tree::{ReprTree, ReprTreeExt, GenericReprTreeMorphism}, edit_tree::EditTree }, std::{ @@ -18,7 +18,7 @@ pub struct Context { /// assigns a name to every type pub type_dict: Arc>, - pub morphisms: MorphismBase, + pub morphisms: laddertypes::morphism::MorphismBase< GenericReprTreeMorphism >, /// named vertices of the graph nodes: HashMap< String, Arc> >, @@ -39,12 +39,15 @@ impl Context { pub fn with_parent( parent: Option>> ) -> Self { + let mut dict = TypeDict::new(); + let list_typeid = dict.add_typename("List".into()); + Context { type_dict: match parent.as_ref() { Some(p) => p.read().unwrap().type_dict.clone(), - None => Arc::new(RwLock::new(TypeDict::new())) + None => Arc::new(RwLock::new(dict)) }, - morphisms: MorphismBase::new(), + morphisms: MorphismBase::new( list_typeid ), nodes: HashMap::new(), list_types: match parent.as_ref() { Some(p) => p.read().unwrap().list_types.clone(), @@ -75,9 +78,35 @@ impl Context { } } + pub fn apply_morphism( &self, rt: &Arc>, ty: &MorphismType ) { + if let Some(path) + = self.morphisms.find_morphism_path( ty.clone().normalize() ) + { + let mut path = path.into_iter(); + if let Some(mut src_type) = path.next() { + for dst_type in path { + 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 { + eprintln!("no path found"); + } + } + pub fn make_repr(ctx: &Arc>, t: &TypeTerm) -> Arc> { let rt = Arc::new(RwLock::new(ReprTree::new( TypeTerm::unit() ))); - ctx.read().unwrap().morphisms.apply_morphism( rt.clone(), &TypeTerm::unit(), t ); + ctx.read().unwrap().apply_morphism( &rt, &MorphismType{ src_type: TypeTerm::unit(), dst_type: t.clone() } ); rt } diff --git a/lib-nested-core/src/repr_tree/mod.rs b/lib-nested-core/src/repr_tree/mod.rs index c2b71d4..5d05bf0 100644 --- a/lib-nested-core/src/repr_tree/mod.rs +++ b/lib-nested-core/src/repr_tree/mod.rs @@ -10,7 +10,7 @@ pub use { context::{Context}, leaf::ReprLeaf, node::ReprTree, - morphism::{MorphismType, GenericReprTreeMorphism, MorphismBase} + morphism::{GenericReprTreeMorphism} }; use { diff --git a/lib-nested-core/src/repr_tree/morphism.rs b/lib-nested-core/src/repr_tree/morphism.rs index 1607d6a..d8eaf3d 100644 --- a/lib-nested-core/src/repr_tree/morphism.rs +++ b/lib-nested-core/src/repr_tree/morphism.rs @@ -1,5 +1,5 @@ use { - laddertypes::{TypeTerm, TypeID}, + laddertypes::{TypeTerm, TypeID, morphism::Morphism}, r3vi::view::{AnyOuterViewPort, port::UpdateTask}, crate::{ repr_tree::{ReprTree, ReprTreeExt, ReprLeaf}, @@ -10,248 +10,144 @@ use { } }; -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> +pub use laddertypes::morphism::MorphismType; -#[derive(Clone, Hash, PartialEq, Eq, Debug)] -pub struct MorphismType { - pub src_type: TypeTerm, - pub dst_type: TypeTerm, -} +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> #[derive(Clone)] pub struct GenericReprTreeMorphism { - morph_type: MorphismType, - setup_projection: Arc< + pub(super) morph_type: MorphismType, + pub(super) setup_projection: Arc< dyn Fn( &mut Arc>, &HashMap ) // -> Result< ReprLeaf, () > + Send + Sync > } -#[derive(Clone)] -pub struct MorphismBase { - morphisms: Vec< GenericReprTreeMorphism > +impl Morphism for GenericReprTreeMorphism { + fn get_type(&self) -> MorphismType { + self.morph_type.clone() + } + + fn list_map_morphism(&self, list_typeid: TypeID) -> Option< GenericReprTreeMorphism > { + self.into_list_map_dyn(list_typeid) + } } -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> +impl GenericReprTreeMorphism { + pub fn new( + src_type: TypeTerm, + dst_type: TypeTerm, -impl MorphismBase { - pub fn new() -> Self { - MorphismBase { - morphisms: Vec::new() + setup: impl Fn( &mut Arc>, &HashMap ) + + Send + Sync + 'static + ) -> Self { + GenericReprTreeMorphism { + morph_type: MorphismType { + src_type, dst_type + }.normalize(), + + setup_projection: Arc::new(setup) } } - pub fn add_morphism( - &mut self, - morph_type: MorphismType, - setup_projection: - impl Fn( &mut Arc>, &HashMap ) -// -> Result< ReprLeaf, () /* TODO: error */ > - + Send + Sync + 'static - ) { - self.morphisms.push( - GenericReprTreeMorphism { - morph_type: MorphismType { - src_type: morph_type.src_type.normalize(), - dst_type: morph_type.dst_type.normalize() - }, - setup_projection: Arc::new(setup_projection) - } - ); - } - - pub fn find_morphism( - &self, - src_type: &TypeTerm, - dst_type: &TypeTerm - ) -> Option<(GenericReprTreeMorphism, HashMap)> { - - // try list-map morphism - if let Ok(σ) = laddertypes::UnificationProblem::new(vec![ - (src_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(TypeID::Fun(10)), TypeTerm::TypeID(TypeID::Var(100)) ])), - (dst_type.clone().param_normalize(), TypeTerm::App(vec![ TypeTerm::TypeID(TypeID::Fun(10)), TypeTerm::TypeID(TypeID::Var(101)) ])), - ]).solve() { - let src_item_type = σ.get(&TypeID::Var(100)).unwrap().clone(); - let dst_item_type = σ.get(&TypeID::Var(101)).unwrap().clone(); -/* - eprintln!("Got a List- Type, check if we find a list-map morphism"); - eprintln!("src-item-type : {:?}", src_item_type); - eprintln!("dst-item-type : {:?}", dst_item_type); -*/ - let src_item_type_lnf = src_item_type.clone().get_lnf_vec(); - let dst_item_type_lnf = dst_item_type.clone().get_lnf_vec(); - - /* if src_item_type ~== "Char", - dst_item_type ~== "machine.UInt64" - */ - if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(0))) && - dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(4))) - { - if let Some((m, σ)) = self.find_list_map_morphism::< char, u64 >( src_item_type, dst_item_type ) { - return Some((m, σ)); - } - } - - /* if src_item_type ~== "machine.UInt64", - dst_item_type ~== "Char" - */ - else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(4))) && - dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(0))) - { - if let Some((m, σ)) = self.find_list_map_morphism::< u64, char >( src_item_type, dst_item_type ) { - return Some((m, σ)); - } - } - - /* if src_item_type ~== "Char" - dst_item_type ~== "EditTree" - */ - else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(0))) && - dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(TypeID::Fun(1))) - { - if let Some((m, σ)) = self.find_list_map_morphism::< char, Arc> >( src_item_type, dst_item_type ) { - return Some((m, σ)); - } - } - } - - // otherwise - for m in self.morphisms.iter() { - let unification_problem = laddertypes::UnificationProblem::new( - vec![ - ( src_type.clone().normalize(), m.morph_type.src_type.clone() ), - ( dst_type.clone().normalize(), m.morph_type.dst_type.clone() ) - ] - ); - - let unification_result = unification_problem.solve(); - if let Ok(σ) = unification_result { - return Some((m.clone(), σ)); - } - } - - None - } - - - pub fn find_morphism_ladder( - &self, - src_type: &TypeTerm, - dst_type: &TypeTerm, - ) -> Option<( - GenericReprTreeMorphism, - TypeTerm, - HashMap - )> { - let mut src_lnf = src_type.clone().get_lnf_vec(); - let mut dst_lnf = dst_type.clone().get_lnf_vec(); - let mut halo = vec![]; - - while src_lnf.len() > 0 && dst_lnf.len() > 0 { - if let Some((m, σ)) = self.find_morphism( &TypeTerm::Ladder(src_lnf.clone()), &TypeTerm::Ladder(dst_lnf.clone()) ) { - return Some((m, TypeTerm::Ladder(halo), σ)); - } else { - if src_lnf[0] == dst_lnf[0] { - src_lnf.remove(0); - halo.push(dst_lnf.remove(0)); - } else { - return None; - } - } - } - - None - } - - pub fn apply_morphism( - &self, - repr_tree: Arc>, - src_type: &TypeTerm, - dst_type: &TypeTerm - ) { - if let Some((m, s, σ)) = self.find_morphism_ladder( &src_type, dst_type ) { - //eprintln!("apply morphism on subtree {:?}", s); - let mut rt = repr_tree.descend( s ).expect("descend"); - (m.setup_projection)( &mut rt, &σ ); - } else { - eprintln!("could not find morphism\n {:?}\n ====>\n {:?}", src_type, dst_type); - } - } - - pub fn find_list_map_morphism< + pub fn into_list_map< SrcItem, DstItem >(&self, list_typeid: TypeID) + -> GenericReprTreeMorphism + where SrcItem: Clone + Send + Sync + 'static, DstItem: Clone + Send + Sync + 'static - >( - &self, - mut src_item_type: TypeTerm, - mut dst_item_type: TypeTerm - ) -> Option< - ( GenericReprTreeMorphism, HashMap< TypeID, TypeTerm > ) - > { - if let Some((item_morphism, σ)) = self.find_morphism( &src_item_type, &dst_item_type ) { - (&mut src_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() ); - (&mut dst_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() ); - - 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 mut lst_map_type = MorphismType { + src_type: TypeTerm::App(vec![ + TypeTerm::TypeID(list_typeid), + self.morph_type.src_type.clone() + ]), + dst_type: TypeTerm::App(vec![ + TypeTerm::TypeID(list_typeid), + self.morph_type.dst_type.clone() + ]) + }.normalize(); - let sigmalol = σ.clone(); - let m = GenericReprTreeMorphism{ - morph_type: MorphismType { - src_type: src_lst_type.clone(), - dst_type: dst_lst_type.clone(), - }, - setup_projection: Arc::new(move |repr_tree, subst| { - let src_port = repr_tree.descend( src_lst_type.clone() ).expect("descend src seq") - .view_list::(); + let item_morph = self.clone(); - let src_item_type = src_item_type.clone(); - let dst_item_type = dst_item_type.clone(); - let item_morphism = item_morphism.clone(); - let subst = subst.clone(); + GenericReprTreeMorphism{ + morph_type: lst_map_type.clone(), + setup_projection: Arc::new(move |repr_tree, subst| { + let mut lst_map_type = lst_map_type.clone(); + lst_map_type.src_type.apply_substitution( &|x| subst.get(x).cloned() ); + lst_map_type.dst_type.apply_substitution( &|x| subst.get(x).cloned() ); - let dst_view = src_port.map( + eprintln!( + "lst map type : {:?}", lst_map_type + ); + + let src_port = repr_tree + .descend( lst_map_type.src_type.clone() ) + .expect("descend src seq") + .view_list::(); + + let subst = subst.clone(); + let item_morph = item_morph.clone(); + + let dst_view = src_port.map( move |x| { - let mut item_ladder = src_item_type.clone().get_lnf_vec(); + let mut item_ladder = item_morph.morph_type.src_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()) ); + // TODO: required? 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, &subst ); - item_rt.descend( dst_item_type.clone() ).expect("descend to item rt") + (item_morph.setup_projection)( &mut item_rt, &subst ); + item_rt.descend( item_morph.morph_type.dst_type.clone() ).expect("descend to item rt") .view_singleton::< DstItem >() .get_view().unwrap() .get() } - ); + ); - repr_tree.attach_leaf_to( - dst_lst_type.clone(), - dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView > - ); - }) - }; + repr_tree.attach_leaf_to( + lst_map_type.dst_type.clone(), + dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView > + ); + }) + } + } - Some((m, σ)) - } else { -// eprintln!("could not find item morphism\n"); + pub fn into_list_map_dyn(&self, typeid_list: TypeID) + -> Option< GenericReprTreeMorphism > + { + let typeid_char = TypeID::Fun(1); + let typeid_u64 = TypeID::Fun(5); + let typeid_edittree = TypeID::Fun(2); + + 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(); + + if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_char)) && + dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_u64)) + { + Some( self.into_list_map::< char, u64 >(typeid_list) ) + } + else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_u64)) && + dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_char)) + { + Some( self.into_list_map::< u64, char >(typeid_list) ) + } + else if src_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_char)) && + dst_item_type_lnf.last() == Some(&TypeTerm::TypeID(typeid_edittree)) + { + Some( self.into_list_map::< char, Arc> >(typeid_list) ) + } + else + { + eprintln!("no list map type for {:?}", dst_item_type_lnf.last()); None } } diff --git a/lib-nested-core/src/repr_tree/node.rs b/lib-nested-core/src/repr_tree/node.rs index 6cb0e2a..d6c3f99 100644 --- a/lib-nested-core/src/repr_tree/node.rs +++ b/lib-nested-core/src/repr_tree/node.rs @@ -13,7 +13,7 @@ use { }, buffer::{singleton::*, vec::*} }, - laddertypes::{TypeTerm}, + laddertypes::{TypeTerm, TypeID}, std::{ collections::HashMap, sync::{Arc, RwLock}, @@ -197,12 +197,23 @@ impl ReprTree { >::new() ); + leaf.attach_to(src_port); + self.leaf = Some(leaf); + } + else if self.type_tag == TypeTerm::App(vec![ + TypeTerm::TypeID(TypeID::Fun(11)), + TypeTerm::TypeID(TypeID::Fun(1)) + ]) { + let mut leaf = ReprLeaf::from_vec_buffer( + VecBuffer::::new() + ); + leaf.attach_to(src_port); self.leaf = Some(leaf); } else { self.leaf = Some(ReprLeaf::from_view(src_port)); } - } + } } pub fn detach(&mut self, ctx: &Arc>) { diff --git a/lib-nested-core/src/repr_tree/tests.rs b/lib-nested-core/src/repr_tree/tests.rs index 4e6aa21..8663cb7 100644 --- a/lib-nested-core/src/repr_tree/tests.rs +++ b/lib-nested-core/src/repr_tree/tests.rs @@ -83,10 +83,12 @@ fn digit_projection_char_to_u64() { //<><><><> // add another representation - ctx.read().unwrap().morphisms.apply_morphism( + ctx.read().unwrap().apply_morphism( rt_digit.clone(), - &Context::parse(&ctx, "~Char"), - &Context::parse(&ctx, "~ℤ_2^64~machine.UInt64") + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~Char"), + dst_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64") + } ); let digit_u64_view = rt_digit @@ -121,10 +123,12 @@ fn digit_projection_u64_to_char() { //<><><><> // add another representation - ctx.read().unwrap().morphisms.apply_morphism( + ctx.read().unwrap().apply_morphism( rt_digit.clone(), - &Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), - &Context::parse(&ctx, "~Char") + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), + dst_type: Context::parse(&ctx, "~Char") + } ); let digit_u64_view = rt_digit @@ -170,10 +174,12 @@ fn char_buffered_projection() { assert_eq!( digit_char_view.get_view().unwrap().get(), '5' ); // now we attach the char-repr to the u64-repr - ctx.read().unwrap().morphisms.apply_morphism( + ctx.read().unwrap().apply_morphism( rt_digit.clone(), - &Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), - &Context::parse(&ctx, "~Char") + &laddertypes::MorphismType { + src_type: Context::parse(&ctx, "~ℤ_2^64~machine.UInt64"), + dst_type: Context::parse(&ctx, "~Char") + } ); // char buffer and view should now follow the u64-buffer diff --git a/lib-nested-tty/src/editors/list.rs b/lib-nested-tty/src/editors/list.rs index f3ae4ee..c9fc849 100644 --- a/lib-nested-tty/src/editors/list.rs +++ b/lib-nested-tty/src/editors/list.rs @@ -228,10 +228,12 @@ impl PTYListController { rt.read().unwrap().get_type().clone(), ctx.type_term_from_str("EditTree").expect("") ]); - ctx.morphisms.apply_morphism( - rt.clone(), - &rt.get_type(), - &ladder + ctx.apply_morphism( + &rt, + &laddertypes::MorphismType { + src_type: rt.get_type(), + dst_type: ladder + } ); let new_edittree = ctx.setup_edittree(