From 6ed456e3ff303234bfbcbe3408002ff39ab6a782 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 1 Sep 2024 23:21:49 +0200 Subject: [PATCH] add morphisms between machine.UInt64 and PosInt --- lib-nested-core/src/editors/integer/ctx.rs | 43 ++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/lib-nested-core/src/editors/integer/ctx.rs b/lib-nested-core/src/editors/integer/ctx.rs index dc6aa61..d7df660 100644 --- a/lib-nested-core/src/editors/integer/ctx.rs +++ b/lib-nested-core/src/editors/integer/ctx.rs @@ -170,9 +170,52 @@ pub fn init_ctx(ctx: Arc>) { } ); + let posint_list_morph_from_u64 = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ machine.UInt64"), + Context::parse(&ctx, "ℕ ~ ~ ~ℤ_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, "ℕ ~ ~ ~ℤ_2^64~machine.UInt64>"), + digits + ); + } + } + ); + let posint_list_morph_to_u64 = GenericReprTreeMorphism::new( + Context::parse(&ctx, "ℕ ~ ~ ~ℤ_2^64~machine.UInt64> ~ "), + Context::parse(&ctx, "ℕ ~ machine.UInt64"), + { + let ctx = ctx.clone(); + move |rt, σ| { + let u64_view = rt + .descend(Context::parse(&ctx, "ℕ ~ ~ ~ℤ_2^64~machine.UInt64> ~ ")).unwrap() + .get_port::< RwLock> >().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 ); }