lt-core/ltcore-intro-examples

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