Compare commits
No commits in common. "8d637a6f325a0c42d7303a487457f65f4fca121c" and "4c0e9da2d31272abc9609438731e23da85e1f3c7" have entirely different histories.
8d637a6f32
...
4c0e9da2d3
14 changed files with 1393 additions and 1026 deletions
|
@ -69,19 +69,16 @@ async fn main() {
|
||||||
/* furthermore, setup projections to and from u8 value,
|
/* furthermore, setup projections to and from u8 value,
|
||||||
* this synchronizes the buffers
|
* this synchronizes the buffers
|
||||||
*/
|
*/
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
&rt_digit,
|
rt_digit.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<Digit 16>~Char"),
|
||||||
src_type: Context::parse(&ctx, "<Digit 16>~Char"),
|
&Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64")
|
||||||
dst_type: Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
ctx.read().unwrap().apply_morphism(
|
|
||||||
&rt_digit,
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
&laddertypes::MorphismType {
|
rt_digit.clone(),
|
||||||
src_type: Context::parse(&ctx, "<Digit 16>~Char"),
|
&Context::parse(&ctx, "<Digit 16>~Char"),
|
||||||
dst_type: Context::parse(&ctx, "<Digit 16>~EditTree")
|
&Context::parse(&ctx, "<Digit 16>~EditTree")
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
/* setup TTY-Display for DigitEditor
|
/* setup TTY-Display for DigitEditor
|
||||||
|
|
|
@ -43,23 +43,24 @@ async fn main() {
|
||||||
|
|
||||||
/* Create a Representation-Tree of type <List Char>
|
/* Create a Representation-Tree of type <List Char>
|
||||||
*/
|
*/
|
||||||
let mut rt_string = ReprTree::from_str(
|
let mut rt_string = ReprTree::new_arc( Context::parse(&ctx, "<List Char>") );
|
||||||
Context::parse(&ctx, "<List Char>~<Vec Char>"),
|
|
||||||
"hello world"
|
let vec = VecBuffer::<Arc<RwLock<EditTree>>>::new();
|
||||||
|
rt_string.insert_leaf(
|
||||||
|
Context::parse(&ctx, "<List EditTree> ~ <Vec EditTree>"),
|
||||||
|
nested::repr_tree::ReprLeaf::from_vec_buffer( vec.clone() )
|
||||||
);
|
);
|
||||||
|
|
||||||
/* create EditTree
|
let v2 = VecBuffer::<char>::new();
|
||||||
*/
|
rt_string.insert_leaf(
|
||||||
ctx.read().unwrap().apply_morphism(
|
Context::parse(&ctx, "<Vec Char>"),
|
||||||
&rt_string,
|
nested::repr_tree::ReprLeaf::from_vec_buffer( v2.clone() )
|
||||||
&laddertypes::MorphismType {
|
);
|
||||||
src_type: Context::parse(&ctx, "<List~Vec Char>"),
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
dst_type: Context::parse(&ctx, "<List Char> ~ EditTree")
|
rt_string.clone(),
|
||||||
}
|
&Context::parse(&ctx, "<List Char~EditTree> ~ <Vec EditTree>"),
|
||||||
|
&Context::parse(&ctx, "<List Char> ~ EditTree")
|
||||||
);
|
);
|
||||||
|
|
||||||
// .. avoid cycle of projections..
|
|
||||||
rt_string.write().unwrap().detach(&ctx);
|
|
||||||
|
|
||||||
/* Setup the Editor-View for this ReprTree
|
/* Setup the Editor-View for this ReprTree
|
||||||
*/
|
*/
|
||||||
|
@ -69,16 +70,14 @@ async fn main() {
|
||||||
SingletonBuffer::new(0).get_port()
|
SingletonBuffer::new(0).get_port()
|
||||||
).unwrap();
|
).unwrap();
|
||||||
|
|
||||||
/* In order to get access to the values that are modified by the Editor,
|
/* In order to get acces to the values that are modified by the Editor,
|
||||||
* we apply a morphism that, given the List of Edit-Trees, extracts
|
* we apply a morphism that, given the List of Edit-Trees, extracts
|
||||||
* the value from each EditTree and shows them in a ListView.
|
* the value from each EditTree and shows them in a ListView.
|
||||||
*/
|
*/
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
&rt_string,
|
rt_string.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<List Char>~EditTree"),
|
||||||
src_type: Context::parse(&ctx, "<List Char>~EditTree"),
|
&Context::parse(&ctx, "<List Char>")
|
||||||
dst_type: Context::parse(&ctx, "<List Char>")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
/* Now, get the ListView that serves our char-values.
|
/* Now, get the ListView that serves our char-values.
|
||||||
|
@ -92,12 +91,10 @@ async fn main() {
|
||||||
/* Lets add another morphism which will store the values
|
/* Lets add another morphism which will store the values
|
||||||
* of the character-list in a `Vec<char>`
|
* of the character-list in a `Vec<char>`
|
||||||
*/
|
*/
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
&rt_string,
|
rt_string.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<List Char>"),
|
||||||
src_type: Context::parse(&ctx, "<List Char>"),
|
&Context::parse(&ctx, "<List Char>~<Vec Char>")
|
||||||
dst_type: Context::parse(&ctx, "<List Char>~<Vec Char>")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
/* Access the Vec<char> object (wrapped behind a VecBuffer<char>)
|
/* Access the Vec<char> object (wrapped behind a VecBuffer<char>)
|
||||||
|
|
|
@ -32,25 +32,131 @@ use {
|
||||||
std::sync::{Arc, RwLock},
|
std::sync::{Arc, RwLock},
|
||||||
};
|
};
|
||||||
|
|
||||||
|
fn rebuild_projections(
|
||||||
|
ctx: Arc<RwLock<Context>>,
|
||||||
|
repr_tree: Arc<RwLock<ReprTree>>,
|
||||||
|
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<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
fn setup_hex_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
rt_int.write().unwrap().detach( ctx );
|
rebuild_projections(
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.clone(),
|
||||||
rt_int,
|
rt_int.clone(),
|
||||||
&laddertypes::MorphismType {
|
vec![
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree"),
|
// extract values from hex-editor
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ EditTree")
|
(
|
||||||
}
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
|
),
|
||||||
|
|
||||||
|
// convert to little-endian
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
|
),
|
||||||
|
// convert digit representation from char to u64
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||||
|
),
|
||||||
|
// convert radix to decimal
|
||||||
|
(
|
||||||
|
"ℕ ~ <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>"
|
||||||
|
),
|
||||||
|
// convert decimal digit representation back to char
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>"
|
||||||
|
),
|
||||||
|
// convert to big-endian
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>"
|
||||||
|
),
|
||||||
|
|
||||||
|
// decimal editor
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char ~ EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char ~ EditTree>",
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char ~ EditTree> ~ <Vec EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char ~ EditTree> ~ <Vec EditTree>",
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ EditTree"
|
||||||
|
),
|
||||||
|
|
||||||
|
].into_iter()
|
||||||
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
|
.collect()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
fn setup_dec_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
fn setup_dec_master(ctx: &Arc<RwLock<Context>>, rt_int: &Arc<RwLock<ReprTree>>) {
|
||||||
rt_int.write().unwrap().detach( ctx );
|
rebuild_projections(
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.clone(),
|
||||||
rt_int,
|
rt_int.clone(),
|
||||||
&laddertypes::MorphismType {
|
vec![
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ EditTree"),
|
// extract values from decimal-editor
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree")
|
(
|
||||||
}
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char> ~ EditTree",
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>"
|
||||||
|
),
|
||||||
|
|
||||||
|
// convert to little-endian
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>"
|
||||||
|
),
|
||||||
|
// convert digit representation to u64
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||||
|
),
|
||||||
|
// convert radix to decimal
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10>> ~ <List <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>"
|
||||||
|
),
|
||||||
|
// convert back digit representation char
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>",
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
|
),
|
||||||
|
// convert back to big-endian
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
|
),
|
||||||
|
|
||||||
|
// hex editor
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree> ~ <Vec EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree> ~ <Vec EditTree>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree"
|
||||||
|
),
|
||||||
|
].into_iter()
|
||||||
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
|
.collect()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -66,31 +172,76 @@ async fn main() {
|
||||||
nested_tty::setup_edittree_hook(&ctx);
|
nested_tty::setup_edittree_hook(&ctx);
|
||||||
|
|
||||||
/* Create a Representation-Tree of type `ℕ`
|
/* Create a Representation-Tree of type `ℕ`
|
||||||
* with a specific representation-path (big-endian hexadecimal string)
|
|
||||||
*/
|
*/
|
||||||
let mut rt_int = nested::repr_tree::ReprTree::from_str(
|
let mut rt_int = ReprTree::new_arc( Context::parse(&ctx, "ℕ") );
|
||||||
/* TYPE */
|
|
||||||
Context::parse(&ctx, "
|
|
||||||
ℕ
|
|
||||||
~ <PosInt 16 BigEndian>
|
|
||||||
~ <Seq <Digit 16>>
|
|
||||||
~ <List <Digit 16>>
|
|
||||||
~ <List Char>
|
|
||||||
~ <Vec Char>
|
|
||||||
"),
|
|
||||||
|
|
||||||
/* VALUE */
|
/* Add a specific Representation-Path (big-endian hexadecimal)
|
||||||
"cff"
|
*/
|
||||||
|
let mut digits_hex = VecBuffer::with_data(vec![ 'c', 'f', 'f' ]);
|
||||||
|
rt_int.insert_leaf(
|
||||||
|
Context::parse(&ctx, "<PosInt 16 BigEndian>~<Seq <Digit 16>>~<List <Digit 16>>~<List Char>~<Vec Char>"),
|
||||||
|
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, "<PosInt 10 BigEndian>~<Seq <Digit 10>>~<List <Digit 10>>~<List Char>~<Vec Char>"),
|
||||||
|
nested::repr_tree::ReprLeaf::from_vec_buffer( digits_dec.clone() )
|
||||||
|
);
|
||||||
|
|
||||||
|
let mut digits_hex_editvec = VecBuffer::<Arc<RwLock<EditTree>>>::new();
|
||||||
|
rt_int.insert_leaf(
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
<PosInt 16 BigEndian>
|
||||||
|
~ <Seq <Digit 16>>
|
||||||
|
~ <List <Digit 16>
|
||||||
|
~ Char
|
||||||
|
~ EditTree>
|
||||||
|
~ <Vec EditTree>
|
||||||
|
"),
|
||||||
|
nested::repr_tree::ReprLeaf::from_vec_buffer( digits_hex_editvec.clone() )
|
||||||
|
);
|
||||||
|
|
||||||
|
let mut digits_dec_editvec = VecBuffer::<Arc<RwLock<EditTree>>>::new();
|
||||||
|
rt_int.insert_leaf(
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
<PosInt 10 BigEndian>
|
||||||
|
~ <Seq <Digit 10>>
|
||||||
|
~ <List <Digit 10>
|
||||||
|
~ Char
|
||||||
|
~ EditTree>
|
||||||
|
~ <Vec EditTree>
|
||||||
|
"),
|
||||||
|
nested::repr_tree::ReprLeaf::from_vec_buffer( digits_dec_editvec.clone() )
|
||||||
);
|
);
|
||||||
|
|
||||||
/* initially copy values from Vec to EditTree...
|
/* initially copy values from Vec to EditTree...
|
||||||
*/
|
*/
|
||||||
ctx.read().unwrap().apply_morphism(
|
rebuild_projections(
|
||||||
&rt_int,
|
ctx.clone(),
|
||||||
&nested::repr_tree::morphism::MorphismType {
|
rt_int.clone(),
|
||||||
src_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ <Vec Char>"),
|
// master representation
|
||||||
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree")
|
vec![
|
||||||
});
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ <Vec Char>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char ~ EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ <List EditTree>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ <List EditTree> ~ <Vec EditTree>"
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ <List EditTree> ~ <Vec EditTree>",
|
||||||
|
"ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16>> ~ <List <Digit 16> ~ Char> ~ EditTree"
|
||||||
|
),
|
||||||
|
].into_iter()
|
||||||
|
.map(|(s,d)| (Context::parse(&ctx, s), Context::parse(&ctx, d)))
|
||||||
|
.collect()
|
||||||
|
);
|
||||||
|
|
||||||
setup_hex_master(&ctx, &rt_int);
|
setup_hex_master(&ctx, &rt_int);
|
||||||
|
|
||||||
|
@ -116,6 +267,7 @@ async fn main() {
|
||||||
SingletonBuffer::new(0).get_port()
|
SingletonBuffer::new(0).get_port()
|
||||||
).unwrap().get();
|
).unwrap().get();
|
||||||
|
|
||||||
|
|
||||||
let hex_digits_view = rt_int.descend(Context::parse(&ctx, "
|
let hex_digits_view = rt_int.descend(Context::parse(&ctx, "
|
||||||
<PosInt 16 LittleEndian>
|
<PosInt 16 LittleEndian>
|
||||||
~ <Seq <Digit 16> >
|
~ <Seq <Digit 16> >
|
||||||
|
@ -126,7 +278,8 @@ async fn main() {
|
||||||
.view_list::<u64>()
|
.view_list::<u64>()
|
||||||
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 16)))
|
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 16)))
|
||||||
.to_sequence()
|
.to_sequence()
|
||||||
.to_grid_horizontal();
|
.to_grid_horizontal()
|
||||||
|
;
|
||||||
|
|
||||||
let dec_digits_view = rt_int.descend(Context::parse(&ctx, "
|
let dec_digits_view = rt_int.descend(Context::parse(&ctx, "
|
||||||
<PosInt 10 LittleEndian>
|
<PosInt 10 LittleEndian>
|
||||||
|
@ -138,7 +291,8 @@ async fn main() {
|
||||||
.view_list::<u64>()
|
.view_list::<u64>()
|
||||||
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 10)))
|
.map(|v| TerminalAtom::from(char::from_digit(*v as u32, 10)))
|
||||||
.to_sequence()
|
.to_sequence()
|
||||||
.to_grid_horizontal();
|
.to_grid_horizontal()
|
||||||
|
;
|
||||||
|
|
||||||
/* list of both editors
|
/* list of both editors
|
||||||
*/
|
*/
|
||||||
|
|
|
@ -9,7 +9,7 @@ use {
|
||||||
},
|
},
|
||||||
laddertypes::{TypeTerm},
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt, GenericReprTreeMorphism},
|
repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt},
|
||||||
edit_tree::{EditTree, TreeNavResult},
|
edit_tree::{EditTree, TreeNavResult},
|
||||||
editors::ObjCommander,
|
editors::ObjCommander,
|
||||||
},
|
},
|
||||||
|
@ -18,16 +18,21 @@ use {
|
||||||
};
|
};
|
||||||
|
|
||||||
pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
|
let morphtype =
|
||||||
|
crate::repr_tree::MorphismType {
|
||||||
|
src_type: Context::parse(&ctx, "Char"),
|
||||||
|
dst_type: Context::parse(&ctx, "Char~EditTree")
|
||||||
|
};
|
||||||
|
|
||||||
let char_morph_to_edittree = GenericReprTreeMorphism::new(
|
ctx.write().unwrap()
|
||||||
Context::parse(&ctx, "Char"),
|
.morphisms
|
||||||
Context::parse(&ctx, "Char~EditTree"),
|
.add_morphism(
|
||||||
{
|
morphtype,
|
||||||
let ctx = ctx.clone();
|
{
|
||||||
move |rt, σ| {
|
let ctx = ctx.clone();
|
||||||
|
move |rt, σ| {
|
||||||
{
|
{
|
||||||
let mut b = rt.write().unwrap().singleton_buffer::<char>();
|
let mut b = rt.write().unwrap().singleton_buffer::<char>();
|
||||||
if let Some(buf) = b {
|
if let Some(buf) = b {
|
||||||
// buffer already exists
|
// buffer already exists
|
||||||
} else {
|
} else {
|
||||||
|
@ -51,11 +56,7 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
|
|
||||||
rt.insert_leaf(
|
rt.insert_leaf(
|
||||||
Context::parse(&ctx, "EditTree"),
|
Context::parse(&ctx, "EditTree"),
|
||||||
ReprLeaf::from_singleton_buffer(
|
ReprLeaf::from_singleton_buffer(SingletonBuffer::new(Arc::new(RwLock::new(edittree))))
|
||||||
SingletonBuffer::new(
|
|
||||||
Arc::new(RwLock::new(edittree))
|
|
||||||
)
|
|
||||||
)
|
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.read().unwrap().setup_edittree(
|
ctx.read().unwrap().setup_edittree(
|
||||||
|
@ -63,11 +64,8 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
SingletonBuffer::new(0).get_port()
|
SingletonBuffer::new(0).get_port()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
}
|
||||||
}
|
);
|
||||||
);
|
|
||||||
|
|
||||||
ctx.write().unwrap().morphisms.add_morphism( char_morph_to_edittree );
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub struct CharEditor {
|
pub struct CharEditor {
|
||||||
|
|
|
@ -9,21 +9,28 @@ use {
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf, GenericReprTreeMorphism},
|
repr_tree::{Context, ReprTree, ReprTreeExt, ReprLeaf},
|
||||||
editors::digit::DigitEditor,
|
editors::digit::DigitEditor,
|
||||||
},
|
},
|
||||||
std::sync::{Arc, RwLock}
|
std::sync::{Arc, RwLock}
|
||||||
};
|
};
|
||||||
|
|
||||||
pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
|
|
||||||
// todo: proper scoping of Radix variable
|
// todo: proper scoping of Radix variable
|
||||||
ctx.write().unwrap().add_varname("Radix");
|
ctx.write().unwrap().add_varname("Radix");
|
||||||
|
|
||||||
let digit_morph_char_to_edittree = GenericReprTreeMorphism::new(
|
let morphtype =
|
||||||
Context::parse(&ctx, "<Digit Radix>~Char"),
|
crate::repr_tree::MorphismType {
|
||||||
Context::parse(&ctx, "<Digit Radix>~EditTree"),
|
src_type: Context::parse(&ctx, "<Digit Radix>~Char"),
|
||||||
|
dst_type: Context::parse(&ctx, "<Digit Radix>~EditTree")
|
||||||
|
};
|
||||||
|
|
||||||
{
|
ctx.write().unwrap()
|
||||||
|
.morphisms
|
||||||
|
.add_morphism(
|
||||||
|
morphtype,
|
||||||
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
let radix =
|
let radix =
|
||||||
|
@ -32,14 +39,32 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
_ => 0
|
_ => 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
|
/* Create EditTree object
|
||||||
*/
|
*/
|
||||||
let mut edittree = DigitEditor::new(
|
let mut edittree = DigitEditor::new(
|
||||||
ctx.clone(),
|
ctx.clone(),
|
||||||
radix,
|
radix,
|
||||||
src_rt
|
src_rt.descend(
|
||||||
.descend( Context::parse(&ctx, "Char") ).unwrap()
|
Context::parse(&ctx, "Char")
|
||||||
.singleton_buffer::<char>()
|
).unwrap()
|
||||||
|
.singleton_buffer::<char>()
|
||||||
).into_node(
|
).into_node(
|
||||||
r3vi::buffer::singleton::SingletonBuffer::<usize>::new(0).get_port()
|
r3vi::buffer::singleton::SingletonBuffer::<usize>::new(0).get_port()
|
||||||
);
|
);
|
||||||
|
@ -52,16 +77,22 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
let digit_morph_char_to_u64 = GenericReprTreeMorphism::new(
|
let morphtype =
|
||||||
Context::parse(&ctx, "<Digit Radix>~Char"),
|
crate::repr_tree::MorphismType {
|
||||||
Context::parse(&ctx, "<Digit Radix>~ℤ_2^64~machine.UInt64"),
|
src_type: Context::parse(&ctx, "<Digit Radix>~Char"),
|
||||||
|
dst_type: Context::parse(&ctx, "<Digit Radix>~ℤ_2^64~machine.UInt64")
|
||||||
|
};
|
||||||
|
|
||||||
{
|
ctx.write().unwrap()
|
||||||
let ctx = ctx.clone();
|
.morphisms
|
||||||
move |rt: &mut Arc<RwLock<ReprTree>>, σ: &std::collections::HashMap<laddertypes::TypeID, TypeTerm>| {
|
.add_morphism(
|
||||||
|
morphtype,
|
||||||
|
{
|
||||||
|
let ctx = ctx.clone();
|
||||||
|
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_typeid = ctx.read().unwrap().get_var_typeid("Radix").unwrap();
|
||||||
|
@ -92,15 +123,19 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
} else {
|
} else {
|
||||||
eprintln!("radix too large ({})", radix);
|
eprintln!("radix too large ({})", radix);
|
||||||
}
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
);
|
||||||
);
|
|
||||||
|
|
||||||
|
|
||||||
let digit_morph_u64_to_char = GenericReprTreeMorphism::new(
|
let morphtype =
|
||||||
Context::parse(&ctx, "<Digit Radix>~ℤ_2^64~machine.UInt64"),
|
crate::repr_tree::MorphismType {
|
||||||
Context::parse(&ctx, "<Digit Radix>~Char"),
|
src_type: Context::parse(&ctx, "<Digit Radix>~ℤ_2^64~machine.UInt64"),
|
||||||
{
|
dst_type: Context::parse(&ctx, "<Digit Radix>~Char")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms
|
||||||
|
.add_morphism(morphtype, {
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
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
|
||||||
|
@ -128,13 +163,7 @@ pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
||||||
eprintln!("radix too large ({})", radix);
|
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 );
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -3,9 +3,9 @@ use {
|
||||||
r3vi::{
|
r3vi::{
|
||||||
view::{OuterViewPort, singleton::*, list::*}
|
view::{OuterViewPort, singleton::*, list::*}
|
||||||
},
|
},
|
||||||
laddertypes::{TypeTerm, MorphismType},
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf, Context, GenericReprTreeMorphism},
|
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf, Context, MorphismType},
|
||||||
editors::{
|
editors::{
|
||||||
list::*,
|
list::*,
|
||||||
integer::*
|
integer::*
|
||||||
|
@ -20,27 +20,45 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
ctx.write().unwrap().add_varname("DstRadix");
|
ctx.write().unwrap().add_varname("DstRadix");
|
||||||
|
|
||||||
|
|
||||||
let posint_seq_morph_big_to_little = GenericReprTreeMorphism::new(
|
/*
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian>
|
* MACHINE INT, SEQ
|
||||||
~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
*/
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian>
|
let morphism_type =
|
||||||
~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
MorphismType {
|
||||||
{
|
src_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >")
|
||||||
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
morphism_type, {
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
let src_digits = src_rt
|
let src_digits = src_rt.descend(
|
||||||
.descend(Context::parse(&ctx, "
|
Context::parse(&ctx, "
|
||||||
<PosInt Radix BigEndian>
|
<PosInt Radix BigEndian>
|
||||||
~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
~ <Seq <Digit Radix>
|
||||||
")
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
|
")
|
||||||
.apply_substitution(&|k|σ.get(k).cloned())
|
.apply_substitution(&|k|σ.get(k).cloned())
|
||||||
.clone()
|
.clone()
|
||||||
).expect("cant descend")
|
).expect("cant descend")
|
||||||
.view_seq::< u64 >();
|
.view_seq::< u64 >();
|
||||||
|
|
||||||
src_rt.attach_leaf_to(Context::parse(&ctx, "
|
src_rt.attach_leaf_to(Context::parse(&ctx, "
|
||||||
<PosInt Radix LittleEndian>
|
<PosInt Radix LittleEndian>
|
||||||
~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
~ <Seq <Digit Radix>
|
||||||
|
~ ℤ_2^64
|
||||||
|
~ machine.UInt64 >
|
||||||
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||||
src_digits.reverse()
|
src_digits.reverse()
|
||||||
);
|
);
|
||||||
|
@ -48,27 +66,125 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
let posint_list_morph_big_to_little = GenericReprTreeMorphism::new(
|
/* MACHINE INT, LIST
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian>
|
*/
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
let morphism_type = MorphismType {
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian>
|
src_type: Context::parse(&ctx, "
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List ℤ_2^64>
|
||||||
|
~ <List machine.UInt64>
|
||||||
|
"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List ℤ_2^64>
|
||||||
|
~ <List machine.UInt64>
|
||||||
|
")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
morphism_type,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
let src_digits = src_rt
|
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||||
.descend(Context::parse(&ctx, "
|
<PosInt Radix BigEndian>
|
||||||
<PosInt Radix BigEndian>
|
~ <Seq <Digit Radix>>
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
~ <List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
||||||
")
|
")
|
||||||
.apply_substitution(&|k|σ.get(k).cloned())
|
.apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
.clone()
|
).expect("cant descend")
|
||||||
).expect("cant descend")
|
.get_port::< dyn ListView<u64> >().unwrap();
|
||||||
.view_list::< u64 >();
|
|
||||||
|
src_rt.attach_leaf_to(
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
<PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>
|
||||||
|
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||||
|
src_digits.reverse()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
);
|
||||||
|
|
||||||
|
|
||||||
|
let mt = MorphismType {
|
||||||
|
src_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
")
|
||||||
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
|
{
|
||||||
|
let ctx = ctx.clone();
|
||||||
|
move |src_rt, σ| {
|
||||||
|
let radix = σ.get( &laddertypes::TypeID::Var(ctx.read().unwrap().get_var_typeid("Radix").unwrap()) );
|
||||||
|
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")
|
||||||
|
.get_port::< dyn ListView<char> >().unwrap();
|
||||||
|
|
||||||
|
let rev_port = src_digits.reverse();
|
||||||
|
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(),
|
||||||
|
rev_port
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
let morphism_type = MorphismType {
|
||||||
|
src_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>"),
|
||||||
|
dst_type: Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
morphism_type,
|
||||||
|
{
|
||||||
|
let ctx = ctx.clone();
|
||||||
|
move |src_rt, σ| {
|
||||||
|
let src_digits = ReprTree::descend(
|
||||||
|
&src_rt,
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
<PosInt Radix LittleEndian>
|
||||||
|
~<Seq <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||||
|
")
|
||||||
|
.apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
|
).expect("cant descend")
|
||||||
|
.view_seq::< u64 >();
|
||||||
|
|
||||||
src_rt.attach_leaf_to(Context::parse(&ctx, "
|
src_rt.attach_leaf_to(Context::parse(&ctx, "
|
||||||
<PosInt Radix LittleEndian>
|
<PosInt Radix BigEndian>
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>
|
||||||
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||||
src_digits.reverse()
|
src_digits.reverse()
|
||||||
);
|
);
|
||||||
|
@ -76,27 +192,45 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
let posint_list_morph_little_to_big = GenericReprTreeMorphism::new(
|
let morphism_type =
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix LittleEndian>
|
MorphismType {
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
src_type: Context::parse(&ctx, "
|
||||||
Context::parse(&ctx, "ℕ ~ <PosInt Radix BigEndian>
|
ℕ
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >"),
|
~ <PosInt Radix LittleEndian>
|
||||||
{
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List ℤ_2^64>
|
||||||
|
~ <List machine.UInt64>
|
||||||
|
"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List ℤ_2^64>
|
||||||
|
~ <List machine.UInt64>
|
||||||
|
")
|
||||||
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
morphism_type, {
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ|
|
||||||
let src_digits = src_rt
|
{
|
||||||
.descend(Context::parse(&ctx, "
|
let src_digits = src_rt.descend(
|
||||||
<PosInt Radix LittleEndian>
|
Context::parse(&ctx, "
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
<PosInt Radix LittleEndian>
|
||||||
")
|
~ <Seq <Digit Radix>>
|
||||||
.apply_substitution(&|k|σ.get(k).cloned())
|
~ <List <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||||
.clone()
|
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
).expect("cant descend")
|
)
|
||||||
.view_list::< u64 >();
|
.expect("cant descend")
|
||||||
|
.view_list::<u64>();
|
||||||
|
|
||||||
src_rt.attach_leaf_to(Context::parse(&ctx, "
|
src_rt.attach_leaf_to(
|
||||||
<PosInt Radix BigEndian>
|
Context::parse(&ctx, "
|
||||||
~ <Seq~List <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64 >
|
<PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>~ℤ_2^64~machine.UInt64 >
|
||||||
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
").apply_substitution(&|k|σ.get(k).cloned()).clone(),
|
||||||
src_digits.reverse()
|
src_digits.reverse()
|
||||||
);
|
);
|
||||||
|
@ -105,8 +239,93 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|
||||||
let posint_list_morph_radix = GenericReprTreeMorphism::new(
|
let mt = MorphismType {
|
||||||
Context::parse(&ctx, "
|
src_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
|
{
|
||||||
|
let ctx = ctx.clone();
|
||||||
|
move |src_rt, σ| {
|
||||||
|
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||||
|
<PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>~Char >
|
||||||
|
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
|
).expect("cant descend")
|
||||||
|
.view_list::<char>();
|
||||||
|
|
||||||
|
src_rt.attach_leaf_to(
|
||||||
|
Context::parse(&ctx, "
|
||||||
|
< PosInt Radix BigEndian >
|
||||||
|
~ < Seq <Digit Radix> >
|
||||||
|
~ < List <Digit Radix>~Char >
|
||||||
|
").apply_substitution(&|k| σ.get(k).cloned()).clone(),
|
||||||
|
src_digits.reverse()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
);
|
||||||
|
/*
|
||||||
|
let mt = MorphismType {
|
||||||
|
src_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
"),
|
||||||
|
dst_type: Context::parse(&ctx, "
|
||||||
|
ℕ
|
||||||
|
~ <PosInt Radix LittleEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>>
|
||||||
|
~ <List Char>
|
||||||
|
")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
|
{
|
||||||
|
let ctx = ctx.clone();
|
||||||
|
move |src_rt, σ| {
|
||||||
|
let src_digits = src_rt.descend(Context::parse(&ctx, "
|
||||||
|
<PosInt Radix BigEndian>
|
||||||
|
~ <Seq <Digit Radix>>
|
||||||
|
~ <List <Digit Radix>~Char >
|
||||||
|
").apply_substitution(&|k|σ.get(k).cloned()).clone()
|
||||||
|
).expect("cant descend")
|
||||||
|
.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 {
|
||||||
|
src_type: Context::parse(&ctx, "
|
||||||
ℕ
|
ℕ
|
||||||
~ <PosInt SrcRadix LittleEndian>
|
~ <PosInt SrcRadix LittleEndian>
|
||||||
~ <Seq <Digit SrcRadix>>
|
~ <Seq <Digit SrcRadix>>
|
||||||
|
@ -114,14 +333,18 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
~ ℤ_2^64
|
~ ℤ_2^64
|
||||||
~ machine.UInt64>
|
~ machine.UInt64>
|
||||||
"),
|
"),
|
||||||
Context::parse(&ctx, "
|
dst_type: Context::parse(&ctx, "
|
||||||
ℕ
|
ℕ
|
||||||
~ <PosInt DstRadix LittleEndian>
|
~ <PosInt DstRadix LittleEndian>
|
||||||
~ <Seq <Digit DstRadix>>
|
~ <Seq <Digit DstRadix>>
|
||||||
~ <List <Digit DstRadix>
|
~ <List <Digit DstRadix>
|
||||||
~ ℤ_2^64
|
~ ℤ_2^64
|
||||||
~ machine.UInt64>
|
~ machine.UInt64>
|
||||||
"),
|
")
|
||||||
|
};
|
||||||
|
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
morphism_type,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
|
@ -166,13 +389,7 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
dst_digits_port
|
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 );
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -10,11 +10,11 @@ use {
|
||||||
},
|
},
|
||||||
laddertypes::{TypeTerm},
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt, GenericReprTreeMorphism},
|
repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt},
|
||||||
edit_tree::{EditTree},
|
edit_tree::{EditTree},
|
||||||
editors::{
|
editors::{
|
||||||
char::{CharEditor},
|
char::{CharEditor},
|
||||||
list::{ListEditor}
|
list::{ListEditor}//, PTYListController, PTYListStyle}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
std::sync::{Arc, RwLock}
|
std::sync::{Arc, RwLock}
|
||||||
|
@ -25,46 +25,49 @@ use {
|
||||||
pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
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 mt = crate::repr_tree::MorphismType {
|
||||||
Context::parse(&ctx, "<List Item>~<List EditTree>~<Vec EditTree>"),
|
src_type: Context::parse(&ctx, "<List Item>~<List EditTree>~<Vec EditTree>"),
|
||||||
Context::parse(&ctx, "<List Item>~EditTree"),
|
dst_type: Context::parse(&ctx, "<List Item>~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, "<List Item~EditTree>~<Vec EditTree>")
|
|
||||||
.apply_substitution(&|id| σ.get(id).cloned()).clone()
|
|
||||||
)
|
|
||||||
.expect("cant descend src repr");
|
|
||||||
|
|
||||||
let item_vec_buffer = item_vec_rt.vec_buffer::< Arc<RwLock<EditTree>> >();
|
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, "<List Item~EditTree>~<Vec EditTree>")
|
||||||
|
.apply_substitution(&|id| σ.get(id).cloned()).clone()
|
||||||
|
)
|
||||||
|
.expect("cant descend src repr");
|
||||||
|
|
||||||
let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer);
|
let item_vec_buffer = item_vec_rt.vec_buffer::< Arc<RwLock<EditTree>> >();
|
||||||
let edittree_list = list_editor.into_node(
|
|
||||||
SingletonBuffer::<usize>::new(0).get_port()
|
|
||||||
);
|
|
||||||
src_rt.insert_leaf(
|
|
||||||
Context::parse(&ctx, "<List Item> ~ EditTree")
|
|
||||||
.apply_substitution(&|id| σ.get(id).cloned()).clone(),
|
|
||||||
|
|
||||||
ReprLeaf::from_singleton_buffer(
|
let mut list_editor = ListEditor::with_data(ctx.clone(), item_type.clone(), item_vec_buffer);
|
||||||
SingletonBuffer::new(Arc::new(RwLock::new(edittree_list)))
|
let edittree_list = list_editor.into_node(
|
||||||
)
|
SingletonBuffer::<usize>::new(0).get_port()
|
||||||
);
|
);
|
||||||
} else {
|
src_rt.insert_leaf(
|
||||||
eprintln!("no item type");
|
Context::parse(&ctx, "<List Item> ~ 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");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
});
|
||||||
|
|
||||||
|
let mt = crate::repr_tree::MorphismType {
|
||||||
let list_morph_editsetup2 = GenericReprTreeMorphism::new(
|
src_type: Context::parse(&ctx, "<List Char>~EditTree"),
|
||||||
Context::parse(&ctx, "<List Char>~EditTree"),
|
dst_type: Context::parse(&ctx, "<List Char>")
|
||||||
Context::parse(&ctx, "<List Char>"),
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
|
@ -90,43 +93,54 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
let list_morph_to_vec_char = GenericReprTreeMorphism::new(
|
|
||||||
Context::parse(&ctx, "<List Char>"),
|
/* todo : unify the following two morphims with generic item parameter ?
|
||||||
Context::parse(&ctx, "<List Char>~<Vec Char>"),
|
*/
|
||||||
|
let mt = crate::repr_tree::MorphismType {
|
||||||
|
src_type: Context::parse(&ctx, "<List Char>"),
|
||||||
|
dst_type: Context::parse(&ctx, "<List Char>~<Vec Char>")
|
||||||
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
src_rt.attach_leaf_to(
|
let list_view = src_rt.view_list::<char>();
|
||||||
Context::parse(&ctx, "<Vec Char>"),
|
|
||||||
src_rt.view_list::<char>()
|
src_rt
|
||||||
);
|
.attach_leaf_to(
|
||||||
|
Context::parse(&ctx, "<Vec Char>"),
|
||||||
|
list_view
|
||||||
|
);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
let list_morph_from_vec_char = GenericReprTreeMorphism::new(
|
let mt = crate::repr_tree::MorphismType {
|
||||||
Context::parse(&ctx, "<List Char>~<Vec Char>"),
|
src_type: Context::parse(&ctx, "<List Char>~<Vec Char>"),
|
||||||
Context::parse(&ctx, "<List Char>"),
|
dst_type: Context::parse(&ctx, "<List Char>")
|
||||||
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
let src_port = src_rt.descend(Context::parse(&ctx, "<List Char>~<Vec Char>")).expect("descend")
|
let src_port = src_rt.descend(Context::parse(&ctx, "<List Char>~<Vec Char>")).expect("descend")
|
||||||
.get_port::<RwLock<Vec<char>>>().unwrap();
|
.get_port::<RwLock<Vec<char>>>().unwrap();
|
||||||
|
|
||||||
src_rt.attach_leaf_to( Context::parse(&ctx, "<List Char>"), src_port.to_list() );
|
src_rt.attach_leaf_to( Context::parse(&ctx, "<List Char>"), src_port.to_list() );
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
|
let mt = crate::repr_tree::MorphismType {
|
||||||
let list_morph_to_vec_edittree = GenericReprTreeMorphism::new(
|
src_type: Context::parse(&ctx, "<List EditTree>"),
|
||||||
Context::parse(&ctx, "<List EditTree>"),
|
dst_type: Context::parse(&ctx, "<List EditTree>~<Vec EditTree>")
|
||||||
Context::parse(&ctx, "<List EditTree> ~ <Vec EditTree>"),
|
};
|
||||||
|
ctx.write().unwrap().morphisms.add_morphism(
|
||||||
|
mt,
|
||||||
{
|
{
|
||||||
let ctx = ctx.clone();
|
let ctx = ctx.clone();
|
||||||
move |src_rt, σ| {
|
move |src_rt, σ| {
|
||||||
|
@ -142,11 +156,5 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
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 );
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,8 +1,8 @@
|
||||||
use {
|
use {
|
||||||
r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}},
|
r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}},
|
||||||
laddertypes::{TypeDict, TypeTerm, TypeID, MorphismType, MorphismBase, Morphism},
|
laddertypes::{TypeDict, TypeTerm, TypeID},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{ReprTree, ReprTreeExt, GenericReprTreeMorphism},
|
repr_tree::{ReprTree, ReprTreeExt, MorphismType, GenericReprTreeMorphism, MorphismBase},
|
||||||
edit_tree::EditTree
|
edit_tree::EditTree
|
||||||
},
|
},
|
||||||
std::{
|
std::{
|
||||||
|
@ -18,7 +18,7 @@ pub struct Context {
|
||||||
/// assigns a name to every type
|
/// assigns a name to every type
|
||||||
pub type_dict: Arc<RwLock<TypeDict>>,
|
pub type_dict: Arc<RwLock<TypeDict>>,
|
||||||
|
|
||||||
pub morphisms: laddertypes::morphism::MorphismBase< GenericReprTreeMorphism >,
|
pub morphisms: MorphismBase,
|
||||||
|
|
||||||
/// named vertices of the graph
|
/// named vertices of the graph
|
||||||
nodes: HashMap< String, Arc<RwLock<ReprTree>> >,
|
nodes: HashMap< String, Arc<RwLock<ReprTree>> >,
|
||||||
|
@ -39,15 +39,12 @@ impl Context {
|
||||||
pub fn with_parent(
|
pub fn with_parent(
|
||||||
parent: Option<Arc<RwLock<Context>>>
|
parent: Option<Arc<RwLock<Context>>>
|
||||||
) -> Self {
|
) -> Self {
|
||||||
let mut dict = TypeDict::new();
|
|
||||||
let list_typeid = dict.add_typename("List".into());
|
|
||||||
|
|
||||||
Context {
|
Context {
|
||||||
type_dict: match parent.as_ref() {
|
type_dict: match parent.as_ref() {
|
||||||
Some(p) => p.read().unwrap().type_dict.clone(),
|
Some(p) => p.read().unwrap().type_dict.clone(),
|
||||||
None => Arc::new(RwLock::new(dict))
|
None => Arc::new(RwLock::new(TypeDict::new()))
|
||||||
},
|
},
|
||||||
morphisms: MorphismBase::new( list_typeid ),
|
morphisms: MorphismBase::new(),
|
||||||
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(),
|
||||||
|
@ -78,35 +75,9 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn apply_morphism( &self, rt: &Arc<RwLock<ReprTree>>, 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<RwLock<Self>>, t: &TypeTerm) -> Arc<RwLock<ReprTree>> {
|
pub fn make_repr(ctx: &Arc<RwLock<Self>>, t: &TypeTerm) -> Arc<RwLock<ReprTree>> {
|
||||||
let rt = Arc::new(RwLock::new(ReprTree::new( TypeTerm::unit() )));
|
let rt = Arc::new(RwLock::new(ReprTree::new( TypeTerm::unit() )));
|
||||||
ctx.read().unwrap().apply_morphism( &rt, &MorphismType{ src_type: TypeTerm::unit(), dst_type: t.clone() } );
|
ctx.read().unwrap().morphisms.apply_morphism( rt.clone(), &TypeTerm::unit(), t );
|
||||||
rt
|
rt
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,216 +0,0 @@
|
||||||
use {
|
|
||||||
r3vi::{
|
|
||||||
view::{
|
|
||||||
ViewPort, OuterViewPort,
|
|
||||||
AnyViewPort, AnyInnerViewPort, AnyOuterViewPort,
|
|
||||||
port::UpdateTask,
|
|
||||||
View, Observer,
|
|
||||||
singleton::*,
|
|
||||||
sequence::*,
|
|
||||||
list::*
|
|
||||||
},
|
|
||||||
buffer::{singleton::*, vec::*}
|
|
||||||
},
|
|
||||||
laddertypes::{TypeTerm},
|
|
||||||
std::{
|
|
||||||
collections::HashMap,
|
|
||||||
sync::{Arc, RwLock},
|
|
||||||
any::Any
|
|
||||||
},
|
|
||||||
};
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
#[derive(Clone)]
|
|
||||||
pub struct ReprLeaf {
|
|
||||||
out_port: AnyViewPort,
|
|
||||||
in_port: AnyInnerViewPort,
|
|
||||||
data: Option< Arc<dyn Any + Send + Sync> >,
|
|
||||||
|
|
||||||
/// keepalive for the observer that updates the buffer from in_port
|
|
||||||
keepalive: Option<Arc<dyn Any + Send + Sync>>,
|
|
||||||
in_keepalive: Option<Arc<dyn Any + Send + Sync>>,
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
impl ReprLeaf {
|
|
||||||
pub fn from_view<V>( src_port: OuterViewPort<V> ) -> Self
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
let mut in_port = ViewPort::<V>::new();
|
|
||||||
let in_keepalive = in_port.attach_to(src_port);
|
|
||||||
|
|
||||||
let mut out_port = ViewPort::<V>::new();
|
|
||||||
let out_keepalive = out_port.attach_to(in_port.outer());
|
|
||||||
|
|
||||||
ReprLeaf {
|
|
||||||
keepalive: Some(out_keepalive),
|
|
||||||
in_keepalive: Some(in_keepalive),
|
|
||||||
in_port: in_port.inner().into(),
|
|
||||||
out_port: out_port.into(),
|
|
||||||
data: None,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn detach<V>(&mut self)
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
self.keepalive = None;
|
|
||||||
self.in_keepalive = None;
|
|
||||||
|
|
||||||
let ip = self.in_port.clone()
|
|
||||||
.downcast::<V>().ok()
|
|
||||||
.unwrap();
|
|
||||||
ip.0.detach();
|
|
||||||
|
|
||||||
if self.data.is_none() {
|
|
||||||
let mut op = self.out_port.clone()
|
|
||||||
.downcast::<V>().ok()
|
|
||||||
.unwrap();
|
|
||||||
|
|
||||||
op.detach();
|
|
||||||
self.keepalive = Some(op.attach_to(ip.0.outer()));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn detach_vec<Item>(&mut self)
|
|
||||||
where Item: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
self.keepalive = None;
|
|
||||||
self.in_keepalive = None;
|
|
||||||
|
|
||||||
let ip = self.in_port.clone()
|
|
||||||
.downcast::<dyn ListView<Item>>().ok()
|
|
||||||
.unwrap();
|
|
||||||
|
|
||||||
ip.0.detach();
|
|
||||||
|
|
||||||
if let Some(data) = self.data.as_mut() {
|
|
||||||
let mut op = self.out_port.clone()
|
|
||||||
.downcast::<RwLock<Vec<Item>>>().ok()
|
|
||||||
.unwrap();
|
|
||||||
op.detach();
|
|
||||||
|
|
||||||
let data = data.clone().downcast::< RwLock<Vec<Item>> >().ok().unwrap();
|
|
||||||
let buffer = VecBuffer::with_data_arc_port(data, op.inner());
|
|
||||||
self.keepalive = Some(buffer.attach_to(ip.0.outer()))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn attach_to<V>(&mut self, src_port: OuterViewPort<V>)
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
self.in_keepalive = Some(self.in_port.clone()
|
|
||||||
.downcast::<V>().ok().unwrap()
|
|
||||||
.0.attach_to( src_port ));
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_singleton_buffer<T>( buffer: SingletonBuffer<T> ) -> Self
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let in_port = ViewPort::<dyn SingletonView<Item = T>>::new();
|
|
||||||
ReprLeaf {
|
|
||||||
in_keepalive: None,
|
|
||||||
keepalive: Some(buffer.attach_to(in_port.outer())),
|
|
||||||
in_port: in_port.inner().into(),
|
|
||||||
out_port: buffer.get_port().0.into(),
|
|
||||||
data: Some(buffer.into_inner())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_vec_buffer<T>( buffer: VecBuffer<T> ) -> Self
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let in_port = ViewPort::< dyn ListView<T> >::new();
|
|
||||||
ReprLeaf {
|
|
||||||
in_keepalive: None,
|
|
||||||
keepalive: Some(buffer.attach_to(in_port.outer())),
|
|
||||||
in_port: in_port.inner().into(),
|
|
||||||
out_port: buffer.get_port().0.into(),
|
|
||||||
data: Some(buffer.into_inner())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn as_singleton_buffer<T>(&mut self) -> Option<SingletonBuffer<T>>
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let sgl_port = self.get_port::< dyn SingletonView<Item = T> >().unwrap().0;
|
|
||||||
|
|
||||||
let data_arc =
|
|
||||||
if let Some(data) = self.data.as_ref() {
|
|
||||||
data.clone().downcast::<RwLock<T>>().ok()
|
|
||||||
} else {
|
|
||||||
sgl_port.update();
|
|
||||||
let value = sgl_port.outer().get_view().unwrap().get();
|
|
||||||
eprintln!("make new data ARC from old value");
|
|
||||||
Some(Arc::new(RwLock::new( value )))
|
|
||||||
};
|
|
||||||
|
|
||||||
if let Some(data_arc) = data_arc {
|
|
||||||
self.data = Some(data_arc.clone() as Arc<dyn Any + Send + Sync>);
|
|
||||||
let buf = SingletonBuffer {
|
|
||||||
value: data_arc,
|
|
||||||
port: sgl_port.inner()
|
|
||||||
};
|
|
||||||
self.keepalive = Some(buf.attach_to(
|
|
||||||
self.in_port.0.clone()
|
|
||||||
.downcast::<dyn SingletonView<Item = T>>()
|
|
||||||
.ok().unwrap()
|
|
||||||
.outer()
|
|
||||||
));
|
|
||||||
Some(buf)
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn as_vec_buffer<T>(&mut self) -> Option<VecBuffer<T>>
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let vec_port = self.get_port::< RwLock<Vec<T>> >().unwrap().0;
|
|
||||||
|
|
||||||
let data_arc =
|
|
||||||
if let Some(data) = self.data.as_ref() {
|
|
||||||
data.clone().downcast::<RwLock<Vec<T>>>().ok()
|
|
||||||
} else {
|
|
||||||
vec_port.update();
|
|
||||||
if let Some(value) = vec_port.outer().get_view() {
|
|
||||||
let value = value.read().unwrap().clone();
|
|
||||||
eprintln!("make new data ARC from old VECTOR-value");
|
|
||||||
Some(Arc::new(RwLock::new( value )))
|
|
||||||
} else {
|
|
||||||
eprintln!("no data vec");
|
|
||||||
Some(Arc::new(RwLock::new( Vec::new() )))
|
|
||||||
// None
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
if let Some(data_arc) = data_arc {
|
|
||||||
self.data = Some(data_arc.clone() as Arc<dyn Any + Send + Sync>);
|
|
||||||
let buf = VecBuffer::with_data_arc_port(data_arc, vec_port.inner());
|
|
||||||
self.keepalive = Some(buf.attach_to(
|
|
||||||
self.in_port.0.clone()
|
|
||||||
.downcast::< dyn ListView<T> >()
|
|
||||||
.ok().unwrap()
|
|
||||||
.outer()
|
|
||||||
));
|
|
||||||
Some(buf)
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_port<V>(&self) -> Option<OuterViewPort<V>>
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
self.out_port.clone().downcast::<V>().ok().map(|p| p.outer())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
|
@ -1,5 +1,3 @@
|
||||||
pub mod node;
|
|
||||||
pub mod leaf;
|
|
||||||
pub mod context;
|
pub mod context;
|
||||||
pub mod morphism;
|
pub mod morphism;
|
||||||
|
|
||||||
|
@ -8,9 +6,7 @@ mod tests;
|
||||||
|
|
||||||
pub use {
|
pub use {
|
||||||
context::{Context},
|
context::{Context},
|
||||||
leaf::ReprLeaf,
|
morphism::{MorphismType, GenericReprTreeMorphism, MorphismBase}
|
||||||
node::ReprTree,
|
|
||||||
morphism::{GenericReprTreeMorphism}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
use {
|
use {
|
||||||
|
@ -34,6 +30,520 @@ use {
|
||||||
},
|
},
|
||||||
};
|
};
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
|
pub struct ReprLeaf {
|
||||||
|
out_port: AnyViewPort,
|
||||||
|
in_port: AnyInnerViewPort,
|
||||||
|
data: Option< Arc<dyn Any + Send + Sync> >,
|
||||||
|
|
||||||
|
/// keepalive for the observer that updates the buffer from in_port
|
||||||
|
keepalive: Option<Arc<dyn Any + Send + Sync>>,
|
||||||
|
in_keepalive: Option<Arc<dyn Any + Send + Sync>>,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Clone)]
|
||||||
|
pub struct ReprTree {
|
||||||
|
halo: TypeTerm,
|
||||||
|
type_tag: TypeTerm,
|
||||||
|
branches: HashMap<TypeTerm, Arc<RwLock<ReprTree>>>,
|
||||||
|
leaf: Option< ReprLeaf >
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
impl std::fmt::Debug for ReprTree {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
writeln!(f, "| type: {:?}", self.type_tag)?;
|
||||||
|
|
||||||
|
for (_k,x) in self.branches.iter() {
|
||||||
|
writeln!(f, "|--> child: {:?}", x)?;
|
||||||
|
}
|
||||||
|
|
||||||
|
Ok(())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
impl ReprLeaf {
|
||||||
|
pub fn from_view<V>( src_port: OuterViewPort<V> ) -> Self
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
let mut in_port = ViewPort::<V>::new();
|
||||||
|
let in_keepalive = in_port.attach_to(src_port);
|
||||||
|
|
||||||
|
let mut out_port = ViewPort::<V>::new();
|
||||||
|
let out_keepalive = out_port.attach_to(in_port.outer());
|
||||||
|
|
||||||
|
ReprLeaf {
|
||||||
|
keepalive: Some(out_keepalive),
|
||||||
|
in_keepalive: Some(in_keepalive),
|
||||||
|
in_port: in_port.inner().into(),
|
||||||
|
out_port: out_port.into(),
|
||||||
|
data: None,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn detach<V>(&mut self)
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
self.keepalive = None;
|
||||||
|
self.in_keepalive = None;
|
||||||
|
|
||||||
|
let ip = self.in_port.clone()
|
||||||
|
.downcast::<V>().ok()
|
||||||
|
.unwrap();
|
||||||
|
ip.0.detach();
|
||||||
|
|
||||||
|
if self.data.is_none() {
|
||||||
|
let mut op = self.out_port.clone()
|
||||||
|
.downcast::<V>().ok()
|
||||||
|
.unwrap();
|
||||||
|
|
||||||
|
op.detach();
|
||||||
|
self.keepalive = Some(op.attach_to(ip.0.outer()));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn detach_vec<Item>(&mut self)
|
||||||
|
where Item: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
self.keepalive = None;
|
||||||
|
self.in_keepalive = None;
|
||||||
|
|
||||||
|
let ip = self.in_port.clone()
|
||||||
|
.downcast::<dyn ListView<Item>>().ok()
|
||||||
|
.unwrap();
|
||||||
|
|
||||||
|
ip.0.detach();
|
||||||
|
|
||||||
|
if let Some(data) = self.data.as_mut() {
|
||||||
|
let mut op = self.out_port.clone()
|
||||||
|
.downcast::<RwLock<Vec<Item>>>().ok()
|
||||||
|
.unwrap();
|
||||||
|
op.detach();
|
||||||
|
|
||||||
|
let data = data.clone().downcast::< RwLock<Vec<Item>> >().ok().unwrap();
|
||||||
|
let buffer = VecBuffer::with_data_arc_port(data, op.inner());
|
||||||
|
self.keepalive = Some(buffer.attach_to(ip.0.outer()))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn attach_to<V>(&mut self, src_port: OuterViewPort<V>)
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
self.in_keepalive = Some(self.in_port.clone()
|
||||||
|
.downcast::<V>().ok().unwrap()
|
||||||
|
.0.attach_to( src_port ));
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_singleton_buffer<T>( buffer: SingletonBuffer<T> ) -> Self
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let in_port = ViewPort::<dyn SingletonView<Item = T>>::new();
|
||||||
|
ReprLeaf {
|
||||||
|
in_keepalive: None,
|
||||||
|
keepalive: Some(buffer.attach_to(in_port.outer())),
|
||||||
|
in_port: in_port.inner().into(),
|
||||||
|
out_port: buffer.get_port().0.into(),
|
||||||
|
data: Some(buffer.into_inner())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_vec_buffer<T>( buffer: VecBuffer<T> ) -> Self
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let in_port = ViewPort::< dyn ListView<T> >::new();
|
||||||
|
ReprLeaf {
|
||||||
|
in_keepalive: None,
|
||||||
|
keepalive: Some(buffer.attach_to(in_port.outer())),
|
||||||
|
in_port: in_port.inner().into(),
|
||||||
|
out_port: buffer.get_port().0.into(),
|
||||||
|
data: Some(buffer.into_inner())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn as_singleton_buffer<T>(&mut self) -> Option<SingletonBuffer<T>>
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let sgl_port = self.get_port::< dyn SingletonView<Item = T> >().unwrap().0;
|
||||||
|
|
||||||
|
let data_arc =
|
||||||
|
if let Some(data) = self.data.as_ref() {
|
||||||
|
data.clone().downcast::<RwLock<T>>().ok()
|
||||||
|
} else {
|
||||||
|
sgl_port.update();
|
||||||
|
let value = sgl_port.outer().get_view().unwrap().get();
|
||||||
|
eprintln!("make new data ARC from old value");
|
||||||
|
Some(Arc::new(RwLock::new( value )))
|
||||||
|
};
|
||||||
|
|
||||||
|
if let Some(data_arc) = data_arc {
|
||||||
|
self.data = Some(data_arc.clone() as Arc<dyn Any + Send + Sync>);
|
||||||
|
let buf = SingletonBuffer {
|
||||||
|
value: data_arc,
|
||||||
|
port: sgl_port.inner()
|
||||||
|
};
|
||||||
|
self.keepalive = Some(buf.attach_to(
|
||||||
|
self.in_port.0.clone()
|
||||||
|
.downcast::<dyn SingletonView<Item = T>>()
|
||||||
|
.ok().unwrap()
|
||||||
|
.outer()
|
||||||
|
));
|
||||||
|
Some(buf)
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn as_vec_buffer<T>(&mut self) -> Option<VecBuffer<T>>
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let vec_port = self.get_port::< RwLock<Vec<T>> >().unwrap().0;
|
||||||
|
|
||||||
|
let data_arc =
|
||||||
|
if let Some(data) = self.data.as_ref() {
|
||||||
|
data.clone().downcast::<RwLock<Vec<T>>>().ok()
|
||||||
|
} else {
|
||||||
|
vec_port.update();
|
||||||
|
if let Some(value) = vec_port.outer().get_view() {
|
||||||
|
let value = value.read().unwrap().clone();
|
||||||
|
eprintln!("make new data ARC from old VECTOR-value");
|
||||||
|
Some(Arc::new(RwLock::new( value )))
|
||||||
|
} else {
|
||||||
|
eprintln!("no data vec");
|
||||||
|
Some(Arc::new(RwLock::new( Vec::new() )))
|
||||||
|
// None
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
if let Some(data_arc) = data_arc {
|
||||||
|
self.data = Some(data_arc.clone() as Arc<dyn Any + Send + Sync>);
|
||||||
|
let buf = VecBuffer::with_data_arc_port(data_arc, vec_port.inner());
|
||||||
|
self.keepalive = Some(buf.attach_to(
|
||||||
|
self.in_port.0.clone()
|
||||||
|
.downcast::< dyn ListView<T> >()
|
||||||
|
.ok().unwrap()
|
||||||
|
.outer()
|
||||||
|
));
|
||||||
|
Some(buf)
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_port<V>(&self) -> Option<OuterViewPort<V>>
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
self.out_port.clone().downcast::<V>().ok().map(|p| p.outer())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
impl ReprTree {
|
||||||
|
pub fn new(type_tag: impl Into<TypeTerm>) -> Self {
|
||||||
|
let type_tag = type_tag.into();
|
||||||
|
|
||||||
|
assert!(type_tag.is_flat());
|
||||||
|
|
||||||
|
ReprTree {
|
||||||
|
halo: TypeTerm::unit(),
|
||||||
|
type_tag: type_tag.clone(),
|
||||||
|
branches: HashMap::new(),
|
||||||
|
leaf: None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn new_arc(type_tag: impl Into<TypeTerm>) -> Arc<RwLock<Self>> {
|
||||||
|
Arc::new(RwLock::new(Self::new(type_tag)))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_type(&self) -> &TypeTerm {
|
||||||
|
&self.type_tag
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn set_halo(&mut self, halo_type: impl Into<TypeTerm>) {
|
||||||
|
self.halo = halo_type.into();
|
||||||
|
for (branch_type, branch) in self.branches.iter() {
|
||||||
|
branch.write().unwrap().set_halo( TypeTerm::Ladder(vec![
|
||||||
|
self.halo.clone(),
|
||||||
|
self.type_tag.clone()
|
||||||
|
]).normalize()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_halo_type(&self) -> &TypeTerm {
|
||||||
|
&self.halo
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_leaf_types(&self) -> Vec< TypeTerm > {
|
||||||
|
let mut leaf_types = Vec::new();
|
||||||
|
if self.leaf.is_some() {
|
||||||
|
leaf_types.push( self.get_type().clone() );
|
||||||
|
}
|
||||||
|
for (branch_type, branch) in self.branches.iter() {
|
||||||
|
for t in branch.read().unwrap().get_leaf_types() {
|
||||||
|
leaf_types.push(TypeTerm::Ladder(vec![
|
||||||
|
self.get_type().clone(),
|
||||||
|
t
|
||||||
|
]).normalize())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
leaf_types
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn insert_branch(&mut self, repr: Arc<RwLock<ReprTree>>) {
|
||||||
|
let branch_type = repr.read().unwrap().get_type().clone();
|
||||||
|
|
||||||
|
assert!(branch_type.is_flat());
|
||||||
|
|
||||||
|
repr.write().unwrap().set_halo( TypeTerm::Ladder(vec![
|
||||||
|
self.halo.clone(),
|
||||||
|
self.type_tag.clone()
|
||||||
|
]).normalize() );
|
||||||
|
|
||||||
|
self.branches.insert(branch_type, repr.clone());
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_char(ctx: &Arc<RwLock<Context>>, c: char ) -> Arc<RwLock<Self>> {
|
||||||
|
ReprTree::from_singleton_buffer(
|
||||||
|
Context::parse(ctx, "Char"),
|
||||||
|
SingletonBuffer::new(c)
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_view<V>( type_tag: impl Into<TypeTerm>, view: OuterViewPort<V> ) -> Arc<RwLock<Self>>
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
let mut rt = ReprTree::new(type_tag);
|
||||||
|
rt.leaf = Some(ReprLeaf::from_view(view));
|
||||||
|
Arc::new(RwLock::new(rt))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_singleton_buffer<T>( type_tag: impl Into<TypeTerm>, buf: SingletonBuffer<T> ) -> Arc<RwLock<Self>>
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let mut rt = ReprTree::new(type_tag);
|
||||||
|
rt.leaf = Some(ReprLeaf::from_singleton_buffer(buf));
|
||||||
|
Arc::new(RwLock::new(rt))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn from_vec_buffer<T>( type_tag: impl Into<TypeTerm>, buf: VecBuffer<T> ) -> Arc<RwLock<Self>>
|
||||||
|
where T: Clone + Send + Sync + 'static
|
||||||
|
{
|
||||||
|
let mut rt = ReprTree::new(type_tag);
|
||||||
|
rt.leaf = Some(ReprLeaf::from_vec_buffer(buf));
|
||||||
|
Arc::new(RwLock::new(rt))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn attach_to<V>(
|
||||||
|
&mut self,
|
||||||
|
src_port: OuterViewPort<V>
|
||||||
|
)
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
if let Some(leaf) = self.leaf.as_mut() {
|
||||||
|
leaf.attach_to(src_port);
|
||||||
|
} else {
|
||||||
|
eprintln!("cant attach branch without leaf");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// find, and if necessary, create corresponding path in repr-tree.
|
||||||
|
/// Attach src_port to input of that node
|
||||||
|
pub fn attach_leaf_to<V>(
|
||||||
|
&mut self,
|
||||||
|
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
||||||
|
src_port: OuterViewPort<V>
|
||||||
|
)
|
||||||
|
where V: View + ?Sized + 'static,
|
||||||
|
V::Msg: Clone
|
||||||
|
{
|
||||||
|
while let Some(rung_type) = type_ladder.next() {
|
||||||
|
if &rung_type != self.get_type() {
|
||||||
|
if let Some(next_repr) = self.branches.get(&rung_type) {
|
||||||
|
next_repr.write().unwrap().attach_leaf_to(type_ladder, src_port);
|
||||||
|
} else {
|
||||||
|
let mut next_repr = ReprTree::new(rung_type.clone());
|
||||||
|
next_repr.attach_leaf_to(type_ladder, src_port);
|
||||||
|
self.insert_branch(Arc::new(RwLock::new(next_repr)));
|
||||||
|
}
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if let Some(leaf) = self.leaf.as_mut() {
|
||||||
|
leaf.attach_to(src_port);
|
||||||
|
} else {
|
||||||
|
self.leaf = Some(ReprLeaf::from_view(src_port));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn detach(&mut self, ctx: &Arc<RwLock<Context>>) {
|
||||||
|
if let Some(leaf) = self.leaf.as_mut() {
|
||||||
|
if self.type_tag == Context::parse(&ctx, "Char") {
|
||||||
|
leaf.detach::<dyn SingletonView<Item = char>>();
|
||||||
|
}
|
||||||
|
if self.type_tag == Context::parse(&ctx, "<Vec Char>") {
|
||||||
|
leaf.detach_vec::<char>();
|
||||||
|
}
|
||||||
|
if self.type_tag == Context::parse(&ctx, "<List Char>") {
|
||||||
|
leaf.detach::<dyn ListView<char>>();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
for (t,b) in self.branches.iter_mut() {
|
||||||
|
b.write().unwrap().detach(&ctx);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn insert_leaf(
|
||||||
|
&mut self,
|
||||||
|
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
||||||
|
leaf: ReprLeaf
|
||||||
|
) {
|
||||||
|
while let Some(type_term) = type_ladder.next() {
|
||||||
|
if &type_term != self.get_type() {
|
||||||
|
if let Some(next_repr) = self.branches.get(&type_term) {
|
||||||
|
next_repr.write().unwrap().insert_leaf(type_ladder, leaf.clone());
|
||||||
|
} else {
|
||||||
|
let mut next_repr = ReprTree::new(type_term.clone());
|
||||||
|
next_repr.insert_leaf(type_ladder, leaf.clone());
|
||||||
|
self.insert_branch(Arc::new(RwLock::new(next_repr)));
|
||||||
|
}
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
self.leaf = Some(leaf);
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
pub fn descend_one(&self, dst_type: impl Into<TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
||||||
|
let dst_type = dst_type.into();
|
||||||
|
assert!( dst_type.is_flat() );
|
||||||
|
self.branches.get(&dst_type).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn descend_ladder(rt: &Arc<RwLock<Self>>, mut repr_ladder: impl Iterator<Item = TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
||||||
|
if let Some(first) = repr_ladder.next() {
|
||||||
|
let rt = rt.read().unwrap();
|
||||||
|
repr_ladder.fold(
|
||||||
|
rt.descend_one(first),
|
||||||
|
|s, t| s?.descend(t))
|
||||||
|
} else {
|
||||||
|
Some(rt.clone())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn descend(rt: &Arc<RwLock<Self>>, dst_type: impl Into<TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
||||||
|
let mut lnf = dst_type.into().get_lnf_vec();
|
||||||
|
if lnf.len() > 0 {
|
||||||
|
if lnf[0] == rt.get_type() {
|
||||||
|
lnf.remove(0);
|
||||||
|
}
|
||||||
|
ReprTree::descend_ladder(rt, lnf.into_iter())
|
||||||
|
} else {
|
||||||
|
Some(rt.clone())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn ascend(rt: &Arc<RwLock<Self>>, type_term: impl Into<TypeTerm>) -> Arc<RwLock<ReprTree>> {
|
||||||
|
let mut n = Self::new(type_term);
|
||||||
|
n.insert_branch(rt.clone());
|
||||||
|
Arc::new(RwLock::new(n))
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
pub fn singleton_buffer<T: Clone + Send + Sync + 'static>(&mut self) -> Option<SingletonBuffer<T>> {
|
||||||
|
if let Some(leaf) = self.leaf.as_mut() {
|
||||||
|
leaf.as_singleton_buffer::<T>()
|
||||||
|
} else {
|
||||||
|
// create new singleton buffer
|
||||||
|
/*
|
||||||
|
// default value??
|
||||||
|
let buf = SingletonBuffer::<T>::default();
|
||||||
|
self.leaf = Some(ReprLeaf::from_singleton_buffer(buf.clone()));
|
||||||
|
Some(buf)
|
||||||
|
*/
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn vec_buffer<T: Clone + Send + Sync + 'static>(&mut self) -> Option<VecBuffer<T>> {
|
||||||
|
if let Some(leaf) = self.leaf.as_mut() {
|
||||||
|
leaf.as_vec_buffer::<T>()
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
pub fn get_port<V: View + ?Sized + 'static>(&self) -> Option<OuterViewPort<V>>
|
||||||
|
where
|
||||||
|
V::Msg: Clone,
|
||||||
|
{
|
||||||
|
if let Some(leaf) = self.leaf.as_ref() {
|
||||||
|
leaf.get_port::<V>()
|
||||||
|
} else {
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_view<V: View + ?Sized + 'static>(&self) -> Option<Arc<V>>
|
||||||
|
where
|
||||||
|
V::Msg: Clone,
|
||||||
|
{
|
||||||
|
self.get_port::<V>()?
|
||||||
|
.get_view()
|
||||||
|
}
|
||||||
|
|
||||||
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
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>> {
|
||||||
|
self.get_port::<dyn SequenceView<Item = T>>().expect("no sequence-view available")
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn view_list<T: Clone + Send + Sync + 'static>(&self) -> OuterViewPort<dyn ListView<T>> {
|
||||||
|
self.get_port::<dyn ListView<T>>().expect("no list-view available")
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn view_char(&self) -> OuterViewPort<dyn SingletonView<Item = char>> {
|
||||||
|
self.get_port::<dyn SingletonView<Item = char>>().expect("no char-view available")
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn view_u8(&self) -> OuterViewPort<dyn SingletonView<Item = u8>> {
|
||||||
|
self.get_port::<dyn SingletonView<Item = u8>>().expect("no u8-view available")
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn view_u64(&self) -> OuterViewPort<dyn SingletonView<Item = u64>> {
|
||||||
|
self.get_port::<dyn SingletonView<Item = u64>>().expect("no u64-view available")
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn view_usize(&self) -> OuterViewPort<dyn SingletonView<Item = usize>> {
|
||||||
|
self.get_port::<dyn SingletonView<Item = usize>>().expect("no usize-view available")
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
pub trait ReprTreeExt {
|
pub trait ReprTreeExt {
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
use {
|
use {
|
||||||
laddertypes::{TypeTerm, TypeID, morphism::Morphism},
|
laddertypes::{TypeTerm, TypeID},
|
||||||
r3vi::view::{AnyOuterViewPort, port::UpdateTask},
|
r3vi::view::{AnyOuterViewPort, port::UpdateTask},
|
||||||
crate::{
|
crate::{
|
||||||
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf},
|
repr_tree::{ReprTree, ReprTreeExt, ReprLeaf},
|
||||||
|
@ -10,144 +10,248 @@ 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)]
|
#[derive(Clone)]
|
||||||
pub struct GenericReprTreeMorphism {
|
pub struct GenericReprTreeMorphism {
|
||||||
pub(super) morph_type: MorphismType,
|
morph_type: MorphismType,
|
||||||
pub(super) setup_projection: Arc<
|
setup_projection: Arc<
|
||||||
dyn Fn( &mut Arc<RwLock<ReprTree>>, &HashMap<TypeID, TypeTerm> )
|
dyn Fn( &mut Arc<RwLock<ReprTree>>, &HashMap<TypeID, TypeTerm> )
|
||||||
// -> Result< ReprLeaf, () >
|
// -> Result< ReprLeaf, () >
|
||||||
+ Send + Sync
|
+ Send + Sync
|
||||||
>
|
>
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Morphism for GenericReprTreeMorphism {
|
#[derive(Clone)]
|
||||||
fn get_type(&self) -> MorphismType {
|
pub struct MorphismBase {
|
||||||
self.morph_type.clone()
|
morphisms: Vec< GenericReprTreeMorphism >
|
||||||
}
|
|
||||||
|
|
||||||
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,
|
|
||||||
|
|
||||||
setup: impl Fn( &mut Arc<RwLock<ReprTree>>, &HashMap<TypeID, TypeTerm> )
|
impl MorphismBase {
|
||||||
+ Send + Sync + 'static
|
pub fn new() -> Self {
|
||||||
) -> Self {
|
MorphismBase {
|
||||||
GenericReprTreeMorphism {
|
morphisms: Vec::new()
|
||||||
morph_type: MorphismType {
|
|
||||||
src_type, dst_type
|
|
||||||
}.normalize(),
|
|
||||||
|
|
||||||
setup_projection: Arc::new(setup)
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn into_list_map< SrcItem, DstItem >(&self, list_typeid: TypeID)
|
pub fn add_morphism(
|
||||||
-> GenericReprTreeMorphism
|
&mut self,
|
||||||
where
|
morph_type: MorphismType,
|
||||||
|
setup_projection:
|
||||||
|
impl Fn( &mut Arc<RwLock<ReprTree>>, &HashMap<TypeID, TypeTerm> )
|
||||||
|
// -> 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<TypeID, TypeTerm>)> {
|
||||||
|
|
||||||
|
// 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<RwLock<crate::edit_tree::EditTree>> >( 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<TypeID, TypeTerm>
|
||||||
|
)> {
|
||||||
|
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<RwLock<ReprTree>>,
|
||||||
|
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<
|
||||||
SrcItem: Clone + Send + Sync + 'static,
|
SrcItem: Clone + Send + Sync + 'static,
|
||||||
DstItem: 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 > )
|
||||||
|
>
|
||||||
{
|
{
|
||||||
let mut lst_map_type = MorphismType {
|
if let Some((item_morphism, σ)) = self.find_morphism( &src_item_type, &dst_item_type ) {
|
||||||
src_type: TypeTerm::App(vec![
|
(&mut src_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||||
TypeTerm::TypeID(list_typeid),
|
(&mut dst_item_type).apply_substitution( &|v| σ.get(v).clone().cloned() );
|
||||||
self.morph_type.src_type.clone()
|
|
||||||
]),
|
|
||||||
dst_type: TypeTerm::App(vec![
|
|
||||||
TypeTerm::TypeID(list_typeid),
|
|
||||||
self.morph_type.dst_type.clone()
|
|
||||||
])
|
|
||||||
}.normalize();
|
|
||||||
|
|
||||||
let item_morph = self.clone();
|
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()
|
||||||
|
]);
|
||||||
|
|
||||||
GenericReprTreeMorphism{
|
let sigmalol = σ.clone();
|
||||||
morph_type: lst_map_type.clone(),
|
let m = GenericReprTreeMorphism{
|
||||||
setup_projection: Arc::new(move |repr_tree, subst| {
|
morph_type: MorphismType {
|
||||||
let mut lst_map_type = lst_map_type.clone();
|
src_type: src_lst_type.clone(),
|
||||||
lst_map_type.src_type.apply_substitution( &|x| subst.get(x).cloned() );
|
dst_type: dst_lst_type.clone(),
|
||||||
lst_map_type.dst_type.apply_substitution( &|x| subst.get(x).cloned() );
|
},
|
||||||
|
setup_projection: Arc::new(move |repr_tree, subst| {
|
||||||
|
let src_port = repr_tree.descend( src_lst_type.clone() ).expect("descend src seq")
|
||||||
|
.view_list::<SrcItem>();
|
||||||
|
|
||||||
eprintln!(
|
let src_item_type = src_item_type.clone();
|
||||||
"lst map type : {:?}", lst_map_type
|
let dst_item_type = dst_item_type.clone();
|
||||||
);
|
let item_morphism = item_morphism.clone();
|
||||||
|
let subst = subst.clone();
|
||||||
|
|
||||||
let src_port = repr_tree
|
let dst_view = src_port.map(
|
||||||
.descend( lst_map_type.src_type.clone() )
|
|
||||||
.expect("descend src seq")
|
|
||||||
.view_list::<SrcItem>();
|
|
||||||
|
|
||||||
let subst = subst.clone();
|
|
||||||
let item_morph = item_morph.clone();
|
|
||||||
|
|
||||||
let dst_view = src_port.map(
|
|
||||||
move |x| {
|
move |x| {
|
||||||
let mut item_ladder = item_morph.morph_type.src_type.clone().get_lnf_vec();
|
let mut item_ladder = src_item_type.clone().get_lnf_vec();
|
||||||
let mut item_rt = ReprTree::from_singleton_buffer(
|
let mut item_rt = ReprTree::from_singleton_buffer(
|
||||||
item_ladder.remove( item_ladder.len() - 1 ),
|
item_ladder.remove( item_ladder.len() - 1 ),
|
||||||
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
r3vi::buffer::singleton::SingletonBuffer::new(x.clone())
|
||||||
);
|
);
|
||||||
|
|
||||||
// TODO: required?
|
|
||||||
while item_ladder.len() > 0 {
|
while item_ladder.len() > 0 {
|
||||||
let mut n = ReprTree::new_arc( item_ladder.remove( item_ladder.len() - 1) );
|
let mut n = ReprTree::new_arc( item_ladder.remove( item_ladder.len() - 1) );
|
||||||
n.insert_branch( item_rt );
|
n.insert_branch( item_rt );
|
||||||
item_rt = n;
|
item_rt = n;
|
||||||
}
|
}
|
||||||
|
|
||||||
(item_morph.setup_projection)( &mut item_rt, &subst );
|
(item_morphism.setup_projection)( &mut item_rt, &subst );
|
||||||
item_rt.descend( item_morph.morph_type.dst_type.clone() ).expect("descend to item rt")
|
item_rt.descend( dst_item_type.clone() ).expect("descend to item rt")
|
||||||
.view_singleton::< DstItem >()
|
.view_singleton::< DstItem >()
|
||||||
.get_view().unwrap()
|
.get_view().unwrap()
|
||||||
.get()
|
.get()
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
repr_tree.attach_leaf_to(
|
repr_tree.attach_leaf_to(
|
||||||
lst_map_type.dst_type.clone(),
|
dst_lst_type.clone(),
|
||||||
dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView<DstItem> >
|
dst_view as r3vi::view::OuterViewPort::< dyn r3vi::view::list::ListView<DstItem> >
|
||||||
);
|
);
|
||||||
})
|
})
|
||||||
}
|
};
|
||||||
}
|
|
||||||
|
|
||||||
pub fn into_list_map_dyn(&self, typeid_list: TypeID)
|
Some((m, σ))
|
||||||
-> Option< GenericReprTreeMorphism >
|
} else {
|
||||||
{
|
// eprintln!("could not find item morphism\n");
|
||||||
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<RwLock<crate::edit_tree::EditTree>> >(typeid_list) )
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
eprintln!("no list map type for {:?}", dst_item_type_lnf.last());
|
|
||||||
None
|
None
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,394 +0,0 @@
|
||||||
|
|
||||||
|
|
||||||
use {
|
|
||||||
r3vi::{
|
|
||||||
view::{
|
|
||||||
ViewPort, OuterViewPort,
|
|
||||||
AnyViewPort, AnyInnerViewPort, AnyOuterViewPort,
|
|
||||||
port::UpdateTask,
|
|
||||||
View, Observer,
|
|
||||||
singleton::*,
|
|
||||||
sequence::*,
|
|
||||||
list::*
|
|
||||||
},
|
|
||||||
buffer::{singleton::*, vec::*}
|
|
||||||
},
|
|
||||||
laddertypes::{TypeTerm, TypeID},
|
|
||||||
std::{
|
|
||||||
collections::HashMap,
|
|
||||||
sync::{Arc, RwLock},
|
|
||||||
any::Any
|
|
||||||
},
|
|
||||||
super::{Context, ReprLeaf, ReprTreeExt}
|
|
||||||
};
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
#[derive(Clone)]
|
|
||||||
pub struct ReprTree {
|
|
||||||
halo: TypeTerm,
|
|
||||||
type_tag: TypeTerm,
|
|
||||||
branches: HashMap<TypeTerm, Arc<RwLock<ReprTree>>>,
|
|
||||||
leaf: Option< ReprLeaf >
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
impl std::fmt::Debug for ReprTree {
|
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
|
||||||
writeln!(f, "| type: {:?}", self.type_tag)?;
|
|
||||||
|
|
||||||
for (_k,x) in self.branches.iter() {
|
|
||||||
writeln!(f, "|--> child: {:?}", x)?;
|
|
||||||
}
|
|
||||||
writeln!(f, "");
|
|
||||||
|
|
||||||
Ok(())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
impl ReprTree {
|
|
||||||
pub fn new(type_tag: impl Into<TypeTerm>) -> Self {
|
|
||||||
let type_tag = type_tag.into();
|
|
||||||
|
|
||||||
assert!(type_tag.is_flat());
|
|
||||||
|
|
||||||
ReprTree {
|
|
||||||
halo: TypeTerm::unit(),
|
|
||||||
type_tag: type_tag.clone(),
|
|
||||||
branches: HashMap::new(),
|
|
||||||
leaf: None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn new_arc(type_tag: impl Into<TypeTerm>) -> Arc<RwLock<Self>> {
|
|
||||||
Arc::new(RwLock::new(Self::new(type_tag)))
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_type(&self) -> &TypeTerm {
|
|
||||||
&self.type_tag
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn set_halo(&mut self, halo_type: impl Into<TypeTerm>) {
|
|
||||||
self.halo = halo_type.into();
|
|
||||||
for (branch_type, branch) in self.branches.iter() {
|
|
||||||
branch.write().unwrap().set_halo( TypeTerm::Ladder(vec![
|
|
||||||
self.halo.clone(),
|
|
||||||
self.type_tag.clone()
|
|
||||||
]).normalize()
|
|
||||||
);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_halo_type(&self) -> &TypeTerm {
|
|
||||||
&self.halo
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_leaf_types(&self) -> Vec< TypeTerm > {
|
|
||||||
let mut leaf_types = Vec::new();
|
|
||||||
if self.leaf.is_some() {
|
|
||||||
leaf_types.push( self.get_type().clone() );
|
|
||||||
}
|
|
||||||
for (branch_type, branch) in self.branches.iter() {
|
|
||||||
for t in branch.read().unwrap().get_leaf_types() {
|
|
||||||
leaf_types.push(TypeTerm::Ladder(vec![
|
|
||||||
self.get_type().clone(),
|
|
||||||
t
|
|
||||||
]).normalize())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
leaf_types
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn insert_branch(&mut self, repr: Arc<RwLock<ReprTree>>) {
|
|
||||||
let branch_type = repr.read().unwrap().get_type().clone();
|
|
||||||
|
|
||||||
assert!(branch_type.is_flat());
|
|
||||||
|
|
||||||
repr.write().unwrap().set_halo( TypeTerm::Ladder(vec![
|
|
||||||
self.halo.clone(),
|
|
||||||
self.type_tag.clone()
|
|
||||||
]).normalize() );
|
|
||||||
|
|
||||||
self.branches.insert(branch_type, repr.clone());
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_char(ctx: &Arc<RwLock<Context>>, c: char ) -> Arc<RwLock<Self>> {
|
|
||||||
ReprTree::from_singleton_buffer(
|
|
||||||
Context::parse(ctx, "Char"),
|
|
||||||
SingletonBuffer::new(c)
|
|
||||||
)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_view<V>( type_tag: impl Into<TypeTerm>, view: OuterViewPort<V> ) -> Arc<RwLock<Self>>
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
let mut rt = ReprTree::new(type_tag);
|
|
||||||
rt.leaf = Some(ReprLeaf::from_view(view));
|
|
||||||
Arc::new(RwLock::new(rt))
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_singleton_buffer<T>( type_tag: impl Into<TypeTerm>, buf: SingletonBuffer<T> ) -> Arc<RwLock<Self>>
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let mut rt = ReprTree::new(type_tag);
|
|
||||||
rt.leaf = Some(ReprLeaf::from_singleton_buffer(buf));
|
|
||||||
Arc::new(RwLock::new(rt))
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
pub fn from_str(
|
|
||||||
type_tag: impl Into<TypeTerm>,
|
|
||||||
val: &str
|
|
||||||
) -> Arc<RwLock<Self>> {
|
|
||||||
let mut lnf = type_tag.into().get_lnf_vec();
|
|
||||||
|
|
||||||
let mut rt = ReprTree::from_vec_buffer(
|
|
||||||
lnf.pop().unwrap(),
|
|
||||||
VecBuffer::with_data( val.chars().collect() )
|
|
||||||
);
|
|
||||||
|
|
||||||
while let Some(t) = lnf.pop() {
|
|
||||||
let mut new_rt = ReprTree::new_arc(t);
|
|
||||||
new_rt.insert_branch(rt);
|
|
||||||
rt = new_rt;
|
|
||||||
}
|
|
||||||
|
|
||||||
rt
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_vec_buffer<T>( type_tag: impl Into<TypeTerm>, buf: VecBuffer<T> ) -> Arc<RwLock<Self>>
|
|
||||||
where T: Clone + Send + Sync + 'static
|
|
||||||
{
|
|
||||||
let mut rt = ReprTree::new(type_tag);
|
|
||||||
rt.leaf = Some(ReprLeaf::from_vec_buffer(buf));
|
|
||||||
Arc::new(RwLock::new(rt))
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn attach_to<V>(
|
|
||||||
&mut self,
|
|
||||||
src_port: OuterViewPort<V>
|
|
||||||
)
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
if let Some(leaf) = self.leaf.as_mut() {
|
|
||||||
leaf.attach_to(src_port);
|
|
||||||
} else {
|
|
||||||
eprintln!("cant attach branch without leaf");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// find, and if necessary, create corresponding path in repr-tree.
|
|
||||||
/// Attach src_port to input of that node
|
|
||||||
pub fn attach_leaf_to<V>(
|
|
||||||
&mut self,
|
|
||||||
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
|
||||||
src_port: OuterViewPort<V>
|
|
||||||
)
|
|
||||||
where V: View + ?Sized + 'static,
|
|
||||||
V::Msg: Clone
|
|
||||||
{
|
|
||||||
while let Some(rung_type) = type_ladder.next() {
|
|
||||||
if &rung_type != self.get_type() {
|
|
||||||
if let Some(next_repr) = self.branches.get(&rung_type) {
|
|
||||||
next_repr.write().unwrap().attach_leaf_to(type_ladder, src_port);
|
|
||||||
} else {
|
|
||||||
let mut next_repr = ReprTree::new(rung_type.clone());
|
|
||||||
next_repr.attach_leaf_to(type_ladder, src_port);
|
|
||||||
self.insert_branch(Arc::new(RwLock::new(next_repr)));
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if let Some(leaf) = self.leaf.as_mut() {
|
|
||||||
leaf.attach_to(src_port);
|
|
||||||
} else {
|
|
||||||
if self.type_tag == TypeTerm::App(vec![
|
|
||||||
TypeTerm::TypeID(TypeID::Fun(11)),
|
|
||||||
TypeTerm::TypeID(TypeID::Fun(2))
|
|
||||||
]) {
|
|
||||||
let mut leaf = ReprLeaf::from_vec_buffer(
|
|
||||||
VecBuffer::<
|
|
||||||
Arc<RwLock<crate::edit_tree::EditTree>>
|
|
||||||
>::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::<char>::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<RwLock<Context>>) {
|
|
||||||
if let Some(leaf) = self.leaf.as_mut() {
|
|
||||||
if self.type_tag == Context::parse(&ctx, "Char") {
|
|
||||||
leaf.detach::<dyn SingletonView<Item = char>>();
|
|
||||||
}
|
|
||||||
if self.type_tag == Context::parse(&ctx, "<Vec Char>") {
|
|
||||||
leaf.detach_vec::<char>();
|
|
||||||
}
|
|
||||||
if self.type_tag == Context::parse(&ctx, "<List Char>") {
|
|
||||||
leaf.detach::<dyn ListView<char>>();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
for (t,b) in self.branches.iter_mut() {
|
|
||||||
b.write().unwrap().detach(&ctx);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn insert_leaf(
|
|
||||||
&mut self,
|
|
||||||
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
|
||||||
leaf: ReprLeaf
|
|
||||||
) {
|
|
||||||
while let Some(type_term) = type_ladder.next() {
|
|
||||||
if &type_term != self.get_type() {
|
|
||||||
if let Some(next_repr) = self.branches.get(&type_term) {
|
|
||||||
next_repr.write().unwrap().insert_leaf(type_ladder, leaf.clone());
|
|
||||||
} else {
|
|
||||||
let mut next_repr = ReprTree::new(type_term.clone());
|
|
||||||
next_repr.insert_leaf(type_ladder, leaf.clone());
|
|
||||||
self.insert_branch(Arc::new(RwLock::new(next_repr)));
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
self.leaf = Some(leaf);
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
pub fn descend_one(&self, dst_type: impl Into<TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
|
||||||
let dst_type = dst_type.into();
|
|
||||||
assert!( dst_type.is_flat() );
|
|
||||||
self.branches.get(&dst_type).cloned()
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn descend_ladder(rt: &Arc<RwLock<Self>>, mut repr_ladder: impl Iterator<Item = TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
|
||||||
if let Some(first) = repr_ladder.next() {
|
|
||||||
let rt = rt.read().unwrap();
|
|
||||||
repr_ladder.fold(
|
|
||||||
rt.descend_one(first),
|
|
||||||
|s, t| s?.descend(t))
|
|
||||||
} else {
|
|
||||||
Some(rt.clone())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn descend(rt: &Arc<RwLock<Self>>, dst_type: impl Into<TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
|
||||||
let mut lnf = dst_type.into().get_lnf_vec();
|
|
||||||
if lnf.len() > 0 {
|
|
||||||
if lnf[0] == rt.get_type() {
|
|
||||||
lnf.remove(0);
|
|
||||||
}
|
|
||||||
ReprTree::descend_ladder(rt, lnf.into_iter())
|
|
||||||
} else {
|
|
||||||
Some(rt.clone())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn ascend(rt: &Arc<RwLock<Self>>, type_term: impl Into<TypeTerm>) -> Arc<RwLock<ReprTree>> {
|
|
||||||
let mut n = Self::new(type_term);
|
|
||||||
n.insert_branch(rt.clone());
|
|
||||||
Arc::new(RwLock::new(n))
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
pub fn singleton_buffer<T: Clone + Send + Sync + 'static>(&mut self) -> Option<SingletonBuffer<T>> {
|
|
||||||
if let Some(leaf) = self.leaf.as_mut() {
|
|
||||||
leaf.as_singleton_buffer::<T>()
|
|
||||||
} else {
|
|
||||||
// create new singleton buffer
|
|
||||||
/*
|
|
||||||
// default value??
|
|
||||||
let buf = SingletonBuffer::<T>::default();
|
|
||||||
self.leaf = Some(ReprLeaf::from_singleton_buffer(buf.clone()));
|
|
||||||
Some(buf)
|
|
||||||
*/
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn vec_buffer<T: Clone + Send + Sync + 'static>(&mut self) -> Option<VecBuffer<T>> {
|
|
||||||
if let Some(leaf) = self.leaf.as_mut() {
|
|
||||||
leaf.as_vec_buffer::<T>()
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
pub fn get_port<V: View + ?Sized + 'static>(&self) -> Option<OuterViewPort<V>>
|
|
||||||
where
|
|
||||||
V::Msg: Clone,
|
|
||||||
{
|
|
||||||
if let Some(leaf) = self.leaf.as_ref() {
|
|
||||||
leaf.get_port::<V>()
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_view<V: View + ?Sized + 'static>(&self) -> Option<Arc<V>>
|
|
||||||
where
|
|
||||||
V::Msg: Clone,
|
|
||||||
{
|
|
||||||
self.get_port::<V>()?
|
|
||||||
.get_view()
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
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>> {
|
|
||||||
self.get_port::<dyn SequenceView<Item = T>>().expect("no sequence-view available")
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn view_list<T: Clone + Send + Sync + 'static>(&self) -> OuterViewPort<dyn ListView<T>> {
|
|
||||||
self.get_port::<dyn ListView<T>>().expect("no list-view available")
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn view_char(&self) -> OuterViewPort<dyn SingletonView<Item = char>> {
|
|
||||||
self.get_port::<dyn SingletonView<Item = char>>().expect("no char-view available")
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn view_u8(&self) -> OuterViewPort<dyn SingletonView<Item = u8>> {
|
|
||||||
self.get_port::<dyn SingletonView<Item = u8>>().expect("no u8-view available")
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn view_u64(&self) -> OuterViewPort<dyn SingletonView<Item = u64>> {
|
|
||||||
self.get_port::<dyn SingletonView<Item = u64>>().expect("no u64-view available")
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn view_usize(&self) -> OuterViewPort<dyn SingletonView<Item = usize>> {
|
|
||||||
self.get_port::<dyn SingletonView<Item = usize>>().expect("no usize-view available")
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
|
@ -83,12 +83,10 @@ fn digit_projection_char_to_u64() {
|
||||||
//<><><><>
|
//<><><><>
|
||||||
// add another representation
|
// add another representation
|
||||||
|
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
rt_digit.clone(),
|
rt_digit.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<Digit 16>~Char"),
|
||||||
src_type: Context::parse(&ctx, "<Digit 16>~Char"),
|
&Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64")
|
||||||
dst_type: Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
let digit_u64_view = rt_digit
|
let digit_u64_view = rt_digit
|
||||||
|
@ -123,12 +121,10 @@ fn digit_projection_u64_to_char() {
|
||||||
//<><><><>
|
//<><><><>
|
||||||
// add another representation
|
// add another representation
|
||||||
|
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
rt_digit.clone(),
|
rt_digit.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64"),
|
||||||
src_type: Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64"),
|
&Context::parse(&ctx, "<Digit 16>~Char")
|
||||||
dst_type: Context::parse(&ctx, "<Digit 16>~Char")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
let digit_u64_view = rt_digit
|
let digit_u64_view = rt_digit
|
||||||
|
@ -174,12 +170,10 @@ fn char_buffered_projection() {
|
||||||
assert_eq!( digit_char_view.get_view().unwrap().get(), '5' );
|
assert_eq!( digit_char_view.get_view().unwrap().get(), '5' );
|
||||||
|
|
||||||
// now we attach the char-repr to the u64-repr
|
// now we attach the char-repr to the u64-repr
|
||||||
ctx.read().unwrap().apply_morphism(
|
ctx.read().unwrap().morphisms.apply_morphism(
|
||||||
rt_digit.clone(),
|
rt_digit.clone(),
|
||||||
&laddertypes::MorphismType {
|
&Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64"),
|
||||||
src_type: Context::parse(&ctx, "<Digit 16>~ℤ_2^64~machine.UInt64"),
|
&Context::parse(&ctx, "<Digit 16>~Char")
|
||||||
dst_type: Context::parse(&ctx, "<Digit 16>~Char")
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
// char buffer and view should now follow the u64-buffer
|
// char buffer and view should now follow the u64-buffer
|
||||||
|
|
|
@ -228,12 +228,10 @@ impl PTYListController {
|
||||||
rt.read().unwrap().get_type().clone(),
|
rt.read().unwrap().get_type().clone(),
|
||||||
ctx.type_term_from_str("EditTree").expect("")
|
ctx.type_term_from_str("EditTree").expect("")
|
||||||
]);
|
]);
|
||||||
ctx.apply_morphism(
|
ctx.morphisms.apply_morphism(
|
||||||
&rt,
|
rt.clone(),
|
||||||
&laddertypes::MorphismType {
|
&rt.get_type(),
|
||||||
src_type: rt.get_type(),
|
&ladder
|
||||||
dst_type: ladder
|
|
||||||
}
|
|
||||||
);
|
);
|
||||||
|
|
||||||
let new_edittree = ctx.setup_edittree(
|
let new_edittree = ctx.setup_edittree(
|
||||||
|
|
Loading…
Reference in a new issue