import { L, P, _ } from './core'; import { GT, LT, Ord } from './ord'; import { Bool, False, True, and } from './bool'; import { Nil, concat, cons } from './list'; import { String, fromString as _s } from './string'; export type Pair = L<(f: L<(f: F) => L<(s: S) => R>>) => R>; export const Pair: L<(f: F) => L<(s: S) => Pair>> = _((f: F) => _((s: S) => _((p: L<(f: F) => L<(s: S) => R>>) => p(f)(s)))); export const fst: L<(p: Pair) => F> = _(p => p(_(f => _(_s => f)))); export const snd: L<(p: Pair) => S> = _(p => p(_(_f => _(s => s)))); export const first: L<(t: L<(f: F) => FR>) => L<(p: Pair) => Pair>> = _((t: L<(f: F) => FR>) => _((p: Pair) => p(_(f => _(s => Pair(t(f))(s)))))); export const second: L<(t: L<(s: S) => SR>) => L<(p: Pair) => Pair>> = _((t: L<(s: S) => SR>) => _((p: Pair) => p(_(f => _(s => Pair(f)(t(s))))))); export const both: L<(tf: L<(f: F) => FR>) => L<(ts: L<(s: S) => SR>) => L<(p: Pair) => Pair>>> = _((tf: L<(f: F) => FR>) => _((ts: L<(s: S) => SR>) => _((p: Pair) => p(_(f => _(s => Pair(tf(f))(ts(s)))))))); export const uncurry: L<(t: L<(f: F) => L<(s: S) => R>>) => L<(p: Pair) => R>> = _((t: L<(f: F) => L<(s: S) => R>>) => _((p: Pair) => p(t))); export const cmp: L<(fcmp: L<(l: F) => L<(r: F) => Ord>>) => L<(scmp: L<(l: S) => L<(r: S) => Ord>>) => L<(l: Pair) => L<(r: Pair) => Ord>>>> = _((fcmp: L<(l: F) => L<(r: F) => Ord>>) => _((scmp: L<(l: S) => L<(r: S) => Ord>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => fcmp(lf)(rf)(LT)(scmp(ls)(rs))(GT))))))))); export const lt: L<(fcmp: L<(l: F) => L<(r: F) => Ord>>) => L<(scmp: L<(l: S) => L<(r: S) => Bool>>) => L<(l: Pair) => L<(r: Pair) => Bool>>>> = _((fcmp: L<(l: F) => L<(r: F) => Ord>>) => _((scmp: L<(l: S) => L<(r: S) => Ord>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => fcmp(lf)(rf)(True)(scmp(ls)(rs)(True)(False)(False))(False))))))))); export const le: L<(fcmp: L<(l: F) => L<(r: F) => Ord>>) => L<(scmp: L<(l: S) => L<(r: S) => Bool>>) => L<(l: Pair) => L<(r: Pair) => Bool>>>> = _((fcmp: L<(l: F) => L<(r: F) => Ord>>) => _((scmp: L<(l: S) => L<(r: S) => Ord>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => fcmp(lf)(rf)(True)(scmp(ls)(rs)(True)(True)(False))(False))))))))); export const eq: L<(feq: L<(l: F) => L<(r: F) => Bool>>) => L<(seq: L<(l: S) => L<(r: S) => Bool>>) => L<(l: Pair) => L<(r: Pair) => Bool>>>> = _((feq: L<(l: F) => L<(r: F) => Bool>>) => _((seq: L<(l: S) => L<(r: S) => Bool>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => and(feq(lf)(rf))(seq(ls)(rs)))))))))); export const ge: L<(fcmp: L<(l: F) => L<(r: F) => Ord>>) => L<(scmp: L<(l: S) => L<(r: S) => Bool>>) => L<(l: Pair) => L<(r: Pair) => Bool>>>> = _((fcmp: L<(l: F) => L<(r: F) => Ord>>) => _((scmp: L<(l: S) => L<(r: S) => Ord>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => fcmp(lf)(rf)(False)(scmp(ls)(rs)(False)(True)(True))(True))))))))); export const gt: L<(fcmp: L<(l: F) => L<(r: F) => Ord>>) => L<(scmp: L<(l: S) => L<(r: S) => Bool>>) => L<(l: Pair) => L<(r: Pair) => Bool>>>> = _((fcmp: L<(l: F) => L<(r: F) => Ord>>) => _((scmp: L<(l: S) => L<(r: S) => Ord>>) => uncurry(_((lf: F) => _((ls: S) => uncurry(_((rf: F) => _((rs: S) => fcmp(lf)(rf)(False)(scmp(ls)(rs)(False)(False)(True))(True))))))))); export const show: L<(fshow: L<(f: F) => String>) => L<(sshow: L<(s: S) => String>) => L<(p: Pair) => String>>> = _((fshow: L<(f: F) => String>) => _((sshow: L<(s: S) => String>) => uncurry(_((f: F) => _((s: S) => concat(cons(_s('('))(cons(fshow(f))(cons(_s(', '))(cons(sshow(s))(cons(_s(')'))(Nil)))))))))));