lt-core/ltcore-intro-examples

245 lines
6.2 KiB
Text
Raw Permalink Normal View History

2024-06-11 15:17:58 +02:00
/**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
* 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)
;
}
;