import { $, Term, _, _l, cnst, g, id, n, pipe, _r as ref } from './core';
import { EQ, GT, LT } from './ord';
import { False, True, iif } from './bool';

n('num');

export const Zero = g('Zero', _l(z => _l(_n => z)));

export const Succ = g('Succ', _l(p => _l(_z => _l(n => n._(p)))));

export const ifz = g('ifz', _l(n => _l(t => _l(f => n._(t)._(cnst._(f))))));

export const succ = g('succ', Succ);

export const pred = g('pred', _l(n => n._(Zero)._(id)));

export const cmp = g('cmp', _l(l => _l(r => l._(r._(EQ)._(cnst._(LT)))._(pipe._(r._(GT))._(ref('num', 'cmp'))))));

export const lt = g('lt', _l(l => _l(r => r._(False)._(l._(cnst._(True))._(ref('num', 'lt'))))));

export const le = g('le', _l(l => _l(r => l._(True)._(r._(cnst._(False))._(ref('num', 'ge'))))));

export const eq = g('eq', _l(l => _l(r => l._(r._(True)._(cnst._(False)))._(r._(cnst._(False))._(ref('num', 'eq'))))));

export const ge = g('ge', _l(l => _l(r => r._(True)._(l._(cnst._(False))._(ref('num', 'ge'))))));

export const gt = g('gt', _l(l => _l(r => l._(False)._(r._(cnst._(True))._(lt)))));

export const even = g('even', _l(n => n._(True)._(ref('num', 'odd'))));

export const odd = g('odd', _l(n => n._(False)._(ref('num', 'even'))));

export const sum = g('sum', _l(l => _l(r => r._(l)._(ref('num', 'sum')._(Succ._(l))))));

export const sub = g('sub', _l(l => _l(r => r._(l)._(l._(cnst._(Zero))._(ref('num', 'sub'))))));

export const mul = g('mul', _l(l => _l(r => l._(Zero)._(_l(pl => sum._(r)._(ref('num', 'mul')._(pl)._(r)))))));

export const div = g('div', _l(l => _l(r => iif._(lt._(l)._(r))._(Zero)._(succ._(ref('num', 'div')._(sub._(l)._(r))._(r))))));

export const mod = g('mod', _l(l => _l(r => iif._(lt._(l)._(r))._(l)._(ref('num', 'mod')._(sub._(l)._(r))._(r)))));

export const fromNumber: (n: number) => Term = n => !n ? Zero : Succ._(_(() => fromNumber(n - 1)));

export const toNumber: (n: Term) => number = n => $(n._(_(0))._(_l(p => _(({ p }) => _(1 + toNumber(p))))));