add morphisms between machine.UInt64 and PosInt

This commit is contained in:
Michael Sippel 2024-09-01 23:21:49 +02:00
parent aed4cad1e4
commit 6ed456e3ff
Signed by: senvas
GPG key ID: F96CF119C34B64A6

View file

@ -170,9 +170,52 @@ pub fn init_ctx(ctx: Arc<RwLock<Context>>) {
}
);
let posint_list_morph_from_u64 = GenericReprTreeMorphism::new(
Context::parse(&ctx, " ~ machine.UInt64"),
Context::parse(&ctx, " ~ <PosInt 0 LittleEndian> ~ <Seq~List <Digit 0>~_2^64~machine.UInt64>"),
{
let ctx = ctx.clone();
move |rt, σ| {
let digits = rt
.descend(Context::parse(&ctx, " ~ machine.UInt64")).unwrap()
.view_u64()
.to_sequence()
.to_list();
rt.attach_leaf_to(
Context::parse(&ctx, "~ <PosInt 0 LittleEndian> ~ <Seq~List <Digit 0>~_2^64~machine.UInt64>"),
digits
);
}
}
);
let posint_list_morph_to_u64 = GenericReprTreeMorphism::new(
Context::parse(&ctx, " ~ <PosInt 0 LittleEndian> ~ <Seq~List <Digit 0>~_2^64~machine.UInt64> ~ <Vec machine.UInt64>"),
Context::parse(&ctx, " ~ machine.UInt64"),
{
let ctx = ctx.clone();
move |rt, σ| {
let u64_view = rt
.descend(Context::parse(&ctx, "~ <PosInt 0 LittleEndian> ~ <Seq~List <Digit 0>~_2^64~machine.UInt64> ~ <Vec machine.UInt64>")).unwrap()
.get_port::< RwLock<Vec< u64 >> >().unwrap()
.to_singleton()
.map(|digits| {
digits.get(0).cloned().unwrap_or(0)
});
rt.attach_leaf_to(
Context::parse(&ctx, " ~ machine.UInt64"),
u64_view
);
}
}
);
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 );
ctx.write().unwrap().morphisms.add_morphism( posint_list_morph_from_u64 );
ctx.write().unwrap().morphisms.add_morphism( posint_list_morph_to_u64 );
}