From ec48109bfe13896b0497d7863b80e6659b4a9e83 Mon Sep 17 00:00:00 2001 From: d_m Date: Tue, 16 Apr 2024 23:53:36 -0400 Subject: [PATCH] optimizations, ostr, hstr, etc --- arith.modal | 174 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 101 insertions(+), 73 deletions(-) diff --git a/arith.modal b/arith.modal index def6e92..597e91e 100644 --- a/arith.modal +++ b/arith.modal @@ -30,57 +30,6 @@ <> (f' (N ?b) (N ?u) ()) (()) <> (f' (N ?b) (N ?u) (?h ?t)) (((mul (N ?h) (N ?u)) f' (N ?b) (mul (N ?u) (N ?b)) ?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))) - --- ( render as a list of characters ) -<> ((tostr (N ?x))) ((tostr1 (N ?x) ())) -<> ((tostr1 (N (0 ())) ?a)) (?a) -<> ((tostr1 (N (?h ?t)) ?a)) ((tostr2 (divmod (N (?h ?t)) (N ten)) ?a)) -<> ((tostr2 ((N ?q) (N ?r)) ?a)) ((tostr1 (N ?q) ((decimal ?r) ?a))) - --- ( concatenate lists ) -<> ((concat (?h ?t) ?r)) ((?h (concat ?t ?r))) -<> ((concat () ?r)) (?r) - --- ( to string ) -<> ((str (N ?x))) (emit force (tostr (N ?x))) -<> ((str (Z (+ ?x)))) ((str (N ?x))) -<> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x)))) -<> ((str (Q (?s ?n ?d)))) ((qstr ?s (force (tostr (N ?n))) (force (tostr (N ?d))))) -<> ((qstr + (force/r ?l) (force/r ?m))) (emit force (concat ?l (/ ?m))) -<> ((qstr - (force/r ?l) (force/r ?m))) (emit force (concat (- ?l) (/ ?m))) - --- ( force a list to evaluate to digits/letters ) -<> ((?h force/r ?t)) (force/r (?h ?t)) -<> (force ()) (force/r ()) -<> (force (- ?t)) ((- force ?t)) -<> (force (/ ?t)) ((/ force ?t)) -<> (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 (N ?x) (N ?y))) ((cmpc #eq ?x ?y)) <> ((cmpc ?e () ())) (?e) @@ -124,27 +73,29 @@ <> (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) +<> ((sub (N ?x) (N ?y))) ((sub1 0 ?x ?y ())) + +<> ((sub1 ?c (?b ?x) (?b ?y) ?s)) ((sub1 ?c ?x ?y (?c ?s))) +<> ((sub1 0 (1 ?x) (0 ?y) ?s)) ((sub1 0 ?x ?y (1 ?s))) +<> ((sub1 1 (1 ?x) (0 ?y) ?s)) ((sub1 0 ?x ?y (0 ?s))) +<> ((sub1 0 (0 ?x) (1 ?y) ?s)) ((sub1 1 ?x ?y (1 ?s))) +<> ((sub1 1 (0 ?x) (1 ?y) ?s)) ((sub1 1 ?x ?y (0 ?s))) + +<> ((sub1 0 () () ?s)) ((sub/u ?s)) +<> ((sub1 1 () ?y ?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) +<> ((sub/u (1 ?t))) ((sub/v (1 ?t) ())) +<> ((sub/u (0 ()))) ((N (0 ()))) +<> ((sub/u (0 ?t))) ((sub/u ?t)) +<> ((sub/v () ?s)) ((N ?s)) +<> ((sub/v (?h ?t) ?s)) ((sub/v ?t (?h ?s))) + <> ((dec (N (1 ())))) ((N (0 ()))) -<> ((dec (N (1 ?t)))) ((N (0 ?t))) +<> ((dec (N (0 ())))) (#err) <> ((dec (N (0 ?t)))) (dec/e (dec1 (0 ?t))) +<> ((dec (N (1 ?t)))) ((N (0 ?t))) <> ((dec1 (0 ?t))) ((1 (dec1 ?t))) <> ((dec1 (1 ()))) (dec/r ()) @@ -181,23 +132,18 @@ <> ((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 (N ?x) (N (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 (N ?x) (N ?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))) @@ -386,4 +332,86 @@ <> ((rat2 ?s (?h ?t) ?a)) ((rat2 ?s ?t (?h ?a))) <> ((rat3 ?s (N ?n) (N ?d))) ((Q (?s ?n ?d))) -(str (pow (rat -2/7) (nat 3))) +-- ( render as a list of characters ) +<> ((tostr (N (0 ())))) ((0 ())) +<> ((tostr (N ?x))) ((tostr1 (N ?x) ())) +<> ((tostr1 (N (0 ())) ?a)) (?a) +<> ((tostr1 (N (?h ?t)) ?a)) ((tostr2 (divmod (N (?h ?t)) (N ten)) ?a)) +<> ((tostr2 ((N ?q) (N ?r)) ?a)) ((tostr1 (N ?q) ((decimal ?r) ?a))) + +-- ( concatenate lists ) +<> ((concat (?h ?t) ?r)) ((?h (concat ?t ?r))) +<> ((concat () ?r)) (?r) + +-- ( to string ) +<> ((str (N ?x))) (emit force (tostr (N ?x))) +<> ((str (Z (+ ?x)))) ((str (N ?x))) +<> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x)))) +<> ((str (Q (?s ?n ?d)))) ((qstr ?s (force (tostr (N ?n))) (force (tostr (N ?d))))) +<> ((qstr + (force/r ?l) (force/r ?m))) (emit force (concat ?l (/ ?m))) +<> ((qstr - (force/r ?l) (force/r ?m))) (emit force (concat (- ?l) (/ ?m))) + +-- ( force a list to evaluate to digits/letters ) +<> ((?h force/r ?t)) (force/r (?h ?t)) +<> (force ()) (force/r ()) +<> (force (- ?t)) ((- force ?t)) +<> (force (/ ?t)) ((/ force ?t)) +<> (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 (o ?t)) ((o force ?t)) +<> (force (x ?t)) ((x force ?t)) + +-- ( emit ) +<> (emit force/r ?*) (?*) + +-- ( to binary string ) +<> ((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 octal string ) +<> ((ostr (N ?x))) ((ostr1 () ?x)) +<> ((ostr1 ?s (?a (?b (?c ?t))))) ((ostr1 ((hdigit ?a ?b ?c 0) ?s) ?t)) +<> ((ostr1 ?s (?a (?b ?t)))) ((ostr1 ((hdigit ?a ?b 0 0) ?s) ?t)) +<> ((ostr1 ?s (?a ?t))) ((ostr1 ((hdigit ?a 0 0 0) ?s) ?t)) +<> ((ostr1 ?s ())) (emit force (0 (o ?s))) + +-- ( to hex string ) +<> ((hstr (N ?x))) ((hstr1 () ?x)) +<> ((hstr1 ?s (?a (?b (?c (?d ?t)))))) ((hstr1 ((hdigit ?a ?b ?c ?d) ?s) ?t)) +<> ((hstr1 ?s (?a (?b (?c ?t))))) ((hstr1 ((hdigit ?a ?b ?c 0) ?s) ?t)) +<> ((hstr1 ?s (?a (?b ?t)))) ((hstr1 ((hdigit ?a ?b 0 0) ?s) ?t)) +<> ((hstr1 ?s (?a ?t))) ((hstr1 ((hdigit ?a 0 0 0) ?s) ?t)) +<> ((hstr1 ?s ())) (emit force (0 (x ?s))) +<> ((hdigit 0 0 0 0)) (0) +<> ((hdigit 1 0 0 0)) (1) +<> ((hdigit 0 1 0 0)) (2) +<> ((hdigit 1 1 0 0)) (3) +<> ((hdigit 0 0 1 0)) (4) +<> ((hdigit 1 0 1 0)) (5) +<> ((hdigit 0 1 1 0)) (6) +<> ((hdigit 1 1 1 0)) (7) +<> ((hdigit 0 0 0 1)) (8) +<> ((hdigit 1 0 0 1)) (9) +<> ((hdigit 0 1 0 1)) (a) +<> ((hdigit 1 1 0 1)) (b) +<> ((hdigit 0 0 1 1)) (c) +<> ((hdigit 1 0 1 1)) (d) +<> ((hdigit 0 1 1 1)) (e) +<> ((hdigit 1 1 1 1)) (f) + +(ostr (pow (nat 19) (nat 19)))