add morphisms between machine.UInt64 and PosInt
This commit is contained in:
parent
fea21dbda1
commit
ca5ba52e53
1 changed files with 43 additions and 0 deletions
|
@ -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 );
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue