1; Simplification and evaluation of Boolean and conditional expressions.
2;
3; Copyright 2006 by Robert Dodier.
4; Released under the terms of the GNU General Public License.
5
6; Ideas that haven't gone anywhere yet:
7;  - given "if foo then bar else baz", simplify bar assuming foo,
8;    and simplify baz assuming not foo
9;  - flatten conditionals -- nested if --> if -- elseif -- elseif -- elseif -- else
10;  - arithmetic on conditionals -- distribute arithmetic ops over if
11;  - make up rules via tellsimp & friends for integrate / sum / diff applied to conditionals
12;  - knock out redundant clauses in simplification (i.e. if x implies y then knock out y)
13
14(in-package :maxima)
15
16; Kill off translation properties of conditionals.
17; Ideally we could avoid calling MEVAL when arguments are declared Boolean.
18; We're not there yet.
19
20(remprop 'mcond 'translate)
21
22; It's OK for MEVALATOMS to evaluate the arguments of MCOND.
23; %MCOND already has this property.
24(defprop mcond t evok)
25
26; X is an expression of the form ((OP) B1 G1 B2 G2 B3 G3 ...)
27; where OP is MCOND or %MCOND,
28; and B1, B2, B3, ... are boolean expressions,
29; and G1, G2, G3, ... are general expressions.
30
31; Evaluation of conditional expressions.
32
33; If any B evaluates to T,
34; then append B and G to the list of evaluated arguments, and ignore any remaining arguments.
35; If any B evaluates to NIL,
36; then ignore B and G, and continue processing arguments.
37; Otherwise, append B and G to the list of evaluated arguments, and continue processing arguments.
38
39; If the first element of the list of evaluated arguments is T,
40; return the second element.
41; Otherwise, construct a new conditional expression from the evaluated arguments.
42
43(defmspec mcond (x)
44  (let ((op (car x)) (args (cdr x)) (conditions) (consequences))
45    (loop while (> (length args) 0) do
46      (let* ((b (car args)) (g (cadr args)) (v (mevalp b)))
47        (cond
48          ((eq v t)
49           (setq conditions (append conditions (list v)))
50           (setq consequences (append consequences (list g)))
51           (setq args nil))
52          ((eq v nil)
53           nil)
54          (t
55            (setq conditions (append conditions (list v)))
56            (setq consequences (append consequences (list g)))))
57        (setq args (cddr args))))
58
59    (cond
60      ((eq (car conditions) t)
61       (meval (car consequences)))
62      (t
63        (setq consequences (mapcar 'mevalatoms consequences))
64        ; Burn off SIMP flag, if any, when constructing the new CAAR
65        (cons `(,(car op))
66              (apply 'append (mapcar #'(lambda (x y) `(,x ,y)) conditions consequences)))))))
67
68; Simplification of conditional expressions.
69
70; If any B simplifies to T or $TRUE,
71; then append B and G to the list of simplified arguments, and ignore any remaining arguments.
72; If any B simplifies to NIL or $FALSE,
73; then ignore B and G, and continue processing arguments.
74; Otherwise, append B and G to the list of simplified arguments, and continue processing arguments.
75
76; If there are no arguments remaining (i.e., expression is just ((MCOND)) or ((%MCOND))) return $FALSE.
77; If the first element of the list of simplified arguments is T or $TRUE, return the second element.
78; Otherwise, construct a new conditional expression from the simplified arguments.
79
80(defun simp-mcond-shorten (x z)
81  (let ((op (car x)) (args (cdr x)) (args-simplified))
82    (loop while (> (length args) 0) do
83      (let ((b (maybe-simplifya (car args) z)) (g (cadr args)))
84        (cond
85          ((or (eq b nil) (eq b '$false)) nil)
86          ((or (eq b t) (eq b '$true))
87           (setq args-simplified (append args-simplified (list b (maybe-simplifya g z)))
88                 args nil))
89          (t
90            (setq args-simplified (append args-simplified (list b (maybe-simplifya g z)))))))
91      (setq args (cddr args)))
92
93    (cond
94      ((null args-simplified) nil)
95      ((or (eq (car args-simplified) t) (eq (car args-simplified) t))
96       (cadr args-simplified))
97      (t
98        ; Indicate that the return value has been simplified.
99        (cons `(,(car op) simp) args-simplified)))))
100
101(defun simp-mcond (x y z)
102  (declare (ignore y))
103  (simp-mcond-shorten x z))
104
105(putprop 'mcond 'simp-mcond 'operators)
106(putprop '%mcond 'simp-mcond 'operators)
107
108; REDEFINE PARSE-CONDITION (IN SRC/NPARSE.LISP) TO APPEND NIL INSTEAD OF $FALSE
109; WHEN INPUT IS LIKE "IF FOO THEN BAR" (WITHOUT ELSE)
110
111(defun parse-condition (op)
112  (list* (parse (rpos op) (rbp op))
113	 (if (eq (first-c) '$then)
114	     (parse '$any (rbp (pop-c)))
115	     (mread-synerr "Missing `then'"))
116	 (case (first-c)
117	   (($else)   (list t (parse '$any (rbp (pop-c)))))
118	   (($elseif) (parse-condition (pop-c)))
119	   (t
120	    (list t nil)))))
121