|
|
|
@ -1,9 +1,9 @@ |
|
|
|
import { $, Term, _, cnst, d, g, id, l, m, pipe, r, undef } from './core'; |
|
|
|
import { $, Term, cnst, _, g, id, l, n, pipe, r, undef } from './core'; |
|
|
|
import { EQ, GT, LT, eq as eqc } from './ord'; |
|
|
|
import { EQ, GT, LT, eq as eqc } from './ord'; |
|
|
|
import { False, True, and, iif, or } from './bool'; |
|
|
|
import { False, True, and, iif, or } from './bool'; |
|
|
|
import { Zero, succ } from './num'; |
|
|
|
import { Zero, succ } from './num'; |
|
|
|
|
|
|
|
|
|
|
|
m('list'); |
|
|
|
n('list'); |
|
|
|
|
|
|
|
|
|
|
|
export const Nil = g('Nil', l('z', l('_', 'z'))); |
|
|
|
export const Nil = g('Nil', l('z', l('_', 'z'))); |
|
|
|
|
|
|
|
|
|
|
|
@ -11,62 +11,62 @@ export const Cons = g('Cons', l('x', l('xs', l('_', l('f', r('f')._('x')._('xs') |
|
|
|
|
|
|
|
|
|
|
|
export const cons = g('cons', Cons); |
|
|
|
export const cons = g('cons', Cons); |
|
|
|
|
|
|
|
|
|
|
|
export const snoc = g('snoc', l('xs', l('x', r('xs')._(cons._('x')._(Nil))._(l('y', l('ys', cons._('y')._(r('list::snoc')._('ys')._('x')))))))); |
|
|
|
export const snoc = g('snoc', l('xs', l('x', r('xs')._(cons._('x')._(Nil))._(l('y', l('ys', cons._('y')._(r('list', 'snoc')._('ys')._('x')))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const nul = g('nul', l('xs', r('xs')._(True)._(cnst._(cnst._(False))))); |
|
|
|
export const nul = g('nul', l('xs', r('xs')._(True)._(cnst._(cnst._(False))))); |
|
|
|
|
|
|
|
|
|
|
|
export const len = g('len', l('xs', r('xs')._(Zero)._(cnst._(pipe._(succ)._(r('list::len')))))); |
|
|
|
export const len = g('len', l('xs', r('xs')._(Zero)._(cnst._(pipe._(succ)._(r('list', 'len')))))); |
|
|
|
|
|
|
|
|
|
|
|
export const singleton = g('singleton', l('x', cons._('x')._(Nil))); |
|
|
|
export const singleton = g('singleton', l('x', cons._('x')._(Nil))); |
|
|
|
|
|
|
|
|
|
|
|
export const append = g('append', l('l', l('r', r('l')._('r')._(l('x', l('xs', cons._('x')._(r('list::append')._('xs')._('r')))))))); |
|
|
|
export const append = g('append', l('l', l('r', r('l')._('r')._(l('x', l('xs', cons._('x')._(r('list', 'append')._('xs')._('r')))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const concat = g('concat', l('ls', r('ls')._(Nil)._(l('x', pipe._(append._('x'))._(r('list::concat')))))); |
|
|
|
export const concat = g('concat', l('ls', r('ls')._(Nil)._(l('x', pipe._(append._('x'))._(r('list', 'concat')))))); |
|
|
|
|
|
|
|
|
|
|
|
export const repeat = g('repeat', l('x', cons._('x')._(r('list::repeat')._('x')))); |
|
|
|
export const repeat = g('repeat', l('x', cons._('x')._(r('list', 'repeat')._('x')))); |
|
|
|
|
|
|
|
|
|
|
|
export const iterate = g('iterate', l('f', l('x', cons._('x')._(r('list::iterate')._('f')._(r('f')._('x')))))); |
|
|
|
export const iterate = g('iterate', l('f', l('x', cons._('x')._(r('list', 'iterate')._('f')._(r('f')._('x')))))); |
|
|
|
|
|
|
|
|
|
|
|
export const head = g('head', l('xs', r('xs')._(undef)._(cnst))); |
|
|
|
export const head = g('head', l('xs', r('xs')._(undef)._(cnst))); |
|
|
|
|
|
|
|
|
|
|
|
export const tail = g('tail', l('xs', r('xs')._(undef)._(cnst._(id)))); |
|
|
|
export const tail = g('tail', l('xs', r('xs')._(undef)._(cnst._(id)))); |
|
|
|
|
|
|
|
|
|
|
|
export const foldl = g('foldl', l('f', l('z', l('xs', r('xs')._('z')._(pipe._(r('list::foldl')._('f'))._(r('f')._('z'))))))); |
|
|
|
export const foldl = g('foldl', l('f', l('z', l('xs', r('xs')._('z')._(pipe._(r('list', 'foldl')._('f'))._(r('f')._('z'))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const foldlz = g('foldlz', l('f', l('xs', r('xs')._(undef)._(foldl._('f'))))); |
|
|
|
export const foldlz = g('foldlz', l('f', l('xs', r('xs')._(undef)._(foldl._('f'))))); |
|
|
|
|
|
|
|
|
|
|
|
export const foldr = g('foldr', l('f', l('z', l('xs', r('xs')._('z')._(l('x', pipe._(r('f')._('x'))._(r('list::foldr')._('f')._('z')))))))); |
|
|
|
export const foldr = g('foldr', l('f', l('z', l('xs', r('xs')._('z')._(l('x', pipe._(r('f')._('x'))._(r('list', 'foldr')._('f')._('z')))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const foldrz = g('foldrz', undef); |
|
|
|
export const foldrz = g('foldrz', undef); |
|
|
|
|
|
|
|
|
|
|
|
export const cmp = g('cmp', l('ecmp', l('l', l('r', r('l')._(r('r')._(EQ)._(cnst._(cnst._(LT))))._(l('lx', l('lxs', r('r')._(GT)._(l('rx', l('rxs', iif._(eqc._(EQ)._(r('ecmp')._('lx')._('rx')))._(r('list::cmp')._('ecmp')._('lxs')._('rxs'))._(r('ecmp')._('lx')._('rx')))))))))))); |
|
|
|
export const cmp = g('cmp', l('ecmp', l('l', l('r', r('l')._(r('r')._(EQ)._(cnst._(cnst._(LT))))._(l('lx', l('lxs', r('r')._(GT)._(l('rx', l('rxs', iif._(eqc._(EQ)._(r('ecmp')._('lx')._('rx')))._(r('list', 'cmp')._('ecmp')._('lxs')._('rxs'))._(r('ecmp')._('lx')._('rx')))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const lt = g('lt', l('ecmp', l('l', l('r', r('r')._(False)._(l('rx', l('rxs', r('l')._(True)._(l('lx', l('lxs', r('ecmp')._('lx')._('rx')._(True)._(r('list::lt')._('ecmp')._('lxs')._('rxs'))._(False))))))))))); |
|
|
|
export const lt = g('lt', l('ecmp', l('l', l('r', r('r')._(False)._(l('rx', l('rxs', r('l')._(True)._(l('lx', l('lxs', r('ecmp')._('lx')._('rx')._(True)._(r('list', 'lt')._('ecmp')._('lxs')._('rxs'))._(False))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const le = g('le', l('ecmp', l('l', l('r', r('l')._(True)._(l('lx', l('lxs', r('r')._(False)._(l('rx', l('rxs', r('ecmp')._('lx')._('rx')._(True)._(r('list::le')._('ecmp')._('lxs')._('rxs'))._(False))))))))))); |
|
|
|
export const le = g('le', l('ecmp', l('l', l('r', r('l')._(True)._(l('lx', l('lxs', r('r')._(False)._(l('rx', l('rxs', r('ecmp')._('lx')._('rx')._(True)._(r('list', 'le')._('ecmp')._('lxs')._('rxs'))._(False))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const eq = g('eq', l('eeq', l('l', l('r', r('l')._(r('r')._(True)._(cnst._(cnst._(False))))._(l('lx', l('lxs', r('r')._(False)._(l('rx', l('rxs', and._(r('eeq')._('lx')._('rx'))._(r('list::eq')._('eeq')._('lxs')._('rxs')))))))))))); |
|
|
|
export const eq = g('eq', l('eeq', l('l', l('r', r('l')._(r('r')._(True)._(cnst._(cnst._(False))))._(l('lx', l('lxs', r('r')._(False)._(l('rx', l('rxs', and._(r('eeq')._('lx')._('rx'))._(r('list', 'eq')._('eeq')._('lxs')._('rxs')))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const ge = g('ge', l('ecmp', l('l', l('r', r('r')._(True)._(l('rx', l('rxs', r('l')._(False)._(l('lx', l('lxs', r('ecmp')._('lx')._('rx')._(False)._(r('list::ge')._('ecmp')._('lxs')._('rxs'))._(True))))))))))); |
|
|
|
export const ge = g('ge', l('ecmp', l('l', l('r', r('r')._(True)._(l('rx', l('rxs', r('l')._(False)._(l('lx', l('lxs', r('ecmp')._('lx')._('rx')._(False)._(r('list', 'ge')._('ecmp')._('lxs')._('rxs'))._(True))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const gt = g('gt', l('ecmp', l('l', l('r', r('l')._(False)._(l('lx', l('lxs', r('r')._(True)._(l('rx', l('rxs', r('ecmp')._('lx')._('rx')._(False)._(r('list::gt')._('ecmp')._('lxs')._('rxs'))._(True))))))))))); |
|
|
|
export const gt = g('gt', l('ecmp', l('l', l('r', r('l')._(False)._(l('lx', l('lxs', r('r')._(True)._(l('rx', l('rxs', r('ecmp')._('lx')._('rx')._(False)._(r('list', 'gt')._('ecmp')._('lxs')._('rxs'))._(True))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const map = g('map', l('f', l('xs', r('xs')._(Nil)._(l('x', pipe._(cons._(r('f')._('x')))._(r('list::map')._('f'))))))); |
|
|
|
export const map = g('map', l('f', l('xs', r('xs')._(Nil)._(l('x', pipe._(cons._(r('f')._('x')))._(r('list', 'map')._('f'))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const filter = g('filter', l('f', l('xs', r('xs')._(Nil)._(l('x', pipe._(iif._(r('f')._('x'))._(cons._('x'))._(id))._(r('list::filter')._('f'))))))); |
|
|
|
export const filter = g('filter', l('f', l('xs', r('xs')._(Nil)._(l('x', pipe._(iif._(r('f')._('x'))._(cons._('x'))._(id))._(r('list', 'filter')._('f'))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const any = g('any', l('f', l('xs', r('xs')._(False)._(l('x', pipe._(or._(r('f')._('x')))._(r('list::any')._('f'))))))); |
|
|
|
export const any = g('any', l('f', l('xs', r('xs')._(False)._(l('x', pipe._(or._(r('f')._('x')))._(r('list', 'any')._('f'))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const all = g('all', l('f', l('xs', r('xs')._(True)._(l('x', pipe._(and._(r('f')._('x')))._(r('list::all')._('f'))))))); |
|
|
|
export const all = g('all', l('f', l('xs', r('xs')._(True)._(l('x', pipe._(and._(r('f')._('x')))._(r('list', 'all')._('f'))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const get = g('get', l('i', l('xs', r('xs')._(undef)._(l('x', r('i')._(cnst._('x'))._('list::get')))))); |
|
|
|
export const get = g('get', l('i', l('xs', r('xs')._(undef)._(l('x', r('i')._(cnst._('x'))._('list', 'get')))))); |
|
|
|
|
|
|
|
|
|
|
|
export const update = g('update', l('f', l('i', l('xs', r('xs')._(undef)._(l('x', l('xs', r('i')._(cons._(r('f')._('x'))._('xs'))._(l('pi', cons._('x')._(r('list::update')._('f')._('pi')._('xs'))))))))))); |
|
|
|
export const update = g('update', l('f', l('i', l('xs', r('xs')._(undef)._(l('x', l('xs', r('i')._(cons._(r('f')._('x'))._('xs'))._(l('pi', cons._('x')._(r('list', 'update')._('f')._('pi')._('xs'))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const set = g('set', pipe._(update)._(cnst)); |
|
|
|
export const set = g('set', pipe._(update)._(cnst)); |
|
|
|
|
|
|
|
|
|
|
|
export const intersperse = g('intersperse', l('v', l('xs', r('xs')._('xs')._(l('x', l('rxs', r('rxs')._('xs')._(cnst._(cnst._(cons._('x')._(cons._('v')._(r('list::intersperse')._('v')._('rxs')))))))))))); |
|
|
|
export const intersperse = g('intersperse', l('v', l('xs', r('xs')._('xs')._(l('x', l('rxs', r('rxs')._('xs')._(cnst._(cnst._(cons._('x')._(cons._('v')._(r('list', 'intersperse')._('v')._('rxs')))))))))))); |
|
|
|
|
|
|
|
|
|
|
|
export const fromArray: (xs: Term[]) => Term = xs => !xs.length ? Nil : Cons._(xs[0])._(d(() => fromArray(xs.slice(1)))); |
|
|
|
export const fromArray: (xs: Term[]) => Term = xs => !xs.length ? Nil : Cons._(xs[0])._(_(() => fromArray(xs.slice(1)))); |
|
|
|
|
|
|
|
|
|
|
|
export const toArray: (xs: Term) => Term[] = xs => $(xs._(_([]))._(l('x', l('xs', d(bs => _([bs['x'], ...toArray(bs['xs'])])))))); |
|
|
|
export const toArray: (xs: Term) => Term[] = xs => $(xs._(_([]))._(l('x', l('xs', _(({ x, xs }) => _([x, ...toArray(xs)])))))); |
|
|
|
|