 (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.

Returns a list ('value VALUE) if we could simplify the entire
FORM to an expression, or a list ('unknown NEW-FORM) if some
parts of FORM could not be simplified."
  (pcase form
    ;; nil and t evaluate to themselves.
    (`nil (list 'value nil))

  (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)))))
