diff --git a/demo.modal b/demo.modal index aa62b1b..abf0af4 100644 --- a/demo.modal +++ b/demo.modal @@ -35,15 +35,6 @@ <> (reverse' ?a ()) (?a) <> (reverse' ?a (?h ?t)) (reverse' (?h ?a) ?t) --- ( normalize, remove trailing zeros ) --- ( currently zero is (0 ()) though arguably it could be () ) --- ( that change would require auditing our rules ) -<> (normalize (?h ?t)) ((?h normalize' () ?t)) -<> (normalize' ?s ()) (()) -<> (normalize' ?s (0 ?t)) (normalize' (0 ?s) ?t) -<> (normalize' () (1 ?t)) ((1 normalize' () ?t)) -<> (normalize' (0 ?s) (1 ?t)) ((0 normalize' ?s (1 ?t))) - -- ( to integer ) <> ((int ?*)) ((sum f (one) g reverse (?*))) <> (g ()) (()) @@ -123,20 +114,21 @@ <> (mulc ?t (1 ?x) ?y) (mulc (?y ?t) ?x (0 ?y)) -- ( subtraction ) -<> ((sub ?x ?y)) (normalize subc 0 ?x ?y) -<> (subc 0 () ()) (()) -<> (subc 1 () ()) (#err) -<> (subc 0 ?x ()) (?x) -<> (subc 1 ?x ()) (subc 1 ?x (0 ())) -<> (subc ?c () ?y) (subc ?c (0 ()) ?y) -<> (subc 0 (0 ?x) (0 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 0 (0 ?x) (1 ?y)) ((1 subc 1 ?x ?y)) -<> (subc 0 (1 ?x) (0 ?y)) ((1 subc 0 ?x ?y)) -<> (subc 0 (1 ?x) (1 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 1 (0 ?x) (0 ?y)) ((1 subc 1 ?x ?y)) -<> (subc 1 (0 ?x) (1 ?y)) ((0 subc 1 ?x ?y)) -<> (subc 1 (1 ?x) (0 ?y)) ((0 subc 0 ?x ?y)) -<> (subc 1 (1 ?x) (1 ?y)) ((1 subc 1 ?x ?y)) +<> ((sub ?x ?y)) (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)) <> (dec (0 ())) (#err) <> (dec (1 ())) ((0 ())) @@ -197,4 +189,4 @@ <> ((mod' (?q ?r))) (?r) -- (bstr (mul (int 2399) (int 3499))) -(str (int 1234567890)) +(str (int 1234567))