wip examples
This commit is contained in:
parent
541702de55
commit
72122bf4fc
12 changed files with 985 additions and 25 deletions
244
ltcore-intro-examples
Normal file
244
ltcore-intro-examples
Normal file
|
@ -0,0 +1,244 @@
|
|||
/**~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~<<~>>~**
|
||||
* 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)
|
||||
;
|
||||
}
|
||||
;
|
||||
|
Loading…
Add table
Add a link
Reference in a new issue