signed integers mostly working
This commit is contained in:
parent
f1d0ad5b1c
commit
6ca9de8f77
184
demo.modal
184
demo.modal
|
|
@ -1,48 +1,34 @@
|
||||||
<> (-- ?x) ()
|
<> (-- ?x) ()
|
||||||
-- ( little endian binary integers )
|
-- ( little endian binary natural numbers and integers )
|
||||||
|
|
||||||
-- ( constants )
|
-- ( constants )
|
||||||
<> zero ((0 ()))
|
<> zero ((0 ()))
|
||||||
<> one ((1 ()))
|
<> one ((1 ()))
|
||||||
|
<> two ((0 (1 ())))
|
||||||
|
<> eight ((0 (0 (0 (1 ())))))
|
||||||
<> ten ((0 (1 (0 (1 ())))))
|
<> ten ((0 (1 (0 (1 ())))))
|
||||||
|
<> sixteen ((0 (0 (0 (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 ()-terminated list
|
||||||
<> (reverse ?x) (reverse1 () ?x)
|
<> (reverse ?x) (reverse1 () ?x)
|
||||||
<> (reverse1 ?a ()) (?a)
|
<> (reverse1 ?a ()) (?a)
|
||||||
<> (reverse1 ?a (?h ?t)) (reverse1 (?h ?a) ?t)
|
<> (reverse1 ?a (?h ?t)) (reverse1 (?h ?a) ?t)
|
||||||
|
|
||||||
-- ( to integer )
|
-- ( to natural number )
|
||||||
<> ((int ?*)) ((sum f (N one) g reverse (?*)))
|
<> ((nat ?*)) ((nat1 (?*)))
|
||||||
|
<> ((nat1 ?x)) ((sum f (N one) g reverse ?x))
|
||||||
<> (g ()) (())
|
<> (g ()) (())
|
||||||
<> (g (?h ?t)) (((binary ?h) g ?t))
|
<> (g (?h ?t)) (((binary ?h) g ?t))
|
||||||
<> (f (N ?u) ()) (())
|
<> (f (N ?u) ()) (())
|
||||||
<> (f (N ?u) (?h ?t)) (((mul (N ?h) (N ?u)) f (mul (N ?u) (N ten)) ?t))
|
<> (f (N ?u) (?h ?t)) (((mul (N ?h) (N ?u)) f (mul (N ?u) (N ten)) ?t))
|
||||||
|
|
||||||
|
-- ( to integer )
|
||||||
|
<> ((nat-base (N ?b) ?*)) ((sum f' (N ?b) (N one) g' reverse (?*)))
|
||||||
|
<> (g' ()) (())
|
||||||
|
<> (g' (?h ?t)) (((binary ?h) g' ?t))
|
||||||
|
<> (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 )
|
-- ( to binary str )
|
||||||
-- ( <> ((bstr ?x)) (emit force (0 (b ?x))) )
|
-- ( <> ((bstr ?x)) (emit force (0 (b ?x))) )
|
||||||
-- ( <> ((bstr ?x)) ((bstr1 () ?x)) )
|
-- ( <> ((bstr ?x)) ((bstr1 () ?x)) )
|
||||||
|
|
@ -50,15 +36,21 @@
|
||||||
<> ((bstr1 force/r () ?a)) (emit force/r (0 (b ?a)))
|
<> ((bstr1 force/r () ?a)) (emit force/r (0 (b ?a)))
|
||||||
<> ((bstr1 force/r (?h ?t) ?a)) ((bstr1 force/r ?t (?h ?a)))
|
<> ((bstr1 force/r (?h ?t) ?a)) ((bstr1 force/r ?t (?h ?a)))
|
||||||
|
|
||||||
-- ( to string: TODO, need division for this one )
|
-- ( render as a list of characters )
|
||||||
<> ((str (N ?x))) ((str1 (N ?x) ()))
|
<> ((tostr (N ?x))) ((tostr1 (N ?x) ()))
|
||||||
<> ((str1 (N (0 ())) ?a)) (emit force ?a)
|
<> ((tostr1 (N (0 ())) ?a)) (?a)
|
||||||
<> ((str1 (N (?h ?t)) ?a)) ((str2 (divmod (N (?h ?t)) (N ten)) ?a))
|
<> ((tostr1 (N (?h ?t)) ?a)) ((tostr2 (divmod (N (?h ?t)) (N ten)) ?a))
|
||||||
<> ((str2 ((N ?q) (N ?r)) ?a)) ((str1 (N ?q) ((decimal ?r) ?a)))
|
<> ((tostr2 ((N ?q) (N ?r)) ?a)) ((tostr1 (N ?q) ((decimal ?r) ?a)))
|
||||||
|
|
||||||
|
-- ( to string )
|
||||||
|
<> ((str (Z (+ ?x)))) ((str (N ?x)))
|
||||||
|
<> ((str (Z (- ?x)))) (emit force (- (tostr (N ?x))))
|
||||||
|
<> ((str (N ?x))) (emit force (tostr (N ?x)))
|
||||||
|
|
||||||
-- ( 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 (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))
|
||||||
|
|
@ -81,7 +73,7 @@
|
||||||
<> (emit force/r ?*) (?*)
|
<> (emit force/r ?*) (?*)
|
||||||
|
|
||||||
-- ( comparison operartions )
|
-- ( comparison operartions )
|
||||||
<> ((cmp ?x ?y)) ((cmpc #eq ?x ?y))
|
<> ((cmp (N ?x) (N ?y))) ((cmpc #eq ?x ?y))
|
||||||
<> ((cmpc ?e () ())) (?e)
|
<> ((cmpc ?e () ())) (?e)
|
||||||
<> ((cmpc ?e (1 ?x) ())) (#gt)
|
<> ((cmpc ?e (1 ?x) ())) (#gt)
|
||||||
<> ((cmpc ?e (0 ?x) ())) ((cmpc ?e ?x ()))
|
<> ((cmpc ?e (0 ?x) ())) ((cmpc ?e ?x ()))
|
||||||
|
|
@ -176,12 +168,12 @@
|
||||||
-- ( o is the next valuet o add to the quotient )
|
-- ( o is the next valuet o add to the quotient )
|
||||||
-- ( m is the next multiple of y to work with )
|
-- ( m is the next multiple of y to work with )
|
||||||
-- ( d is the quotient, so far )
|
-- ( d is the quotient, so far )
|
||||||
<> ((divmod (N ?x) (N ?y))) (divmod/p (divmod1 ?x ?y (cmp ?x ?y)))
|
<> ((divmod (N ?x) (N ?y))) (divmod/p (divmod1 ?x ?y (cmp (N ?x) (N ?y))))
|
||||||
<> ((divmod1 ?x ?y #lt)) (((N zero) (N ?x)))
|
<> ((divmod1 ?x ?y #lt)) (((N zero) (N ?x)))
|
||||||
<> ((divmod1 ?x ?y #eq)) (((N one) (N zero)))
|
<> ((divmod1 ?x ?y #eq)) (((N one) (N zero)))
|
||||||
<> ((divmod1 ?x ?y #gt)) ((divmod2 (N ?x) (N ?y) (N zero) (N ?y)))
|
<> ((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))))
|
<> ((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) #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) #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)))
|
<> ((divmod3 (N ?x) (N ?y) (N ?s) (N ?m) #lt)) ((divmod4 (N ?x) (N ?y) (N ?s) (N ?m) (N zero)))
|
||||||
|
|
@ -190,7 +182,7 @@
|
||||||
<> ((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)))))
|
<> ((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 (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)))
|
<> ((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 (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) #lt)) ((divmod5 (N ?x) (N ?y) (dec (N ?s)) (rshift1 (N ?m)) (N ?d)))
|
||||||
|
|
@ -216,7 +208,7 @@
|
||||||
<> ((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))))
|
||||||
|
|
||||||
-- ( greatest common denominator )
|
-- ( greatest common denominator )
|
||||||
<> ((gcd ?a ?b)) ((gcd1 ?a ?b (cmp ?b (0 ()))))
|
<> ((gcd ?a ?b)) ((gcd1 ?a ?b (cmp ?b (N (0 ())))))
|
||||||
<> ((gcd1 ?a ?b #eq)) (?a)
|
<> ((gcd1 ?a ?b #eq)) (?a)
|
||||||
<> ((gcd1 ?a ?b #gt)) ((gcd ?b (mod ?a ?b)))
|
<> ((gcd1 ?a ?b #gt)) ((gcd ?b (mod ?a ?b)))
|
||||||
<> ((gcd1 ?a ?b #lt)) ((gcd ?b (mod ?a ?b)))
|
<> ((gcd1 ?a ?b #lt)) ((gcd ?b (mod ?a ?b)))
|
||||||
|
|
@ -224,7 +216,117 @@
|
||||||
-- ( least common multiple )
|
-- ( least common multiple )
|
||||||
<> ((lcm ?a ?b)) ((mul ?a (div ?b (gcd ?a ?b))))
|
<> ((lcm ?a ?b)) ((mul ?a (div ?b (gcd ?a ?b))))
|
||||||
|
|
||||||
-- (str (pow (int 17) (int 17)))
|
-- ( 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 a)) ((0 (1 (0 (1 ())))))
|
||||||
|
<> ((binary b)) ((1 (1 (0 (1 ())))))
|
||||||
|
<> ((binary c)) ((0 (0 (1 (1 ())))))
|
||||||
|
<> ((binary d)) ((1 (0 (1 (1 ())))))
|
||||||
|
<> ((binary e)) ((0 (1 (1 (1 ())))))
|
||||||
|
<> ((binary f)) ((1 (1 (1 (1 ())))))
|
||||||
|
<> ((binary g)) ((0 (0 (0 (0 (1 ()))))))
|
||||||
|
<> ((binary h)) ((1 (0 (0 (0 (1 ()))))))
|
||||||
|
<> ((binary i)) ((0 (1 (0 (0 (1 ()))))))
|
||||||
|
<> ((binary j)) ((1 (1 (0 (0 (1 ()))))))
|
||||||
|
<> ((binary k)) ((0 (0 (1 (0 (1 ()))))))
|
||||||
|
<> ((binary l)) ((1 (0 (1 (0 (1 ()))))))
|
||||||
|
<> ((binary m)) ((0 (1 (1 (0 (1 ()))))))
|
||||||
|
<> ((binary n)) ((1 (1 (1 (0 (1 ()))))))
|
||||||
|
<> ((binary o)) ((0 (0 (0 (1 (1 ()))))))
|
||||||
|
<> ((binary p)) ((1 (0 (0 (1 (1 ()))))))
|
||||||
|
<> ((binary q)) ((0 (1 (0 (1 (1 ()))))))
|
||||||
|
<> ((binary r)) ((1 (1 (0 (1 (1 ()))))))
|
||||||
|
<> ((binary s)) ((0 (0 (1 (1 (1 ()))))))
|
||||||
|
<> ((binary t)) ((1 (0 (1 (1 (1 ()))))))
|
||||||
|
<> ((binary u)) ((0 (1 (1 (1 (1 ()))))))
|
||||||
|
<> ((binary v)) ((1 (1 (1 (1 (1 ()))))))
|
||||||
|
<> ((binary w)) ((0 (0 (0 (0 (0 (1 ())))))))
|
||||||
|
<> ((binary x)) ((1 (0 (0 (0 (0 (1 ())))))))
|
||||||
|
<> ((binary y)) ((0 (1 (0 (0 (0 (1 ())))))))
|
||||||
|
<> ((binary z)) ((1 (1 (0 (0 (0 (1 ())))))))
|
||||||
|
|
||||||
|
-- ( binary to digits )
|
||||||
|
<> ((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)
|
||||||
|
|
||||||
|
<> ((nat>int + (N ?x))) ((Z (+ ?x)))
|
||||||
|
<> ((nat>int - (N ?x))) ((Z (- ?x)))
|
||||||
|
<> ((nat>pos (N ?x))) ((Z (+ ?x)))
|
||||||
|
<> ((nat>neg (N ?x))) ((Z (- ?x)))
|
||||||
|
|
||||||
|
<> ((negate (Z (+ ?x)))) ((Z (- ?x)))
|
||||||
|
<> ((negate (Z (+ ?x)))) ((Z (- ?x)))
|
||||||
|
|
||||||
|
<> ((cmp (Z (?s (0 ()))) (Z (?s (0 ()))))) (#eq)
|
||||||
|
<> ((cmp (Z (+ ?x)) (Z (+ ?y)))) ((cmp (N ?x) (N ?y)))
|
||||||
|
<> ((cmp (Z (+ ?x)) (Z (- ?y)))) (#gt)
|
||||||
|
<> ((cmp (Z (- ?x)) (Z (- ?y)))) ((cmp (N ?y) (N ?x)))
|
||||||
|
<> ((cmp (Z (- ?x)) (Z (?s ?y)))) (#lt)
|
||||||
|
|
||||||
|
<> ((add (Z (+ ?x)) (Z (+ ?y)))) ((nat>pos (add (N ?x) (N ?y))))
|
||||||
|
<> ((add (Z (- ?x)) (Z (- ?y)))) ((nat>neg (add (N ?x) (N ?y))))
|
||||||
|
<> ((add (Z (+ ?x)) (Z (- ?y)))) ((zadd ?x ?y (cmp (N ?x) (N ?y))))
|
||||||
|
<> ((add (Z (- ?x)) (Z (+ ?y)))) ((zadd ?y ?x (cmp (N ?y) (N ?x))))
|
||||||
|
<> ((zadd ?p ?n #gt)) ((nat>pos (sub (N ?p) (N ?n))))
|
||||||
|
<> ((zadd ?p ?n #eq)) ((Z (+ (0 ()))))
|
||||||
|
<> ((zadd ?p ?n #lt)) ((nat>neg (sub (N ?n) (N ?p))))
|
||||||
|
|
||||||
|
<> ((mul (Z (?s ?x)) (Z (?s ?y)))) ((nat>pos (mul (N ?x) (N ?y))))
|
||||||
|
<> ((mul (Z (?s ?x)) (Z (?t ?y)))) ((nat>neg (mul (N ?x) (N ?y))))
|
||||||
|
|
||||||
|
<> ((sub (Z (+ ?x)) (Z (+ ?y)))) ((add (Z (+ ?x)) (Z (- ?y))))
|
||||||
|
<> ((sub (Z (+ ?x)) (Z (- ?y)))) ((add (Z (+ ?x)) (Z (+ ?y))))
|
||||||
|
<> ((sub (Z (- ?x)) (Z (+ ?y)))) ((add (Z (- ?x)) (Z (- ?y))))
|
||||||
|
<> ((sub (Z (- ?x)) (Z (- ?y)))) ((add (Z (- ?x)) (Z (+ ?y))))
|
||||||
|
|
||||||
|
-- ( n/d = q, n%d = r )
|
||||||
|
-- ( n = d * q + r )
|
||||||
|
-- ( ---------------- )
|
||||||
|
-- ( 9 = 2 * 4 + 1 )
|
||||||
|
-- ( -9 = 2 * -4 - 1 )
|
||||||
|
-- ( 9 = -2 * -4 + 1 )
|
||||||
|
-- ( -9 = -2 * 4 - 1 )
|
||||||
|
<> ((divmod (Z (+ ?x)) (Z (+ ?y)))) ((zdm + + (divmod (N ?x) (N ?y))))
|
||||||
|
<> ((divmod (Z (- ?x)) (Z (+ ?y)))) ((zdm - - (divmod (N ?x) (N ?y))))
|
||||||
|
<> ((divmod (Z (+ ?x)) (Z (- ?y)))) ((zdm - + (divmod (N ?x) (N ?y))))
|
||||||
|
<> ((divmod (Z (- ?x)) (Z (- ?y)))) ((zdm + - (divmod (N ?x) (N ?y))))
|
||||||
|
<> ((zdm ?s ?t ((N ?q) (N ?r)))) (((Z (?s ?q)) (Z (?t ?r))))
|
||||||
|
|
||||||
|
<> ((div (Z (?s ?x)) (Z (?s ?y)))) ((nat>pos (div (N ?x) (N ?y))))
|
||||||
|
<> ((div (Z (?s ?x)) (Z (?t ?y)))) ((nat>neg (div (N ?x) (N ?y))))
|
||||||
|
|
||||||
|
<> ((mod (Z (+ ?x)) (Z (?s ?y)))) ((nat>pos (div (N ?x) (N ?y))))
|
||||||
|
<> ((mod (Z (- ?x)) (Z (?s ?y)))) ((nat>neg (div (N ?x) (N ?y))))
|
||||||
|
|
||||||
|
<> ((pow (Z (+ ?x)) (N ?k))) ((nat>pos (pow (N ?x) (N ?k))))
|
||||||
|
<> ((pow (Z (- ?x)) (N (0 ?k)))) ((nat>pos (pow (N ?x) (N (0 ?k)))))
|
||||||
|
<> ((pow (Z (- ?x)) (N (1 ?k)))) ((nat>neg (pow (N ?x) (N (1 ?k)))))
|
||||||
|
|
||||||
|
-- ( to natural number )
|
||||||
|
<> ((int ?*)) ((int1 (?*)))
|
||||||
|
<> ((int1 (- ?t))) ((int2 - (nat1 ?t)))
|
||||||
|
<> ((int1 (?h ?t))) ((int2 + (nat1 (?h ?t))))
|
||||||
|
<> ((int2 ?s (N ?x))) ((Z (?s ?x)))
|
||||||
|
|
||||||
|
-- (str (pow (nat 17) (nat 17)))
|
||||||
|
|
||||||
<> (a) ((N (1 (1 (1 ())))))
|
<> (a) ((N (1 (1 (1 ())))))
|
||||||
<> (b) ((N (0 (1 (1 ())))))
|
<> (b) ((N (0 (1 (1 ())))))
|
||||||
|
|
@ -233,4 +335,6 @@
|
||||||
-- (add a b)
|
-- (add a b)
|
||||||
-- (sum (a (b (c ()))))
|
-- (sum (a (b (c ()))))
|
||||||
-- (str (div (mul a b) c))
|
-- (str (div (mul a b) c))
|
||||||
(bstr (pow (int 20) (int 20)))
|
|
||||||
|
-- (mul (nat>neg (nat 13)) (nat>neg (nat 7)))
|
||||||
|
(str (mul (int 13) (int 7)))
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue