import { $, Term, _, cnst, d, g, id, l, m, pipe, r } from './core';
import { EQ, GT, LT } from './ord';
import { False, True, iif } from './bool';

m('num');

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

export const Succ = g('Succ', l('p', l('_z', l('n', r('n')._('p')))));

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

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

export const pred = g('pred', l('n', r('n')._(Zero)._(id)));

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

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

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

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

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

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

export const even = g('even', l('n', r('n')._(True)._('num::odd')));

export const odd = g('odd', l('n', r('n')._(False)._('num::even')));

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

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

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

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

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

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

export const toNumber: (n: Term) => number = n => $(n._(_(0))._(l('p', d(bs => _(1 + toNumber(bs['p']))))));