Discussion of how if-then-else objects are dealt with in FGL.
One of the most powerful and advantageous things about FGL is that it can
avoid case splits in proofs by encoding the case splits into Boolean functions
that are later handled by fast solvers. For example, if a function might
return either 3 or 5, then instead of considering the two cases separately we
can encode both cases into a symbolic integer value. But for some case splits
the cases aren't so easily merged into a single symbolic value, except by
directly encoding the case split. For example, if we have
Such cases can cause dilemmas and problems for FGL's symbolic interpretation. For example, suppose we have the following rewrite rules:
(foo (bar x) y) = (baz x y) (foo (zar x) y) = (fuz x y)
But suppose that when we encounter a call of
(foo (if c a b) y) = (if c (foo a y) (foo b y))
But this means the user needs to know all of the places this might happen and make a rewrite rule for each of them, and by that time it might be just as catastrophic for performance.
Because of the dilemma above, the default approach in FGL is to cause an error whenever we are unable to merge the two branches of an if-then-else into a single symbolic form automatically. When this happens, the FGL clause processor will produce an error saying that an if-then-else failed to merge and to look at the debug object. This behavior can be disabled as follows:
(assign :fgl-make-ites t)
It is also possible to use rewrite rules to allow if-then-else objects to be
created in certain cases; we discuss how this is used to handle a couple of
common cases in the next section. The FGL interpreter includes support for
FGL uses a function
To force the creation of an if-then-else, overriding the setting of
(def-gl-branch-merge if-with-if-with-nil-nil (equal (if test (if test2 then nil) nil) (if! (and test test2) then nil)))
This will ensure that a
The FGL interpreter can be told to distribute calls of a given function over if-then-else objects that might appear in their arguments as follows:
This is similar to creating a rewrite rule matching an
(def-gl-rewrite foo-of-if-1 (equal (foo (if test a1 a2) b) (if test (foo a1 b) (foo a2 b)))) (def-gl-rewrite foo-of-if-2 (equal (foo a (if test b1 b2)) (if test (foo a b1) (foo a b2))))
(Enabling if splitting for a function enables it for all the arguments; if this isn't desired, then providing rewrite rules like the ones above is a reasonable alternative.)
Generally speaking, it is likely to be advantageous to enable splitting ifs on a couple of kinds of functions:
Conversely, it is likely not advantageous to enable splitting ifs on functions that are handled by expanding a definition-style rule where the arguments to the function on the LHS are just variables.
Here are some general ideas for encoding data so as to avoid if-then-elses. After that, we provide some examples to give a flavor for how this works.
(Note: the built-in support for symbols as enum types makes the following example largely unnecessary, but still illustrative.)
(defun vector-kind (x) (cond ((equal (loghead 2 x) 0) :big) ((equal (logtail 2 x) 0) :little) (t :neither))) ;; Want to prove: (fgl::fgl-thm :hyp (unsigned-byte-p 4 x) :concl (let* ((kind (vector-kind x))) (case kind (:big (not (logbitp 0 x))) (:little (and (or (logbitp 0 x) (logbitp 1 x)) (not (logbitp 2 x)))) (:neither (or (logbitp 2 x) (logbitp 3 x)))))) ;; But when we try this we get a merge error -- (@ :fgl-interp-error-debug-obj) shows ;; (14 :LITTLE :NEITHER) and (@ :fgl-interp-error-debug-stack) shows we were ;; applying the definition of VECTOR-KIND. ;; Vector-kind produces a symbol that is one of (:big :little :neither) -- an enumeration type. ;; We can encode that in a few different ways -- as a number or as a priority-encoding. (defun vector-kind-encoding (littlep bigp) (cond (littlep :little) (bigp :big) (t :neither))) ;; Turn off this function's definition! Keep the if-then-else inside it hidden. (fgl::disable-definition vector-kind-encoding) (table fgl::fgl-fn-modes 'vector-kind-encoding (fgl::make-fgl-function-mode :dont-concrete-exec t)) ;; Now rephrase vector-kind in terms of vector-kind-encoding: (fgl::def-fgl-rewrite vector-kind-to-encoding2 (equal (vector-kind x) (cond ((equal (loghead 2 x) 0) (vector-kind-encoding nil t)) ((equal (logtail 2 x) 0) (vector-kind-encoding t nil)) (t (vector-kind-encoding nil nil))))) ;; At minimum we need a rule for checking equality of a vector-kind-encoding. ;; Note: EQUAL will unify both ways, so no need to worry about the order of the ;; arguments! (fgl::def-fgl-rewrite equal-of-vector-kind-encoding (equal (equal (vector-kind-encoding littlep bigp) x) (cond (littlep (equal x :little)) (bigp (equal x :big)) (t (equal x :neither))))) ;; Now the fgl-thm above will go through. ;; Often we might also need a rule for merging if-then-elses where the encoding ;; is one branch. But we can only merge if the other branch is also one of the ;; symbols in the enumeration, so we need to test for that. (defun vector-kind-p (x) (or (equal x :big) (equal x :little) (equal x :neither))) (fgl::disable-definition vector-kind-p) (fgl::def-fgl-rewrite vector-kind-p-of-vector-kind-encoding (vector-kind-p (vector-kind-encoding littlep bigp))) (fgl::def-fgl-branch-merge if-with-vector-kind-encoding (implies (vector-kind-p else) (equal (if test (vector-kind-encoding littlep bigp) else) (vector-kind-encoding (if test littlep (equal else :little)) (if test bigp (equal else :big)))))) ;; Alternatively, we could instead turn off expansion of (vector-kind x) and ;; write rules directly on that: :ubt! vector-kind-encoding (fgl::disable-definition vector-kind) (fgl::def-fgl-rewrite equal-of-vector-kind (equal (equal y (vector-kind x)) (cond ((equal (loghead 2 x) 0) (equal y :big)) ((equal (logtail 2 x) 0) (equal y :little)) (t (equal y :neither))))) (defun vector-kind-p (x) (or (equal x :big) (equal x :little) (equal x :neither))) (fgl::disable-definition vector-kind-p) (fgl::def-fgl-rewrite vector-kind-p-of-vector-kind (vector-kind-p (vector-kind x))) (fgl::def-fgl-branch-merge if-then-else-of-vector-kind (implies (vector-kind-p else) (equal (if test (vector-kind x) else) (vector-kind (if test x (case else (:big 4) (:little 2) (otherwise 6)))))))
Member-equal is often used to just test whether or not an object is a member of a list. But it returns much more information than that -- it returns the tail of the list beginning with that object. Because that extra information is inconvenient to represent in FGL, we represent it instead in a way that prevents us from needing to reason about this extra information.
;; This function is just IF, but we'll turn off its definition. (defun fgl-hidden-if (test then else) (if test then else)) (fgl::disable-definition fgl-hidden-if) ;; This function represents a value that is likely to be just treated as ;; Boolean, but may not actually be T when it is non-NIL. The TRUE input ;; determines its truth value and VAL determines its actual form when non-NIL. ;; We use this function when we think we won't need the actual value of val, ;; just its truth value. (defun maybe-value (true val) (and true (or val t))) (fgl::disable-definition maybe-value) ;; Under IFF, maybe-value is just its truth value. (def-fgl-rewrite maybe-value-under-iff (iff (maybe-value true val) true)) ;; To merge a maybe-value with some other object, merge with the test under an ;; IFF context and then merge the value using fgl-hidden-if. (def-fgl-branch-merge maybe-value-merge (equal (if test (maybe-value true val) else) (maybe-value (if test true (and else t)) (fgl-hidden-if test val else)))) ;; We probably shouldn't need to compare maybe-value with equal, but this might ;; succeed if we end up needing to. (def-fgl-rewrite equal-of-maybe-value (equal (equal (maybe-value true val) x) (if true (if val (equal x val) (equal x t)) (not x)))) ;; We'll represent member-equal using maybe-value. Memberp-equal gives its ;; truth value: (defun memberp-equal (x lst) (if (atom lst) nil (or (equal x (car lst)) (memberp-equal x (cdr lst))))) ;; We introduce a version of member-equal about which we won't prove any rules, ;; so as to hide it away in the value of the maybe-value: (defun hide-member-equal (x lst) (member-equal x lst)) ;; Turn off both member-equal and hide-member-equal... (fgl::disable-definition member-equal) (fgl::disable-definition hide-member-equal) (defthm memberp-equal-iff-member-equal (iff (memberp-equal x lst) (member-equal x lst))) ;; Now when we see member-equal, we'll hide its full value away using ;; hide-member-equal and expose its Boolean value (memberp-equal) through ;; maybe-value. (def-fgl-rewrite member-equal-to-maybe-value (equal (member-equal x lst) (maybe-value (memberp-equal x lst) (hide-member-equal x lst))))