morphism base: new syntax
This commit is contained in:
parent
64e8b96c92
commit
4674e75e99
16 changed files with 218 additions and 205 deletions
morphisms
angle.morphism-basecolor.morphism-basecomplex.morphism-basederef.morphism-basedigit.morphism-baseenergy.morphism-baselength_prefix.morphism-baseposint.morphism-basereal.morphism-basetemperature.morphism-basetimepoint.morphism-baseuint.morphism-baseunicode.morphism-basevalue_delim.morphism-basewheatstone.morphism-basezigzag.morphism-base
|
@ -2,45 +2,45 @@
|
|||
#define PHI 6.28318530718
|
||||
```
|
||||
|
||||
morph_angle_as_degrees_to_turns_float ()
|
||||
morph angle_as_degrees_to_turns_float :
|
||||
Angle ~ Degrees ~ ℝ ~ native.Float32
|
||||
--> Angle ~ Turns ~ ℝ ~ native.Float32
|
||||
```*dst = *src / 360.0;```
|
||||
= ```*dst = *src / 360.0;```
|
||||
|
||||
morph_angle_as_degrees_to_turns_double ()
|
||||
morph angle_as_degrees_to_turns_double :
|
||||
Angle ~ Degrees ~ ℝ ~ native.Float64
|
||||
--> Angle ~ Turns ~ ℝ ~ native.Float64
|
||||
```*dst = *src / 360.0;```
|
||||
= ```*dst = *src / 360.0;```;
|
||||
|
||||
|
||||
morph_angle_as_turns_to_degrees_float ()
|
||||
morph angle_as_turns_to_degrees_float :
|
||||
Angle ~ Turns ~ ℝ ~ native.Float32
|
||||
--> Angle ~ Degrees ~ ℝ ~ native.Float32
|
||||
```*dst = *src * 360.0;```
|
||||
= ```*dst = *src * 360.0;```;
|
||||
|
||||
morph_angle_as_turns_to_degrees_double ()
|
||||
morph angle_as_turns_to_degrees_double :
|
||||
Angle ~ Turns ~ ℝ ~ native.Float64
|
||||
--> Angle ~ Degrees ~ ℝ ~ native.Float64
|
||||
```*dst = *src * 360.0;```
|
||||
= ```*dst = *src * 360.0;```;
|
||||
|
||||
|
||||
morph_angle_as_radians_to_turns_float ()
|
||||
morph angle_as_radians_to_turns_float :
|
||||
Angle ~ Radians ~ ℝ ~ native.Float32
|
||||
--> Angle ~ Turns ~ ℝ ~ native.Float32
|
||||
```*dst = *src / PHI;```
|
||||
= ```*dst = *src / PHI;```;
|
||||
|
||||
morph_angle_as_radians_to_turns_double ()
|
||||
morph angle_as_radians_to_turns_double :
|
||||
Angle ~ Radians ~ ℝ ~ native.Float64
|
||||
--> Angle ~ Turns ~ ℝ ~ native.Float64
|
||||
```*dst = *src / PHI;```
|
||||
= ```*dst = *src / PHI;```;
|
||||
|
||||
|
||||
morph_angle_as_turns_to_radians_float ()
|
||||
morph angle_as_turns_to_radians_float :
|
||||
Angle ~ Turns ~ ℝ ~ native.Float32
|
||||
--> Angle ~ Radians ~ ℝ ~ native.Float32
|
||||
```*dst = *src * PHI;```
|
||||
= ```*dst = *src * PHI;```;
|
||||
|
||||
morph_angle_as_turns_to_radians_double ()
|
||||
morph angle_as_turns_to_radians_double :
|
||||
Angle ~ Turns ~ ℝ ~ native.Float64
|
||||
--> Angle ~ Radians ~ ℝ ~ native.Float64
|
||||
```*dst = *src * PHI;```
|
||||
= ```*dst = *src * PHI;```;
|
||||
|
|
|
@ -2,7 +2,7 @@
|
|||
#include <math.h>
|
||||
```
|
||||
|
||||
morph_color_as_rgb_to_hsv ()
|
||||
morph color_as_rgb_to_hsv :
|
||||
RgbaColor ~ RGB ~ <Struct
|
||||
<red ℝ ~ native.Float32>
|
||||
<green ℝ ~ native.Float32>
|
||||
|
@ -15,7 +15,7 @@ morph_color_as_rgb_to_hsv ()
|
|||
<value ℝ ~ native.Float32>
|
||||
<alpha ℝ ~ native.Float32>
|
||||
>
|
||||
```
|
||||
= ```
|
||||
float max = fmaxf(fmaxf(src->red, src->green), src->blue);
|
||||
float min = fminf(fminf(src->red, src->green), src->blue);
|
||||
float delta = max - min;
|
||||
|
@ -35,10 +35,10 @@ morph_color_as_rgb_to_hsv ()
|
|||
dst->saturation = (max == 0) ? 0 : (delta / max);
|
||||
dst->value = max;
|
||||
dst->alpha = src->alpha;
|
||||
```
|
||||
```;
|
||||
|
||||
|
||||
morph_color_as_hsv_to_rgb ()
|
||||
morph color_as_hsv_to_rgb :
|
||||
RgbaColor ~ HSV ~ <Struct
|
||||
<hue Angle ~ Turns ~ ℝ ~ native.Float32>
|
||||
<saturation ℝ ~ native.Float32>
|
||||
|
@ -51,7 +51,7 @@ morph_color_as_hsv_to_rgb ()
|
|||
<blue ℝ ~ native.Float32>
|
||||
<alpha ℝ ~ native.Float32>
|
||||
>
|
||||
```
|
||||
= ```
|
||||
float C = src->value * src->saturation;
|
||||
float X = C * (1 - fabsf(fmodf(src->hue * 6.0, 2) - 1));
|
||||
float m = src->value - C;
|
||||
|
@ -76,4 +76,4 @@ morph_color_as_hsv_to_rgb ()
|
|||
dst->green = g + m;
|
||||
dst->blue = b + m;
|
||||
dst->alpha = src->alpha;
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,16 +1,32 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_complex_as_polar_to_cartesian ()
|
||||
ℂ ~ Polar ~ <Struct~Aligned <phi Angle~Radians~ℝ~native.Float64> <val ℝ~native.Float64>>
|
||||
--> ℂ ~ Cartesian ~ <Struct~Aligned <x ℝ~native.Float64> <y ℝ~native.Float64>>
|
||||
```
|
||||
morph complex_as_polar_to_cartesian :
|
||||
ℂ ~ Polar
|
||||
~ <Struct~Aligned
|
||||
<phi Angle~Radians~ℝ~native.Float64>
|
||||
<val ℝ~native.Float64>
|
||||
>
|
||||
--> ℂ ~ Cartesian
|
||||
~ <Struct~Aligned
|
||||
<x ℝ~native.Float64>
|
||||
<y ℝ~native.Float64>
|
||||
>
|
||||
= ```
|
||||
return 0;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_complex_as_cartesian_to_polar ()
|
||||
ℂ ~ Cartesian ~ <Struct~Aligned <x ℝ~native.Float64> <y ℝ~native.Float64>>
|
||||
--> ℂ ~ Polar ~ <Struct~Aligned <phi Angle~Radians~ℝ~native.Float64> <val ℝ~native.Float64>>
|
||||
```
|
||||
morph complex_as_cartesian_to_polar :
|
||||
ℂ ~ Cartesian
|
||||
~ <Struct~Aligned
|
||||
<x ℝ~native.Float64>
|
||||
<y ℝ~native.Float64>
|
||||
>
|
||||
--> ℂ ~ Polar
|
||||
~ <Struct~Aligned
|
||||
<phi Angle~Radians~ℝ~native.Float64>
|
||||
<val ℝ~native.Float64>
|
||||
>
|
||||
= ```
|
||||
return 0;
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,21 +1,21 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_ref_to_val8 (T: Type) where (T<=native.UInt8)
|
||||
morph ref_to_val8 : (T: Type) where (T native.UInt8)
|
||||
< Ref~Ptr T >
|
||||
~ native.Address
|
||||
--> T~native.UInt8
|
||||
```
|
||||
=```
|
||||
*dst = **src ;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_ref_to_val16 (T: Type) where (T<=native.UInt8)
|
||||
morph ref_to_val16 : ∀(T: Type) where (T<native.UInt8)
|
||||
< Ref~Ptr T~native.UInt16 >
|
||||
~ native.Address
|
||||
--> T~native.UInt16
|
||||
```
|
||||
=```
|
||||
*dst = **src ;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_ref_to_val32 (T: Type)
|
||||
< Ref~Ptr T~native.UInt32 >
|
||||
|
|
|
@ -1,11 +1,10 @@
|
|||
```
|
||||
#include <stdio.h>
|
||||
```
|
||||
|
||||
morph_digit_as_char_to_uint8 (Radix:ℤ)
|
||||
morph digit_as_char_to_uint8 : ∀(Radix:ℤ).
|
||||
<Digit Radix> ~ Char ~ Ascii ~ native.UInt8
|
||||
--> <Digit Radix> ~ ℕ ~ native.UInt8
|
||||
```
|
||||
--> <Digit Radix> ~ <ℤ Radix> ~ <ℤ 256> ~ native.UInt8
|
||||
= ```
|
||||
if( *src >= '0' && *src <= '9' )
|
||||
*dst = *src - '0';
|
||||
else if( *src >= 'a' && *src <= 'f')
|
||||
|
@ -23,12 +22,12 @@ morph_digit_as_char_to_uint8 (Radix:ℤ)
|
|||
fprintf(stderr, "digit %u is out of range for radix %u\n", *dst, Radix);
|
||||
return -1;
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
||||
morph_digit_as_uint8_to_char (Radix:ℤ_16)
|
||||
<Digit Radix> ~ ℕ ~ native.UInt8
|
||||
morph digit_as_uint8_to_char : ∀(Radix:<ℤ 16>).
|
||||
<Digit Radix> ~ <ℤ Radix> ~ <ℤ 256> ~ native.UInt8
|
||||
--> <Digit Radix> ~ Char ~ Ascii ~ native.UInt8
|
||||
```
|
||||
= ```
|
||||
if ( *src < 10 )
|
||||
*dst = *src + '0';
|
||||
else if( *dst < 16 )
|
||||
|
@ -37,4 +36,4 @@ morph_digit_as_uint8_to_char (Radix:ℤ_16)
|
|||
fprintf(stderr, "digit %u is out of rage for char\n", *dst);
|
||||
return -1;
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,16 +1,18 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_energy_as_wh_to_joule ()
|
||||
type Joule = Energy ~ Ws;
|
||||
|
||||
morph energy_as_wh_to_joule :
|
||||
Energy ~ Wh ~ ℝ ~ native.Float64
|
||||
--> Energy ~ Joule ~ ℝ ~ native.Float64
|
||||
```
|
||||
--> Energy ~ Ws ~ ℝ ~ native.Float64
|
||||
= ```
|
||||
*dst = *src * 3600.0;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_energy_as_joule_to_wh ()
|
||||
Energy ~ Joule ~ ℝ ~ native.Float64
|
||||
morph energy_as_joule_to_wh :
|
||||
Energy ~ Ws ~ ℝ ~ native.Float64
|
||||
--> Energy ~ Wh ~ ℝ ~ native.Float64
|
||||
```
|
||||
= ```
|
||||
*dst = *src / 3600.0;
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -3,50 +3,52 @@
|
|||
#include <array/length-prefix.h>
|
||||
```
|
||||
|
||||
morph_array_as_static_to_lenpfx (Len: ℤ, T: Type)
|
||||
morph array_as_static_to_lenpfx : ∀(Len: ℕ). ∀(T: Type).
|
||||
<Seq~<StaticLength Len> T>
|
||||
--> <Seq~<LengthPrefix native.UInt64> T>
|
||||
```
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, clear)( dst );
|
||||
= ```
|
||||
//PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, clear)( dst );
|
||||
length_prefix_nativeUInt64_array_##T##_clear(dst);
|
||||
for( nativeUInt64 i = 0; i < Len; ++i )
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, push)( dst, src->items[i] );
|
||||
```
|
||||
length_prefix_nativeUInt64_array_##T##_push(dst, src->items[i]);
|
||||
//PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, push)( dst, src->items[i] );
|
||||
```;
|
||||
|
||||
morph_array_as_lenpfx_to_static (Len: ℤ, T: Type)
|
||||
morph array_as_lenpfx_to_static : ∀(Len: ℕ). ∀(T: Type).
|
||||
<Seq~<LengthPrefix native.UInt64> T>
|
||||
--> <Seq~<StaticLength Len> T>
|
||||
```
|
||||
= ```
|
||||
nativeUInt64 i;
|
||||
for( i = 0; i < Len && i < src->len; ++i )
|
||||
dst->items[i] = src->items[i];
|
||||
|
||||
if( i < Len )
|
||||
memset( &dst[i], 0, (Len-i) * sizeof(T) );
|
||||
```
|
||||
```;
|
||||
|
||||
morph_array_as_valterm_to_lenpfx (T: Type, Terminator:T)
|
||||
morph array_as_valterm_to_lenpfx : ∀(T: Type). ∀(Terminator:T).
|
||||
<Seq~<ValueTerminated Terminator> T>
|
||||
--> <Seq~<LengthPrefix native.UInt64> T>
|
||||
```
|
||||
= ```
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, push)( dst );
|
||||
while( *src != Terminator )
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, push)( dst, *src++ );
|
||||
```
|
||||
```;
|
||||
|
||||
morph_array_as_lenpfx_to_valterm (T: Type, Terminator: T)
|
||||
morph array_as_lenpfx_to_valterm : ∀(T: Type). ∀(Terminator: T).
|
||||
<Seq~<LengthPrefix native.UInt64> T>
|
||||
--> <Seq~<ValueTerminated Terminator> T>
|
||||
```
|
||||
=```
|
||||
for( uint64_t i = 0; i < src->len; ++i )
|
||||
*dst++ = src->items[i];
|
||||
|
||||
*dst = Terminator;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_array_as_lenpfx_to_continuation_bit (T:Type)
|
||||
morph array_as_lenpfx_to_continuation_bit : ∀(T:Type).
|
||||
<Seq~<LengthPrefix native.UInt64> T>
|
||||
--> <Seq~MsbCont T>
|
||||
```
|
||||
= ```
|
||||
for( uint64_t i = 0; i < src->len; ++i ) {
|
||||
const size_t n_bits = 8*sizeof(T);
|
||||
if( src->items[i] & ((uint64_t)1<<(n_bits-1)) ) {
|
||||
|
@ -58,4 +60,4 @@ morph_array_as_lenpfx_to_continuation_bit (T:Type)
|
|||
if( i+1 < src->len )
|
||||
dst[i] |= ((uint64_t)1<<(n_bits-1));
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -2,36 +2,37 @@
|
|||
#include <array/length-prefix.h>
|
||||
```
|
||||
|
||||
morph_nat_as_u64_to_pos ()
|
||||
morph nat_as_u64_to_pos :
|
||||
ℕ
|
||||
~ native.UInt64
|
||||
--> ℕ
|
||||
~ <PosInt 0 LittleEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit 0> ~ℕ~ native.UInt64>
|
||||
```
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit 0> ~ℕ~ native.UInt64
|
||||
> = ```
|
||||
dst->len = 1;
|
||||
dst->items[0] = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_nat_as_pos_to_u64 (Endianness:Type)
|
||||
morph nat_as_pos_to_u64 : (Endianness:Type)
|
||||
ℕ
|
||||
~ <PosInt 0 Endianness>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit 0> ~ℕ~ native.UInt64>
|
||||
--> ℕ
|
||||
-->
|
||||
ℕ
|
||||
~ native.UInt64
|
||||
```
|
||||
= ```
|
||||
*dst = src->items[0];
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_radix_le (SrcRadix:ℤ, DstRadix:ℤ)
|
||||
morph posint_radix_le : ∀(SrcRadix:ℤ). ∀(DstRadix:ℤ).
|
||||
ℕ
|
||||
~ <PosInt SrcRadix LittleEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit SrcRadix> ~ℕ~ native.UInt64>
|
||||
-->
|
||||
ℕ
|
||||
ℕ
|
||||
~ <PosInt DstRadix LittleEndian>
|
||||
~ <Seq~<LenghtPrefix native.UInt64> <Digit DstRadix> ~ℕ~ native.UInt64>
|
||||
```
|
||||
= ```
|
||||
uint64_t value = 0;
|
||||
|
||||
for( uint64_t i = 0; i < src->len; ++i ) {
|
||||
|
@ -51,16 +52,16 @@ morph_posint_radix_le (SrcRadix:ℤ, DstRadix:ℤ)
|
|||
value /= DstRadix;
|
||||
}
|
||||
#endif
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_radix_be (SrcRadix:ℤ, DstRadix:ℤ)
|
||||
morph posint_radix_be : ∀(SrcRadix:ℤ).∀(DstRadix:ℤ).
|
||||
ℕ
|
||||
~ <PosInt SrcRadix BigEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit SrcRadix> ~ℕ~ native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt DstRadix BigEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit DstRadix> ~ℕ~ native.UInt64>
|
||||
```
|
||||
= ```
|
||||
uint64_t value = 0;
|
||||
|
||||
for( uint64_t i = 0; i < src->len; ++i ) {
|
||||
|
@ -88,48 +89,48 @@ morph_posint_radix_be (SrcRadix:ℤ, DstRadix:ℤ)
|
|||
value /= DstRadix;
|
||||
}
|
||||
#endif
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_endianness_le_to_be (Radix:ℤ)
|
||||
morph posint_endianness_le_to_be : ∀(Radix:ℤ).
|
||||
ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ℕ~ native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ℕ~ native.UInt64>
|
||||
```
|
||||
= ```
|
||||
return length_prefix_nativeUInt64_array_nativeUInt64_reverse( (void*)src, (void*)dst );
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_endianness_be_to_le (Radix:ℤ)
|
||||
morph posint_endianness_be_to_le : ∀(Radix:ℤ).
|
||||
ℕ
|
||||
~ <PosInt Radix BigEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ℕ~ native.UInt64>
|
||||
--> ℕ
|
||||
~ <PosInt Radix LittleEndian>
|
||||
~ <Seq~<LengthPrefix native.UInt64> <Digit Radix> ~ℕ~ native.UInt64>
|
||||
```
|
||||
= ```
|
||||
return length_prefix_nativeUInt64_array_nativeUInt64_reverse( (void*)src, (void*)dst );
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_uint32_endianness_be_to_le ()
|
||||
morph posint_uint32_endianness_be_to_le :
|
||||
ℕ
|
||||
~ <PosInt 256 BigEndian>
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~ℕ~ native.UInt8 >
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~<ℤ 256>~ native.UInt8 >
|
||||
--> ℕ
|
||||
~ <PosInt 256 LittleEndian>
|
||||
~ <Seq~<StaticLength 8> <Digit 256> ~ℕ~ native.UInt8 >
|
||||
```
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~<ℤ 256>~ native.UInt8 >
|
||||
= ```
|
||||
*dst = __builtin_bswap32(*src);
|
||||
```
|
||||
```;
|
||||
|
||||
morph_posint_uint32_endianness_le_to_be ()
|
||||
morph posint_uint32_endianness_le_to_be :
|
||||
ℕ
|
||||
~ <PosInt 256 LittleEndian>
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~ℕ~ native.UInt8 >
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~<ℤ 256>~ native.UInt8 >
|
||||
--> ℕ
|
||||
~ <PosInt 256 BigEndian>
|
||||
~ <Seq~<StaticLength 8> <Digit 256> ~ℕ~ native.UInt8 >
|
||||
```
|
||||
~ < Seq~<StaticLength 8> <Digit 256> ~<ℤ 256>~ native.UInt8 >
|
||||
= ```
|
||||
*dst = __builtin_bswap32(*src);
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -2,89 +2,87 @@
|
|||
#include <stdio.h>
|
||||
```
|
||||
|
||||
morph_real_as_decimalstr_to_float ()
|
||||
morph real_as_decimalstr_to_float :
|
||||
ℝ ~ <PosInt 10 BigEndian> ~ <Seq~<ValueTerminated 0> <Digit 10>~Char~Ascii~native.UInt8>
|
||||
--> ℝ ~ native.Float32
|
||||
```sscanf(src, "%f", dst);```
|
||||
= ```sscanf(src, "%f", dst);```;
|
||||
|
||||
morph_real_as_decimalstr_to_double ()
|
||||
morph real_as_decimalstr_to_double :
|
||||
ℝ ~ <PosInt 10 BigEndian> ~ <Seq~<ValueTerminated 0> <Digit 10>~Char~Ascii~native.UInt8>
|
||||
--> ℝ ~ native.Float64
|
||||
```sscanf(src, "%lf", dst);```
|
||||
= ```sscanf(src, "%lf", dst);```;
|
||||
|
||||
morph_real_as_float_to_decimalstr ()
|
||||
morph real_as_float_to_decimalstr :
|
||||
ℝ ~ native.Float32
|
||||
--> ℝ ~ <PosInt 10 BigEndian> ~ <Seq~<ValueTerminated 0> <Digit 10>~Char~Ascii~native.UInt8>
|
||||
```sprintf(dst, "%f", *src);```
|
||||
= ```sprintf(dst, "%f", *src);```;
|
||||
|
||||
morph_real_as_double_to_decimalstr ()
|
||||
morph real_as_double_to_decimalstr :
|
||||
ℝ ~ native.Float64
|
||||
--> ℝ ~ <PosInt 10 BigEndian> ~ <Seq~<ValueTerminated 0> <Digit 10>~Char~Ascii~native.UInt8>
|
||||
```sprintf(dst, "%f", *src);```
|
||||
= ```sprintf(dst, "%f", *src);```;
|
||||
|
||||
morph_real_as_float_to_double ()
|
||||
morph real_as_float_to_double :
|
||||
ℝ ~ native.Float32
|
||||
--> ℝ ~ native.Float64
|
||||
```*dst = *src;```
|
||||
= ```*dst = *src;```;
|
||||
|
||||
morph_real_as_double_to_float ()
|
||||
morph real_as_double_to_float :
|
||||
ℝ ~ native.Float64
|
||||
--> ℝ ~ native.Float32
|
||||
```
|
||||
= ```
|
||||
fprintf(stderr, "Warning: morphin Double -> Float. Precision loss!");
|
||||
*dst = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_real_as_u64_to_float ()
|
||||
morph real_as_u64_to_float :
|
||||
ℝ ~ ℕ ~ native.UInt64
|
||||
--> ℝ ~ native.Float32
|
||||
```
|
||||
= ```
|
||||
fprintf(stderr, "Warning: morphin UInt64 -> Float. Precision loss!");
|
||||
*dst = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_real_as_u64_to_double ()
|
||||
morph real_as_u64_to_double :
|
||||
ℝ ~ ℕ ~ native.UInt64
|
||||
--> ℝ ~ native.Float64
|
||||
```
|
||||
= ```
|
||||
fprintf(stderr, "Warning: morphin UInt64 -> Double. Precision loss!");
|
||||
*dst = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
|
||||
morph_real_as_nat_to_quantized_linear ()
|
||||
morph real_as_nat_to_quantized_linear :
|
||||
ℝ ~ ℕ ~ native.UInt64
|
||||
--> ℝ ~ <QuantizedLinear 0 1 1> ~ ℕ ~ native.UInt64
|
||||
```
|
||||
= ```
|
||||
*dst = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_real_as_quantized_linear_to_float (Begin: ℝ, End: ℝ, Steps: ℤ)
|
||||
morph real_as_quantized_linear_to_float : ∀(Begin: ℝ). ∀(End: ℝ). ∀(Steps: ℤ).
|
||||
ℝ ~ <QuantizedLinear Begin End Steps> ~ ℕ ~ native.UInt64
|
||||
--> ℝ ~ native.Float32
|
||||
```
|
||||
= ```
|
||||
*dst = (float)Begin + ( *src * ((float)End - (float)Begin) ) / (float)Steps;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_real_as_float_to_quantized_linear (Begin: ℝ, End: ℝ, Steps: ℤ)
|
||||
morph real_as_float_to_quantized_linear : ∀(Begin: ℝ). ∀(End: ℝ). ∀(Steps: ℤ).
|
||||
ℝ ~ native.Float32
|
||||
--> ℝ ~ <QuantizedLinear Begin End Steps> ~ ℕ ~ native.UInt64
|
||||
```
|
||||
= ```
|
||||
*dst = ((*src - (float)Begin) * (float)Steps) / ((float)End - (float)Begin);
|
||||
```
|
||||
```;
|
||||
|
||||
|
||||
|
||||
morph_real_as_quantized_linear_to_double (Begin: ℝ, End: ℝ, Steps: ℤ)
|
||||
morph real_as_quantized_linear_to_double : ∀(Begin: ℝ). ∀(End: ℝ). ∀(Steps: ℤ).
|
||||
ℝ ~ <QuantizedLinear Begin End Steps> ~ ℕ ~ native.UInt64
|
||||
--> ℝ ~ native.Float64
|
||||
```
|
||||
*dst = (double)Begin + ( *src * ((double)End - (double)Begin) ) / (double)Steps;
|
||||
```
|
||||
= ```
|
||||
*dst = (double)Begin + ( *src * ((double)End - (double)Begin) ) / (double)Steps;
|
||||
```;
|
||||
|
||||
morph_real_as_double_to_quantized_linear (Begin: ℝ, End: ℝ, Steps: ℤ)
|
||||
morph real_as_double_to_quantized_linear : ∀(Begin: ℝ). ∀(End: ℝ). ∀(Steps: ℤ).
|
||||
ℝ ~ native.Float64
|
||||
--> ℝ ~ <QuantizedLinear Begin End Steps> ~ ℕ ~ native.UInt64
|
||||
```
|
||||
= ```
|
||||
*dst = ((*src - (double)Begin) * (double)Steps) / ((double)End - (double)Begin);
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,30 +1,30 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_celsius_to_kelvin ()
|
||||
morph celsius_to_kelvin :
|
||||
Temperature ~ Celsius ~ ℝ ~ native.Float32
|
||||
--> Temperature ~ Kelvin ~ ℝ ~ native.Float32
|
||||
```*dst = *src + 273.15;```
|
||||
= ```*dst = *src + 273.15;```;
|
||||
|
||||
morph_kelvin_to_celsius ()
|
||||
morph kelvin_to_celsius :
|
||||
Temperature ~ Kelvin ~ ℝ ~ native.Float32
|
||||
--> Temperature ~ Celsius ~ ℝ ~ native.Float32
|
||||
```*dst = *src - 273.15;```
|
||||
= ```*dst = *src - 273.15;```;
|
||||
|
||||
morph_celsius_to_fahrenheit ()
|
||||
morph celsius_to_fahrenheit :
|
||||
Temperature ~ Celsius ~ ℝ ~ native.Float32
|
||||
--> Temperature ~ Fahrenheit ~ ℝ ~ native.Float32
|
||||
```*dst = (*src * 9.0 / 5.0) + 32.0;```
|
||||
= ```*dst = (*src * 9.0 / 5.0) + 32.0;```;
|
||||
|
||||
morph_fahrenheit_to_celsius ()
|
||||
morph fahrenheit_to_celsius :
|
||||
Temperature ~ Fahrenheit ~ ℝ ~ native.Float32
|
||||
--> Temperature ~ Celsius ~ ℝ ~ native.Float32
|
||||
```*dst = (*src - 32.0) * 5.0 / 9.0;```
|
||||
=```*dst = (*src - 32.0) * 5.0 / 9.0;```;
|
||||
|
||||
morph_pt100_resistance_to_celsius ()
|
||||
morph pt100_resistance_to_celsius :
|
||||
Temperature ~ PT100 ~ Resistance ~ Ohms ~ ℝ ~ native.Float64
|
||||
--> Temperature ~ Celsius ~ ℝ ~ native.Float64
|
||||
```
|
||||
= ```
|
||||
double resistance = *src;
|
||||
|
||||
// Constants for PT100 (ITS-90 standard)
|
||||
|
@ -46,4 +46,4 @@ morph_pt100_resistance_to_celsius ()
|
|||
}
|
||||
|
||||
*dst = (-b + sqrt(discriminant)) / (2 * a); // use positive root
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -2,13 +2,13 @@
|
|||
#include <time.h>
|
||||
```
|
||||
|
||||
morph_unixtime_to_iso ()
|
||||
morph unixtime_to_iso :
|
||||
TimePoint ~ <TimeSince UnixEpoch> ~ Duration ~ Seconds ~ ℝ ~ <QuantizedLinear 0 1 1> ~ ℕ ~ native.UInt64
|
||||
--> TimePoint ~ ISO8601 ~ <Seq~<ValueTerminated 0> Char~Ascii~native.UInt8>
|
||||
```
|
||||
= ```
|
||||
time_t rawtime = (time_t)(*src);
|
||||
struct tm *timeinfo = gmtime(&rawtime);
|
||||
if (!timeinfo) return -1;
|
||||
|
||||
strftime((char*)dst, 20, "%Y-%m-%dT%H:%M:%SZ", timeinfo);
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,37 +1,36 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_nat_as_u8_to_u16 ()
|
||||
morph nat_as_u8_to_u16 :
|
||||
ℕ ~ native.UInt8
|
||||
--> ℕ ~ native.UInt16
|
||||
```*dst = *src;```
|
||||
= ```*dst = *src;```;
|
||||
|
||||
morph_nat_as_u16_to_u32 ()
|
||||
morph nat_as_u16_to_u32 :
|
||||
ℕ ~ native.UInt16
|
||||
--> ℕ ~ native.UInt32
|
||||
```*dst = *src;```
|
||||
= ```*dst = *src;```;
|
||||
|
||||
morph_nat_as_u32_to_u64 ()
|
||||
morph nat_as_u32_to_u64 :
|
||||
ℕ ~ native.UInt32
|
||||
--> ℕ ~ native.UInt64
|
||||
```*dst = *src;```
|
||||
= ```*dst = *src;```;
|
||||
|
||||
|
||||
morph_nat_as_u64_to_u16 ()
|
||||
morph nat_as_u64_to_u16 :
|
||||
ℕ ~ native.UInt64
|
||||
--> ℕ ~ native.UInt16
|
||||
```
|
||||
= ```
|
||||
if( *src > 65535 ) {
|
||||
fprintf(stderr, "error: value out of range for native.UInt16");
|
||||
return -1;
|
||||
}
|
||||
*dst = *src;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_nat_as_uint64_to_uint8
|
||||
morph nat_as_uint64_to_uint8 :
|
||||
ℕ ~ native.UInt64
|
||||
--> ℕ ~ native.UInt8
|
||||
```
|
||||
= ```
|
||||
if ( *src < 256 ) {
|
||||
*dst = *src;
|
||||
}
|
||||
|
@ -39,4 +38,4 @@ morph_nat_as_uint64_to_uint8
|
|||
fprintf(stderr, "value %u is out of rage for UInt8\n", *dst);
|
||||
return -1;
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -2,23 +2,23 @@
|
|||
#include <stdio.h>
|
||||
```
|
||||
|
||||
morph_string_as_ascii_to_utf8 ()
|
||||
morph string_as_ascii_to_utf8 :
|
||||
<Seq ~ <ValueTerminated 0> Char~Ascii~native.UInt8>
|
||||
--> <Seq Char~Unicode>
|
||||
~ UTF-8
|
||||
~ <Seq~<ValueTerminated 0> native.UInt8>
|
||||
```
|
||||
= ```
|
||||
while( *src ) { *dst++ = *src++; }
|
||||
*dst = 0;
|
||||
return 0;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_string_as_utf8_to_ascii ()
|
||||
morph string_as_utf8_to_ascii :
|
||||
<Seq Char~Unicode>
|
||||
~ UTF-8
|
||||
~ <Seq~<ValueTerminated 0> native.UInt8>
|
||||
--> <Seq ~ <ValueTerminated 0> Char~Ascii~native.UInt8>
|
||||
```
|
||||
= ```
|
||||
while( *src ) {
|
||||
if( *src < 128 ) {
|
||||
*dst++ = *src++;
|
||||
|
@ -28,29 +28,26 @@ morph_string_as_utf8_to_ascii ()
|
|||
}
|
||||
}
|
||||
*dst = 0;
|
||||
```
|
||||
```;
|
||||
|
||||
morph_string_as_ascii_to_utf32 ()
|
||||
morph string_as_ascii_to_utf32 :
|
||||
<Seq ~ <ValueTerminated 0> Char~Ascii~native.UInt8>
|
||||
--> <Seq Char~Unicode>
|
||||
~ UTF-32
|
||||
~ <Seq~<ValueTerminated 0> native.UInt32>
|
||||
```
|
||||
= ```
|
||||
while( *src ) { *dst++ = *src++; }
|
||||
*dst = 0;
|
||||
```
|
||||
|
||||
morph_string_as_utf8_to_utf32 ()
|
||||
```;
|
||||
|
||||
morph string_as_utf8_to_utf32 :
|
||||
<Seq Char~Unicode>
|
||||
~ UTF-8
|
||||
~ <Seq~<ValueTerminated 0> native.UInt8>
|
||||
|
||||
--> <Seq Char~Unicode>
|
||||
~ UTF-32
|
||||
~ <Seq~<ValueTerminated 0> native.UInt32>
|
||||
|
||||
```
|
||||
= ```
|
||||
bool has_multibyte = false;
|
||||
uint32_t val = 0;
|
||||
while( *src ) {
|
||||
|
@ -87,4 +84,4 @@ morph_string_as_utf8_to_utf32 ()
|
|||
*dst++ = val;
|
||||
|
||||
*dst++ = 0;
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
#include <stdlib.h>
|
||||
```
|
||||
|
||||
morph_valsep_delim (T: Type, SrcDelim: T, DstDelim: T)
|
||||
morph valsep_delim : ∀(T: Type). ∀(SrcDelim: T). ∀(DstDelim: T).
|
||||
< Seq <Seq T> >
|
||||
~ < ValueSep SrcDelim T >
|
||||
~ < Seq~<LengthPrefix native.UInt64> T >
|
||||
|
@ -11,7 +11,7 @@ morph_valsep_delim (T: Type, SrcDelim: T, DstDelim: T)
|
|||
--> < Seq <Seq T> >
|
||||
~ < ValueSep DstDelim T >
|
||||
~ < Seq~<LengthPrefix native.UInt64> T >
|
||||
```
|
||||
=```
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, clear)( dst );
|
||||
|
||||
uint8_t * dst_items = dst->items;
|
||||
|
@ -30,9 +30,9 @@ morph_valsep_delim (T: Type, SrcDelim: T, DstDelim: T)
|
|||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, push)( dst, src->items[i] );
|
||||
}
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
||||
morph_seqseq_as_valsep_to_lenpfx (T: Type, Delim: T, EscKey: T)
|
||||
morph seqseq_as_valsep_to_lenpfx : ∀(T: Type). ∀(Delim: T). ∀(EscKey: T).
|
||||
< Seq <Seq T> >
|
||||
~ < ValueSep T Delim >
|
||||
~ < Seq~<LengthPrefix native.UInt64> T >
|
||||
|
@ -43,7 +43,7 @@ morph_seqseq_as_valsep_to_lenpfx (T: Type, Delim: T, EscKey: T)
|
|||
~ native.Address
|
||||
~ native.UInt64
|
||||
>
|
||||
```
|
||||
= ```
|
||||
length_prefix_nativeUInt64_array_nativeUInt64_clear( dst );
|
||||
|
||||
LENGTH_PREFIX_ARRAY_TYPE( nativeUInt64, T ) * cur_item = NULL;
|
||||
|
@ -66,9 +66,9 @@ morph_seqseq_as_valsep_to_lenpfx (T: Type, Delim: T, EscKey: T)
|
|||
cur++;
|
||||
}
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
||||
morph_seqeq_as_lenpfx_to_valsep (T: Type, Delim: T, EscKey: T)
|
||||
morph seqeq_as_lenpfx_to_valsep : ∀(T: Type). ∀(Delim: T). ∀(EscKey: T).
|
||||
< Seq~<LengthPrefix native.UInt64>
|
||||
<Seq~<LengthPrefix native.UInt64> T >
|
||||
~ <RefMut < Seq~<LengthPrefix native.UInt64> T>>
|
||||
|
@ -78,7 +78,7 @@ morph_seqeq_as_lenpfx_to_valsep (T: Type, Delim: T, EscKey: T)
|
|||
--> < Seq <Seq T> >
|
||||
~ < ValueSep T Delim >
|
||||
~ < Seq~<LengthPrefix native.UInt64> T >
|
||||
```
|
||||
= ```
|
||||
PRESCAN_LENGTH_PREFIX_CALL(nativeUInt64, T, clear)( dst );
|
||||
|
||||
for( uint64_t i = 0; i < src->len; ++i ) {
|
||||
|
@ -92,4 +92,4 @@ morph_seqeq_as_lenpfx_to_valsep (T: Type, Delim: T, EscKey: T)
|
|||
PRESCAN_LENGTH_PREFIX_CALL( nativeUInt64, T, push )( Delim );
|
||||
}
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,15 +1,14 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_wheatstone_reading_to_ohms (
|
||||
vin: Resistance ~ Ohms ~ ℝ,
|
||||
r1: Resistance ~ Ohms ~ ℝ,
|
||||
r2: Resistance ~ Ohms ~ ℝ,
|
||||
r3: Resistance ~ Ohms ~ ℝ
|
||||
)
|
||||
morph wheatstone_reading_to_ohms :
|
||||
∀(vin: Resistance ~ Ohms ~ ℝ).
|
||||
∀(r1: Resistance ~ Ohms ~ ℝ).
|
||||
∀(r2: Resistance ~ Ohms ~ ℝ).
|
||||
∀(r3: Resistance ~ Ohms ~ ℝ).
|
||||
Resistance ~ <WheatstoneBridge vin r1 r2 r3> ~ ℝ ~ native.Float64
|
||||
--> Resistance ~ Ohms ~ ℝ ~ native.Float64
|
||||
```
|
||||
= ```
|
||||
// Voltage at midpoints of two voltage dividers:
|
||||
double v1 = vin * (r2 / (r1 + r2));
|
||||
double v2 = *src; // From the ADC
|
||||
|
@ -21,4 +20,4 @@ morph_wheatstone_reading_to_ohms (
|
|||
}
|
||||
|
||||
*dst = r3 * v2 / (vin - v2);
|
||||
```
|
||||
```;
|
||||
|
|
|
@ -1,24 +1,24 @@
|
|||
```
|
||||
```
|
||||
|
||||
morph_i64_as_twos_complement_to_zigzag ()
|
||||
morph i64_as_twos_complement_to_zigzag :
|
||||
ℤ ~ native.Int64
|
||||
--> ℤ ~ ZigZagInt ~ ℕ ~ native.UInt64
|
||||
```
|
||||
= ```
|
||||
if( *src >= 0 ) {
|
||||
*dst = (2 * (uint64_t)*src)
|
||||
} else {
|
||||
*dst = (2 * (uint64_t)(- *src)) - 1;
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
||||
morph_i64_as_zigzag_to_twos_complement ()
|
||||
morph i64_as_zigzag_to_twos_complement :
|
||||
ℤ ~ ZigZagInt ~ ℕ ~ native.UInt64
|
||||
--> ℤ ~ native.Int64
|
||||
```
|
||||
= ```
|
||||
if( *src % 2 == 0 ) {
|
||||
*dst = *src / 2;
|
||||
} else {
|
||||
*dst = - ((*src+1) / 2);
|
||||
}
|
||||
```
|
||||
```;
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue