 (require 'cl-lib)
+
+(defun whatif--simplify-progn-body (forms bindings)
+  "Simplify all the forms in FORMS using partial application.
+If any form evaluates to a simple value, discard it unless
+it is is the final form."
+  (let (simplified-exprs current)
+    ;; Evaluate every expression in the progn body.
+    (dolist (form forms)
+      (setq current (whatif--simplify form bindings))
+      ;; If we evaluated the expression to a value, just throw it
+      ;; away.
+      (pcase current
+        (`(unknown ,subform)
+         (push (list 'unknown subform) simplified-exprs))))
+    ;; If the last expression was a value, we still need to return
+    ;; it.
+    (pcase current
+      (`(value ,value)
+       (push (list 'value value) simplified-exprs)))
+    (nreverse simplified-exprs)))
 
 (defun whatif--simplify (form bindings)
   "Simplify FORM in the context of BINDINGS using partial application.

    ;; Remove pointless values in progn, e.g.
    ;; (progn nil (foo) (bar)) -> (progn (foo) (bar))
    (`(progn . ,exprs)
     (let (simplified-exprs current)
       ;; Evaluate every expression in the progn body.
       (dolist (expr exprs)
         (setq current (whatif--simplify expr bindings))
         ;; If we evaluated the expression to a value, just throw it
         ;; away.
         (pcase current
           (`(unknown ,subform)
            (push (list 'unknown subform) simplified-exprs))))
       ;; If the last expression was a value, we still need to return
       ;; it.
       (pcase current
         (`(value ,value)
          (push (list 'value value) simplified-exprs)))
       (setq simplified-exprs (nreverse simplified-exprs))

       (if (eq 1 (length simplified-exprs))
           (car simplified-exprs)
         (list 'unknown `(progn ,@(mapcar #'cl-second simplified-exprs))))))
    
    ;; Eliminate or simplify a when statement if we can evaluate the
    ;; condition.
    (`(when ,cond . ,body)
     (pcase (whatif--simplify cond bindings)
       (`(value ,value)
        (if value (whatif--simplify (cons 'progn body) bindings)
          (list 'value nil)))
       (`(unknown ,_) (list 'unknown form))))
    
    (_ (list 'unknown form))))

(ert-deftest simplify--bool ()

  (should
   (equal
    (whatif--simplify '(when t x y) nil)
    (list 'unknown '(progn x y))))
  (should
   (equal
    (whatif--simplify '(when x y) '((y . 1)))
    (list 'unknown '(when x 1)))))

(ert-deftest simplify--unless ()
  (should
   (equal
    (whatif--simplify '(unless nil x y) nil)
    (list 'unknown '(progn x y))))
  (should
   (equal
    (whatif--simplify '(unless t x y) nil)
    (list 'value nil)))
  (should
   (equal
    (whatif--simplify '(unless x y) '((y . 1)))
    (list 'unknown '(unless x 1)))))
