lt-core/ltcore-intro-examples
2024-06-11 15:17:58 +02:00

244 lines
6.2 KiB
Text
Raw Permalink Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
* 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)
;
}
;