1 ;; -*- Mode: Lisp; Package: Maxima; Syntax: Common-Lisp; Base: 10 -*- ;;;;
2 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3 ;;; The data in this file contains enhancments. ;;;;;
5 ;;; Copyright (c) 1984,1987 by William Schelter,University of Texas ;;;;;
6 ;;; All rights reserved ;;;;;
7 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
8 ;;; (c) Copyright 1982 Massachusetts Institute of Technology ;;;
9 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13 (macsyma-module compar
)
15 (load-macsyma-macros mrgmac
)
17 (declare-top (special success $props
))
19 (defvar *debug-compar
* nil
20 "Enables debugging code for this file.")
22 (defvar %initiallearnflag
)
24 (defvar $context
'$global
25 "Whenever a user assumes a new fact, it is placed in the context
26 named as the current value of the variable CONTEXT. Similarly, FORGET
27 references the current value of CONTEXT. To add or DELETE a fact from a
28 different context, one must bind CONTEXT to the intended context and then
29 perform the desired additions or deletions. The context specified by the
30 value of CONTEXT is automatically activated. All of MACSYMA's built-in
31 relational knowledge is contained in the default context GLOBAL.")
33 (defvar $contexts
'((mlist) $global
)
34 "A list of the currently active contexts.")
36 (defvar $activecontexts
'((mlist))
37 "A list of the currently activated contexts")
39 (defmvar sign-imag-errp t
40 "If T errors out in case COMPAR meets up with an imaginary quantity.
41 If NIL THROWs in that case."
44 (defmvar complexsign nil
45 "If T, COMPAR attempts to work in a complex mode.
46 This scheme is only very partially developed at this time."
49 (defvar *complexsign
* nil
50 "If T, COMPAR works in a complex mode.")
52 (defmvar $prederror nil
)
53 (defmvar $signbfloat t
)
56 (defmvar $assume_pos nil
)
57 (defmvar $assume_pos_pred nil
)
59 (defmvar factored nil
)
61 ;; The *LOCAL-SIGNS* variable contains a list of facts that are local to the
62 ;; current evaluation. These are stored in the assume database (in the global
63 ;; context) by asksign1 when the user answers questions. A "top-level"
64 ;; evaluation is run by MEVAL* and that function calls CLEARSIGN when it
65 ;; finishes to discard them.
66 (defmvar *local-signs
* nil
)
75 ;; Remove this (nil'ed out) function after a while. We should be
76 ;; using POWER instead of POW.
78 (defmacro pow
(&rest x
)
82 (simplify (cons '(mtimes) l
)))
87 (do ((x (cdr x
) (cdr x
))
90 (incf sz
(1+ (conssize (car x
)))))))
92 ;;; Functions for creating, activating, manipulating, and killing contexts
94 ;;; This "turns on" a context, making its facts visible.
96 (defmfun $activate
(&rest args
)
98 (cond ((not (symbolp c
)) (nc-err '$activate c
))
99 ((member c
(cdr $activecontexts
) :test
#'eq
))
100 ((member c
(cdr $contexts
) :test
#'eq
)
101 (setq $activecontexts
(mcons c $activecontexts
))
103 (t (merror (intl:gettext
"activate: no such context ~:M") c
))))
106 ;;; This "turns off" a context, keeping the facts, but making them invisible
108 (defmfun $deactivate
(&rest args
)
110 (cond ((not (symbolp c
)) (nc-err '$deactivate c
))
111 ((member c
(cdr $contexts
) :test
#'eq
)
112 (setq $activecontexts
($delete c $activecontexts
))
114 (t (merror (intl:gettext
"deactivate: no such context ~:M") c
))))
117 ;;; This function prints out a list of the facts in the specified context.
118 ;;; No argument implies the current context.
120 (defmfun $facts
(&optional
(ctxt $context
))
121 (if (member ctxt
(cdr $contexts
))
127 (do ((l (zl-get con
'data
) (cdr l
))
130 ((null l
) (cons '(mlist) nl
))
131 (when (visiblep (car l
))
132 (setq u
(intext (caaar l
) (cdaar l
)))
133 (unless (memalike u nl
)
136 ;; Look up facts from the database which contain expr. expr can be a symbol or
137 ;; a more general expression.
139 (labels ((among (x l
)
144 (do ((ll (cdr l
) (cdr ll
)))
146 (if (among x
(car ll
)) (return t
)))))))
147 (do ((facts (cdr ($facts $context
)) (cdr facts
))
149 ((null facts
) (return (cons '(mlist) (reverse ans
))))
150 (when (or (among expr
(cadar facts
))
151 (among expr
(caddar facts
)))
152 (push (car facts
) ans
)))))
154 (defun intext (rel body
)
155 (setq body
(mapcar #'doutern body
))
156 (cond ((eq 'kind rel
) (cons '($kind
) body
))
157 ((eq 'par rel
) (cons '($par
) body
))
158 ((eq 'mgrp rel
) (cons '(mgreaterp) body
))
159 ((eq 'mgqp rel
) (cons '(mgeqp) body
))
160 ((eq 'meqp rel
) (cons '($equal
) body
))
161 ((eq 'mnqp rel
) (list '(mnot) (cons '($equal
) body
)))))
163 (defprop $context asscontext assign
)
165 ;;; This function switches contexts, creating one if necessary.
167 (defun asscontext (xx y
)
168 (declare (ignore xx
))
169 (cond ((not (symbolp y
)) (nc-err "context assignment" y
))
170 ((member y $contexts
:test
#'eq
) (setq context y $context y
))
171 (t ($newcontext y
))))
173 ;;; This function actually creates a context whose subcontext is $GLOBAL.
174 ;;; It also switches contexts to the newly created one.
175 ;;; If no argument supplied, then invent a name via gensym and use that.
177 (defmfun $newcontext
(&rest args
)
179 ($newcontext
($gensym
"context")) ;; make up a name and try again
180 (if (> (length args
) 1)
181 (merror "newcontext: found more than one argument.")
182 (let ((x (first args
)))
184 ((not (symbolp x
)) (nc-err '$newcontext x
))
185 ((member x $contexts
:test
#'eq
)
186 (mtell (intl:gettext
"newcontext: context ~M already exists.") x
) nil
)
188 (setq $contexts
(mcons x $contexts
))
189 (putprop x
'($global
) 'subc
)
190 (setq context x $context x
)))))))
192 ;;; This function creates a supercontext. If given one argument, it
193 ;;; makes the current context be the subcontext of the argument. If
194 ;;; given more than one argument, the first is assumed the name of the
195 ;;; supercontext and the rest are the subcontexts.
196 ;;; If no arguments supplied, then invent a name via gensym and use that.
198 (defmfun $supcontext
(&rest x
)
199 (cond ((null x
) ($supcontext
($gensym
"context"))) ;; make up a name and try again
200 ((caddr x
) (merror (intl:gettext
"supcontext: found more than two arguments.")))
201 ((not (symbolp (car x
))) (nc-err '$supcontext
(car x
)))
202 ((member (car x
) $contexts
:test
#'eq
)
203 (merror (intl:gettext
"supcontext: context ~M already exists.") (car x
)))
204 ((and (cadr x
) (not (member (cadr x
) $contexts
:test
#'eq
)))
205 (merror (intl:gettext
"supcontext: no such context ~M") (cadr x
)))
206 (t (setq $contexts
(mcons (car x
) $contexts
))
207 (putprop (car x
) (ncons (or (cadr x
) $context
)) 'subc
)
208 (setq context
(car x
) $context
(car x
)))))
210 ;;; This function kills a context or a list of contexts
212 (defmfun $killcontext
(&rest args
)
216 (nc-err '$killcontext c
)))
217 (if (and (= (length args
) 1) (eq (car args
) '$global
))
221 (defun killallcontexts ()
222 (mapcar #'killcontext
(cdr $contexts
))
223 (setq $context
'$initial context
'$initial current
'$initial
224 $contexts
'((mlist) $initial $global
) dobjects
())
226 ;;conmark, conunmrk, conindex, connumber, and contexts
227 ;;concern garbage-collectible contexts, and so we're
228 ;;better off not resetting them.
229 (defprop $global
1 cmark
) (defprop $initial
1 cmark
)
230 (defprop $initial
($global
) subc
))
232 (defun killcontext (x)
233 (cond ((not (member x $contexts
:test
#'eq
))
234 (mtell (intl:gettext
"killcontext: no such context ~M.") x
))
235 ((eq x
'$global
) '$global
)
237 (mapc #'remov
(zl-get '$initial
'data
))
238 (remprop '$initial
'data
)
240 ((and (not (eq $context x
)) (contextmark) (< 0 (zl-get x
'cmark
)))
241 (mtell (intl:gettext
"killcontext: context ~M is currently active.") x
))
242 (t (if (member x $activecontexts
)
243 ;; Context is on the list of active contexts. The test above
244 ;; checks for active contexts, but it seems not to work in all
245 ;; cases. So deactivate the context at this place to remove it
246 ;; from the list of active contexts before it is deleted.
248 (setq $contexts
($delete x $contexts
))
249 (cond ((and (eq x $context
)
250 (equal ;;replace eq ?? wfs
251 (zl-get x
'subc
) '($global
)))
252 (setq $context
'$initial
)
253 (setq context
'$initial
))
255 (setq $context
(car (zl-get x
'subc
)))
256 (setq context
(car (zl-get x
'subc
)))))
261 (merror (intl:gettext
"~M: context name must be a symbol; found ~M") fn x
))
263 ;; Simplification and evaluation of boolean expressions
265 ;; Simplification of boolean expressions:
267 ;; and and or are declared nary. The sole effect of this is to allow Maxima to
268 ;; flatten nested expressions, e.g., a and (b and c) => a and b and c
269 ;; (The nary declaration does not make and and or commutative, and and and or
270 ;; are not otherwise declared commutative.)
272 ;; and: if any argument simplifies to false, return false
273 ;; otherwise omit arguments which simplify to true and simplify others
274 ;; if only one argument remains, return it
275 ;; if none remain, return true
277 ;; or: if any argument simplifies to true, return true
278 ;; otherwise omit arguments which simplify to false and simplify others
279 ;; if only one argument remains, return it
280 ;; if none remain, return false
282 ;; not: if argument simplifies to true / false, return false / true
283 ;; otherwise reverse sense of comparisons (if argument is a comparison)
284 ;; otherwise return not <simplified argument>
286 ;; Evaluation (MEVAL) of boolean expressions:
287 ;; same as simplification except evaluating (MEVALP) arguments instead of simplifying
288 ;; When prederror = true, complain if expression evaluates to something other than T / NIL
289 ;; (otherwise return unevaluated boolean expression)
291 ;; Evaluation (MEVALP) of boolean expressions:
292 ;; same as simplification except evaluating (MEVALP) arguments instead of simplifying
293 ;; When prederror = true, complain if expression evaluates to something other than T / NIL
294 ;; (otherwise return unevaluated boolean expression)
296 ;; Simplification of "is" expressions:
297 ;; if argument simplifies to true/false, return true/false
298 ;; otherwise return is (<simplified argument>)
300 ;; Evaluation of "is" expressions:
301 ;; if argument evaluates to true/false, return true/false
302 ;; otherwise return unknown if prederror = false, else trigger an error
304 ;; Simplification of "maybe" expressions:
305 ;; if argument simplifies to true/false, return true/false
306 ;; otherwise return maybe (<simplified expression>)
308 ;; Evaluation of "maybe" expressions:
309 ;; if argument evaluates to true/false, return true/false
310 ;; otherwise return unknown
312 (defprop $is simp-$is operators
)
313 (defprop %is simp-$is operators
)
314 (defprop $maybe simp-$is operators
)
315 (defprop %maybe simp-$is operators
)
317 ; I'VE ASSUMED (NULL Z) => SIMPLIFIY ARGUMENTS
318 ; SAME WITH SIMPCHECK (SRC/SIMP.LISP)
319 ; SAME WITH TELLSIMP-GENERATED SIMPLIFICATION FUNCTIONS
320 ; SAME WITH SIMPLIFICATION OF %SIN
321 ; PRETTY SURE I'VE SEEN OTHER EXAMPLES AS WELL
322 ; Z SEEMS TO SIGNIFY "ARE THE ARGUMENTS SIMPLIFIED YET"
324 (defun maybe-simplifya (x z
)
325 (if z x
(simplifya x z
)))
327 (defun maybe-simplifya-protected (x z
)
328 (let ((errcatch t
) ($errormsg nil
))
329 (declare (special errcatch $errormsg
))
330 (ignore-errors (maybe-simplifya x z
) x
)))
332 (defun simp-$is
(x yy z
)
333 (declare (ignore yy
))
334 (let ((a (maybe-simplifya (cadr x
) z
)))
335 (if (or (eq a t
) (eq a nil
))
337 `((,(caar x
) simp
) ,a
))))
340 (unless (= 1 (length (rest form
)))
341 (merror (intl:gettext
"is() expects a single argument. Found ~A")
342 (length (rest form
))))
343 (destructuring-bind (answer patevalled
)
344 (mevalp1 (cadr form
))
345 (cond ((member answer
'(t nil
) :test
#'eq
) answer
)
346 ;; I'D RATHER HAVE ($PREDERROR ($THROW `(($PREDERROR) ,PATEVALLED))) HERE
347 ($prederror
(pre-err patevalled
))
350 (defmspec $maybe
(form)
351 (let* ((pat (cadr form
))
352 (x (let (($prederror nil
)) (mevalp1 pat
)))
354 (if (member ans
'(t nil
) :test
#'eq
)
359 (let (($prederror t
))
362 ; The presence of OPERS tells SIMPLIFYA to call OPER-APPLY,
363 ; which calls NARY1 to flatten nested "and" and "or" expressions
364 ; (due to $NARY property of MAND and MOR, declared elsewhere).
366 (putprop 'mand t
'opers
)
367 (putprop 'mor t
'opers
)
369 (putprop 'mnot
'simp-mnot
'operators
)
370 (putprop 'mand
'simp-mand
'operators
)
371 (putprop 'mor
'simp-mor
'operators
)
373 (defun simp-mand (x yy z
)
374 (declare (ignore yy
))
375 (do ((l (cdr x
) (cdr l
))
379 (cond ((= (length simplified
) 0) t
)
380 ((= (length simplified
) 1) (car simplified
))
381 (t (cons '(mand simp
) (reverse simplified
)))))
382 (setq a
(maybe-simplifya (car l
) z
))
383 (cond ((null a
) (return nil
))
384 ((eq a
'$unknown
) (unless (member '$unknown simplified
:test
#'eq
) (push a simplified
)))
385 ((not (member a
'(t nil
) :test
#'eq
)) (push a simplified
)))))
387 (defun simp-mor (x yy z
)
388 (declare (ignore yy
))
389 (do ((l (cdr x
) (cdr l
))
393 (cond ((= (length simplified
) 0) nil
)
394 ((= (length simplified
) 1) (car simplified
))
395 (t (cons '(mor simp
) (reverse simplified
)))))
396 (setq a
(maybe-simplifya (car l
) z
))
397 (cond ((eq a t
) (return t
))
398 ((eq a
'$unknown
) (unless (member '$unknown simplified
:test
#'eq
) (push a simplified
)))
399 ((not (member a
'(t nil
) :test
#'eq
)) (push a simplified
)))))
401 ; ALSO CUT STUFF ABOUT NOT EQUAL => NOTEQUAL AT TOP OF ASSUME
403 (defun simp-mnot (x yy z
)
404 (declare (ignore yy
))
405 (let ((arg (maybe-simplifya (cadr x
) z
)))
407 (cond ((or (eq arg t
) (eq arg
'$true
))
409 ((or (eq arg nil
) (eq arg
'$false
))
413 (t `((mnot simp
) ,arg
)))
414 (let ((arg-op (caar arg
)) (arg-arg (cdr arg
)))
415 ;;(setq arg-arg (mapcar #'(lambda (a) (maybe-simplifya a z)) arg-arg))
416 (cond ((eq arg-op
'mlessp
)
417 (simplify `((mgeqp) ,@arg-arg
)))
419 (simplify `((mgreaterp) ,@arg-arg
)))
421 (simplify `((mnotequal) ,@arg-arg
)))
423 (simplify `(($notequal
) ,@arg-arg
)))
424 ((eq arg-op
'mnotequal
)
425 (simplify `((mequal) ,@arg-arg
)))
426 ((eq arg-op
'$notequal
)
427 (simplify `(($equal
) ,@arg-arg
)))
429 (simplify `((mlessp) ,@arg-arg
)))
430 ((eq arg-op
'mgreaterp
)
431 (simplify `((mleqp) ,@arg-arg
)))
434 ;; Distribute negation over conjunction and disjunction;
435 ;; analogous to '(- (a + b)) --> - a - b.
437 (let ((L (mapcar #'(lambda (e) `((mnot) ,e
)) arg-arg
)))
438 (simplifya `((mor) ,@L
) nil
)))
440 (let ((L (mapcar #'(lambda (e) `((mnot) ,e
)) arg-arg
)))
441 (simplifya `((mand) ,@L
) nil
)))
442 (t `((mnot simp
) ,arg
)))))))
445 ;; The translator depends on some stuff in here.
446 ;; Check it out in the transl module ACALL before proceeding.
449 (let* ((x (mevalp1 pat
))
451 (patevalled (cadr x
)))
452 (cond ((member ans
'(t ()) :test
#'eq
) ans
)
453 ;; I'D RATHER HAVE ($PREDERROR ($THROW `(($PREDERROR) ,PATEVALLED))) HERE
454 ($prederror
(pre-err patevalled
))
455 (t (or patevalled ans
)))))
458 (let (patevalled ans
)
460 (cond ((and (not (atom pat
))
461 (member (caar pat
) '(mnot mand mor
) :test
#'eq
))
462 (cond ((eq 'mnot
(caar pat
)) (is-mnot #'mevalp
(cadr pat
)))
463 ((eq 'mand
(caar pat
)) (is-mand #'mevalp
(cdr pat
)))
464 (t (is-mor #'mevalp
(cdr pat
)))))
465 ((atom (setq patevalled
(specrepcheck (meval pat
))))
467 ((member (caar patevalled
) '(mnot mand mor
) :test
#'eq
)
468 (return-from mevalp1
(mevalp1 patevalled
)))
473 (caddr patevalled
)))))
474 (list ans patevalled
)))
476 (defun mevalp2 (patevalled pred arg1 arg2
)
477 (cond ((eq 'mequal pred
) (like arg1 arg2
))
478 ((eq '$equal pred
) (meqp arg1 arg2
))
479 ((eq 'mnotequal pred
) (not (like arg1 arg2
)))
480 ((eq '$notequal pred
) (mnqp arg1 arg2
))
481 ((eq 'mgreaterp pred
) (mgrp arg1 arg2
))
482 ((eq 'mlessp pred
) (mgrp arg2 arg1
))
483 ((eq 'mgeqp pred
) (mgqp arg1 arg2
))
484 ((eq 'mleqp pred
) (mgqp arg2 arg1
))
485 (t (isp (munformat patevalled
)))))
488 (merror (intl:gettext
"Unable to evaluate predicate ~M") pat
))
490 (defun is-mnot (pred-eval pred
)
491 (setq pred
(funcall pred-eval pred
))
492 (cond ((eq t pred
) nil
)
494 (t (pred-reverse pred
))))
496 (defun pred-reverse (pred)
499 (defun is-mand (pred-eval pl
)
502 ((null pl
) (cond ((null npl
))
503 ((null (cdr npl
)) (car npl
))
504 (t (cons '(mand) (nreverse npl
)))))
505 (setq dummy
(funcall pred-eval
(car pl
)) pl
(cdr pl
))
507 ((null dummy
) (return nil
))
508 (t (push dummy npl
)))))
510 (defun is-mor (pred-eval pl
)
513 ((null pl
) (cond ((null npl
) nil
)
514 ((null (cdr npl
)) (car npl
))
515 (t (cons '(mor) (nreverse npl
)))))
516 (setq dummy
(funcall pred-eval
(car pl
)) pl
(cdr pl
))
517 (cond ((eq t dummy
) (return t
))
519 (t (push dummy npl
)))))
521 (defmspec $assume
(x)
523 (do ((nl)) ((null x
) (cons '(mlist) (nreverse nl
)))
524 (cond ((atom (car x
)) (push (assume (meval (car x
))) nl
))
525 ((eq 'mand
(caaar x
))
526 (mapc #'(lambda (l) (push (assume (meval l
)) nl
))
528 ((eq 'mnot
(caaar x
))
529 (push (assume (meval (pred-reverse (cadar x
)))) nl
))
531 (merror (intl:gettext
"assume: argument cannot be an 'or' expression; found ~M") (car x
)))
532 ((eq (caaar x
) 'mequal
)
533 (merror (intl:gettext
"assume: argument cannot be an '=' expression; found ~M~%assume: maybe you want 'equal'.") (car x
)))
534 ((eq (caaar x
) 'mnotequal
)
535 (merror (intl:gettext
"assume: argument cannot be a '#' expression; found ~M~%assume: maybe you want 'not equal'.") (car x
)))
536 (t (push (assume (meval (car x
))) nl
)))
540 (if (and (not (atom pat
))
541 (eq (caar pat
) 'mnot
)
542 (eq (caaadr pat
) '$equal
))
543 (setq pat
`(($notequal
) ,@(cdadr pat
))))
544 (let ((dummy (let ($assume_pos
) (car (mevalp1 pat
)))))
545 (cond ((eq dummy t
) '$redundant
)
546 ((null dummy
) '$inconsistent
)
547 ((atom dummy
) '$meaningless
)
550 (defun learn (pat flag
)
552 ;; Check for abs function in pattern.
554 (learn-abs pat flag
)))
555 ;; Check for constant expression in pattern.
557 (learn-numer pat flag
)))
558 ((zl-get (caar pat
) (if flag
'learn
'unlearn
))
559 (funcall (zl-get (caar pat
) (if flag
'learn
'unlearn
)) pat
))
560 ((eq (caar pat
) 'mgreaterp
) (daddgr flag
(sub (cadr pat
) (caddr pat
))))
561 ((eq (caar pat
) 'mgeqp
) (daddgq flag
(sub (cadr pat
) (caddr pat
))))
562 ((member (caar pat
) '(mequal $equal
) :test
#'eq
)
563 (daddeq flag
(sub (cadr pat
) (caddr pat
))))
564 ((member (caar pat
) '(mnotequal $notequal
) :test
#'eq
)
565 (daddnq flag
(sub (cadr pat
) (caddr pat
))))
566 ((eq (caar pat
) 'mleqp
) (daddgq flag
(sub (caddr pat
) (cadr pat
))))
567 ((eq (caar pat
) 'mlessp
) (daddgr flag
(sub (caddr pat
) (cadr pat
))))
568 (flag (true* (munformat pat
)))
571 ((eq (caar pat
) '$kind
)
572 (unkind (second pat
) (third pat
)))
573 (t (untrue (munformat pat
))))
576 ;;; When abs(x)<a is in the pattern, where a is a positive expression,
577 ;;; then learn x<a and -x<a too. The additional facts are put into the context
578 ;;; '$learndata, if the current context is user context 'initial
580 (defun learn-abs (pat flag
)
582 (when (and (setq tmp
(isinop pat
'mabs
))
583 (or (and (member (caar pat
) '(mlessp mleqp
))
584 (isinop (cadr pat
) 'mabs
)
585 (member ($sign
(caddr pat
)) '($pos $pz
)))
586 (and (member (caar pat
) '(mgreaterp mgeqp
))
587 (member ($sign
(cadr pat
)) '($pos $pz
))
588 (isinop (caddr pat
) 'mabs
))))
589 (let ((oldcontext context
))
590 (if (eq oldcontext
'$initial
)
591 (asscontext nil
'$learndata
)) ; switch to context '$learndata
592 ; learn additional facts
593 (learn ($substitute
(cadr tmp
) tmp pat
) flag
)
594 (learn ($substitute
(mul -
1 (cadr tmp
)) tmp pat
) flag
)
595 (when (eq oldcontext
'$initial
)
596 (asscontext nil oldcontext
) ; switch back to context on entry
597 ($activate
'$learndata
)))) ; context '$learndata is active
600 ;;; The value of a constant expression which can be numerically evaluated is
601 ;;; put into the context '$learndata.
603 (defun learn-numer (pat flag
)
604 (let (dum expr patnew
)
605 (do ((x (cdr pat
) (cdr x
)))
606 ((null x
) (setq patnew
(reverse patnew
)))
607 (setq dum
(constp (car x
))
609 (cond ((or (numberp (car x
))
613 (setq dum
($bfloat
(car x
)))
617 (if (and (setq dum
(numer (car x
)))
620 ((and (member dum
'(numer symbol
) :test
#'eq
)
622 (setq dum
(numer (car x
)))
627 (< (abs dum
) 1.0e-6))))))
629 (and (setq dum
($bfloat
(car x
)))
632 (setq patnew
(cons expr patnew
)))
633 (setq patnew
(cons (car pat
) patnew
))
634 (when (and (not (alike (cdr pat
) (cdr patnew
)))
635 (or (not (mnump (cadr patnew
))) ; not both sides of the
636 (not (mnump (caddr patnew
))))) ; relation can be number
637 (let ((oldcontext $context
))
638 (if (eq oldcontext
'$initial
)
639 (asscontext nil
'$learndata
)) ; switch to context '$learndata
640 (learn patnew flag
) ; learn additional fact
641 (when (eq oldcontext
'$initial
)
642 (asscontext nil oldcontext
) ; switch back to context on entry
643 ($activate
'$learndata
)))) ; context '$learndata is active
646 (defmspec $forget
(x)
649 ((null x
) (cons '(mlist) (nreverse nl
)))
650 (cond ((atom (car x
)) (push (forget (meval (car x
))) nl
))
651 ((eq 'mand
(caaar x
))
652 (mapc #'(lambda (l) (push (forget (meval l
)) nl
)) (cdar x
)))
653 ((eq 'mnot
(caaar x
))
654 (push (forget (meval (pred-reverse (cadar x
)))) nl
))
656 (merror (intl:gettext
"forget: argument cannot be an 'or' expression; found ~M") (car x
)))
657 (t (push (forget (meval (car x
))) nl
)))
662 (cons '(mlist simp
) (mapcar #'forget1
(cdr pat
))))
666 (cond ((and (not (atom pat
))
667 (eq (caar pat
) 'mnot
)
668 (eq (caaadr pat
) '$equal
))
669 (setq pat
`(($notequal
) ,@(cdadr pat
)))))
672 (defun restore-facts (factl) ; used by SAVE
674 (cond ((eq (caar fact
) '$kind
)
675 (declarekind (cadr fact
) (caddr fact
))
676 (add2lnc (getop (cadr fact
)) $props
))
677 ((eq (caar fact
) '$par
))
680 (defmacro compare
(a b
)
681 `(sign1 (sub* ,a
,b
)))
689 (defmspec mand
(form)
690 (setq form
(cdr form
))
691 (do ((l form
(cdr l
))
695 (cond ((= (length unevaluated
) 0) t
)
696 ((= (length unevaluated
) 1) (car unevaluated
))
697 (t (cons '(mand) (reverse unevaluated
)))))
698 (setq x
(mevalp (car l
)))
699 (cond ((null x
) (return nil
))
700 ((not (member x
'(t nil
) :test
#'eq
)) (push x unevaluated
)))))
703 (setq form
(cdr form
))
704 (do ((l form
(cdr l
))
708 (cond ((= (length unevaluated
) 0) nil
)
709 ((= (length unevaluated
) 1) (car unevaluated
))
710 (t (cons '(mor) (reverse unevaluated
)))))
711 (setq x
(mevalp (car l
)))
712 (cond ((eq x t
) (return t
))
713 ((not (member x
'(t nil
) :test
#'eq
)) (push x unevaluated
)))))
715 (defmspec mnot
(form)
716 (setq form
(cdr form
))
717 (let ((x (mevalp (car form
))))
718 (if (member x
'(t nil
) :test
#'eq
)
722 ;;;Toplevel functions- $askequal, $asksign, and $sign.
723 ;;;Switches- LIMITP If TRUE $ASKSIGN and $SIGN will look for special
724 ;;; symbols such as EPSILON, $INF, $MINF and attempt
725 ;;; to do the correct thing. In addition calls to
726 ;;; $REALPART and $IMAGPART are made to assure that
727 ;;; the expression is real.
729 ;;; if NIL $ASKSIGN and $SIGN assume the expression
730 ;;; given is real unless it contains an $%I, in which
731 ;;; case they call $RECTFORM.
735 (defmfun $askequal
(a b
)
736 (let ((answer (meqp (sratsimp a
) (sratsimp b
)))) ; presumably handles mbags and extended reals.
737 (cond ((eq answer t
) '$yes
)
738 ((eq answer nil
) '$no
)
740 (setq answer
(retrieve `((mtext) ,(intl:gettext
"Is ") ,a
,(intl:gettext
" equal to ") ,b
,(intl:gettext
"?")) nil
))
741 (cond ((member answer
'($no |$n| |$N|
) :test
#'eq
)
744 ((member answer
'($yes |$y| |$Y|
) :test
#'eq
)
748 (mtell (intl:gettext
"Acceptable answers are yes, y, Y, no, n, N. ~%"))
749 ($askequal a b
)))))))
751 (defmfun $asksign
(exp)
752 (let (sign minus odds evens factored
)
753 (asksign01 (cond (limitp (restorelim exp
))
754 ((among '$%i exp
) ($rectform exp
))
757 (defun asksign-p-or-n (e)
758 (unwind-protect (prog2
759 (assume `(($notequal
) ,e
0))
761 (forget `(($notequal
) ,e
0))))
764 (let ((e (sign-prep a
)))
765 (cond ((eq e
'$pnz
) '$pnz
)
766 ((member (setq e
(asksign1 e
)) '($pos $neg
) :test
#'eq
) e
)
767 (limitp (eps-sign a
))
770 ;; csign returns t if x appears to be complex.
771 ;; Else, it returns the sign.
773 (or (not (free x
'$%i
))
774 (let (sign-imag-errp limitp
) (catch 'sign-imag-err
($sign x
)))))
776 ;;; $csign works like $sign but switches the sign-functions into a complex
777 ;;; mode. In complex mode complex and imaginary expressions give the results
778 ;;; imagarinary or complex.
781 (let ((*complexsign
* t
)
786 (let ((x (specrepcheck x
))
787 sign minus odds evens factored
)
788 (sign01 (cond (limitp (restorelim x
))
790 ;; No rectform in Complex mode. Rectform ask unnecessary
791 ;; questions about complex expressions and can not handle
792 ;; imaginary expressions completely. Thus $csign can not
793 ;; handle something like (1+%i)*(1-%i) which is real.
794 ;; After improving rectform, we can change this. (12/2008)
796 (format t
"~&$SIGN with ~A~%" x
))
798 ((not (free x
'$%i
)) ($rectform x
))
802 (let ((e (sign-prep a
)))
803 (cond ((eq e
'$pnz
) '$pnz
)
804 (t (setq e
(sign1 e
))
805 (if (and limitp
(eq e
'$zero
)) (eps-sign a
) e
)))))
807 ;;; Preparation for asking questions from DEFINT or LIMIT.
810 (destructuring-let (((rpart . ipart
) (trisplit x
)))
811 (cond ((and (equal (sratsimp ipart
) 0)
812 (free rpart
'$infinity
))
813 (setq x
(nmr (sratsimp rpart
)))
814 (if (free x
'prin-inf
)
816 ($limit x
'prin-inf
'$inf
'$minus
)))
817 (t '$pnz
))) ; Confess ignorance if COMPLEX.
820 ;; don't ask about internal variables created by gruntz
821 (defun has-int-symbols (e)
822 (cond ((and (symbolp e
) (get e
'internal
))
825 (t (or (has-int-symbols (car e
))
826 (has-int-symbols (cdr e
))))))
828 ;;; Do substitutions for special symbols.
830 (unless (free a
'$zeroa
) (setq a
($limit a
'$zeroa
0 '$plus
)))
831 (unless (free a
'$zerob
) (setq a
($limit a
'$zerob
0 '$minus
)))
832 (unless (free a
'z
**) (setq a
($limit a
'z
** 0 '$plus
)))
833 (unless (free a
'*z
*) (setq a
($limit a
'*z
* 0 '$plus
)))
834 (unless (free a
'epsilon
) (setq a
($limit a
'epsilon
0 '$plus
)))
837 ;;; Get the sign of EPSILON-like terms. Could be made MUCH hairier.
839 (let (temp1 temp2 temp3 free1 free2 free3 limitp
)
840 ;; unset limitp to prevent infinite recursion
841 (cond ((not (free b
'$zeroa
))
842 (setq temp1
(eps-coef-sign b
'$zeroa
)))
844 (cond ((not (free b
'$zerob
))
845 (setq temp2
(eps-coef-sign b
'$zerob
)))
847 (cond ((not (free b
'epsilon
))
848 (setq temp3
(eps-coef-sign b
'epsilon
)))
850 (cond ((and free1 free2 free3
) '$zero
)
851 ((or (not (null temp1
)) (not (null temp2
)) (not (null temp3
)))
852 (cond ((and (null temp1
) (null temp2
)) temp3
)
853 ((and (null temp2
) (null temp3
)) temp1
)
854 ((and (null temp1
) (null temp3
)) temp2
)
855 (t (merror (intl:gettext
"asksign: internal error."))))))))
857 (defun eps-coef-sign (exp epskind
)
858 (let ((eps-power ($lopow exp epskind
)) eps-coef
)
859 (cond ((and (not (equal eps-power
0))
860 (not (equal (setq eps-coef
(ratcoeff exp epskind eps-power
))
862 (eq (ask-integer eps-power
'$integer
) '$yes
))
863 (cond ((eq (ask-integer eps-power
'$even
) '$yes
)
865 ((eq (ask-integer eps-power
'$odd
) '$yes
)
866 (setq eps-coef
($sign eps-coef
))
867 (cond ((or (and (eq eps-coef
'$pos
)
868 (or (eq epskind
'epsilon
)
869 (eq epskind
'$zeroa
)))
870 (and (eq eps-coef
'$neg
)
871 (or (alike epskind
(mul2* -
1 'epsilon
))
872 (eq epskind
'$zerob
))))
875 (t (merror (intl:gettext
"sign or asksign: insufficient information.")))))
876 (t (let ((deriv (sdiff exp epskind
)) deriv-sign
)
877 (cond ((not (eq (setq deriv-sign
($sign deriv
)) '$zero
))
878 (total-sign epskind deriv-sign
))
880 (eq (let ((deriv (sdiff deriv epskind
)))
881 (setq deriv-sign
($sign deriv
)))
884 (t (merror (intl:gettext
"sign or asksign: insufficient data.")))))))))
886 ;;; The above code does a partial Taylor series analysis of something
887 ;;; that isn't a polynomial.
889 (defun total-sign (epskind factor-sign
)
890 (cond ((or (eq epskind
'$zeroa
) (eq epskind
'epsilon
))
891 (cond ((eq factor-sign
'$pos
) '$pos
)
892 ((eq factor-sign
'$neg
) '$neg
)
893 ((eq factor-sign
'$zero
) '$zero
)))
894 ((eq epskind
'$zerob
)
895 (cond ((eq factor-sign
'$pos
) '$neg
)
896 ((eq factor-sign
'$neg
) '$pos
)
897 ((eq factor-sign
'$zero
) '$zero
)))))
900 (setq x
($asksign x
))
901 (cond ((eq '$pos x
) '$positive
)
902 ((eq '$neg x
) '$negative
)
903 ((eq '$pnz x
) '$pnz
) ;COMPLEX expression encountered here.
906 (defun asksign1 ($askexp
)
908 (declare (special $radexpand
))
911 ((has-int-symbols $askexp
) '$pnz
)
912 ((member sign
'($pos $neg $zero $imaginary
) :test
#'eq
) sign
)
914 (let ((domain sign
) (squared nil
))
917 (setq $askexp
(lmul evens
)
921 (if minus
(setq sign
(flip sign
)))
923 (lmul (nconc odds
(mapcar #'(lambda (l) (power l
2)) evens
))))))
924 (setq sign
(cdr (assol $askexp
*local-signs
*)))
925 (ensure-sign $askexp domain squared
)))))
927 (defun match-sign (sgn domain expression squared
)
928 "If SGN makes sense for DOMAIN store the result (see ENSURE-SIGN) and return
929 it. Otherwise, return NIL. If SQUARED is true, we are actually looking for the
930 sign of the square, so any negative results are converted to positive."
931 ;; The entries in BEHAVIOUR are of the form
932 ;; (MATCH DOMAINS REGISTRAR SIGN SIGN-SQ)
934 ;; The algorithm goes as follows:
936 ;; Look for SGN in MATCH. If found, use REGISTRAR to store SIGN for the
937 ;; expression and then return SIGN if SQUARED is false or SIGN-SQ if it is
940 '((($pos |$P| |$p| $positive
) (nil $znz $pz $pn $pnz
) tdpos $pos $pos
)
941 (($neg |$N| |$n| $negative
) (nil $znz $nz $pn $pnz
) tdneg $neg $pos
)
942 (($zero |$Z| |$z|
0 0.0) (nil $znz $pz $nz $pnz
) tdzero $zero $zero
)
943 (($pn $nonzero $nz $nonz $non0
) ($znz
) tdpn $pn $pos
)))
944 (hit (find-if (lambda (bh)
945 (and (member sgn
(first bh
) :test
#'equal
)
946 (member domain
(second bh
) :test
#'eq
)))
949 (let ((registrar (third hit
))
950 (found-sign (if squared
(fifth hit
) (fourth hit
))))
951 (funcall registrar expression
)
953 (if minus
(flip found-sign
) found-sign
))))))
955 (defun ensure-sign (expr &optional domain squared
)
956 "Try to determine the sign of EXPR. If DOMAIN is not one of the special values
957 described below, we try to tell whether EXPR is positive, negative or zero. It
958 can be more specialised ($pz => positive or zero; $nz => negative or zero; $pn
959 => positive or negative; $znz => zero or nonzero).
961 If SQUARED is true, then we're actually interested in the sign of EXPR^2. As
962 such, a nonzero sign should be regarded as positive.
964 When calling ENSURE-SIGN, set the special variable SIGN to the best current
965 guess for the sign of EXPR. The function returns the sign, calls one of (TDPOS
966 TDNEG TDZERO TDPN) to store it, and also sets SIGN."
968 (let ((new-sign (match-sign sign domain expr squared
)))
969 (when new-sign
(return new-sign
)))
975 '(($znz
" zero or nonzero?")
976 ($pz
" positive or zero?")
977 ($nz
" negative or zero?")
978 ($pn
" positive or negative?"))))
979 " positive, negative or zero?"))
982 ;; During one evaluation phase asksign writes answers from the user into the
983 ;; global context '$initial. These facts are removed by clearsign after
984 ;; finishing the evaluation phase. clearsign is called from the top-level
985 ;; evaluation function meval*. The facts which have to be removed are stored
986 ;; in the global variable *local-signs*.
989 (let ((context '$initial
))
990 (dolist (cons-pair *local-signs
*)
991 (destructuring-bind (x . sgn
) cons-pair
993 ((eq '$pos sgn
) (daddgr nil x
))
994 ((eq '$neg sgn
) (daddgr nil
(neg x
)))
995 ((eq '$zero sgn
) (daddeq nil x
))
996 ((eq '$pn sgn
) (daddnq nil x
))
997 ((eq '$pz sgn
) (daddgq nil x
))
998 ((eq '$nz sgn
) (daddgq nil
(neg x
))))))
999 (setf *local-signs
* nil
)))
1002 (alike1 (specrepcheck x
) (specrepcheck y
)))
1004 (setf (get '$und
'sysconst
) t
)
1005 (setf (get '$ind
'sysconst
) t
)
1006 (setf (get '$zeroa
'sysconst
) t
)
1007 (setf (get '$zerob
'sysconst
) t
)
1009 ;; There have been some conversations about NaN on the list, but
1010 ;; the issue hasn't been settled.
1012 (defvar indefinites
`($und $ind
))
1014 ;; Other than sums, products, and lambda forms, meqp knows nothing
1015 ;; about dummy variables. Because of the way niceindices chooses names
1016 ;; for the sum indices, it's necessary to locally assign a new value to
1019 (defun meqp-by-csign (z a b
)
1020 (let (($niceindicespref
`((mlist) ,(gensym) ,(gensym) ,(gensym))))
1021 (setq z
($niceindices z
))
1022 (setq z
(if ($constantp z
) ($rectform z
) (sratsimp z
)))
1023 (let ((sgn ($csign z
))
1024 (dunno `(($equal
) ,a
,b
)))
1025 (cond ((eq '$zero sgn
) t
)
1026 ((memq sgn
'($pos $neg $pn
)) nil
)
1028 ;; previously checked also for (linearp z '$%i))
1029 ((memq sgn
'($complex $imaginary
))
1030 ;; We call trisplit here, which goes back to general evaluation and
1031 ;; could cause an infinite recursion. To make sure that doesn't
1032 ;; happen, use the with-safe-recursion macro.
1034 (with-safe-recursion meqp-by-csign z
1035 (let* ((ri-parts (trisplit z
))
1036 (rsgn ($csign
(car ri-parts
)))
1037 (isgn ($csign
(cdr ri-parts
))))
1038 (cond ((and (eq '$zero rsgn
)
1039 (eq '$zero isgn
)) t
)
1041 ((or (memq rsgn
'($neg $pos $pn
))
1042 (memq isgn
'($neg $pos $pn
))) nil
)
1045 (unsafe-recursion () dunno
)))
1049 ;; For each fact of the form equal(a,b) in the active context, do e : ratsubst(b,a,e).
1051 (defun equal-facts-simp (e)
1052 (let ((f (margs ($facts
))))
1054 (if (op-equalp fi
'$equal
)
1055 (setq e
($ratsubst
(nth 2 fi
) (nth 1 fi
) e
))))))
1057 (defun maxima-declared-arrayp (x)
1061 (get (mget x
'array
) 'array
)))
1063 (defun maxima-undeclared-arrayp (x)
1067 (get (mget x
'hashar
) 'array
)))
1070 ;; Check for some particular types before falling into the general case.
1072 (and (stringp b
) (equal a b
)))
1075 (and (arrayp b
) (array-meqp a b
)))
1077 ((maxima-declared-arrayp a
)
1078 (and (maxima-declared-arrayp b
) (maxima-declared-array-meqp a b
)))
1079 ((maxima-declared-arrayp b
) nil
)
1080 ((maxima-undeclared-arrayp a
)
1081 (and (maxima-undeclared-arrayp b
) (maxima-undeclared-array-meqp a b
)))
1082 ((maxima-undeclared-arrayp b
) nil
)
1085 (setq a
(specrepcheck a
))
1086 (setq b
(specrepcheck b
))
1087 (cond ((or (like a b
)) (not (member a indefinites
)))
1088 ((or (member a indefinites
) (member b indefinites
)
1089 (member a infinities
) (member b infinities
)) nil
)
1090 ((and (symbolp a
) (or (eq t a
) (eq nil a
) (get a
'sysconst
))
1091 (symbolp b
) (or (eq t b
) (eq nil b
) (get b
'sysconst
))) nil
)
1092 ((or (mbagp a
) (mrelationp a
) (mbagp b
) (mrelationp b
))
1093 (cond ((and (or (and (mbagp a
) (mbagp b
)) (and (mrelationp a
) (mrelationp b
)))
1094 (eq (mop a
) (mop b
)) (= (length (margs a
)) (length (margs b
))))
1095 (setq z
(list-meqp (margs a
) (margs b
)))
1096 (if (or (eq z t
) (eq z nil
)) z
`(($equal
) ,a
,b
)))
1098 ((and (op-equalp a
'lambda
) (op-equalp b
'lambda
)) (lambda-meqp a b
))
1099 (($setp a
) (set-meqp a b
))
1100 ;; 0 isn't in the range of an exponential function.
1101 ((or (and (mexptp a
) (not (eq '$minf
(third a
))) (zerop1 b
) (eq t
(mnqp (second a
) 0)))
1102 (and (mexptp b
) (not (eq '$minf
(third b
))) (zerop1 a
) (eq t
(mnqp (second b
) 0))))
1105 ;; DCOMPARE emits new stuff (via DINTERNP) into the assume database.
1106 ;; Let's avoid littering the database with numbers.
1107 ((and (mnump a
) (mnump b
)) (zerop1 (sub a b
)))
1109 ;; lookup in assumption database
1110 ((and (dcompare a b
) (eq '$zero sign
))) ; dcompare sets sign
1111 ((memq sign
'($pos $neg $pn
)) nil
)
1113 ;; if database lookup failed, apply all equality facts
1114 (t (meqp-by-csign (equal-facts-simp (sratsimp (sub a b
))) a b
)))))))
1116 ;; Two arrays are equal (according to MEQP)
1117 ;; if (1) they have the same dimensions,
1118 ;; and (2) their elements are MEQP.
1120 (defun array-meqp (p q
)
1122 (equal (array-dimensions p
) (array-dimensions q
))
1124 (dotimes (i (array-total-size p
))
1125 (let ((z (let ($ratprint
)
1126 (declare (special $ratprint
))
1127 (meqp (row-major-aref p i
) (row-major-aref q i
)))))
1128 (cond ((eq z nil
) (return-from array-meqp nil
))
1130 (t (return-from array-meqp
`(($equal
) ,p
,q
))))))
1133 (defun maxima-declared-array-meqp (p q
)
1134 (array-meqp (get (mget p
'array
) 'array
) (get (mget q
'array
) 'array
)))
1136 (defun maxima-undeclared-array-meqp (p q
)
1138 (alike1 (mfuncall '$arrayinfo p
) (mfuncall '$arrayinfo q
))
1140 (declare (special $ratprint
))
1141 (meqp ($listarray p
) ($listarray q
)))))
1143 (defun list-meqp (p q
)
1145 (cond ((or (null p
) (null q
)) (and (null p
) (null q
)))
1147 (setq z
(meqp (car p
) (car q
)))
1148 (cond ((eq z nil
) nil
)
1149 ((or (eq z
'$unknown
) (op-equalp z
'$equal
)) z
)
1150 (t (list-meqp (cdr p
) (cdr q
))))))))
1152 (defun lambda-meqp (a b
)
1154 (cond ((= (length (second a
)) (length (second b
)))
1155 (let ((x) (n ($length
(second a
))))
1156 (dotimes (i n
(push '(mlist) x
)) (push (gensym) x
))
1157 (setq z
(meqp (mfuncall '$apply a x
) (mfuncall '$apply b x
)))
1158 (if (or (eq t z
) (eq nil z
)) z
`(($equal
) ,a
,b
))))
1161 (defun set-meqp (a b
)
1162 (let ((aa (equal-facts-simp a
))
1163 (bb (equal-facts-simp b
)))
1164 (cond ((or (not ($setp bb
))
1165 (and ($emptyp aa
) (not ($emptyp bb
)))
1166 (and ($emptyp bb
) (not ($emptyp aa
))))
1168 ((and (= (length aa
) (length bb
))
1169 (every #'(lambda (p q
) (eq t
(meqp p q
))) (margs aa
) (margs bb
))) t
)
1170 ((set-not-eqp (margs aa
) (margs bb
)) nil
)
1171 (t `(($equal
,a
,b
))))))
1173 (defun set-not-eqp (a b
)
1176 (if (every #'(lambda (s) (eq nil
(meqp ak s
))) b
) (throw 'done t
)))
1178 (if (every #'(lambda (s) (eq nil
(meqp bk s
))) a
) (throw 'done t
)))
1182 (let ((*complexsign
* t
))
1184 (let ((sgn (csign a
)))
1185 (cond ((eq sgn
'$pos
) t
)
1186 ((eq sgn t
) nil
) ;; csign thinks a - b isn't real
1187 ((member sgn
'($neg $zero $nz
) :test
#'eq
) nil
)
1188 (t `((mgreaterp) ,a
0))))))
1194 (let ((*complexsign
* t
))
1196 (let ((sgn (csign a
)))
1197 (cond ((member sgn
'($pos $zero $pz
) :test
#'eq
) t
)
1198 ((eq sgn t
) nil
) ;; csign thinks a - b isn't real
1199 ((eq sgn
'$neg
) nil
)
1200 (t `((mgeqp) ,a
0))))))
1203 (let ((b (meqp x y
)))
1204 (cond ((eq b
'$unknown
) b
)
1205 ((or (eq b t
) (eq b nil
)) (not b
))
1206 (t `(($notequal
) ,x
,y
)))))
1209 (list '(mnot) (c-$zero o e
)))
1211 (defun c-$zero
(o e
)
1212 (list '($equal
) (lmul (nconc o e
)) 0))
1215 (cond ((null o
) (list '(mnot) (list '($equal
) (lmul e
) 0)))
1216 ((null e
) (list '(mgreaterp) (lmul o
) 0))
1217 (t (setq e
(mapcar #'(lambda (l) (power l
2)) e
))
1218 (list '(mgreaterp) (lmul (nconc o e
)) 0))))
1221 (cond ((null o
) (list '(mnot) (list '($equal
) (lmul e
) 0)))
1222 ((null e
) (list '(mgeqp) (lmul o
) 0))
1223 (t (setq e
(mapcar #'(lambda (l) (power l
2)) e
))
1224 (list '(mgeqp) (lmul (nconc o e
)) 0))))
1227 (let (sign minus odds evens
)
1231 (if (or (atom e
) (and (free e
'$inf
) (free e
'$minf
)))
1235 ;; Like WITH-COMPSPLT, but runs COMPSPLT-EQ instead
1236 (defmacro with-compsplt-eq
((lhs rhs x
) &body forms
)
1237 `(multiple-value-bind (,lhs
,rhs
) (compsplt-eq ,x
)
1240 ;; Call FORMS with LHS and RHS bound to the splitting of EXPR by COMPSPLT.
1241 (defmacro with-compsplt
((lhs rhs expr
) &body forms
)
1242 `(multiple-value-bind (,lhs
,rhs
) (compsplt ,expr
)
1246 (setq x
(specrepcheck x
))
1247 (setq x
(infsimp* x
))
1248 (when (and *complexsign
* (atom x
) (eq x
'$infinity
))
1249 ;; In Complex Mode the sign of infinity is complex.
1250 (when *debug-compar
* (format t
"~& in sign1 detect $infinity.~%"))
1251 (return-from sign1
'$complex
))
1252 (if (member x
'($und $ind $infinity
) :test
#'eq
)
1253 (if limitp
'$pnz
(merror (intl:gettext
"sign: sign of ~:M is undefined.") x
)))
1255 (setq dum
(constp x
) exp x
)
1256 (cond ((or (numberp x
) (ratnump x
)))
1258 (if (prog2 (setq dum
($bfloat x
)) ($bfloatp dum
))
1261 (if (and (setq dum
(numer x
)) (numberp dum
)) (setq exp dum
)))
1262 ((and (member dum
'(numer symbol
) :test
#'eq
)
1263 (prog2 (setq dum
(numer x
))
1266 (prog2 (setq exp dum
)
1267 (< (abs dum
) 1.0e-6))))))
1269 (and (setq dum
($bfloat x
)) ($bfloatp dum
) (setq exp dum
)))
1270 (t (setq sign
'$pnz evens nil odds
(ncons x
) minus nil
)
1272 (or (and (not (atom x
)) (not (mnump x
)) (equal x exp
)
1274 (with-compsplt (lhs rhs x
)
1276 (cond ((member sign
'($pos $neg
) :test
#'eq
))
1277 ((eq sign
'$pnz
) nil
)
1278 (t (setq s sign o odds e evens m minus
)
1280 (if (not (strongp sign s
))
1281 (if (and (eq sign
'$pnz
) (eq s
'$pn
))
1283 (setq sign s odds o evens e minus m
)))
1289 (let (($numer t
) ; currently, no effect on $float, but proposed to
1292 ;; Catch a Lisp error, if a floating point overflow occurs.
1293 (setq result
(let ((errset nil
)) (errset ($float x
))))
1294 (if result
(car result
) nil
)))
1297 (cond ((floatp x
) 'float
)
1298 ((numberp x
) 'numer
)
1299 ((symbolp x
) (if (member x
'($%pi $%e $%phi $%gamma
) :test
#'eq
) 'symbol
))
1301 ((eq (caar x
) 'rat
) 'numer
)
1302 ((eq (caar x
) 'bigfloat
) 'bigfloat
)
1303 ((specrepp x
) (constp (specdisrep x
)))
1304 (t (do ((l (cdr x
) (cdr l
)) (dum) (ans 'numer
))
1306 (setq dum
(constp (car l
)))
1307 (cond ((eq dum
'float
) (return 'float
))
1309 ((eq dum
'bigfloat
) (setq ans
'bigfloat
))
1311 (if (eq ans
'numer
) (setq ans
'symbol
)))
1312 (t (return nil
)))))))
1314 (mapcar #'(lambda (s) (putprop (first s
) (second s
) 'sign-function
))
1316 (list 'mtimes
'sign-mtimes
)
1317 (list 'mplus
'sign-mplus
)
1318 (list 'mexpt
'sign-mexpt
)
1319 (list '%log
'sign-log
)
1320 (list 'mabs
'sign-mabs
)
1321 (list '$min
#'(lambda (x) (sign-minmax (caar x
) (cdr x
))))
1322 (list '$max
#'(lambda (x) (sign-minmax (caar x
) (cdr x
))))
1323 (list '%csc
#'(lambda (x) (sign (inv* (cons (ncons (zl-get (caar x
) 'recip
)) (cdr x
))))))
1324 (list '%csch
#'(lambda (x) (sign (inv* (cons (ncons (zl-get (caar x
) 'recip
)) (cdr x
))))))
1326 (list '%signum
#'(lambda (x) (sign (cadr x
))))
1327 (list '%erf
#'(lambda (x) (sign (cadr x
))))
1328 (list '$li
#'(lambda (x)
1329 (let ((z (first (margs x
))) (n (cadadr x
)))
1330 (if (and (mnump n
) (eq t
(mgrp z
0)) (eq t
(mgrp 1 z
))) (sign z
) (sign-any x
)))))))
1332 (cond ((mnump x
) (setq sign
(rgrp x
0) minus nil odds nil evens nil
))
1333 ((and *complexsign
* (symbolp x
) (eq x
'$%i
))
1334 ;; In Complex Mode the sign of %i is $imaginary.
1335 (setq sign
'$imaginary
))
1336 ((symbolp x
) (if (eq x
'$%i
) (imag-err x
)) (sign-any x
))
1337 ((and (consp x
) (symbolp (caar x
)) (not (specrepp x
)) (get (caar x
) 'sign-function
))
1338 (funcall (get (caar x
) 'sign-function
) x
))
1339 ((and (consp x
) (not (specrepp x
)) ($subvarp
(mop x
)) (get (mop (mop x
)) 'sign-function
))
1340 (funcall (get (mop (mop x
)) 'sign-function
) x
))
1341 ((specrepp x
) (sign (specdisrep x
)))
1342 ((kindp (caar x
) '$posfun
) (sign-posfun x
))
1343 ((kindp (caar x
) '$oddfun
) (sign-oddfun x
))
1347 (cond ((and *complexsign
*
1350 ;; In Complex Mode look for symbols declared to be complex.
1351 (if ($featurep x
'$imaginary
)
1352 (setq sign
'$imaginary
)
1353 (setq sign
'$complex
)))
1356 (decl-complexp (caar x
)))
1357 ;; A function f(x), where f is declared to be imaginary or complex.
1358 (if ($featurep
(caar x
) '$imaginary
)
1359 (setq sign
'$imaginary
)
1360 (setq sign
'$complex
)))
1363 (if (and $assume_pos
1364 (member sign
'($pnz $pz $pn
) :test
#'eq
)
1365 (if $assume_pos_pred
1367 (declare (special *x
*))
1368 (is '(($assume_pos_pred
) *x
*)))
1371 (setq minus nil evens nil
1372 odds
(if (not (member sign
'($pos $neg $zero
) :test
#'eq
))
1375 (defun sign-mtimes (x)
1377 (do ((s '$pos
) (m) (o) (e)) ((null x
) (setq sign s minus m odds o evens e
))
1379 (cond ((eq sign
'$zero
) (return t
))
1380 ((and *complexsign
* (eq sign
'$complex
))
1381 ;; Found a complex factor. We don't return immediately
1382 ;; because another factor could be zero.
1384 ((and *complexsign
* (eq s
'$complex
))) ; continue the loop
1385 ((and *complexsign
* (eq sign
'$imaginary
))
1386 ;; Found an imaginary factor. Look if we have already one.
1387 (cond ((eq s
'$imaginary
)
1388 ;; imaginary*imaginary is real. But remember the sign in m.
1389 (setq s
(if m
'$pos
'$neg
) m
(not m
)))
1391 ((and *complexsign
* (eq s
'$imaginary
))) ; continue the loop
1393 ((eq sign
'$neg
) (setq s
(flip s
) m
(not m
)))
1394 ((prog2 (setq m
(not (eq m minus
)) o
(nconc odds o
) e
(nconc evens e
))
1396 ((eq s sign
) (when (eq s
'$nz
) (setq s
'$pz
)))
1397 ((eq s
'$pos
) (setq s sign
))
1398 ((eq s
'$neg
) (setq s
(flip sign
)))
1399 ((or (and (eq s
'$pz
) (eq sign
'$nz
))
1400 (and (eq s
'$nz
) (eq sign
'$pz
)))
1405 (defun sign-mplus (x &aux s o e m
)
1406 (cond ((signdiff x
))
1407 ((prog2 (setq s sign e evens o odds m minus
) nil
))
1409 ((prog2 (cond ((strongp s sign
))
1410 (t (setq s sign e evens o odds m minus
)))
1412 ((and (not factored
) (signfactor x
)))
1414 (t (setq sign s evens e odds o minus m
))))
1418 (let ((swapped nil
) (retval))
1419 (with-compsplt (lhs rhs x
)
1420 (if (and (mplusp lhs
) (equal rhs
0) (null (cdddr lhs
)))
1421 (cond ((and (negp (cadr lhs
)) (not (negp (caddr lhs
))))
1422 (setq rhs
(neg (cadr lhs
)) lhs
(caddr lhs
)))
1423 ;; The following fixes SourceForge bug #3148
1424 ;; where sign(a-b) returned pnz and sign(b-a) returned pos.
1425 ;; Previously, only the case (-a)+b was handled.
1426 ;; Now we also handle a+(-b) by swapping lhs and rhs,
1427 ;; setting a flag "swapped", running through the same code and
1428 ;; then flipping the answer.
1429 ((and (negp (caddr lhs
)) (not (negp (cadr lhs
))))
1430 (setq rhs
(cadr lhs
) lhs
(neg (caddr lhs
)) swapped t
))))
1433 (cond ((or (equal rhs
0) (mplusp lhs
)) nil
)
1434 ((and (member (constp rhs
) '(numer symbol
) :test
#'eq
)
1435 (numberp (setq dum
(numer rhs
)))
1436 (prog2 (setq rhs dum
) nil
)))
1438 ((and (dcompare lhs rhs
) (member sign
'($pos $neg $zero
) :test
#'eq
)))
1439 ((and (not (atom lhs
)) (not (atom rhs
))
1440 (eq (caar lhs
) (caar rhs
))
1441 (kindp (caar lhs
) '$increasing
))
1442 (sign (sub (cadr lhs
) (cadr rhs
)))
1444 ((and (not (atom lhs
)) (not (atom rhs
))
1445 (eq (caar lhs
) (caar rhs
))
1446 (kindp (caar lhs
) '$decreasing
))
1447 (sign (sub (cadr rhs
) (cadr lhs
)))
1449 ((and (not (atom lhs
)) (eq (caar lhs
) 'mabs
)
1450 (alike1 (cadr lhs
) rhs
))
1451 (setq sign
'$pz minus nil odds nil evens nil
) t
)
1452 ((signdiff-special lhs rhs
))))))
1454 (setq sign
(flip sign
)))
1457 (defun signdiff-special (xlhs xrhs
)
1458 ;; xlhs may be a constant
1460 (when (or (and (realp xrhs
) (minusp xrhs
)
1461 (not (atom xlhs
)) (eq (sign* xlhs
) '$pos
))
1462 ; e.g. sign(a^3+%pi-1) where a>0
1464 ;; e.g. sign(%e^x-1) where x>0
1465 (eq (sign* (caddr xlhs
)) '$pos
)
1467 ;; Q^Rpos - S, S<=1, Q>1
1468 (member (sign* (sub 1 xrhs
)) '($pos $zero $pz
) :test
#'eq
)
1469 (eq (sign* (sub (cadr xlhs
) 1)) '$pos
))
1470 (and (not (eq $domain
'$complex
))
1471 ;; Qpos ^ Rpos - Spos => Qpos - Spos^(1/Rpos)
1472 (eq (sign* (cadr xlhs
)) '$pos
)
1473 (eq (sign* xrhs
) '$pos
)
1474 (eq (sign* (sub (cadr xlhs
)
1475 (power xrhs
(div 1 (caddr xlhs
)))))
1477 (and (mexptp xlhs
) (mexptp xrhs
)
1478 ;; Q^R - Q^T, Q>1, (R-T) > 0
1479 ;; e.g. sign(2^x-2^y) where x>y
1480 (alike1 (cadr xlhs
) (cadr xrhs
))
1481 (eq (sign* (sub (cadr xlhs
) 1)) '$pos
)
1482 (eq (sign* (sub (caddr xlhs
) (caddr xrhs
))) '$pos
)))
1486 (when (and (not (atom xlhs
))
1487 (member (caar xlhs
) '(%sin %cos
))
1488 (zerop1 ($imagpart
(cadr xlhs
))))
1489 (cond ((eq (sign* (add xrhs
1)) '$neg
) ;; c > 1
1491 ((eq (sign* (add xrhs -
1)) '$pos
) ;; c < -1
1493 ((zerop1 (add xrhs
1)) ;; c = 1
1495 ((zerop1 (add xrhs -
1)) ;; c = -1
1498 (when (and $useminmax
(or (minmaxp xlhs
) (minmaxp xrhs
)))
1499 (setq sgn
(signdiff-minmax xlhs xrhs
)))
1500 (when sgn
(setq sign sgn minus nil odds nil evens nil
)
1503 ;;; Look for symbols with an assumption a > n or a < -n, where n is a number.
1504 ;;; For this case shift the symbol a -> a+n in a summation and multiplication.
1505 ;;; This handles cases like a>1 and b>1 gives sign(a+b-2) -> pos.
1507 (defun sign-shift (expr)
1508 (do ((l (cdr expr
) (cdr l
))
1511 ((null l
) (addn acc nil
))
1512 (cond ((symbolp (car l
))
1513 ;; Get the facts related to the symbol (car l)
1514 ;; Reverse the order to test the newest facts first.
1515 (setq fl
(reverse (cdr (facts1 (car l
)))))
1518 (cond ((and (eq (caar f
) 'mgreaterp
)
1520 (eq ($sign
(caddr f
)) '$pos
))
1521 ;; The case a > n, where a is a symbol and n a number.
1522 ;; Add the number to the list of terms.
1523 (return (push (caddr f
) acc
)))
1524 ((and (eq (caar f
) 'mgreaterp
)
1526 (eq ($sign
(cadr f
)) '$neg
))
1527 ;; The case a < -n, where a is a symbol and n a number.
1528 ;; Add the number to the list of terms.
1529 (return (push (cadr f
) acc
))))))
1531 (let ((acctimes) (flag))
1532 ;; Go through the factors of the multiplication.
1533 (dolist (ll (cdar l
))
1535 ;; Get the facts related to the symbol (car l)
1536 ;; Reverse the order to test the newest facts first.
1537 (setq fl
(reverse (cdr (facts1 ll
))))
1539 (cond ((and (eq (caar f
) 'mgreaterp
)
1541 (eq ($sign
(caddr f
)) '$pos
))
1542 ;; The case a > n, where a is a symbol and n a
1543 ;; number. Add the number to the list of terms.
1545 (return (push (add ll
(caddr f
)) acctimes
)))
1546 ((and (eq (caar f
) 'mgreaterp
)
1548 (eq ($sign
(cadr f
)) '$neg
))
1549 ;; The case a < -n, where a is a symbol and n a
1550 ;; number. Add the number to the list of terms.
1552 (return (push (add ll
(cadr f
)) acctimes
)))))
1553 (when (not flag
) (push ll acctimes
)))
1555 (push ll acctimes
))))
1557 ;; If a shift has been done expand the factors.
1558 (push ($multthru
(muln acctimes nil
)) acc
)
1559 (push (muln acctimes nil
) acc
))))
1561 (push (car l
) acc
)))))
1564 (setq x
(sign-shift x
))
1565 ;; x might be simplified to an atom in sign-shift.
1566 (when (atom x
) (setq x
(cons '(mplus) (list x
))))
1567 (do ((l (cdr x
) (cdr l
)) (s '$zero
))
1568 ((null l
) (setq sign s minus nil odds
(list x
) evens nil
)
1569 (cond (*complexsign
*
1570 ;; Because we have continued the loop in Complex Mode
1571 ;; we have to look for the sign '$pnz and return nil.
1572 (if (eq s
'$pnz
) nil t
))
1573 (t t
))) ; in Real Mode return T
1574 ;; Call sign1 and not sign, because sign1 handles constant expressions.
1576 (cond ((and *complexsign
*
1577 (or (eq sign
'$complex
) (eq sign
'$imaginary
)))
1578 ;; Found a complex or imaginary expression. The sign is $complex.
1579 (setq sign
'$complex odds nil evens nil minus nil
)
1581 ((or (and (eq sign
'$zero
)
1582 (setq x
(sub x
(car l
))))
1583 (and (eq s sign
) (not (eq s
'$pn
))) ; $PN + $PN = $PNZ
1584 (and (eq s
'$pos
) (eq sign
'$pz
))
1585 (and (eq s
'$neg
) (eq sign
'$nz
))))
1586 ((or (and (member sign
'($pz $pos
) :test
#'eq
) (member s
'($zero $pz
) :test
#'eq
))
1587 (and (member sign
'($nz $neg
) :test
#'eq
) (member s
'($zero $nz
) :test
#'eq
))
1588 (and (eq sign
'$pn
) (eq s
'$zero
)))
1591 (cond (*complexsign
*
1592 ;; In Complex Mode we have to continue the loop to look further
1593 ;; for a complex or imaginay expression.
1596 ;; In Real mode the loop stops when the sign is 'pnz.
1597 (setq sign
'$pnz odds
(list x
) evens nil minus nil
)
1600 (defun signfactor (x)
1601 (let (y (factored t
))
1602 (setq y
(factor-if-small x
))
1603 (cond ((or (mplusp y
) (> (conssize y
) 50.
))
1608 (defun factor-if-small (x)
1609 (if (< (conssize x
) 51.
)
1611 (declare (special $ratprint
))
1614 (defun sign-mexpt (x)
1615 (let* ((expt (caddr x
)) (base1 (cadr x
))
1616 (sign-expt (sign1 expt
)) (sign-base (sign1 base1
))
1618 (cond ((and *complexsign
* (or (eq sign-expt
'$complex
)
1619 (eq sign-expt
'$imaginary
)
1620 (eq sign-base
'$complex
)))
1621 ;; Base is complex or exponent is complex or imaginary.
1622 ;; The sign is $complex.
1623 (when *debug-compar
*
1624 (format t
"~&in SIGN-MEXPT for ~A, sign is complex.~%" x
))
1625 (setq sign
'$complex
))
1628 (eq sign-base
'$neg
)
1629 (eq (evod ($expand
(mul 2 expt
))) '$odd
))
1630 ;; Base is negative and the double of the exponent is odd.
1631 ;; Result is imaginary.
1632 (when *debug-compar
*
1633 (format t
"~&in SIGN-MEXPT for ~A, sign is $imaginary.~%" x
))
1634 (setq sign
'$imaginary
))
1637 (eq sign-base
'$imaginary
))
1638 ;; An imaginary base. Look for even or odd exponent.
1639 (when *debug-compar
*
1640 (format t
"~&in SIGN-MEXPT for ~A, base is $imaginary.~%" x
))
1642 ((and (integerp expt
) (eq evod
'$even
))
1643 (setq sign
(if (eql (mod expt
4) 0) '$pz
'$nz
)))
1644 ((and (integerp expt
) (eq evod
'$odd
))
1645 (setq sign
'$imaginary
1646 minus
(if (eql (mod (- expt
1) 4) 0) t nil
)))
1647 (t (setq sign
'$complex
))))
1649 ((and (eq sign-base
'$zero
)
1650 (member sign-expt
'($zero $neg
) :test
#'eq
))
1652 ((eq sign-expt
'$zero
) (setq sign
'$pos
))
1653 ((eq sign-base
'$pos
))
1654 ((eq sign-base
'$zero
))
1656 (cond ((eq sign-expt
'$neg
)
1657 (setq sign
'$pos minus nil evens
(ncons base1
) odds nil
))
1658 ((member sign-base
'($pn $neg
) :test
#'eq
)
1659 (setq sign
'$pos minus nil
1660 evens
(nconc odds evens
)
1662 (t (setq sign
'$pz minus nil
1663 evens
(nconc odds evens
)
1665 ((and (member sign-expt
'($neg $nz
) :test
#'eq
)
1666 (member sign-base
'($nz $pz $pnz
) :test
#'eq
))
1667 (setq sign
(cond ((eq sign-base
'$pnz
) '$pn
)
1668 ((eq sign-base
'$pz
) '$pos
)
1669 ((eq sign-expt
'$neg
) '$neg
)
1671 ((member sign-expt
'($pz $nz $pnz
) :test
#'eq
)
1672 (cond ((eq sign-base
'$neg
)
1673 (setq odds
(ncons x
) sign
'$pn
))))
1674 ((eq sign-expt
'$pn
))
1676 (cond ((mevenp (cadr expt
))
1677 (cond ((member sign-base
'($pn $neg
) :test
#'eq
)
1678 (setq sign-base
'$pos
))
1679 ((member sign-base
'($pnz $nz
) :test
#'eq
)
1680 (setq sign-base
'$pz
)))
1681 (setq evens
(nconc odds evens
)
1682 odds nil minus nil
))
1683 ((mevenp (caddr expt
))
1684 (cond ((and *complexsign
* (eq sign-base
'$neg
))
1685 ;; In Complex Mode the sign is $complex.
1686 (setq sign-base
(setq sign-expt
'$complex
)))
1688 ;; The only place the variable complexsign
1689 ;; is used. Unfortunately, one routine in
1690 ;; to_poly.lisp in /share/to_poly_solve depends on
1691 ;; this piece of code. Perhaps we can remove
1692 ;; the dependency. (12/2008)
1693 (setq sign-base
(setq sign-expt
'$pnz
)))
1694 ((eq sign-base
'$neg
) (imag-err x
))
1695 ((eq sign-base
'$pn
)
1696 (setq sign-base
'$pos
))
1697 ((eq sign-base
'$nz
)
1698 (setq sign-base
'$zero
))
1699 (t (setq sign-base
'$pz
)))))
1700 (cond ((eq sign-expt
'$neg
)
1701 (cond ((eq sign-base
'$zero
) (dbzs-err x
))
1702 ((eq sign-base
'$pz
)
1703 (setq sign-base
'$pos
))
1704 ((eq sign-base
'$nz
)
1705 (setq sign-base
'$neg
))
1706 ((eq sign-base
'$pnz
)
1707 (setq sign-base
'$pn
)))))
1708 (setq sign sign-base
))
1709 ((eq sign-base
'$pos
)
1711 ((eq sign-base
'$neg
)
1714 (setq sign
(if *complexsign
* '$complex
'$pn
)))))))
1716 ;;; Determine the sign of log(expr). This function changes the special variable sign.
1721 (cond ((eq t
(mgrp x
0))
1722 (cond ((eq t
(mgrp 1 x
)) '$neg
)
1723 ((eq t
(meqp x
1)) '$zero
);; log(1) = 0.
1724 ((eq t
(mgqp 1 x
)) '$nz
)
1725 ((eq t
(mgrp x
1)) '$pos
)
1726 ((eq t
(mgqp x
1)) '$pz
)
1727 ((eq t
(mnqp x
1)) '$pn
)
1729 ((and *complexsign
* (eql 1 (cabs x
))) '$imaginary
)
1730 (*complexsign
* '$complex
)
1733 (defun sign-mabs (x)
1734 (let ((*complexsign
* t
))
1736 (cond ((member sign
'($pos $zero
) :test
#'eq
))
1737 ((member sign
'($neg $pn
) :test
#'eq
) (setq sign
'$pos
))
1738 (t (setq sign
'$pz minus nil evens
(nconc odds evens
) odds nil
)))))
1742 ;;; Macros used in simp min/max
1743 ;;; If op is min, use body; if not, negate sign constants in body
1744 ;;; Used to avoid writing min and max code separately: just write the min code
1745 ;;; in such a way that its dual works for max
1746 (defmacro minmaxforms
(op &rest body
)
1749 ,@(sublis '(($neg . $pos
)
1764 (defun sign-minmax (op args
)
1765 (do ((sgn (minmaxforms op
'$pos
) ;identity element for min
1766 (sminmax op sgn
(sign* (car l
))))
1767 (end (minmaxforms op
'$neg
))
1769 ((or (null l
) (eq sgn end
))
1771 odds
(if (not (member sgn
'($pos $neg $zero
) :test
#'eq
))
1772 (ncons (cons (list op
) args
)))
1776 ;; sign(op(a,b)) = sminmax(sign(a),sign(b))
1777 ;; op is $min/$max; s1/s2 in neg, nz, zero, pz, pos, pn, pnz
1778 (defun sminmax (op s1 s2
)
1781 ;; Many of these cases don't come up in simplified expressions,
1782 ;; since e.g. sign(a)=neg and sign(b)=pos implies min(a,b)=a
1783 ;; the order of these clauses is important
1784 (cond ((eq s1
'$pos
) s2
)
1787 ((or (eq s1
'$neg
) (eq s2
'$neg
)) '$neg
)
1788 ((or (eq s1
'$nz
) (eq s2
'$nz
)) '$nz
)
1789 ((eq s1
'$zero
) (if (eq s2
'$pz
) '$zero
'$nz
))
1790 ((eq s2
'$zero
) (if (eq s1
'$pz
) '$zero
'$nz
))
1794 (cond ((atom ex
) nil
)
1795 ((member (caar ex
) '($min $max
) :test
#'eq
) (caar ex
))
1798 (defun signdiff-minmax (l r
)
1799 ;; sign of l-r; nil if unknown (not PNZ)
1800 (let* ((lm (minmaxp l
))
1802 (ll (if lm
(cdr l
)))
1803 (rr (if rm
(cdr r
)))) ;distinguish between < and <= argument lists of min/max
1806 (cond ((eq lm rm
) ; min(a,...) - min(b,...)
1807 (multiple-value-bind (both onlyl onlyr
) (intersect-info ll rr
)
1808 (declare (ignore both
))
1809 (cond ((null onlyl
) '$pz
) ; min(a,b) - min(a,b,c)
1810 ((null onlyr
) '$nz
) ; min(a,b,c) - min(a,b)
1811 ;; TBD: add processing for full onlyl/onlyr case
1813 ;; TBD: memalike and set-disjointp are crude approx.
1814 ((null lm
) (if (memalike l rr
) '$pz
)) ; a - min(a,b)
1815 ((null rm
) (if (memalike r ll
) '$nz
)) ; min(a,b) - a
1816 (t ; min/max or max/min
1817 (if (not (set-disjointp ll rr
)) '$pz
)))))) ; max(a,q,r) - min(a,s,t)
1819 (defun intersect-info (a b
)
1827 #'(lambda (x) (push x both
))
1828 #'(lambda (x) (push x onlya
))
1829 #'(lambda (x) (push x onlyb
)))
1835 ;;; end compare min/max
1837 (defun sign-posfun (xx)
1838 (declare (ignore xx
))
1844 (defun sign-oddfun (x)
1845 (cond ((kindp (caar x
) '$increasing
)
1846 ; Take the sign of the argument
1848 ((kindp (caar x
) '$decreasing
)
1849 ; Take the sign of negative of the argument
1850 (sign (neg (cadr x
))))
1852 ; If the sign of the argument is zero, then we're done (the sign of
1853 ; the function value is the same). Otherwise, punt to SIGN-ANY.
1855 (unless (eq sign
'$zero
)
1860 (merror (intl:gettext
"sign: argument cannot be imaginary; found ~M") x
)
1861 (throw 'sign-imag-err t
)))
1864 (merror (intl:gettext
"sign: division by zero in ~M") x
))
1866 ;; Return true iff e is an expression with operator op1, op2,...,or opn.
1868 (defun op-equalp (e &rest op
)
1869 (and (consp e
) (consp (car e
)) (some #'(lambda (s) (equal (caar e
) s
)) op
)))
1871 ;; Return true iff the operator of a is a Maxima relation operator.
1873 (defun mrelationp (a)
1874 (op-equalp a
'mlessp
'mleqp
'mequal
'mnotequal
'mgeqp
'mgreaterp
))
1876 ;; This version of featurep applies ratdisrep to the first argument. This
1877 ;; change allows things like featurep(rat(n),integer) --> true when n has
1878 ;; been declared an integer.
1880 (defmfun $featurep
(e ind
)
1881 (setq e
($ratdisrep e
))
1882 (cond ((not (symbolp ind
))
1884 (intl:gettext
"featurep: second argument must be a symbol; found ~M")
1886 ;; Properties not related to the assume database.
1887 ((and (member ind opers
) (safe-get e ind
)))
1888 ((and (member ind
'($evfun $evflag $bindtest $nonarray
))
1889 (safe-get e
(stripdollar ind
))))
1890 ((and (eq ind
'$noun
)
1891 (safe-get e
(stripdollar ind
))
1893 ((and (member ind
'($scalar $nonscalar $mainvar
))
1895 ((and (eq ind
'$feature
)
1896 (member e $features
)
1898 ((eq ind
'$alphabetic
)
1899 (dolist (l (coerce e
'list
) t
)
1900 (when (not (member l
*alphabet
*)) (return nil
))))
1901 ;; Properties related to the assume database.
1902 ((eq ind
'$integer
) (maxima-integerp e
))
1903 ((eq ind
'$noninteger
) (nonintegerp e
))
1904 ((eq ind
'$even
) (mevenp e
))
1905 ((eq ind
'$odd
) (moddp e
))
1908 (or (numberp e
) (kindp e
'$real
) (numberp (numer e
)))
1909 (free ($rectform e
) '$%i
)))
1910 ((symbolp e
) (kindp e ind
))))
1912 ;; Give a function the maps-integers-to-integers property when it is integer
1913 ;; valued on the integers; give it the integer-valued property when its
1914 ;; range is a subset of the integers. What have I missed?
1916 (setf (get 'mplus
'maps-integers-to-integers
) t
)
1917 (setf (get 'mtimes
'maps-integers-to-integers
) t
)
1918 (setf (get 'mabs
'maps-integers-to-integers
) t
)
1919 (setf (get '$max
'maps-integers-to-integers
) t
)
1920 (setf (get '$min
'maps-integers-to-integers
) t
)
1922 (setf (get '$floor
'integer-valued
) t
)
1923 (setf (get '$ceiling
'integer-valued
) t
)
1924 (setf (get '$charfun
'integer-valued
) t
)
1926 (defun maxima-integerp (x)
1927 (cond ((integerp x
))
1930 (or (kindp x
'$integer
)
1933 (check-integer-facts x
))))
1934 (t (let ((x-op (and (consp x
) (consp (car x
)) (caar x
))) ($prederror nil
))
1935 (cond ((null x-op
) nil
)
1936 ((not (symbolp x-op
)) nil
) ; fix for mqapply at some point?
1937 ((eq x-op
'mrat
) (and (integerp (cadr x
)) (equal (cddr x
) 1)))
1938 ;; mtimes and mplus are generally handled by this clause
1939 ((and (get x-op
'maps-integers-to-integers
) (every #'maxima-integerp
(margs x
))))
1940 ;; Special case for 1/2*...*even
1942 (and (mnump (cadr x
))
1943 (integerp (mul 2 (cadr x
)))
1944 (every 'maxima-integerp
(cddr x
))
1945 (some #'(lambda (s) ($featurep s
'$even
)) (rest (margs x
)))))
1947 (and (every #'maxima-integerp
(margs x
))
1948 (null (mevalp (mlsp (caddr x
) 0)))))
1949 ;; ! in Maxima allows real arguments
1950 ((eq x-op
'mfactorial
)
1951 (and (maxima-integerp (cadr x
))
1952 (not (mevalp (mlsp (cadr x
) 0)))))
1954 (and (maxima-integerp (cadr x
))
1955 (not (mevalp (mlsp (cadr x
) 1)))))
1957 ((or ($featurep
($verbify x-op
) '$integervalued
)
1958 (get x-op
'integer-valued
))))))))
1960 ;; When called with mode 'integer look into the database for symbols which are
1961 ;; declared to be equal to an integer or an expression which is an integer.
1962 ;; In mode 'evod look for odd and even expressions.
1963 (defun check-integer-facts (x &optional
(mode 'integer
))
1964 (do ((factsl (cdr (facts1 x
)) (cdr factsl
))
1967 (setq fact
(car factsl
))
1968 (cond ((and (not (atom fact
))
1969 (eq (caar fact
) '$equal
))
1970 (cond ((and (symbolp (cadr fact
))
1972 ;; Case equal(x,expr): Test expr to be an integer.
1973 (cond ((symbolp (caddr fact
))
1974 (cond ((and (eq mode
'integer
)
1975 (or (kindp (caddr fact
) '$integer
)
1976 (kindp (caddr fact
) '$odd
)
1977 (kindp (caddr fact
) '$even
)))
1980 (cond ((kindp (caddr fact
) '$odd
)
1982 ((kindp (caddr fact
) '$even
)
1987 (cond ((eq mode
'integer
)
1988 (return (maxima-integerp (caddr fact
))))
1990 (return (evod (caddr fact
))))
1991 (t (return nil
))))))
1992 ((and (symbolp (caddr fact
))
1993 (eq (caddr fact
) x
))
1994 ;; Case equal(expr,x): Test expr to be an integer.
1995 (cond ((symbolp (caddr fact
))
1996 (cond ((and (eq mode
'integer
)
1997 (or (kindp (cadr fact
) '$integer
)
1998 (kindp (cadr fact
) '$odd
)
1999 (kindp (cadr fact
) '$even
)))
2002 (cond ((kindp (cadr fact
) '$odd
)
2004 ((kindp (cadr fact
) '$even
)
2009 (cond ((eq mode
'integer
)
2010 (return (maxima-integerp (cadr fact
))))
2012 (return (evod (cadr fact
))))
2013 (t (return nil
)))))))))))
2015 (defun nonintegerp (e)
2016 (cond ((and (symbolp e
) (or (kindp e
'$noninteger
) (check-noninteger-facts e
) (kindp e
'$irrational
)))) ;declared noninteger
2018 (if (integerp e
) nil t
)) ;all floats are noninteger and integers are not nonintegers
2020 (nonintegerp ($ratdisrep e
)))
2021 (t (eq t
(mgrp e
(take '($floor
) e
))))))
2024 ;; Look into the database for symbols which are declared to be equal
2025 ;; to a noninteger or an expression which is a noninteger.
2026 (defun check-noninteger-facts (x)
2027 (do ((factsl (cdr (facts1 x
)) (cdr factsl
)))
2029 (cond ((and (not (atom (car factsl
)))
2030 (eq (caar (car factsl
)) '$equal
))
2031 (cond ((and (symbolp (cadr (car factsl
)))
2032 (eq (cadr (car factsl
)) x
))
2033 ;; Case equal(x,expr): Test expr to be a noninteger.
2034 (cond ((symbolp (caddr (car factsl
)))
2035 (if (kindp (caddr (car factsl
)) '$noninteger
)
2038 (return (nonintegerp (caddr (car factsl
)))))))
2039 ((and (symbolp (caddr (car factsl
)))
2040 (eq (caddr (car factsl
)) x
))
2041 ;; Case equal(expr,x): Test expr to be a noninteger.
2042 (cond ((symbolp (cadr (car factsl
)))
2043 (if (kindp (cadr (car factsl
)) '$noninteger
)
2046 (return (nonintegerp (cadr (car factsl
))))))))))))
2049 (every #'maxima-integerp
(cdr l
)))
2052 (cond ((integerp e
) (not (oddp e
)))
2054 (t (eq '$even
(evod e
)))))
2057 (cond ((integerp e
) (oddp e
))
2059 (t (eq '$odd
(evod e
)))))
2061 ;; An extended evod that recognizes that abs(even) is even and
2065 (cond ((integerp e
) (if (oddp e
) '$odd
'$even
))
2068 (cond ((kindp e
'$odd
) '$odd
)
2069 ((kindp e
'$even
) '$even
)
2070 ;; Check the database for facts.
2071 ((symbolp e
) (check-integer-facts e
'evod
))))
2072 ((eq 'mtimes
(caar e
)) (evod-mtimes e
))
2073 ((eq 'mplus
(caar e
)) (evod-mplus e
))
2074 ((eq 'mabs
(caar e
)) (evod (cadr e
))) ;; extra code
2075 ((eq 'mexpt
(caar e
)) (evod-mexpt e
))))
2077 (defun evod-mtimes (x)
2078 (do ((l (cdr x
) (cdr l
)) (flag '$odd
))
2080 (setq x
(evod (car l
)))
2081 (cond ((eq '$odd x
))
2082 ((eq '$even x
) (setq flag
'$even
))
2083 ((maxima-integerp (car l
)) (cond ((eq '$odd flag
) (setq flag nil
))))
2086 (defun evod-mplus (x)
2087 (do ((l (cdr x
) (cdr l
)) (flag))
2088 ((null l
) (cond (flag '$odd
) (t '$even
)))
2089 (setq x
(evod (car l
)))
2090 (cond ((eq '$odd x
) (setq flag
(not flag
)))
2094 (defun evod-mexpt (x)
2095 (when (and (integerp (caddr x
)) (not (minusp (caddr x
))))
2098 (declare-top (special mgqp mlqp
))
2101 (atom (selector +labs
) (selector -labs
) (selector data
)))
2103 (defmacro c-dobj
(&rest x
)
2106 (defun dcompare (x y
)
2107 (setq odds
(list (sub x y
)) evens nil minus nil
2108 sign
(cond ((eq x y
) '$zero
)
2109 ((or (eq '$inf x
) (eq '$minf y
)) '$pos
)
2110 ((or (eq '$minf x
) (eq '$inf y
)) '$neg
)
2115 (setq x
(dinternp x
) y
(dinternp y
))
2116 (cond ((or (null x
) (null y
)) '$pnz
)
2117 ((progn (clear) (deq x y
) (sel y
+labs
)))
2121 (cond ((dmark x
'$zero
) nil
)
2123 (t (do ((l (sel x data
) (cdr l
))) ((null l
))
2124 (if (and (visiblep (car l
)) (deqf x y
(car l
))) (return t
))))))
2127 (cond ((eq 'meqp
(caar f
))
2128 (if (eq x
(cadar f
)) (deq (caddar f
) y
) (deq (cadar f
) y
)))
2129 ((eq 'mgrp
(caar f
))
2130 (if (eq x
(cadar f
)) (dgr (caddar f
) y
) (dls (cadar f
) y
)))
2131 ((eq 'mgqp
(caar f
))
2132 (if (eq x
(cadar f
)) (dgq (caddar f
) y
) (dlq (cadar f
) y
)))
2133 ((eq 'mnqp
(caar f
))
2134 (if (eq x
(cadar f
)) (dnq (caddar f
) y
) (dnq (cadar f
) y
)))))
2137 (cond ((dmark x
'$pos
) nil
)
2139 (t (do ((l (sel x data
) (cdr l
)))
2141 (when (or mlqp
(and (visiblep (car l
)) (dgrf x y
(car l
))))
2145 (cond ((eq 'mgrp
(caar f
)) (if (eq x
(cadar f
)) (dgr (caddar f
) y
)))
2146 ((eq 'mgqp
(caar f
)) (if (eq x
(cadar f
)) (dgr (caddar f
) y
)))
2147 ((eq 'meqp
(caar f
))
2148 (if (eq x
(cadar f
))
2150 (dgr (cadar f
) y
)))))
2153 (cond ((dmark x
'$neg
) nil
)
2155 (t (do ((l (sel x data
) (cdr l
)))
2157 (when (or mgqp
(and (visiblep (car l
)) (dlsf x y
(car l
))))
2161 (cond ((eq 'mgrp
(caar f
)) (if (eq x
(caddar f
)) (dls (cadar f
) y
)))
2162 ((eq 'mgqp
(caar f
)) (if (eq x
(caddar f
)) (dls (cadar f
) y
)))
2163 ((eq 'meqp
(caar f
))
2164 (if (eq x
(cadar f
)) (dls (caddar f
) y
) (dls (cadar f
) y
)))))
2167 (cond ((member (sel x
+labs
) '($pos $zero
) :test
#'eq
) nil
)
2168 ((eq '$nz
(sel x
+labs
)) (deq x y
))
2169 ((eq '$pn
(sel x
+labs
)) (dgr x y
))
2170 ((dmark x
'$pz
) nil
)
2171 ((eq x y
) (setq mgqp t
) nil
)
2172 (t (do ((l (sel x data
) (cdr l
))) ((null l
))
2173 (if (and (visiblep (car l
)) (dgqf x y
(car l
))) (return t
))))))
2176 (cond ((eq 'mgrp
(caar f
)) (if (eq x
(cadar f
)) (dgr (caddar f
) y
)))
2177 ((eq 'mgqp
(caar f
)) (if (eq x
(cadar f
)) (dgq (caddar f
) y
)))
2178 ((eq 'meqp
(caar f
))
2179 (if (eq x
(cadar f
)) (dgq (caddar f
) y
) (dgq (cadar f
) y
)))))
2182 (cond ((member (sel x
+labs
) '($neg $zero
) :test
#'eq
) nil
)
2183 ((eq '$pz
(sel x
+labs
)) (deq x y
))
2184 ((eq '$pn
(sel x
+labs
)) (dls x y
))
2185 ((dmark x
'$nz
) nil
)
2186 ((eq x y
) (setq mlqp t
) nil
)
2187 (t (do ((l (sel x data
) (cdr l
))) ((null l
))
2188 (if (and (visiblep (car l
)) (dlqf x y
(car l
))) (return t
))))))
2191 (cond ((eq 'mgrp
(caar f
)) (if (eq x
(caddar f
)) (dls (cadar f
) y
)))
2192 ((eq 'mgqp
(caar f
)) (if (eq x
(caddar f
)) (dlq (cadar f
) y
)))
2193 ((eq 'meqp
(caar f
))
2194 (if (eq x
(cadar f
)) (dlq (caddar f
) y
) (dlq (cadar f
) y
)))))
2197 (cond ((member (sel x
+labs
) '($pos $neg
) :test
#'eq
) nil
)
2198 ((eq '$pz
(sel x
+labs
)) (dgr x y
))
2199 ((eq '$nz
(sel x
+labs
)) (dls x y
))
2200 ((dmark x
'$pn
) nil
)
2202 (t (do ((l (sel x data
) (cdr l
))) ((null l
))
2203 (if (and (visiblep (car l
)) (dnqf x y
(car l
))) (return t
))))))
2206 (cond ((eq 'meqp
(caar f
))
2207 (if (eq x
(cadar f
)) (dnq (caddar f
) y
) (dnq (cadar f
) y
)))))
2209 ;; mark sign of x to be m, relative to current comparison point for dcomp.
2210 ;; returns true if this fact is already known, nil otherwise.
2212 (cond ((eq m
(sel x
+labs
)))
2213 ((and dbtrace
(prog1
2215 (mtell (intl:gettext
"DMARK: marking ~M ~M") (if (atom x
) x
(car x
)) m
))
2219 (push+sto
(sel x
+labs
) m
)
2222 (defun daddgr (flag x
)
2223 (with-compsplt (lhs rhs x
)
2224 (mdata flag
'mgrp
(dintern lhs
) (dintern rhs
))
2225 (if (or (mnump lhs
) (constant lhs
))
2226 (list '(mlessp) rhs lhs
)
2227 (list '(mgreaterp) lhs rhs
))))
2229 (defun daddgq (flag x
)
2230 (with-compsplt (lhs rhs x
)
2231 (mdata flag
'mgqp
(dintern lhs
) (dintern rhs
))
2232 (if (or (mnump lhs
) (constant lhs
))
2233 (list '(mleqp) rhs lhs
)
2234 (list '(mgeqp) lhs rhs
))))
2236 (defun daddeq (flag x
)
2237 (with-compsplt-eq (lhs rhs x
)
2238 (mdata flag
'meqp
(dintern lhs
) (dintern rhs
))
2239 (list '($equal
) lhs rhs
)))
2241 (defun daddnq (flag x
)
2242 (with-compsplt-eq (lhs rhs x
)
2243 (cond ((and (mtimesp lhs
) (equal rhs
0))
2244 (dolist (term (cdr lhs
)) (daddnq flag term
)))
2245 ((and (mexptp lhs
) (mexptp rhs
)
2246 (integerp (caddr lhs
)) (integerp (caddr rhs
))
2247 (equal (caddr lhs
) (caddr rhs
)))
2248 (mdata flag
'mnqp
(dintern (cadr lhs
)) (dintern (cadr rhs
)))
2249 (cond ((not (oddp (caddr lhs
)))
2250 (mdata flag
'mnqp
(dintern (cadr lhs
))
2251 (dintern (neg (cadr rhs
)))))))
2252 (t (mdata flag
'mnqp
(dintern lhs
) (dintern rhs
))))
2253 (list '(mnot) (list '($equal
) lhs rhs
))))
2255 ;; The following functions are used by asksign to write answers into the
2256 ;; database. We make sure that these answers are written into the global
2257 ;; context '$initial and not in a local context which might be generated during
2258 ;; the evaluation phase and which will be destroyed before the evaluation has
2260 ;; The additional facts are removed from the global context '$initial after
2261 ;; finishing the evaluation phase of meval with a call to clearsign.
2264 (let ((context '$initial
))
2266 (push (cons x
'$pos
) *local-signs
*)))
2269 (let ((context '$initial
))
2271 (push (cons x
'$neg
) *local-signs
*)))
2274 (let ((context '$initial
))
2276 (push (cons x
'$zero
) *local-signs
*)))
2279 (let ((context '$initial
))
2281 (push (cons x
'$pn
) *local-signs
*)))
2284 (let ((context '$initial
))
2286 (push (cons x
'$pz
) *local-signs
*)))
2288 (defun compsplt-eq (x)
2289 (with-compsplt (lhs rhs x
)
2291 (setq lhs rhs rhs
0))
2292 (if (and (equal rhs
0)
2294 (and (not (atom lhs
))
2295 (kindp (caar lhs
) '$oddfun
)
2296 (kindp (caar lhs
) '$increasing
))))
2297 (setq lhs
(cadr lhs
)))
2300 (defun mdata (flag r x y
)
2305 (defun mfact (r x y
)
2306 (let ((f (datum (list r x y
))))
2311 (defun mkill (r x y
)
2312 (let ((f (car (datum (list r x y
)))))
2318 (kind (dintern x
) (dintern y
)))
2320 ;; To guess from the previous incarnation of this code,
2321 ;; each argument is assumed to be a float, bigfloat, integer, or Maxima rational.
2322 ;; Convert Maxima rationals to Lisp rationals to make them comparable to others.
2325 (when (or ($bfloatp x
) ($bfloatp y
))
2327 x
(let (($float2bf t
))
2328 (declare (special $float2bf
))
2329 (cadr ($bfloat
(sub x y
))))
2331 (if (not (numberp x
))
2332 (setq x
(/ (cadr x
) (caddr x
))))
2333 (if (not (numberp y
))
2334 (setq y
(/ (cadr y
) (caddr y
))))
2336 (#-ecl
(> x y
) #+ecl
(> (- x y
) 0) '$pos
)
2337 (#-ecl
(> y x
) #+ecl
(> (- y x
) 0) '$neg
)
2341 (cons (car l
) (cons x
(cdr l
))))
2344 (cond ((eq '$pos s
) '$neg
)
2345 ((eq '$neg s
) '$pos
)
2350 (defun strongp (x y
)
2351 (cond ((eq '$pnz y
))
2353 ((member y
'($pz $nz $pn
) :test
#'eq
))))
2355 (defun munformat (form)
2358 (cons (caar form
) (mapcar #'munformat
(cdr form
)))))
2360 (defun declarekind (var prop
) ; This function is for $DECLARE to use.
2362 (cond ((truep (list 'kind var prop
)) t
)
2363 ((or (falsep (list 'kind var prop
))
2364 (and (setq prop2
(assoc prop
'(($integer . $noninteger
)
2365 ($noninteger . $integer
)
2366 ($increasing . $decreasing
)
2367 ($decreasing . $increasing
)
2368 ($symmetric . $antisymmetric
)
2369 ($antisymmetric . $symmetric
)
2370 ($rational . $irrational
)
2371 ($irrational . $rational
)
2372 ($oddfun . $evenfun
)
2373 ($evenfun . $oddfun
)) :test
#'eq
))
2374 (truep (list 'kind var
(cdr prop2
)))))
2375 (merror (intl:gettext
"declare: inconsistent declaration ~:M") `(($declare
) ,var
,prop
)))
2376 (t (mkind var prop
) t
))))
2378 ;;; These functions reformat expressions to be stored in the data base.
2380 ;; Return a list of all the atoms in X that aren't either numbers or constants
2381 ;; whose numerical value we know.
2382 (defun unknown-atoms (x)
2383 (let (($listconstvars t
))
2384 (declare (special $listconstvars
))
2385 (remove-if (lambda (sym) (mget sym
'$numer
))
2386 (cdr ($listofvars x
)))))
2388 ;; Rewrite a^b to a simpler expression that has the same sign:
2389 ;; If b is odd or 1/b is odd, remove the exponent, e.g. x^3 becomes x.
2390 ;; If b has a negative sign, return a^-b, e.g. 1/x^a becomes x^a.
2391 ;; Otherwise, do nothing.
2392 (defun rewrite-mexpt-retaining-sign (x)
2394 (let ((base (cadr x
)) (exponent (caddr x
)))
2395 (cond ((or (eq (evod exponent
) '$odd
) (eq (evod (inv exponent
)) '$odd
)) base
)
2396 ((negp exponent
) (inv x
))
2402 ;; Split X into (values LHS RHS) so that X>0 <=> LHS > RHS. This is supposed to
2403 ;; be a canonical form for X that can be stored in the database and then looked
2406 ;; This uses two worker routines: COMPSPLT-SINGLE and COMPSPLT-GENERAL. The
2407 ;; former assumes that X only contains one symbol whose value is not known (eg not %e,
2408 ;; %pi etc.). The latter tries to deal with arbitrary collections of variables.
2410 (multiple-value-bind (lhs rhs
)
2412 ((or (atom x
) (atom (car x
))) (values x
0))
2413 ((null (cdr (unknown-atoms x
))) (compsplt-single x
))
2414 (t (compsplt-general x
)))
2415 (let ((swapped nil
))
2416 ;; If lhs is zero, swap lhs and rhs to make the following code simpler.
2417 ;; Remember that they were swapped to swap them back afterwards.
2419 (setq lhs rhs rhs
0 swapped t
))
2421 ;; Rewrite mexpts in factors so that e.g. x^3/y>0 becomes x*y>0. */
2424 (cons (car lhs
) (mapcar #'rewrite-mexpt-retaining-sign
(cdr lhs
)))
2425 (rewrite-mexpt-retaining-sign lhs
))))
2426 ;; Undo swapping lhs and rhs.
2429 (values lhs rhs
)))))
2431 (defun compsplt-single (x)
2432 (do ((exp (list x
0)) (success nil
))
2433 ((or success
(symbols (cadr exp
))) (values (car exp
) (cadr exp
)))
2434 (cond ((atom (car exp
)) (setq success t
))
2435 ((eq (caaar exp
) 'mplus
) (setq exp
(splitsum exp
)))
2436 ((eq (caaar exp
) 'mtimes
) (setq exp
(splitprod exp
)))
2437 (t (setq success t
)))))
2439 (defun compsplt-general (x)
2440 ;; Let compsplt-single work on it first to treat constant factors/terms.
2441 (multiple-value-bind (lhs rhs
) (compsplt-single x
) (setq x
(sub lhs rhs
)))
2443 ;; If x is an atom or a single level list then we won't change it any.
2444 ((or (atom x
) (atom (car x
)))
2446 ;; If x is a negative expression but not a sum, then get rid of the
2448 ((negp x
) (values 0 (neg x
)))
2449 ;; If x is not a sum, or is a sum with more than 2 terms, or has some
2450 ;; symbols common to both summands, then do nothing.
2452 (not (eq (caar x
) 'mplus
))
2453 (intersect* (symbols (cadr x
)) (symbols (caddr x
))))
2455 ;; -x + y gives (y, x)
2456 ((and (or (negp (cadr x
)) (mnump (cadr x
)))
2457 (not (negp (caddr x
))))
2458 (values (caddr x
) (neg (cadr x
))))
2459 ;; x - y gives (x, y)
2460 ((and (not (negp (cadr x
)))
2461 (or (negp (caddr x
)) (mnump (caddr x
))))
2462 (values (cadr x
) (neg (caddr x
))))
2463 ;; - x - y gives (0, x+y)
2464 ((and (negp (cadr x
)) (negp (caddr x
)))
2471 (and (mtimesp x
) (mnegp (cadr x
))))
2473 (defun splitsum (exp)
2474 (do ((llist (cdar exp
) (cdr llist
))
2478 (if (mplusp lhs1
) (setq success t
))
2480 (cond ((member '$inf llist
:test
#'eq
)
2481 (setq rhs1
(add2 '$inf
(sub* rhs1
(addn llist t
)))
2482 lhs1
(add2 '$inf
(sub* lhs1
(addn llist t
)))
2484 ((member '$minf llist
:test
#'eq
)
2485 (setq rhs1
(add2 '$minf
(sub* rhs1
(addn llist t
)))
2486 lhs1
(add2 '$minf
(sub* lhs1
(addn llist t
)))
2488 ((null (symbols (car llist
)))
2489 (setq lhs1
(sub lhs1
(car llist
))
2490 rhs1
(sub rhs1
(car llist
)))))))
2492 (defun splitprod (exp)
2496 (llist (cdar exp
) (cdr llist
))
2502 (if (mtimesp lhs1
) (setq success t
))
2506 (t (list lhs1 rhs1
))))
2507 (when (null (symbols (car llist
)))
2509 (if (eq sign
'$neg
) (setq flipsign
(not flipsign
)))
2510 (if (member sign
'($pos $neg
) :test
#'eq
)
2511 (setq lhs1
(div lhs1
(car llist
))
2512 rhs1
(div rhs1
(car llist
)))))))
2515 (let (($listconstvars %initiallearnflag
))
2516 (declare (special $listconstvars
))
2517 (cdr ($listofvars x
))))
2519 ;; %initiallearnflag is only necessary so that %PI, %E, etc. can be LEARNed.
2521 (defun initialize-numeric-constant (c)
2522 (setq %initiallearnflag t
)
2523 (let ((context '$global
))
2524 (learn `((mequal) ,c
,(mget c
'$numer
)) t
))
2525 (setq %initiallearnflag nil
))
2527 (eval-when (:load-toplevel
:execute
)
2529 '(;; even and odd are integer
2530 (par ($even $odd
) $integer
)
2532 ; Cutting out inferences for integer, rational, real, complex (DK 10/2009).
2533 ; (kind $integer $rational)
2534 ; (par ($rational $irrational) $real)
2535 ; (par ($real $imaginary) $complex)
2537 ;; imaginary is complex
2538 (kind $imaginary $complex
)
2540 ;; Declarations for constants
2541 (kind $%i $noninteger
)
2542 (kind $%i $imaginary
)
2543 (kind $%e $noninteger
)
2545 (kind $%pi $noninteger
)
2547 (kind $%gamma $noninteger
)
2548 (kind $%gamma $real
)
2549 (kind $%phi $noninteger
)
2551 (kind $%pi $irrational
)
2552 (kind $%e $irrational
)
2553 (kind $%phi $irrational
)
2555 ;; Declarations for functions
2556 (kind %log $increasing
)
2557 (kind %atan $increasing
) (kind %atan $oddfun
)
2558 (kind $delta $evenfun
)
2559 (kind %sinh $increasing
) (kind %sinh $oddfun
)
2560 (kind %cosh $posfun
)
2561 (kind %tanh $increasing
) (kind %tanh $oddfun
)
2562 (kind %coth $oddfun
)
2563 (kind %csch $oddfun
)
2564 (kind %sech $posfun
)
2565 (kind %asinh $increasing
) (kind %asinh $oddfun
)
2566 ;; It would be nice to say %acosh is $posfun, but then
2567 ;; assume(xn<0); abs(acosh(xn)) -> acosh(xn), which is wrong
2568 ;; since acosh(xn) is complex.
2569 (kind %acosh $increasing
)
2570 (kind %atanh $increasing
) (kind %atanh $oddfun
)
2572 (kind $lambert_w $complex
)
2573 (kind %cabs $complex
)))
2575 ;; Create an initial context for the user which is a subcontext of $global.
2576 ($newcontext
'$initial
))
