modal/demo.modal

<> (-- ?x) ()
-- ( little endian binary integers )

-- ( constants )
<> zero ((0 ()))
<> one ((1 ()))
<> ten ((0 (1 (0 (1 ())))))

-- ( decimal digit to binary )
<> ((binary 0)) ((0 ()))
<> ((binary 1)) ((1 ()))
<> ((binary 2)) ((0 (1 ())))
<> ((binary 3)) ((1 (1 ())))
<> ((binary 4)) ((0 (0 (1 ()))))
<> ((binary 5)) ((1 (0 (1 ()))))
<> ((binary 6)) ((0 (1 (1 ()))))
<> ((binary 7)) ((1 (1 (1 ()))))
<> ((binary 8)) ((0 (0 (0 (1 ())))))
<> ((binary 9)) ((1 (0 (0 (1 ())))))

-- ( binary to decimal digit )
<> ((decimal ())) (0)
<> ((decimal (0 ()))) (0)
<> ((decimal (1 ()))) (1)
<> ((decimal (0 (1 ())))) (2)
<> ((decimal (1 (1 ())))) (3)
<> ((decimal (0 (0 (1 ()))))) (4)
<> ((decimal (1 (0 (1 ()))))) (5)
<> ((decimal (0 (1 (1 ()))))) (6)
<> ((decimal (1 (1 (1 ()))))) (7)
<> ((decimal (0 (0 (0 (1 ())))))) (8)
<> ((decimal (1 (0 (0 (1 ())))))) (9)

-- reverse ()-terminated list
<> (reverse ?x) (reverse1 () ?x)
<> (reverse1 ?a ()) (?a)
<> (reverse1 ?a (?h ?t)) (reverse1 (?h ?a) ?t)

-- ( to integer )
<> ((int ?*)) ((sum f (N one) g reverse (?*)))
<> (g ()) (())
<> (g (?h ?t)) (((binary ?h) g ?t))
<> (f (N ?u) ()) (()) 
<> (f (N ?u) (?h ?t)) (((mul (N ?h) (N ?u)) f (mul (N ?u) (N ten)) ?t))

-- ( to binary str )
-- ( <> ((bstr ?x)) (emit force (0 (b  ?x))) )
-- ( <> ((bstr ?x)) ((bstr1 () ?x)) )
<> ((bstr (N ?x))) ((bstr1 force ?x ()))
<> ((bstr1 force/r () ?a)) (emit force/r (0 (b ?a)))
<> ((bstr1 force/r (?h ?t) ?a)) ((bstr1 force/r ?t (?h ?a)))

-- ( to string: TODO, need division for this one )
<> ((str (N ?x))) ((str1 (N ?x) ()))
<> ((str1 (N (0 ())) ?a)) (emit force ?a)
<> ((str1 (N (?h ?t)) ?a)) ((str2 (divmod (N (?h ?t)) (N ten)) ?a))
<> ((str2 ((N ?q) (N ?r)) ?a)) ((str1 (N ?q) ((decimal ?r) ?a)))

-- ( force a list to evaluate to digits/letters )
<> ((?h force/r ?t)) (force/r (?h ?t))
<> (force ()) (force/r ())
<> (force (0 ?t)) ((0 force ?t))
<> (force (1 ?t)) ((1 force ?t))
<> (force (2 ?t)) ((2 force ?t))
<> (force (3 ?t)) ((3 force ?t))
<> (force (4 ?t)) ((4 force ?t))
<> (force (5 ?t)) ((5 force ?t))
<> (force (6 ?t)) ((6 force ?t))
<> (force (7 ?t)) ((7 force ?t))
<> (force (8 ?t)) ((8 force ?t))
<> (force (9 ?t)) ((9 force ?t))
<> (force (a ?t)) ((a force ?t))
<> (force (b ?t)) ((b force ?t))
<> (force (c ?t)) ((c force ?t))
<> (force (d ?t)) ((d force ?t))
<> (force (e ?t)) ((e force ?t))
<> (force (f ?t)) ((f force ?t))
<> (force (x ?t)) ((x force ?t))

-- ( emit )
<> (emit force/r ?*) (?*)

-- ( comparison operartions )
<> ((cmp ?x ?y)) ((cmpc #eq ?x ?y))
<> ((cmpc ?e () ())) (?e)
<> ((cmpc ?e (1 ?x) ())) (#gt)
<> ((cmpc ?e (0 ?x) ())) ((cmpc ?e ?x ()))
<> ((cmpc ?e () (1 ?y))) (#lt)
<> ((cmpc ?e () (0 ?y))) ((cmpc ?e () ?y))
<> ((cmpc ?e (0 ?x) (0 ?y))) ((cmpc ?e ?x ?y))
<> ((cmpc ?e (1 ?x) (0 ?y))) ((cmpc #gt ?x ?y))
<> ((cmpc ?e (0 ?x) (1 ?y))) ((cmpc #lt ?x ?y))
<> ((cmpc ?e (1 ?x) (1 ?y))) ((cmpc ?e ?x ?y))

-- ( addition )
<> ((add (N ?x) (N ?y))) (add/e force (addc 0 ?x ?y))
<> ((addc 0 () ())) (())
<> ((addc 1 () ())) ((1 ()))
<> ((addc 0 ?x ())) (?x)
<> ((addc 0 () ?y)) (?y)
<> ((addc 1 ?x ())) ((addc 1 ?x (0 ())))
<> ((addc 1 () ?y)) ((addc 1 (0 ()) ?y))
<> ((addc 0 (0 ?x) (0 ?y))) ((0 (addc 0 ?x ?y)))
<> ((addc 0 (0 ?x) (1 ?y))) ((1 (addc 0 ?x ?y)))
<> ((addc 0 (1 ?x) (0 ?y))) ((1 (addc 0 ?x ?y)))
<> ((addc 0 (1 ?x) (1 ?y))) ((0 (addc 1 ?x ?y)))
<> ((addc 1 (0 ?x) (0 ?y))) ((1 (addc 0 ?x ?y)))
<> ((addc 1 (0 ?x) (1 ?y))) ((0 (addc 1 ?x ?y)))
<> ((addc 1 (1 ?x) (0 ?y))) ((0 (addc 1 ?x ?y)))
<> ((addc 1 (1 ?x) (1 ?y))) ((1 (addc 1 ?x ?y)))
<> (add/e force/r ?x) ((N ?x))

-- ( summation )
<> ((sum ())) ((N (0 ())))
<> ((sum (?a ()))) (?a)
<> ((sum (?a (?b ?c)))) ((sum ((add ?a ?b) ?c)))

-- ( multiplication )
<> ((mul (N ?x) (N ?y))) (mul/e (mulc () ?x ?y))
<> ((mulc ?t () ?y)) ((sum ?t))
<> ((mulc ?t (0 ?x) ?y)) ((mulc ?t ?x (0 ?y)))
<> ((mulc ?t (1 ?x) ?y)) ((mulc ((N ?y) ?t) ?x (0 ?y)))
<> (mul/e (N ?x)) ((N ?x))

-- ( subtraction )
<> ((sub (N ?x) (N ?y))) (sub/e force (sub1 0 ?x ?y ()))
<> ((sub1 0 () () ?s)) (())
<> ((sub1 1 () () ?s)) (#err)
<> ((sub1 ?c ?x () ?s)) ((sub1 ?c ?x (0 ()) ?s))
<> ((sub1 ?c () ?y ?s)) ((sub1 ?c (0 ()) ?y ?s))
<> ((sub1 0 (0 ?x) (0 ?y) ?s)) ((sub1 0 ?x ?y (0 ?s)))
<> ((sub1 0 (0 ?x) (1 ?y) ?s)) ((sub2 1 ?x ?y ?s))
<> ((sub1 0 (1 ?x) (0 ?y) ?s)) ((sub2 0 ?x ?y ?s))
<> ((sub1 0 (1 ?x) (1 ?y) ?s)) ((sub1 0 ?x ?y (0 ?s)))
<> ((sub1 1 (0 ?x) (0 ?y) ?s)) ((sub2 1 ?x ?y ?s))
<> ((sub1 1 (0 ?x) (1 ?y) ?s)) ((sub1 1 ?x ?y (0 ?s)))
<> ((sub1 1 (1 ?x) (0 ?y) ?s)) ((sub1 0 ?x ?y (0 ?s)))
<> ((sub1 1 (1 ?x) (1 ?y) ?s)) ((sub2 1 ?x ?y ?s))
<> ((sub2 ?c ?x ?y ())) ((1 (sub1 ?c ?x ?y ())))
<> ((sub2 ?c ?x ?y (?h ?t))) ((0 (sub2 ?c ?x ?y ?t)))
<> (sub/e force/r ?x) ((N ?x))

<> ((dec (N (0 ())))) (#err)
<> ((dec (N (1 ())))) ((N (0 ())))
<> ((dec (N (1 ?t)))) ((N (0 ?t)))
<> ((dec (N (0 ?t)))) (dec/e (dec1 (0 ?t)))

<> ((dec1 (0 ?t))) ((1 (dec1 ?t)))
<> ((dec1 (1 ()))) (dec/r ())
<> ((dec1 (1 ?t))) (dec/r (0 ?t))
<> ((?h dec/r ?t)) (dec/r (?h ?t))
<> (dec/e dec/r ?x) ((N ?x))

-- ( inc )
<> ((inc (N ?x))) (inc/e force (inc1 ?x))
<> ((inc1 ())) ((1 ()))
<> ((inc1 (0 ?t))) ((1 ?t))
<> ((inc1 (1 ?t))) ((0 (inc1 ?t)))
<> (inc/e force/r ?x) ((N ?x))

-- ( left shift; lshift x b means x<<b )
<> ((lshift (N ?x) (N ?k))) (lshift/e force/r (lshift1 ?x (N ?k)))
<> ((lshift1 ?x (N (0 ())))) (?x)
<> ((lshift1 ?x (N (1 ())))) ((0 ?x))
<> ((lshift1 ?x (N (0 (?a ?b))))) ((lshift1 (0 ?x) (dec (N (0 (?a ?b))))))
<> ((lshift1 ?x (N (1 (?a ?b))))) ((lshift1 (0 ?x) (N (0 (?a ?b)))))
<> (lshift/e force/r ?x) ((N ?x))

<> ((rshift1 (N (?a ())))) ((N (0 ())))
<> ((rshift1 (N (?a (?b ?c))))) ((N (?b ?c)))

-- ( divmod, i.e. quotient and remainder )
-- ( x is the dividend, or what's left of it )
-- ( y is the divisor )
-- ( s is the number of bits to shift, so far )
-- ( o is the next valuet o add to the quotient )
-- ( m is the next multiple of y to work with )
-- ( d is the quotient, so far )
<> ((divmod (N ?x) (N ?y))) (divmod/p (divmod1 ?x ?y (cmp ?x ?y)))
<> ((divmod1 ?x ?y #lt)) (((N zero) (N ?x)))
<> ((divmod1 ?x ?y #eq)) (((N one) (N zero)))
<> ((divmod1 ?x ?y #gt)) ((divmod2 (N ?x) (N ?y) (N zero) (N ?y)))

<> ((divmod2 (N ?x) (N ?y) (N ?s) (N ?m))) ((divmod3 (N ?x) (N ?y) (N ?s) (N ?m) (cmp ?x (0 ?m))))
<> ((divmod3 (N ?x) (N ?y) (N ?s) (N ?m) #gt)) ((divmod2 (N ?x) (N ?y) (inc (N ?s)) (N (0 ?m))))
<> ((divmod3 (N ?x) (N ?y) (N ?s) (N ?m) #eq)) ((divmod4 (N ?x) (N ?y) (inc (N ?s)) (N (0 ?m)) (N zero)))
<> ((divmod3 (N ?x) (N ?y) (N ?s) (N ?m) #lt)) ((divmod4 (N ?x) (N ?y) (N ?s) (N ?m) (N zero)))

<> ((divmod4 (N ?x) (N ?y) (N (0 ())) (N ?m) (N ?d))) (((add (N ?d) (N one)) (sub (N ?x) (N ?y))))
<> ((divmod4 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d))) ((divmod5 (sub (N ?x) (N ?m)) (N ?y) (dec (N ?s)) (rshift1 (N ?m)) (add (N ?d) (lshift (N one) (N ?s)))))

<> ((divmod5 (N (0 ())) (N ?y) (N ?s) (N ?m) (N ?d))) (((N ?d) (N (0 ()))))
<> ((divmod5 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d))) ((divmod6 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d) (cmp ?x ?m)))

<> ((divmod6 (N ?x) (N ?y) (N (0 ())) (N ?m) (N ?d) #lt)) (((N ?d) (N ?x)))
<> ((divmod6 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d) #lt)) ((divmod5 (N ?x) (N ?y) (dec (N ?s)) (rshift1 (N ?m)) (N ?d)))
<> ((divmod6 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d) #eq)) ((divmod4 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d)))
<> ((divmod6 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d) #gt)) ((divmod4 (N ?x) (N ?y) (N ?s) (N ?m) (N ?d)))

<> (divmod/p ((N ?q) (N ?r))) (divmod/e (force ?q force ?r))
<> (divmod/e (force/r ?q force/r ?r)) (((N ?q) (N ?r)))

-- ( floor divison )
<> ((div (N ?x) (N ?y))) ((div1 (divmod (N ?x) (N ?y))))
<> ((div1 (?q ?r))) (?q)

-- ( remainder )
<> ((mod (N ?x) (N ?y))) ((mod1 (divmod (N ?x) (N ?y))))
<> ((mod1 (?q ?r))) (?r)

-- ( expontentiation )
<> ((pow (N ?x) ())) ((N (1 ())))
<> ((pow (N ?x) (N (0 ())))) ((N (1 ())))
<> ((pow (N ?x) (N (1 ())))) ((N ?x))
<> ((pow (N ?x) (N (0 ?k)))) ((pow (mul (N ?x) (N ?x)) (N ?k)))
<> ((pow (N ?x) (N (1 ?k)))) ((mul (N ?x) (pow (mul (N ?x) (N ?x)) (N ?k))))

-- ( greatest common denominator )
<> ((gcd ?a ?b)) ((gcd1 ?a ?b (cmp ?b (0 ()))))
<> ((gcd1 ?a ?b #eq)) (?a)
<> ((gcd1 ?a ?b #gt)) ((gcd ?b (mod ?a ?b)))
<> ((gcd1 ?a ?b #lt)) ((gcd ?b (mod ?a ?b)))

-- ( least common multiple )
<> ((lcm ?a ?b)) ((mul ?a (div ?b (gcd ?a ?b))))

-- (str (pow (int 17) (int 17)))

<> (a) ((N (1 (1 (1 ())))))
<> (b) ((N (0 (1 (1 ())))))
<> (c) ((N (0 (1 ()))))

-- (add a b)
-- (sum (a (b (c ()))))
-- (str (div (mul a b) c))
(bstr (pow (int 20) (int 20)))