Compare commits
No commits in common. "72122bf4fcbe5a767735fb0fbcf1f3740d510fbc" and "f5f22ad65d6d6475eed66beadca32dcf7f72a961" have entirely different histories.
72122bf4fc
...
f5f22ad65d
13 changed files with 32 additions and 996 deletions
31
fetch.lt
31
fetch.lt
|
|
@ -1,31 +0,0 @@
|
|||
|
||||
export {
|
||||
let fetch-word :
|
||||
&machine.Word ~ <AlignedPtr 8> ~ machine.Address ~ machine.UInt64
|
||||
-> machine.Word;
|
||||
|
||||
let fetch-byte :
|
||||
&<Bits 8>
|
||||
~ <AlignedPtr 8>
|
||||
~ machine.Address
|
||||
~ machine.UInt64
|
||||
-> <Bits 8>
|
||||
~ machine.Word
|
||||
= λ ptr ↦ {
|
||||
fetch-word (align ptr);
|
||||
bit-shr (* 8 (ptr % 8));
|
||||
bit-and 0xff;
|
||||
};
|
||||
|
||||
let fetch-nibble
|
||||
: &<Bits 4>
|
||||
~ <AlignedPtr 4>
|
||||
~ machine.UInt64
|
||||
|
||||
-> <Bits 4>
|
||||
~ machine.Word
|
||||
= λ idx ↦ {
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
export {
|
||||
let angle-normalize =
|
||||
λ a : Angle
|
||||
~ Degree
|
||||
~ ℝ_0,360
|
||||
~ ℤ_360
|
||||
~ ℤ_2^64
|
||||
~ machine.UInt64
|
||||
~ machine.Word
|
||||
↦ Angle~Degree~ℝ_0,360~ℤ_360: machine.UInt64.rem a 360;
|
||||
|
||||
let angle-degree-to-turns =
|
||||
λ a : Angle
|
||||
~ Degree
|
||||
~ ℝ_0,360
|
||||
~ ℝ
|
||||
~ machine.Float64
|
||||
↦ f/ a 360 ;
|
||||
}
|
||||
|
|
@ -1,35 +1,36 @@
|
|||
export {
|
||||
/* todo: allow machine.UInt8 in the VM
|
||||
*/
|
||||
let morph-rgb-to-hsv = λ{
|
||||
{
|
||||
red: ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64;
|
||||
green: ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64;
|
||||
blue: ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64;
|
||||
red: ℝ_0,1 ~ ℤ_256 ~ machine.UInt64;
|
||||
green: ℝ_0,1 ~ ℤ_256 ~ machine.UInt64;
|
||||
blue: ℝ_0,1 ~ ℤ_256 ~ machine.UInt64;
|
||||
} : <Color sRGB>
|
||||
~ RGB
|
||||
~ <Vec3 ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64>;
|
||||
}
|
||||
/*
|
||||
-> <Color sRGB>
|
||||
~ HSV
|
||||
~ {
|
||||
hue: Angle ~ Degrees ~ ℝ_0,360 ~ ℤ_360 ~ machine.UInt64 ;
|
||||
sat: ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64;
|
||||
val: ℝ_[0,1] ~ ℤ_256 ~ machine.UInt64;
|
||||
}
|
||||
~ <Vec3 machine.UInt64>
|
||||
*/
|
||||
↦ {
|
||||
~ <Vec3 ℝ_0,1 ~ ℤ_256 ~ machine.UInt64>;
|
||||
/*
|
||||
::> Color
|
||||
~ HSV
|
||||
~ {
|
||||
hue: Angle
|
||||
~ Degrees
|
||||
~ ℝ_0,360
|
||||
~ ℤ_360
|
||||
~ machine.UInt64 ;
|
||||
|
||||
saturation: ℝ_0,1 ~ ℤ_256 ~ machine.UInt64 ;
|
||||
value: ℝ_0,1 ~ ℤ_256 ~ machine.UInt64 ;
|
||||
}
|
||||
~ <Vec3 machine.UInt64>
|
||||
*/
|
||||
} ↦ {
|
||||
let channel_max = int-max (int-max red green) blue;
|
||||
let channel_min = int-min (int-min red green) blue;
|
||||
let channel_delta = i- channel_max channel_min;
|
||||
|
||||
/* value */
|
||||
/* value */
|
||||
channel_max;
|
||||
|
||||
/* saturation */
|
||||
i/ (i* 255 channel_delta) channel_max;
|
||||
i/ (i* 255 (i- channel_max channel_min)) channel_max;
|
||||
|
||||
/* hue */
|
||||
i% (i/ (i* 60
|
||||
|
|
@ -39,25 +40,8 @@ export {
|
|||
else { i+ (i* 4 255) (i- red green); };
|
||||
}
|
||||
)
|
||||
channel_delta
|
||||
(i- channel_max channel_min)
|
||||
)
|
||||
360;
|
||||
};
|
||||
|
||||
/*
|
||||
let get-srgb-luminance =
|
||||
-> ℝ_[0,1] ~ machine.Float64
|
||||
λ{r:ℝ,g:ℝ,b:ℝ} : <Color sRGB> ~ RGB ~ <Vec3 ℝ_[0,1] ~ machine.Float64>
|
||||
↦
|
||||
{
|
||||
machine.Float64.mul red 0.22248840;
|
||||
machine.Float64.mul green 0.71690369;
|
||||
machine.Float64.mul blue 0.06060791;
|
||||
machine.Float64.add;
|
||||
machine.Float64.add;
|
||||
|
||||
// add (add (mul r 0.2) (mul g 0.7)) (mul b 0.6)
|
||||
};
|
||||
*/
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,10 +0,0 @@
|
|||
export {
|
||||
let complex-magnitude = λ{
|
||||
{ re: ℝ, im: ℝ }
|
||||
: ℂ
|
||||
~ Cartesian
|
||||
~ <Vec2 ℝ ~ machine.Float64>
|
||||
} -> ℝ ↦ {
|
||||
|
||||
}
|
||||
}
|
||||
|
|
@ -1,61 +0,0 @@
|
|||
export {
|
||||
/* Platform Specific Types */
|
||||
type machine.Float16 = IEEE-754.half ~ <machine.Bits 16>;
|
||||
type machine.Float32 = IEEE-754.single ~ <machine.Bits 32>;
|
||||
type machine.Float64 = IEEE-754.double ~ <machine.Bits 64>;
|
||||
|
||||
overload + = λ{
|
||||
a:ℝ ~ machine.Float16 ;
|
||||
b:ℝ ~ machine.Float16 ;
|
||||
} -> ℝ ~ machine.Float16 ↦ {
|
||||
machine.Float16.add a b;
|
||||
};
|
||||
|
||||
overload * = λ{
|
||||
a:ℝ ~ machine.Float16 ;
|
||||
b:ℝ ~ machine.Float16 ;
|
||||
} -> ℝ ~ machine.Float16 ↦ {
|
||||
machine.Float16.mul a b;
|
||||
};
|
||||
|
||||
let Sign = enum { Positive; Negative; };
|
||||
let Sign.Positive : <machine.Bits 1> = 0;
|
||||
let Sign.Negative : <machine.Bits 1> = 1;
|
||||
|
||||
let softfloat16-mul = λ{
|
||||
{
|
||||
a.sign: Sign
|
||||
~ <machine.Bits 1>
|
||||
;
|
||||
a.exponent: ℤ_[-14,15]
|
||||
~ <BiasedInt -14>
|
||||
~ ℤ_32
|
||||
~ <PosInt 2 BigEndian>
|
||||
~ <Seq <Digit 2>~Bit >
|
||||
~ <machine.Bits 5>
|
||||
;
|
||||
a.significand: ℤ_2048
|
||||
~ <PosInt 2 BigEndian>
|
||||
~ <Seq <Digit2> ~ Bit>
|
||||
~ <machine.Bits 11>
|
||||
;
|
||||
} : ℝ
|
||||
~ IEEE-754.Half
|
||||
~ <machine.Bits 16>
|
||||
;
|
||||
{
|
||||
b.sign: <machine.Bits 1>;
|
||||
} : ℝ ~ IEEE-754.Half ~ <machine.Bits 16> ;
|
||||
} -> result: ℝ ~ IEEE~754.Half ~ <machine.Bits 16> ↦ {
|
||||
|
||||
/* 1. unify */
|
||||
|
||||
/* 2. add exponent */
|
||||
+ a.exponent b.exponent;
|
||||
|
||||
/* 3. normaize */
|
||||
|
||||
result.sign = bit-xor a.sign b.sign ;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1,138 +0,0 @@
|
|||
/* C++ */
|
||||
|
||||
template <typename T>
|
||||
struct Sample {
|
||||
T value;
|
||||
};
|
||||
|
||||
template<> struct Sample< uint8_t > {
|
||||
constexpr uint8_t min = std::numeric_limits<uint8_t>::min();
|
||||
constexpr uint8_t max = std::numeric_limits<uint8_t>::max();
|
||||
};
|
||||
template<> struct Sample< uint16_t > {
|
||||
constexpr uint16_t min = std::numeric_limits<uint16_t>::min();
|
||||
constexpr uint16_t max = std::numeric_limits<uint16_t>::max();
|
||||
};
|
||||
template<> struct Sample< uint32_t > {
|
||||
constexpr uint32_t min = std::numeric_limits<uint32_t>::min();
|
||||
constexpr uint32_t max = std::numeric_limits<uint32_t>::max();
|
||||
};
|
||||
template<> struct Sample< float > {
|
||||
constexpr float min = 0.0;
|
||||
constexpr float max = 1.0;
|
||||
};
|
||||
template<> struct Sample< double > {
|
||||
constexpr double min = 0.0;
|
||||
constexpr double max = 1.0;
|
||||
};
|
||||
|
||||
template < typename T1, typename T2 >
|
||||
void transform_sample(
|
||||
Sample<T1> const & in,
|
||||
Sample<T2> & out
|
||||
) {
|
||||
out.value = static_cast<T1>( in.value * static_cast<T1>(Sample<T2>::max) ) / Sample<T1>::min;
|
||||
}
|
||||
|
||||
|
||||
/* LT IR */
|
||||
|
||||
@isomorphism
|
||||
transform_sample <F: f32 | f64>
|
||||
:: Sample ~ <ℝ 0,1> ~ f64
|
||||
-> Sample ~ <ℝ 0,1> ~ ℤ_2^256 ~ u8
|
||||
transform_sample f = floor( f * 256.0 ) as ℤ_2^256 ~ u8
|
||||
|
||||
@isomorphism
|
||||
transform_sample :: Sample ~ <ℝ 0,1> ~ ℤ_2^256 ~ u8
|
||||
-> Sample ~ <ℝ 0,1> ~ f64
|
||||
transform_sample i = (i as ℝ~f64) / 256.0
|
||||
|
||||
transform_sample <T1 T2> :: Sample~ℝ~T1 -> ℝ~T2
|
||||
transform_sample v
|
||||
|
||||
|
||||
void main() {
|
||||
|
||||
// read Audio streams
|
||||
for( unsigned i = 0; i < )
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
/* LT IR */
|
||||
|
||||
type Color~RGB = { r|red: ℝ_0,1; g|green: ℝ_0,1; b|blue: ℝ_0,1; }
|
||||
type Color~HSL = { h|hue: ℝ_0,1; s|saturation: ℝ_0,1; l|lightness: ℝ_0,1; }
|
||||
|
||||
validate <ℝ> :: f64 -> {}
|
||||
validate x = {}
|
||||
|
||||
morph :: Color~RGB -> Color~HSL
|
||||
morph (r,g,b) = {
|
||||
let h = .. TODO ..
|
||||
...
|
||||
(h,s,l)
|
||||
}
|
||||
|
||||
morph :: ℝ_0,1 ~ f64 -> ℝ_0,1 ~ ℤ_256
|
||||
morph x = (x * 256.0) % 256
|
||||
|
||||
morph :: ℝ_0,1 ~ ℤ_256 -> ℝ_0,1 ~ f64
|
||||
morph x = (x as f64 / 256.0)
|
||||
|
||||
infix * :: ℝ~f64 -> ℝ~f64 -> ℝ~f64
|
||||
infix * a b = f64.mul a b
|
||||
|
||||
clamp :: ℝ -> ℝ -> ℝ -> ℝ
|
||||
clamp minVal maxVal x = if x < minVal { minVal }
|
||||
else if x > maxVal { maxVal }
|
||||
else { x }
|
||||
|
||||
saturate :: ℝ -> Color~HSL -> Color~HSL
|
||||
saturate f {h,s,l} = { h, clamp(f*s, 0.0, 1.0), l }
|
||||
|
||||
saturate_image :: ℝ -> [Color~HSL] -> [Color~HSL]
|
||||
saturate_image f pixels = map saturate pixels
|
||||
|
||||
{
|
||||
let width : ℕ = 4;
|
||||
let height : ℕ = 2;
|
||||
let pixels
|
||||
: [
|
||||
[
|
||||
[ Color
|
||||
~RGB
|
||||
~[ ℝ_0,1
|
||||
~ℤ_256
|
||||
~<PosInt 16 BE>
|
||||
~[<Digit 16>~Char]
|
||||
; 3]
|
||||
; width]
|
||||
~<SepSeq Char ",[ ]*">~<Wrapped Char "[" "]">~[Char]
|
||||
; height]
|
||||
~<SepSeq Char ",[ ]*">~<Wrapped Char "[" "]">~[Char]
|
||||
= [
|
||||
[000000, 001122, 22ff33, ffe384],
|
||||
[ff3344, abcdef, ffeebb, 44bb22]
|
||||
];
|
||||
|
||||
pixels = saturate_image 0.3 pixels
|
||||
|
||||
let packed_buf = array_layout_rot
|
||||
<
|
||||
[[Color~RGB~[ℝ_0,1; 3]; width]; height],
|
||||
[[Color; width]; height]; 3]
|
||||
>
|
||||
pixels;
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
brighten_image :: ℕ -> ℕ -> [Color] [[ Color~RGB~[ℝ~f64; 3]; width]; height] )
|
||||
|
||||
|
||||
|
||||
|
|
@ -16,19 +16,3 @@ export {
|
|||
let int-max = λ{ a:ℤ~machine.Int64; b:ℤ~machine.Int64; } ↦ if( int-gt a b ) { a; } else { b; };
|
||||
};
|
||||
|
||||
|
||||
/* syntax ambiguity */
|
||||
|
||||
let f'0 = λx:A -> B ↦ { ... };
|
||||
|
||||
/* could be interpreted as .. */
|
||||
let f'1 = λ{x: A -> B} ↦ {};
|
||||
/* ..or.. */
|
||||
let f'2 = λx:A ↦ B:{};
|
||||
|
||||
|
||||
do {
|
||||
!a 10;
|
||||
!b 20;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,41 +0,0 @@
|
|||
|
||||
#complexity O(n)
|
||||
let strlen-nullterm =
|
||||
λ str : &[Char~Ascii~machine::Word]
|
||||
~ &<NullTerminatedSeq machine::Word>
|
||||
~ machine::Address
|
||||
~ machine::Word
|
||||
-> ℤ
|
||||
~ ℤ_2^64
|
||||
~ machine::UInt64
|
||||
~ machine::Word
|
||||
{
|
||||
let mut len = 0;
|
||||
while ( @str ) {
|
||||
! len (i+ len 1);
|
||||
! str (i+ str 1);
|
||||
}
|
||||
len;
|
||||
};
|
||||
|
||||
#complexity O(1)
|
||||
let strlen-lenprefix =
|
||||
λ str : &[Char~Ascii~machine::Word]
|
||||
~ &<LenPrefixArray machine::Word>
|
||||
~ &{
|
||||
len : ℤ_2^64
|
||||
~ machine::UInt64
|
||||
~ machine::Word,
|
||||
data : [machine::Word]
|
||||
}
|
||||
~ machine::Address
|
||||
~ machine::Word
|
||||
-> ℤ
|
||||
~ ℤ_2^64
|
||||
~ machine::UInt64
|
||||
~ machine::Word
|
||||
{
|
||||
str.len
|
||||
};
|
||||
|
||||
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
|
||||
type Vec = ΛT ↦ Struct {
|
||||
len : ℤ_2^64 ~ machine.UInt64 ~ machine.Word ;
|
||||
capacity : ℤ_2^64 ~ machine.UInt64 ~ machine.Word ;
|
||||
data : <RefMut T> ~ machine.Address ~ machine.UInt64 ~ machine.Word ;
|
||||
};
|
||||
|
||||
let yellow:Color~RGB~Vec3i = {
|
||||
0;
|
||||
220;
|
||||
220;
|
||||
};
|
||||
|
||||
let fn = λx:ℤ ↦ ℤ:{
|
||||
3;
|
||||
};
|
||||
|
||||
let swap = λ{x;y;}:{T;T;} ↦ ℤ:{x;y;}
|
||||
|
||||
let n : ℤ
|
||||
~ℤ_2^64
|
||||
~machine.UInt64
|
||||
~machine.Word
|
||||
=
|
||||
ℤ
|
||||
~<PosInt 16 BigEndian>
|
||||
~<Seq <Digit 16>
|
||||
~ Char >
|
||||
: CF03;
|
||||
|
||||
λ{} -> {x y} : <Vec2 ℤ>
|
||||
↦ {
|
||||
10;
|
||||
5;
|
||||
}
|
||||
|
||||
let Vec.new = ΛT ↦ λ{} ↦ self:<Vec T>{
|
||||
let sizeofT = 1;
|
||||
!self <Vec T>{
|
||||
|
||||
};
|
||||
|
||||
!self.len 0;
|
||||
!self.capacity 10;
|
||||
!self.data malloc (i* self.capacity sizeofT);
|
||||
};
|
||||
|
||||
let Vec.drop = ΛT ↦ λself:<Vec T> ↦ {
|
||||
mfree self.data;
|
||||
};
|
||||
|
||||
let vec-get =
|
||||
Λ T
|
||||
↦ λ vec: <Vec T>
|
||||
↦ λ idx: ℤ_2^64 ~ machine.UInt64 ~ machine.Word
|
||||
↦ T {
|
||||
if( int-lt idx vec.len ) {
|
||||
let j = 0;
|
||||
let sizeofT = 1; /* todo: <sizeof T> */
|
||||
|
||||
while( int-lt j sizeofT ) {
|
||||
@ (i+ vec.data
|
||||
(i+ (i* idx sizeofT) j));
|
||||
! j (i+ j 1);
|
||||
};
|
||||
} else {
|
||||
print-nullterm 'o''u''t'' ''o''f'' ''b''o''u''n''d''s''\n''\0'
|
||||
};
|
||||
};
|
||||
|
||||
|
|
@ -1,244 +0,0 @@
|
|||
/**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
|
||||
* Brief Syntax Definition *
|
||||
* of the functional language kernel LT-core *
|
||||
* (please suggest a better name) *
|
||||
**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
|
||||
* (Placeholders are written in CAPS-LOCK) *
|
||||
**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
|
||||
*
|
||||
*
|
||||
* Type-Application
|
||||
* ------------------
|
||||
* specializes a generic symbol
|
||||
* ``
|
||||
* <GENERIC-SYMBOL-NAME TYPE-ARG>
|
||||
* ``
|
||||
*
|
||||
* Type-Abstraction
|
||||
* ------------------
|
||||
* creates a generic symbol with a type-variable and optional trait bounds
|
||||
* ``
|
||||
* let GENERIC-SYMBOL-NAME = Λ TYPE-ARG-NAME : TYPE-ARG-BOUNDS . VAL-EXPR ;
|
||||
* ``
|
||||
*
|
||||
* Term-Application
|
||||
* ------------------
|
||||
* calculates result from applying arguments to a function
|
||||
* with prefix-notation and left-associative `(` `)` parens.
|
||||
* ``
|
||||
* FUNCTION-NAME ARG-EXPR
|
||||
* ``
|
||||
*
|
||||
* Term-Abstraction
|
||||
* ------------------
|
||||
* binds a function definition to a symbol
|
||||
* ``
|
||||
* let SYMBOL-NAME = λ ARG-BINDING -> RESULT-BINDING ↦ RESULT-EXPR ;
|
||||
* ``
|
||||
*
|
||||
* Argument-Binding-Block
|
||||
* ------------------------
|
||||
* binds variable names to function arguments
|
||||
* ``
|
||||
* λ {
|
||||
* ARG-NAME-1 : ARG-TYPE-1 ;
|
||||
* ARG-NAME-2 : ARG-TYPE-2 ;
|
||||
* ... ;
|
||||
* ARG-NAME-N : ARG-TYPE-N ;
|
||||
* }
|
||||
* ``
|
||||
*
|
||||
* Result-Binding-Block
|
||||
* ----------------------
|
||||
* binds variable names to function result
|
||||
* ``
|
||||
* -> {
|
||||
* RESULT-NAME-1 : RESULT-TYPE-1 ;
|
||||
* RESULT-NAME-2 : RESULT-TYPE-2 ;
|
||||
* ...
|
||||
* RESULT-NAME-N : RESULT-TYPE-N ;
|
||||
* }
|
||||
* ``
|
||||
*
|
||||
* Construction-Block
|
||||
* --------------------
|
||||
* builds up result value of the function
|
||||
* by sequentially pushing values to the stack
|
||||
* ``
|
||||
* ↦ {
|
||||
* VAL-EXPR-N ;
|
||||
* ...
|
||||
* VAL-EXPR-2 ;
|
||||
* VAL-EXPR-1 ;
|
||||
* }
|
||||
* ``
|
||||
*
|
||||
* Symbol visibility
|
||||
* -------------------
|
||||
* Symbols defined through `let` are local
|
||||
* to the scope of the block they are contained in,
|
||||
* but can be made visible in the parent block with `export`.
|
||||
*
|
||||
* ``
|
||||
* {
|
||||
* export { let x = 5; };
|
||||
* x;
|
||||
* }
|
||||
* ``
|
||||
*
|
||||
* Explicit Dataflow
|
||||
* -------------------
|
||||
* write to memory referenced a symbol or expression
|
||||
* ``
|
||||
* ! REF-EXPR VAL-EXPR ;
|
||||
* ``
|
||||
* where
|
||||
* - `REF-EXPR` is an expression of type &T
|
||||
* - `VAL-EXPR` is of type T
|
||||
*
|
||||
**~<<~>>~<<~>>>~<<~>>~<<<~>>>~<<~>>~<<<~>>>~<<~>>~<<<~>>~<<~>>**
|
||||
*/
|
||||
|
||||
|
||||
/* Results of a function can be defined either by construction blocks
|
||||
* or by statement blocks that write variables bound to the result.
|
||||
* The following function definitions of dup'n|n∈ℕ are equivalent:
|
||||
*/
|
||||
let dup'0 = λx ↦ { x; x; };
|
||||
let dup'1 = ΛT . λx:T -> { _:T; _:T; } ↦ { x; x; };
|
||||
let dup'2 = ΛT . λx:T -> { a:T; b:T; } ↦ { !a x; !b x; };
|
||||
|
||||
/* note that construction blocks build up a stack, i.e.
|
||||
* the topmost element / the first element of a structure
|
||||
* is at the last position (like expressions in postfix).
|
||||
*/
|
||||
let swap'0 = ΛT . λ{ x:T; y:T; } ↦ { x; y; };
|
||||
let swap'1 = ΛT . λ{ x:T; y:T; } -> { yo:T; xo:T } ↦ { !yo x; !xo y; };
|
||||
|
||||
/* binding blocks can be curried
|
||||
*/
|
||||
let swap'2 = ΛT . λx:T ↦ λy:T ↦ { x; y; };
|
||||
|
||||
/* Type-Annotations are possible in many places.
|
||||
* With an annotation of a function-type, the types
|
||||
* of its argument variables can be deduced.
|
||||
*/
|
||||
let swap'3 : { T; T; } -> { T; T; } = ΛT . λ{ x y } ↦ { x; y; };
|
||||
|
||||
/*
|
||||
* T.F.A.E.:
|
||||
*/
|
||||
let fun'1 : {A, B} -> C = λ{a b} ↦ { ... } ;
|
||||
let fun'2 : A -> B -> C = λ{a b} ↦ { ... } ;
|
||||
let fun'3 = λ{a: A; b: B;} ↦ C: { ... };
|
||||
let fun'4 = λ{a: A} ↦ λ{b: B} ↦ C: { ... };
|
||||
|
||||
/* Argument-Bindings with a structure-type will
|
||||
* result in further (localized) variable bindings
|
||||
* according to the struct-type definition.
|
||||
*/
|
||||
let vec2.magnitude'0 = λ{ x:ℝ; y: ℝ; } ↦ sqrt (+ (* x x) (* y y)) ;
|
||||
let vec2.magnitude'1 = λa:{ x:ℝ; y:ℝ; } ↦ sqrt (+ (* a.x a.x) (* a.y a.y)) ;
|
||||
|
||||
|
||||
|
||||
/* And now more advanced stuff...
|
||||
*/
|
||||
let Iterator = ΛItem . trait Self {
|
||||
next : &!Self -> <Option Item> ;
|
||||
};
|
||||
|
||||
trait Field F {
|
||||
#[infix] + : F -> F -> F ;
|
||||
#[infix] - : F -> F -> F ;
|
||||
#[infix] * : F -> F -> F ;
|
||||
#[infix] / : F -> F -> F ;
|
||||
};
|
||||
|
||||
impl Field for ℝ ~ machine.Float64 {
|
||||
let + = machine.Float64.add ;
|
||||
let - = machine.Float64.sub ;
|
||||
let * = machine.Float64.mul ;
|
||||
let / = machine.Float64.div ;
|
||||
}
|
||||
|
||||
impl Field for ℤ_2^64 ~ machine.UInt64 {
|
||||
let + = λ{a b} ↦ machine.UInt64.add a b ;
|
||||
let - = λ{a b} ↦ machine.UInt64.sub a b ;
|
||||
let * = λ{a b} ↦ machine.UInt64.mul a b ;
|
||||
let / = λ{a b} ↦ machine.UInt64.div a b ;
|
||||
};
|
||||
|
||||
impl ℤ_2^64 ~ machine.UInt64 {
|
||||
let % = machine.UInt64.rem ;
|
||||
}
|
||||
|
||||
let <square F:Field> : F -> F = λ x : F ↦ F:{x * x};
|
||||
|
||||
|
||||
|
||||
let SeqIter = ΛT . type { seq: &[T]; idx: ℤ; };
|
||||
let SeqIterMut = ΛT . type { seq: &![T]; idx: ℤ; };
|
||||
|
||||
impl Iterator for <SeqIter T> {
|
||||
let next = λ self: &!Self ↦ {
|
||||
self.seq.get self.idx;
|
||||
!self.idx (self.idx + 1);
|
||||
};
|
||||
};
|
||||
|
||||
/* finds the index of the first item in the sequence
|
||||
* which satisfies the given predicate.
|
||||
*/
|
||||
let seq.position = ΛT . λ{ seq: &[T]; pred: T -> Bool; } -> ℤ ↦ {
|
||||
let mut idx : ℤ_2^64 ~ machine.UInt64 = 0;
|
||||
while( bit-and
|
||||
(ℤ.lt idx seq.len)
|
||||
(not (pred (seq.get idx)))
|
||||
) {
|
||||
!idx (+ idx 1);
|
||||
}
|
||||
idx;
|
||||
};
|
||||
|
||||
let iter-get-position = ΛT . λ iter: &<Iterator T> ~ &<SeqIter T> ↦ iter.idx ;
|
||||
|
||||
|
||||
|
||||
#[isomorphism]
|
||||
let morph-fractpos-point2scale =
|
||||
λ x : ℝ
|
||||
~ <FractPosInt 10 LittleEndian>
|
||||
~ [ <Digit 10>+'.' ~ Char ]
|
||||
~ <Vec Char>
|
||||
-> ℝ
|
||||
~ <FractPosInt 10 LittleEndian>
|
||||
~ {
|
||||
digits: [<Digit 10>~Char] ~ <Vec Char> ;
|
||||
scale: ℤ ~ ℤ_2^64 ~ machine.UInt64 ;
|
||||
}
|
||||
↦ {
|
||||
!scale (digits.position λc ↦ (eq c '.'));
|
||||
!digits (digits.filter λc ↦ (not (eq c '.')));
|
||||
}
|
||||
;
|
||||
|
||||
#[isomorphism]
|
||||
let morph-fractpos2float =
|
||||
Λ Radix : ℕ
|
||||
.λ x : ℝ
|
||||
~ <FractPosInt Radix BigEndian>
|
||||
~ {
|
||||
digits: [<Digit Radix>~Char] ~ <Vec Char> ;
|
||||
scale: ℤ ;
|
||||
}
|
||||
-> ℝ
|
||||
~ machine.Float64
|
||||
↦ {
|
||||
machine.Float64.div
|
||||
((digits as ℝ~ℕ~<PosInt Radix BigEndian>) as ℝ~machine.Float64)
|
||||
((ℤ.pow Radix scale) as machine.Float64)
|
||||
;
|
||||
}
|
||||
;
|
||||
|
||||
2
main.lt
2
main.lt
|
|
@ -26,7 +26,7 @@
|
|||
print-nullterm
|
||||
(fmt-vec3i green-u8rgb)
|
||||
' ''+'' '
|
||||
(fmt-vec3i blue-u8rgb)
|
||||
(fmt-vec3i blue-u8rgb)
|
||||
' ''='' '
|
||||
(fmt-vec3i (vec3i-add green-u8rgb blue-u8rgb))
|
||||
'\n''\0';
|
||||
|
|
|
|||
|
|
@ -1,314 +0,0 @@
|
|||
Mit der Motivation, auf generische Art Farbräume und deren
|
||||
Repräsentationen zu definieren, nehmen wir als erstes Beispiel das HSV
|
||||
Modell. Der Hue-wert wird über einen Winkel dargestellt. Die
|
||||
einfachste Variante hier wäre, diesen Winkel als eine Variable vom Typ
|
||||
'float' zu implementieren.
|
||||
|
||||
```c++
|
||||
float angle = 28.0; // this is an angle represented in degrees
|
||||
```
|
||||
|
||||
Da Winkel aber gerne in unterschiedlichsten Einheiten ausgedrückt
|
||||
werden wie Grad, Umdrehungen, Bogenmaß, etc.. muss der Programmierer
|
||||
achtgeben, hier nicht diese Einheiten zu vermischen und gegebenenfalls
|
||||
je nach Kontext mit Bibliotheksfunktionen / Nutzereingaben /
|
||||
Dateiformaten eine korrekte Umrechnung definieren.
|
||||
|
||||
```c++
|
||||
#include <cmath>
|
||||
|
||||
// remember to perform conversion from degrees to radians!!!
|
||||
std::sin( 6.283 * angle / 360.0 );
|
||||
```
|
||||
|
||||
Um dieses Problem zu beheben, könnte man in Sprachen mit 'flachem'
|
||||
Typsystem wie C/C++ einen *Wrapper-Typ* erstellen. Dies ist ein gängiges
|
||||
Pattern um diesen und andere ähnliche Sachverhalte zu modellieren, was
|
||||
allerdings oft viel Boilerplatecode bedeutet, welcher daher in vielen
|
||||
solcher Libraries durch Macros generiert wird.
|
||||
|
||||
```c++
|
||||
struct Degrees {
|
||||
float value;
|
||||
|
||||
/* need to overload all arithmetic operators for the new
|
||||
* Degree type.. much boilerplate
|
||||
*/
|
||||
friend Degrees operator+ ( Degrees a, Degrees b ) {
|
||||
return Degrees{ a.value + b.value };
|
||||
}
|
||||
|
||||
/* define type conversions */
|
||||
|
||||
operator Turns() {
|
||||
return Turns{ value / 360.0 };
|
||||
}
|
||||
operator Radians() {
|
||||
Turns turns = *this;
|
||||
Radians rad = turns;
|
||||
return rad;
|
||||
}
|
||||
};
|
||||
|
||||
struct Turns {
|
||||
float value;
|
||||
|
||||
/* overload all arithmetic operators, much boilerplate
|
||||
...
|
||||
*/
|
||||
|
||||
/* type conversions */
|
||||
|
||||
operator Radians() {
|
||||
return Radians{ 6.283 * value };
|
||||
}
|
||||
operator Degrees() {
|
||||
return std::sin()
|
||||
}
|
||||
};
|
||||
|
||||
struct Radians {
|
||||
float value;
|
||||
|
||||
operator Turns() {
|
||||
return Turns{ value / 6.283 };
|
||||
}
|
||||
|
||||
/* overload all operators, much boilerplate
|
||||
...
|
||||
*/
|
||||
}
|
||||
|
||||
/* overload `sin` function
|
||||
* to accept wrapped angle types
|
||||
*/
|
||||
float sin( Radians angle_rad ) {
|
||||
return std::sin( angle_rad.value );
|
||||
}
|
||||
float sin( Turns angle_turns ) {
|
||||
Radians angle_rad = angle_turns;
|
||||
return sin( angle_rad );
|
||||
}
|
||||
float sin( Degrees angle_deg ) {
|
||||
Radians angle_rad = angle_deg;
|
||||
return sin( angle_rad );
|
||||
}
|
||||
```
|
||||
|
||||
Soweit kann nun ausgeschlossen werden, dass Einheiten verwechselt
|
||||
werden. Diese Winkel, welche zunächst reele Zahlen sind, können aber
|
||||
auch wieder auf unterschiedliche weise repräsentiert werden: Als
|
||||
Fließkommazahl oder als lineare Abbildung in einen Ganzzahlraum
|
||||
(z.B. normierte reele Zahlen dargestellt als 8-bit Integer mit dem
|
||||
Mapping 0.0 => 0 und 0.99 => 255), jeweils mit verschiedenen
|
||||
Auflösungen. Dafür würde man nun einen Typ-parameter einführen, welcher
|
||||
die zugrundeliegende Zahlenrepräsentation bestimmt. Durch concepts bzw
|
||||
traits können die benötigten arithmetischen Operationen auf dem
|
||||
Zahlentyp statisch abgesichert werden.
|
||||
|
||||
```c++
|
||||
template< typename T >
|
||||
struct Degrees {
|
||||
T value;
|
||||
//...
|
||||
};
|
||||
|
||||
template< typename T >
|
||||
struct Turns {
|
||||
T value;
|
||||
//...
|
||||
};
|
||||
|
||||
template< typename T >
|
||||
struct Radians {
|
||||
T value;
|
||||
//...
|
||||
};
|
||||
```
|
||||
|
||||
Dieser weitere Parameter multipliziert allerdings die möglichen
|
||||
Transformationen zwischen den vielen verschiedenen möglichen
|
||||
Angle-Typen. Außerdem pflanzt sich dieser Typparameter weiter in
|
||||
unsere HSV Abstraktion fort, obwohl er dort garnicht von Bedeutung
|
||||
ist, da hier eigentlich die Semantik des HSV Modells nur mit dem
|
||||
abstrakten Interface des 'Angle' traits definiert werden kann.
|
||||
(Der Typparameter ließe sich theoretisch durch virtual dispatch
|
||||
vermeiden, tradeoff gegen runtime overhead).
|
||||
|
||||
```c++
|
||||
template < typename Angle, typename UnitInterval >
|
||||
struct HSV {
|
||||
Angle hue;
|
||||
UnitInterval saturation;
|
||||
UnitInterval value;
|
||||
};
|
||||
```
|
||||
|
||||
```c++
|
||||
HSV<Turns<float>, float> hsv;
|
||||
```
|
||||
|
||||
In Rust sieht es ähnlich aus (gekürzt aus dem `angular-units` crate):
|
||||
|
||||
```rust
|
||||
pub struct Degrees<T>(pub T);
|
||||
pub struct Radians<T>(pub T);
|
||||
pub struct Turns<T>(pub T);
|
||||
pub struct ArcMinutes<T>(pub T);
|
||||
pub struct ArcSeconds<T>(pub T);
|
||||
|
||||
pub trait Angle: Clone + FromAngle<Self> + PartialEq + PartialOrd + num::Zero
|
||||
{
|
||||
/// Internal type storing the angle value.
|
||||
type Scalar: Float;
|
||||
|
||||
fn new(value: Self::Scalar) -> Self;
|
||||
|
||||
/// The length of a full rotation.
|
||||
fn period() -> Self::Scalar;
|
||||
|
||||
fn scalar(&self) -> Self::Scalar;
|
||||
fn set_scalar(&mut self, value: Self::Scalar);
|
||||
|
||||
fn normalize(self) -> Self;
|
||||
fn sin(self) -> Self::Scalar;
|
||||
}
|
||||
|
||||
/// Construct `Self` from an angle.
|
||||
///
|
||||
/// Analogous to the traits in the standard library,
|
||||
/// FromAngle and IntoAngle provide a way to convert between angle
|
||||
/// types and to mix various angle types in a single operation.
|
||||
pub trait FromAngle<T>
|
||||
where T: Angle
|
||||
{
|
||||
/// Construct `Self` by converting a `T`.
|
||||
fn from_angle(from: T) -> Self;
|
||||
}
|
||||
|
||||
/* and implement all required boilerplate via macros
|
||||
*/
|
||||
|
||||
macro_rules! impl_angle {
|
||||
($Struct: ident, $period: expr) => {
|
||||
// ...
|
||||
|
||||
impl<U, T> Add<U> for $Struct<T>
|
||||
where T: Float + Add<T, Output=T>,
|
||||
U: IntoAngle<$Struct<T>, OutputScalar=T>
|
||||
{
|
||||
type Output=$Struct<T>;
|
||||
fn add(self, rhs: U) -> $Struct<T> {
|
||||
$Struct(self.0 + rhs.into_angle().0)
|
||||
}
|
||||
}
|
||||
|
||||
// ...
|
||||
// repeat for all operations
|
||||
}
|
||||
}
|
||||
|
||||
impl_angle!(Degrees, 360.0);
|
||||
impl_angle!(Radians, 2.0*consts::PI);
|
||||
impl_angle!(Turns, 1.0);
|
||||
```
|
||||
|
||||
Ladder-Types kehren diesen inneren Repräsentationstyp, welcher in der
|
||||
C++ und Rust Variante durch generische Typparameter wieder nach außen
|
||||
getragen werden muss, auf einer der metastrukturellen Ebene nach außen.
|
||||
Da die 'Represented-As' Relation schon nativ durch das Typsystem erfasst
|
||||
werden kann, müssen weder weitere Typvariablen eingeführt werden noch
|
||||
müssen komplexe macros zur generierung von Boilerplate eingesetzt
|
||||
werden, während die typisierung immernoch statisch bleibt.
|
||||
|
||||
Mit Ladder-Types ist es möglich, Funktionen auf dem Abstrakten Typ
|
||||
'Angle' zu definieren, während man auf einer konkreten
|
||||
Repräsentationsform, gegeben durch den Ladder-Type arbeitet (in diesem
|
||||
Fall Float64). Gleichzeitig werden Funktionen zwischen gleichwertigen
|
||||
Repräsentationen eines abstrakten Typs als Isomorphismus gekennzeichnet
|
||||
und dürfen daher vom Compiler als implizite Konvertierung eingesetzt
|
||||
werden, um Ausdrücke in denen mehrere Repräsentationen des gleichen
|
||||
abstrakten Typs gemischt werden, ohne "typcast-noise" zu ermöglichen.
|
||||
|
||||
Eine Funktion wie 'sin', welche für alle Winkeltypen gelten soll, aber
|
||||
nur für eine konkrete Repräsentation wie Angle~Radians~.. definiert ist,
|
||||
kann durch das einsetzen implizieter Konvertierungen durch alle anderen
|
||||
Repräsentationen auch genutzt werden. Ein Polymorphismus über
|
||||
verschiedene Repräsentationsformen ist nun ohne generische Typparameter
|
||||
und Macros möglich.
|
||||
|
||||
```
|
||||
#[isomorphism]
|
||||
let angle-degree-to-turns =
|
||||
λ a : Angle
|
||||
~ Degrees
|
||||
~ ℝ_[0,360)
|
||||
~ machine.Float64
|
||||
-> Angle
|
||||
~ Turns
|
||||
~ ℝ_[0,1)
|
||||
~ machine.Float64
|
||||
↦ {
|
||||
float64div a 360.0
|
||||
};
|
||||
|
||||
#[isomorphism]
|
||||
let angle-turns-to-radians =
|
||||
λ a : Angle
|
||||
~ Turns
|
||||
~ ℝ_[0,1)
|
||||
~ machine.Float64
|
||||
-> Angle
|
||||
~ Radians
|
||||
~ ℝ_[0,pi2)
|
||||
~ machine.Float64
|
||||
↦ {
|
||||
float64mul a 6.283
|
||||
};
|
||||
|
||||
let sin =
|
||||
λ a : Angle
|
||||
~ Radians
|
||||
~ ℝ_[0,2π)
|
||||
~ machine.Float64
|
||||
-> ℝ_[-1,1]
|
||||
~ machine.Float64
|
||||
↦ {
|
||||
// original sin implementation in radians as float
|
||||
};
|
||||
|
||||
// now it is possible to call `sin` which is
|
||||
// implemented on radians with a value of degrees,
|
||||
// because conversions can be inserted implicitly.
|
||||
|
||||
let some_angle : Angle ~ Degrees = 120;
|
||||
let y : ℝ ~ machine.Float64 = sin some_angle;
|
||||
|
||||
// the previous line will be expanded to:
|
||||
let y : ℝ ~ machine.Float64 = sin (angle-turns-to-radians (angle-degree-to-turns some_angle));
|
||||
|
||||
```
|
||||
|
||||
Auf die gleiche Weise könnten jetzt auch Konvertierungen zwischen Int
|
||||
und Float repräsentationen definiert werden:
|
||||
|
||||
```
|
||||
#[isomorphism]
|
||||
let normalized-float-from-uint =
|
||||
λ value : ℝ_[0,1) ~ ℤ_256 ~ machine.UInt8
|
||||
-> ℝ_[0,1) ~ machine.Float64
|
||||
↦ {
|
||||
float64div (value as machine.Float64) 256.0
|
||||
};
|
||||
|
||||
let half_turn : Angle ~ Turns ~ ℝ_[0,1) ~ ℤ_256 ~ machine.UInt8 = 128;
|
||||
let y = sin half_turn;
|
||||
|
||||
// last line will be expanded to:
|
||||
let y = sin (angle-turns-to-radians (normalized-float-from-uint half_turn));
|
||||
|
||||
```
|
||||
|
||||
Weiterführend könnten die Konvertierungsfunktionen auch mit
|
||||
Komplexitätsannotationen versehen werden, welche bei der Suche eines
|
||||
optimalen Konvertierungspfades als Gewichte herangezogen wereden können.
|
||||
18
src/main.rs
18
src/main.rs
|
|
@ -54,21 +54,21 @@ fn print_diagnostic(
|
|||
// display the source line
|
||||
for (j,ll) in last_lines.iter() {
|
||||
print!("{}\t{}{}",
|
||||
format!("{}",j).to_string().bright_black(),
|
||||
"|".bright_black().bold(),
|
||||
ll.bright_white());
|
||||
format!("{}",j).to_string().bright_white(),
|
||||
"|".yellow().bold(),
|
||||
ll.white());
|
||||
}
|
||||
|
||||
print!("\t{}", "|".bright_magenta());
|
||||
print!("\t{}", "|".yellow().bold());
|
||||
for _ in 0..column_begin { print!("{}", ".".magenta().bold()); }
|
||||
for _ in column_begin..column_end { print!("{}", "^".magenta().bold()); }
|
||||
print!("\n");
|
||||
|
||||
print!("{} [{}-{}]: {}\n", "error".bright_red(), column_begin, column_end, message.white());
|
||||
print!("{} [{}-{}]: {}\n", "error".bright_red(), column_begin, column_end, message);
|
||||
}
|
||||
else if next_lines > 0 {
|
||||
next_lines -= 1;
|
||||
print!("{}\t{}{}", format!("{}", i+1).to_string().bright_black(), "|".bright_black().bold(), l.bright_white());
|
||||
print!("{}:\t{}{}", format!("{}", i+1).to_string().bright_white(), "|".yellow().bold(), l.white());
|
||||
}
|
||||
|
||||
line_region.begin = line_region.end;
|
||||
|
|
@ -126,11 +126,7 @@ fn main() {
|
|||
.into_asm(&path);
|
||||
|
||||
for (region, message) in diagnostics {
|
||||
print_diagnostic(
|
||||
path.as_str(),
|
||||
region,
|
||||
format!("{}", message)
|
||||
);
|
||||
print_diagnostic(path.as_str(), region, message);
|
||||
}
|
||||
|
||||
eprintln!("{} {}", "Compiled".green(), path.bold());
|
||||
|
|
|
|||
Loading…
Reference in a new issue