d6
/
modal
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

rationals working, sort of

This commit is contained in:
~d6 2024-04-14 16:07:27 -04:00
parent 921afea1d3
commit effc98d589
1 changed files with 55 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
arith.modal
View File

@ -1,5 +1,6 @@
<> (-- ?x) () <> (-- ?x) ()
-- ( little endian binary natural numbers and integers )
-- ( N: little-endian natural numbers )
-- ( constants ) -- ( constants )
<> zero ((0 ())) <> zero ((0 ()))
@ -42,15 +43,23 @@
<> ((tostr1 (N (?h ?t)) ?a)) ((tostr2 (divmod (N (?h ?t)) (N ten)) ?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))) <> ((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 ) -- ( to string )
<> ((str (N ?x))) (emit force (tostr (N ?x)))
<> ((str (Z (+ ?x)))) ((str (N ?x))) <> ((str (Z (+ ?x)))) ((str (N ?x)))
<> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x)))) <> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x))))
<> ((str (N ?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 ) -- ( force a list to evaluate to digits/letters )
<> ((?h force/r ?t)) (force/r (?h ?t)) <> ((?h force/r ?t)) (force/r (?h ?t))
<> (force ()) (force/r ()) <> (force ()) (force/r ())
<> (force (- ?t)) ((- force ?t)) <> (force (- ?t)) ((- force ?t))
<> (force (/ ?t)) ((/ force ?t))
<> (force (0 ?t)) ((0 force ?t)) <> (force (0 ?t)) ((0 force ?t))
<> (force (1 ?t)) ((1 force ?t)) <> (force (1 ?t)) ((1 force ?t))
<> (force (2 ?t)) ((2 force ?t)) <> (force (2 ?t)) ((2 force ?t))
@ -201,8 +210,8 @@
<> ((mod1 (?q ?r))) (?r) <> ((mod1 (?q ?r))) (?r)
-- ( expontentiation ) -- ( expontentiation )
<> ((pow (N ?x) ())) ((N (1 ()))) <> ((pow (N ?x) ())) ((N one))
<> ((pow (N ?x) (N (0 ())))) ((N (1 ()))) <> ((pow (N ?x) (N (0 ())))) ((pow (N ?x) ()))
<> ((pow (N ?x) (N (1 ())))) ((N ?x)) <> ((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 (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)))) <> ((pow (N ?x) (N (1 ?k)))) ((mul (N ?x) (pow (mul (N ?x) (N ?x)) (N ?k))))
@ -267,6 +276,8 @@
<> ((decimal (0 (0 (0 (1 ())))))) (8) <> ((decimal (0 (0 (0 (1 ())))))) (8)
<> ((decimal (1 (0 (0 (1 ())))))) (9) <> ((decimal (1 (0 (0 (1 ())))))) (9)
-- ( Z: signed integers )
<> ((nat>int + (N ?x))) ((Z (+ ?x))) <> ((nat>int + (N ?x))) ((Z (+ ?x)))
<> ((nat>int - (N ?x))) ((Z (- ?x))) <> ((nat>int - (N ?x))) ((Z (- ?x)))
<> ((nat>pos (N ?x))) ((Z (+ ?x))) <> ((nat>pos (N ?x))) ((Z (+ ?x)))
@ -277,7 +288,7 @@
<> ((cmp (Z (?s (0 ()))) (Z (?s (0 ()))))) (#eq) <> ((cmp (Z (?s (0 ()))) (Z (?s (0 ()))))) (#eq)
<> ((cmp (Z (+ ?x)) (Z (+ ?y)))) ((cmp (N ?x) (N ?y))) <> ((cmp (Z (+ ?x)) (Z (+ ?y)))) ((cmp (N ?x) (N ?y)))
<> ((cmp (Z (+ ?x)) (Z (- ?y)))) (#gt) <> ((cmp (Z (+ ?x)) (Z (?s ?y)))) (#gt)
<> ((cmp (Z (- ?x)) (Z (- ?y)))) ((cmp (N ?y) (N ?x))) <> ((cmp (Z (- ?x)) (Z (- ?y)))) ((cmp (N ?y) (N ?x)))
<> ((cmp (Z (- ?x)) (Z (?s ?y)))) (#lt) <> ((cmp (Z (- ?x)) (Z (?s ?y)))) (#lt)
@ -326,4 +337,42 @@
<> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t)))) <> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t))))
<> ((int2 ?s (N ?x))) ((Z (?s ?x))) <> ((int2 ?s (N ?x))) ((Z (?s ?x)))
(str (mul (int -133) (int 77))) -- ( Q: rational numbers )
-- ( ensure n and d are coprime by dividing both by their gcd )
<> ((ratify ?s (N (0 ())) (N ?d))) ((Q (+ zero one)))
<> ((ratify ?s (N ?n) (N ?d))) ((ratify1 ?s (N ?n) (N ?d) (gcd (N ?n) (N ?d))))
<> ((ratify1 ?s (N ?n) (N ?d) (N ?g))) ((ratify2 ?s (div (N ?n) (N ?g)) (div (N ?d) (N ?g))))
<> ((ratify2 ?s (N ?n) (N ?d))) ((Q (?s ?n ?d)))
-- ( convert N to Q )
<> ((nat>rat + (N ?x))) ((Q (+ ?x one)))
<> ((nat>rat - (N ?x))) ((Q (- ?x one)))
-- ( convert Z to Q )
<> ((int>rat (Z (+ ?x)))) ((Q (+ ?x one)))
<> ((int>rat (Z (- ?x)))) ((Q (- ?x one)))
<> ((negate (Q (+ ?n ?d)))) ((Q (- ?n ?d)))
<> ((negate (Q (- ?n ?d)))) ((Q (+ ?n ?d)))
<> ((cmp (Q (?s (0 ()) (1 ()))) (Q (?s (0 ()) (1 ()))))) (#eq)
<> ((cmp (Q (+ ?x ?d)) (Q (+ ?y ?e)))) ((cmp (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d))))
<> ((cmp (Q (+ ?x ?d)) (Q (?s ?y ?e)))) (#gt)
<> ((cmp (Q (- ?x ?d)) (Q (- ?y ?e)))) ((cmp (mul (N ?y) (N ?d)) (mul (N ?x) (N ?e))))
<> ((cmp (Q (- ?x ?d)) (Q (?s ?y ?e)))) (#lt)
<> ((add (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qadd1 ?s ?t (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d)) (mul (N ?d) (N ?e))))
<> ((qadd1 ?s ?t (N ?x) (N ?y) (N ?d))) ((qadd2 (add (Z (?s ?x)) (Z (?t ?y))) (N ?d)))
<> ((qadd2 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d)))
<> ((sub (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qsub1 ?s ?t (mul (N ?x) (N ?e)) (mul (N ?y) (N ?d)) (mul (N ?d) (N ?e))))
<> ((qsub1 ?s ?t (N ?x) (N ?y) (N ?d))) ((qsub2 (sub (Z (?s ?x)) (Z (?t ?y))) (N ?d)))
<> ((qsub2 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d)))
<> ((mul (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((qmul1 (mul (Z (?s ?x)) (Z (?t ?y))) (mul (N ?d) (N ?e))))
<> ((qmul1 (Z (?s ?n)) (N ?d))) ((ratify ?s (N ?n) (N ?d)))
<> ((div (Q (?s ?x ?d)) (Q (?t ?y ?e)))) ((mul (Q (?s ?x ?d)) (Q (?t ?e ?y))))
(str (mul (Q (+ sixteen ten)) (Q (- sixteen ten))))