optimizations, ostr, hstr, etc
This commit is contained in:
parent
ff919d23c8
commit
ec48109bfe
174
arith.modal
174
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)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue