#lang scribble/doc
@(require scribble/manual scribble/eval "../evaluator.ss"
          (for-label "../../lang/dracula.ss"))

@title{Rational and Complex Arithmetic}

@defform[(* num ...)]{
Multiplies the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function @scheme[binary-*]
@examples[
#:eval the-evaluator
(*)
(* 2)
(* 1 2 3)
]
}

@defform[(+ num ...)]{
Adds the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function @scheme[binary-+].
@examples[
#:eval the-evaluator
(+)
(+ 2)
(+ 1 2 3)
]
}

@defform[(- num num)]{
Subtracts the given numbers. If only one argument is given, returns the negation of the input.
@examples[
#:eval the-evaluator
(- 5)
(- 5 3)
]
}

@defform[(/ num num)]{
Divides the first number by the second. If only one argument is given, returns the reciprocal of the input.
@examples[
#:eval the-evaluator
(/ 2)
(/ 16 4)
]
}

@defform[(1+ num)]{
Adds 1 to the given number.
@examples[
#:eval the-evaluator
(1+ 1)
]
}

@defform[(1- num)]{
Subtracts 1 from the given number.
@examples[
#:eval the-evaluator
(1- 1)
]
}

@defproc[(binary-* [x (acl2-numberp x)] [y (acl2-numberp y)]) t]{
Takes exactly two numbers and multiplies them together.
@examples[
#:eval the-evaluator
(binary-* 9 8)
]
}

@defproc[(binary-+ [x (acl2-numberp x)] [y (acl2-numberp y)]) t]{
Takes exactly two numbers and adds them together.
@examples[
#:eval the-evaluator
(binary-+ 9 8)
]
}

@defproc[(/= [x (acl2-numberp x)] [y (acl2-numberp y)]) t]{
Determines if the given numbers are not equal. Logically equivalent to @scheme[(not (equal x y))]
@examples[
#:eval the-evaluator
(/= 2 2)
(/= 3 2)
]
}

@defproc[(< [x (rationalp x)] [y (rationalp y)]) t]{
Determines if @scheme[x] is less than @scheme[y].
@examples[
#:eval the-evaluator
(< 1 2)
(< 2 1)
(< 2 2)
]
}

@defproc[(<= [x (rationalp x)] [y (rationalp y)]) t]{
Determines if @scheme[x] is less than or equal to @scheme[y].
@examples[
#:eval the-evaluator
(<= 1 2)
(<= 2 1)
(<= 2 2)
]
}

@defproc[(= [x (acl2-numberp x)] [y (acl2-numberp y)]) t]{
Determines if @scheme[x] is equal to @scheme[y]. This is like @scheme[equal], but has the guard that both of its arguments must be numbers. It usually executes more efficiently thatn @scheme[equal].
@examples[
#:eval the-evaluator
(= 1 2)
(= 2 1)
(= 2 2)
]
}

@defproc[(> [x (rationalp x)] [y (rationalp y)]) t]{
Determines if @scheme[x] is greater than @scheme[y].
@examples[
#:eval the-evaluator
(> 1 2)
(> 2 1)
(> 2 2)
]
}

@defproc[(>= [x (rationalp x)] [y (rationalp y)]) t]{
Determines if @scheme[x] is greater than or equal to @scheme[y].
@examples[
#:eval the-evaluator
(>= 1 2)
(>= 2 1)
(>= 2 2)
]
}

@defform[(acl2-numberp x)]{
Returns true if and only if @scheme[x] is a rational or complex rational number.
@examples[
#:eval the-evaluator
(acl2-numberp 1)
(acl2-numberp 12/5)
(acl2-numberp "no")
]
}

@defform[(complex-rationalp z)]{
Determines if @scheme[z] is a complex number consisting of rational parts.
@examples[
#:eval the-evaluator
(complex-rationalp 3)
(complex-rationalp (complex 3 0))
(complex-rationalp t)
(complex-rationalp (complex 3 1))
]
}

@defproc[(complex/complex-rationalp [z t]) t]{
For most cases, this is simply a macro abbreviating @scheme[complex-rationalp]. 
@examples[
#:eval the-evaluator
(complex/complex-rationalp 3)
(complex/complex-rationalp (complex 3 0))
(complex/complex-rationalp t)
(complex/complex-rationalp (complex 3 1))
]
}

@defproc[(minusp [x (real/rationalp x)]) t]{
Determines whether @scheme[x] is a negative number.
@examples[
#:eval the-evaluator
(minusp 1)
(minusp -1)
]
}

@defproc[(natp [x t]) t]{
Determines if @scheme[x] is a natural number.
@examples[
#:eval the-evaluator
(natp 1)
(natp 0)
(natp -1)
]
}

@defproc[(oddp [x (integerp x)]) t]{
Determines if @scheme[x] is odd.
@examples[
#:eval the-evaluator
(oddp 3)
(oddp 2)
]
}

@defproc[(plusp [x (real/rationalp x)]) t]{
Determines if @scheme[x] is positive.
@examples[
#:eval the-evaluator
(plusp 1)
(plusp -1)
(plusp 1/2)
]
}

@defproc[(posp [x t]) t]{
Determines if @scheme[x] is a positive integer.
@examples[
#:eval the-evaluator
(posp 1)
(posp -1)
(posp 1/2)
(posp (complex 1 2))
(posp "asdf")
]
}

@defform[(rationalp x)]{
Determines if @scheme[x] is a rational number.
@examples[
#:eval the-evaluator
(rationalp 2/5)
(rationalp 2)
(rationalp (complex 1 2))
(rationalp "number")
]
}

@defform[(real/rationalp x)]{
In most cases, this is just a macro abbreviating @scheme[rationalp].
@examples[
#:eval the-evaluator
(real/rationalp 2/5)
(real/rationalp "number")
]
}

@defproc[(abs [x (real/rationalp x)]) t]{
Computes the absolute value of @scheme[x].
@examples[
#:eval the-evaluator
(abs 1)
(abs -1)
]
}

@defproc[(ceiling [i (real/rationalp i)] [j (and (real/rationalp j) (not (eql j 0)))]) t]{
Returns the smallest integer greater the value of @scheme[(/ i j)].
@examples[
#:eval the-evaluator
(ceiling 4 2)
(ceiling 4 3)
]
}

@defproc[(complex [n (rationalp n)] [i (rationalp i)]) t]{
Creates a complex number with real part @scheme[n] and imaginary part @scheme[i].
@examples[
#:eval the-evaluator
(complex 2 1)
(complex 2 0)
(complex 0 2)
(complex 1/2 3/2)
]
}

@defproc[(conjugate [x (acl2-numberp x)]) t]{
Computes the complex conjugate of @scheme[x] (the result of negating its imaginary part).
@examples[
#:eval the-evaluator
(conjugate (complex 3 1))
]
}

@defproc[(denominator [x (rationalp x)]) t]{
Returns the divisor of a rational number in lowest terms.
@examples[
#:eval the-evaluator
(denominator 5)
(denominator 5/3)
(denominator 10/6)
]
}

@defproc[(evenp [x (integerp x)]) t]{
Determines if @scheme[x] is even.
@examples[
#:eval the-evaluator
(evenp 1)
(evenp 2)
]
}

@defproc[(explode-nonnegative-integer [n (and (integerp n) (>= n 0))] [r (print-base-p r)]) l]{
Returns a list of characters representing @scheme[n] in base-@scheme[r], and appends @scheme[l] to the end.
@examples[
#:eval the-evaluator
(explode-nonnegative-integer 925 10 nil)
(explode-nonnegative-integer 325 16 nil)
(explode-nonnegative-integer 325 16 (list 'a 'b 'c))
(explode-nonnegative-integer 325 16 'a)
]
}

@defproc[(expt [i (acl2-numberp i)] [j (and (integerp j) (not (and (eql i 0) (< j 0))))]) t]{
Raises @scheme[i] to the @scheme[j]th power.
@examples[
#:eval the-evaluator
(expt 10 2)
(expt 10 -2)
]
}

@defproc[(fix [x t]) t]{
Coerces @scheme[x] to a number. If @scheme[x] is a number, @scheme[(fix x)] returns the argument unchanged. Otherwise, it returns 0.
@examples[
#:eval the-evaluator
(fix 20)
(fix 2/3)
(fix "hello")
(fix nil)
]
}

@defproc[(floor [i (real/rationalp i)] [j (and (real/rationalp j) (not (eql j 0)))]) t]{
Returns the greatest integer not exceeding the value of @scheme[(/ i j)].
@examples[
#:eval the-evaluator
(floor 4 2)
(floor 4 3)
]
}

@defform[(ifix [x t]) t]{
Coerces @scheme[x] to an integer. If @scheme[x] is an integer, @scheme[(ifix x)] returns the argument unchanged. Otherwise, it returns 0.
@examples[
#:eval the-evaluator
(ifix 16)
(ifix 22/3)
(ifix "hello")
]
}

@defproc[(imagpart [i (acl2-numberp i)]) t]{
Returns the imaginary part of a complex number.
@examples[
#:eval the-evaluator
(imagpart (complex 3 2))
(imagpart 5)
]
}

@defform[(int= i j)]{
Checks to see if the two integers @scheme[i] and @scheme[j] are equal. This is like @scheme[equal] and @scheme[=], but with the added guard that the inputs are integers. This generally executes more efficiently on integers than @scheme[equal] or @scheme[=].
@examples[
#:eval the-evaluator
(int= 1 2)
(int= 2 1)
(int= 2 2)
]
}

@defproc[(integer-length [x (integerp x)]) t]{
Returns the number of bits in the two's complement binary representation of @scheme[x].
@examples[
#:eval the-evaluator
(integer-length 12)
(integer-length 1234)
]
}

@defform[(integerp x)]{
Determines whether @scheme[x] is an integer.
@examples[
#:eval the-evaluator
(integerp 12)
(integerp '12)
(integerp nil)
]
}

@defproc[(max [i (real/rationalp i)] [j (real/rationalp j)]) t]{
Returns the greater of the two given numbers.
@examples[
#:eval the-evaluator
(max 1 2)
(max 4 3)
]
}

@defproc[(min [i (real/rationalp i)] [j (real/rationalp j)]) t]{
Returns the lesser of the two given numbers.
@examples[
#:eval the-evaluator
(min 1 2)
(min 4 3)
]
}

@defproc[(mod [i (real/rationalp i)] [j (and (real/rationalp j) (not (eql j 0)))]) t]{
Computes the remainder of dividing @scheme[i] by @scheme[j].
@examples[
#:eval the-evaluator
(mod 4 2)
(mod 8 3)
]
}

@defproc[(nfix [x t]) t]{
Coerces @scheme[x] to a natural number. If @scheme[x] is a natural number, @scheme[(nfix x)] returns the argument unchanged. Otherwise, it returns 0.
@examples[
#:eval the-evaluator
(nfix 1)
(nfix -1)
(nfix 1/2)
(nfix "5")
]
}

@defproc[(nonnegative-integer-quotient [x (and (integerp x) (not (< x 0)))] [y (and (integerp j) (< 0 j))]) t]{
Returns the integer quotient of @scheme[x] and @scheme[y]. That is, @scheme[(nonnegative-integer-quotient x y)] is the largest integer @scheme[k] such that @scheme[(* j k)] is less than or equal to @scheme[x].
@examples[
#:eval the-evaluator
(nonnegative-integer-quotient 14 3)
(nonnegative-integer-quotient 15 3)
]
}

@defproc[(numerator [x (rationalp x)]) t]{
Returns the dividend of a rational number in lowest terms.
@examples[
#:eval the-evaluator
(numerator 4)
(numerator 6/7)
(numerator 4/8)
]
}

@defproc[(realfix [x t]) t]{
Coerces @scheme[x] to a real number. If @scheme[x] satisfies @scheme[(real/rationalp x)], then it returns the argument unchanged. Otherwise, returns 0.
@examples[
#:eval the-evaluator
(realfix 2/5)
(realfix (complex 3 2))
(realfix "5")
]
}

@defproc[(realpart [x (acl2-numberp x)]) t]{
Returns the real part of a complex number.
@examples[
#:eval the-evaluator
(realpart (complex 3 2))
(realpart 1/2)
]
}

@defproc[(rem [i (real/rationalp i)] [j (and (real/rationalp j) (not (eql j 0)))]) t]{
Calculates the remainder of @scheme[(/ i j)] using @scheme[truncate].
@examples[
#:eval the-evaluator
(rem 4 2)
(rem 8 3)
]
}

@defproc[(rfix [x t]) t]{
Coerces @scheme[x] into a rational number. If @scheme[x] is a rational number, then it returns @scheme[x] unchanged. Otherwise, it returns 0.
@examples[
#:eval the-evaluator
(rfix 2/5)
(rfix (complex 3 2))
(rfix "5")
]
}

@defproc[(round [i (real/rationalp i)] [j (real/rationalp j)]) t]{
Rounds @scheme[(/ i j)] to the nearest integer. When the quotient is exactly halfway between to integers, it rounds to the even one.
@examples[
#:eval the-evaluator
(round 4 2)
(round 3 2)
(round 5 2)
(round 4 3)
]
}

@defproc[(signum [x (real/rationalp x)]) t]{
Returns 0 if @scheme[x] is 0, -1 if it is negative, and 1 if it is positive.
@examples[
#:eval the-evaluator
(signum 5)
(signum 0)
(signum -5)
]
}

@defproc[(truncate [i (real/rationalp i)] [j (and (real/rationalp j) (not (eql j 0)))]) t]{
Computes @scheme[(/ i j)] and rounds down to the nearest integer.
@examples[
#:eval the-evaluator
(truncate 5 2)
(truncate 4 2)
(truncate 19 10)
(truncate 1 10)
]
}

@defproc[(unary-- [x (acl2-numberp x)]) t]{
Computes the negative of the input. 
@examples[
#:eval the-evaluator
(unary-- 5)
(unary-- -5)
(unary-- (complex 1 -2))
]
}

@defproc[(unary-/ [x (and (acl2-numberp x) (not (eql x 0)))]) t]{
Computes the reciprocal of the input.
@examples[
#:eval the-evaluator
(unary-/ 5)
(unary-/ 1/5)
(unary-/ (complex 1 2))
]
}