
\subsection{Opportunistic laziness}

\begin{frame}[fragile]
\frametitle{Opportunistic laziness}

Sometimes the result of a function call may be apparent even without evaluating
all of its arguments
\begin{itemize}
\item \Code{(* (fib x) 0)}
\item \Code{(difference nil (mergesort x))}
\item \Code{(q-and nil (q-not x))}
\end{itemize}

\SmallSkip
Matt has improved MBE to facilitate this
\begin{itemize}
\item Defthm has improved awareness of MBE
\item Restrictions on nested MBEs have been loosened
\item Induction schemes may still have some issues
\end{itemize}

\end{frame}


\begin{frame}[fragile]
\frametitle{A simple example: q-ite}

Avoid evaluating \Code{y} or \Code{z} when \Code{x} evaluates to a constant

\begin{verbatim}
(defmacro q-ite (x y z) 
  `(mbe :logic (q-ite-fn ,x ,y ,z)
        :exec (let ((_x ,x))
                (cond ((null _x) ,z)
                      ((atom _x) ,y)
                      (t
                       (q-ite-fn _x ,y ,z)))))))

(add-macro-alias q-ite q-ite-fn)
(add-untranslate-pattern (q-ite-fn ?x ?y ?z)
                         (q-ite ?x ?y ?z))
\end{verbatim}
\end{frame}



\begin{frame}
\frametitle{Identifying additional opportunities}

In \Code{(q-and x$_1$ x$_2$ $\dots$ x$_n$)}, when any \Code{x$_i$} $=$ \Code{NIL}
then the answer is \Code{NIL}

\SmallSkip

Which order should we use?
\begin{itemize}
\item \Code{(q-and nil (q-not y))}
\item \Code{(q-and (q-not x) y)}
\item \Code{(q-and (q-not x) (q-not y))}
\end{itemize}

\SmallSkip
Surely cheap
\begin{itemize}
\item quoted constants, (``don't need to be evaluated'')
\item variables, (``already evaluated'')
\end{itemize}

\SmallSkip 
So we evaluate the surely-cheap arguments first
\end{frame}
