replace x86.T with native.T
This commit is contained in:
parent
e29a5a3475
commit
f67f8c0118
12 changed files with 91 additions and 91 deletions
morphisms
|
@ -4,10 +4,10 @@
|
|||
|
||||
morph_nat_as_u64_to_pos ()
|
||||
ℕ
|
||||
~ x86.UInt64
|
||||
~ native.UInt64
|
||||
--> ℕ
|
||||
~ <PosInt 0 LittleEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit 0>~x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit 0>~native.UInt64>
|
||||
```
|
||||
dst->len = 1;
|
||||
dst->items[0] = *src;
|
||||
|
@ -17,9 +17,9 @@ morph_nat_as_u64_to_pos ()
|
|||
morph_nat_as_pos_to_u64 (Endianness:Type)
|
||||
ℕ
|
||||
~ <PosInt 0 Endianness>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit 0>~x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit 0>~native.UInt64>
|
||||
--> ℕ
|
||||
~ x86.UInt64
|
||||
~ native.UInt64
|
||||
```
|
||||
*dst = src->items[0];
|
||||
return 0;
|
||||
|
@ -28,10 +28,10 @@ morph_nat_as_pos_to_u64 (Endianness:Type)
|
|||
morph_posint_radix_le (SrcRadix:ℤ, DstRadix:ℤ)
|
||||
ℕ
|
||||
~ <PosInt SrcRadix LittleEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit SrcRadix>~x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit SrcRadix>~native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt DstRadix LittleEndian>
|
||||
~ <Seq~<LenghtPrefix x86.UInt64> <Digit DstRadix>~x86.UInt64>
|
||||
~ <Seq~<LenghtPrefix native.UInt64> <Digit DstRadix>~native.UInt64>
|
||||
```
|
||||
uint64_t value = 0;
|
||||
|
||||
|
@ -59,10 +59,10 @@ morph_posint_radix_le (SrcRadix:ℤ, DstRadix:ℤ)
|
|||
morph_posint_radix_be (SrcRadix:ℤ, DstRadix:ℤ)
|
||||
ℕ
|
||||
~ <PosInt SrcRadix BigEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit SrcRadix>~x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit SrcRadix>~native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt DstRadix BigEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit DstRadix>~x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit DstRadix>~native.UInt64>
|
||||
```
|
||||
uint64_t value = 0;
|
||||
|
||||
|
@ -98,10 +98,10 @@ morph_posint_radix_be (SrcRadix:ℤ, DstRadix:ℤ)
|
|||
morph_posint_endianness (Radix:ℤ)
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit Radix> ~ x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit Radix> ~ x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ native.UInt64>
|
||||
```
|
||||
return length_prefix_uint64_t_array_uint64_t_reverse( src, dst );
|
||||
```
|
||||
|
@ -109,10 +109,10 @@ morph_posint_endianness (Radix:ℤ)
|
|||
morph_posint_endianness (Radix:ℤ)
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit Radix> ~ x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq~<LengthPrefix x86.UInt64> <Digit Radix> ~ x86.UInt64>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ native.UInt64>
|
||||
```
|
||||
return length_prefix_uint64_t_array_uint64_t_reverse( src, dst );
|
||||
```
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue