You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
40 lines
1.3 KiB
40 lines
1.3 KiB
import { Bool, not, True } from './bool';
|
|
import { Lazy, _, id } from './core';
|
|
|
|
export type Num = <T>(z: Lazy<T>) => (n: (p: Lazy<Num>) => Lazy<T>) => Lazy<T>;
|
|
|
|
export const Zero: Lazy<Num>
|
|
= _<Num>(z => _ => z);
|
|
|
|
export const Succ: (p: Lazy<Num>) => Lazy<Num>
|
|
= p => _(_ => n => n(p));
|
|
|
|
export const ifz: <T>(n: Lazy<Num>) => (t: Lazy<T>) => (f: Lazy<T>) => Lazy<T>
|
|
= n => t => f => n.then(n => n(t)(_ => f));
|
|
|
|
export const succ: (n: Lazy<Num>) => Lazy<Num>
|
|
= Succ;
|
|
|
|
export const pred: (n: Lazy<Num>) => Lazy<Num>
|
|
= n => n.then(n => n(Zero)(id));
|
|
|
|
export const even: (n: Lazy<Num>) => Lazy<Bool>
|
|
= n => n.then(n => n(True)(odd));
|
|
|
|
export const odd: (n: Lazy<Num>) => Lazy<Bool>
|
|
= n => not(even(n));
|
|
|
|
export const sum: (l: Lazy<Num>) => (r: Lazy<Num>) => Lazy<Num>
|
|
= l => r => r.then(r => r(l)(sum(Succ(l))));
|
|
|
|
export const sub: (l: Lazy<Num>) => (r: Lazy<Num>) => Lazy<Num>
|
|
= l => r => r.then(r => r(l)(pr => l.then(l => l(Zero)(pl => sub(pl)(pr)))));
|
|
|
|
export const mul: (l: Lazy<Num>) => (r: Lazy<Num>) => Lazy<Num>
|
|
= l => r => l.then(l => l(Zero)(pl => sum(r)(mul(pl)(r))));
|
|
|
|
export const fromNumber: (n: number) => Lazy<Num>
|
|
= n => !n ? Zero : new Lazy(() => Succ(fromNumber(n - 1)).value);
|
|
|
|
export const toNumber: (n: Lazy<Num>) => Lazy<number>
|
|
= n => n.then(n => n(_(0))(p => toNumber(p).then(p => _(1 + p))));
|
|
|