		Search-engine friendly clone of the ACL2 documentation.

Add-io-pairs

Add-io-pairs-details

Details about add-io-pairs

This rather technical topic is intended for those who have read the documentation for add-io-pairs and related topics but would like a more complete understanding of how add-io-pairs works. Our hope is that very few will have any reason to read the present topic!

A key aspect of the implementation of add-io-pairs is the use of a table, io-pairs-table, to store all I/O pairs. Indeed, the utilities show-io-pairs and get-io-pairs retrieve I/O pairs from this table. When add-io-pairs is invoked on I/O pairs for a function symbol, fn, it extends that table with those I/O pairs and then generates a defun event for a new function. The documentation topic add-io-pairs explains that this new function, new-fn, computes by looking up the inputs in the available I/O pairs to get the result immediately if possible, otherwise calling fn. Finally, it uses a special form of memoization to compute calls of fn by calling new-fn.

The following log fleshes out the explanation above. It shows that add-io-pairs generates a call of make-event, which we expand below to see the events created by that make-event invocation. Comments have been inserted in lower case into the final output below.

ACL2 !>(defun f (x)
         (declare (xargs :guard t))
         (cons x x))
[[.. output elided ..]]
 F
ACL2 !>:trans1 (add-io-pair (f 3) (cons 3 (/ 6 2)))
 (ADD-IO-PAIRS (((F 3) (CONS 3 (/ 6 2)))))
ACL2 !>:trans1 (add-io-pairs (((f 3) (cons 3 (/ 6 2)))))
 (WITH-OUTPUT
  :OFF :ALL :ON ERROR :GAG-MODE NIL
  (MAKE-EVENT
    (B* ((TUPLES '(((F 3) (CONS 3 (/ 6 2)))))
         (HINTS 'NIL)
         (DEBUG 'NIL)
         (TEST 'EQUAL)
         (WRLD (W STATE))
         ((WHEN (NULL TUPLES))
          (VALUE '(VALUE-TRIPLE :EMPTY-IO-PAIRS)))
         (CTX 'ADD-IO-PAIRS)
         ((ER IO-DOUBLET-LST)
          (ADD-IO-PAIRS-TRANSLATE-TUPLES TUPLES CTX WRLD STATE))
         (FN (CAAR (CAR TUPLES)))
         (EVENTS (ADD-IO-PAIRS-EVENTS FN
                                      IO-DOUBLET-LST HINTS DEBUG TEST WRLD)))
        (VALUE (CONS 'PROGN EVENTS)))
    :ON-BEHALF-OF :QUIET!))
ACL2 !>(b* ((tuples '(((f 3) (cons 3 (/ 6 2)))))
            (hints 'nil)
            (debug 'nil)
            (test 'equal)
            (wrld (w state))
            ((when (null tuples))
             (value '(value-triple :empty-io-pairs)))
            (ctx 'add-io-pairs)
            ((er io-doublet-lst)
             (add-io-pairs-translate-tuples tuples ctx wrld state))
            (fn (caar (car tuples)))
            (events (add-io-pairs-events fn io-doublet-lst hints debug
                                         test wrld)))
         (value (cons 'progn events)))
 (PROGN

 ; Cause an error when including a book or running the second pass of an
 ; encapsulate, if the I/O pairs for F in the io-pairs table do not match
 ; those in the table from a previous invocation -- unless we are in the
 ; scope of merge-io-pairs for F.
  (CHECK-IO-PAIRS-LENIENCE F NIL ADD-IO-PAIRS)

 ; Update the I/O pairs for F in the io-pairs-table.
  (TABLE
      IO-PAIRS-TABLE 'F
      (LET ((OLD-ENTRY (CDR (ASSOC-EQ 'F
                                      (TABLE-ALIST 'IO-PAIRS-TABLE WORLD)))))
           (UPDATE-IO-LOOKUP-LST '(((3) (3 . 3)))
                                 OLD-ENTRY)))

 ; Define the new-fn for F.
  (DEFUN F29623679 (X)
         (DECLARE (XARGS :VERIFY-GUARDS T))
         (DECLARE (XARGS :GUARD T))
         (LET* ((IO-LOOKUP-VAR0 '((3 (3 . 3))))
                (IO-LOOKUP-VAR0 (IO-LOOKUP IO-LOOKUP-VAR0 EQUAL X)))
               (IF IO-LOOKUP-VAR0 (CAR IO-LOOKUP-VAR0)
                   (F X))))

 ; Prove that F equals its new-fn, as required by the memoize call below.
  (DEFTHM F52318143 (EQUAL (F X) (F29623679 X))
          :RULE-CLASSES NIL)

 ; Remove any existing memoization of F (redundant if F is not memoized).
  (UNMEMOIZE 'F)

 ; Arrange for F to call its new-fn.
  (MEMOIZE 'F :INVOKE 'F29623679))
ACL2 !>

It is also instructive to look at the implementation of merge-io-pairs. We can see what is going on by using single-step macroexpansion, below: first, push-io-pairs-lenience removes any check-io-pairs-lenience checks discussed above for the indicated function symbols; next, the books are included; then, install-io-pairs merges all I/O pairs for each function (as discussed below); and finally, the pop-io-pairs-lenience call undoes the effect of the push-io-pairs-lenience call.

ACL2 !>:trans1 (merge-io-pairs (f g h)
                               (include-book "book1")
                               (include-book "book2"))
 (PROGN (PUSH-IO-PAIRS-LENIENCE F G H)
        (INCLUDE-BOOK "book1")
        (INCLUDE-BOOK "book2")
        (INSTALL-IO-PAIRS F)
        (INSTALL-IO-PAIRS G)
        (INSTALL-IO-PAIRS H)
        (POP-IO-PAIRS-LENIENCE F G H))
ACL2 !>

The discussion above leads us to look at the implementation of install-io-pairs, again using a log (below). Notice that the events are essentially the same as for add-io-pairs, except that the table is not changed. In particular, there is still a call of check-io-pairs-lenience, for essentially the same reason: imagine if (install-io-pairs f) is in a certified book that is included after having added I/O pairs for f in the current session.

ACL2 !>:trans1 (install-io-pairs f)
 (WITH-OUTPUT
  :OFF :ALL :ON ERROR :GAG-MODE NIL
  (MAKE-EVENT
    (B* ((FN 'F)
         (HINTS 'NIL)
         (DEBUG 'NIL)
         (TEST 'EQUAL)
         (WRLD (W STATE))
         (IO-DOUBLET-LST :SKIP)
         (EVENTS (ADD-IO-PAIRS-EVENTS FN
                                      IO-DOUBLET-LST HINTS DEBUG TEST WRLD)))
        (VALUE (CONS 'PROGN EVENTS)))
    :ON-BEHALF-OF :QUIET!))
ACL2 !>(b* ((fn 'f)
            (hints 'nil)
            (debug 'nil)
            (test 'equal)
            (wrld (w state))
            (io-doublet-lst :skip)
            (events (add-io-pairs-events fn io-doublet-lst hints debug
                                         test wrld)))
         (value (cons 'progn events)))
 (PROGN (CHECK-IO-PAIRS-LENIENCE F NIL INSTALL-IO-PAIRS)
        (DEFUN F1824557376 (X)
               (DECLARE (XARGS :VERIFY-GUARDS T))
               (DECLARE (XARGS :GUARD T))
               (LET* ((IO-LOOKUP-VAR0 'NIL)
                      (IO-LOOKUP-VAR0 (IO-LOOKUP IO-LOOKUP-VAR0 EQUAL X)))
                     (IF IO-LOOKUP-VAR0 (CAR IO-LOOKUP-VAR0)
                         (F X))))
        (DEFTHM F1847247744
                (EQUAL (F X) (F1824557376 X))
                :RULE-CLASSES NIL)
        (UNMEMOIZE 'F)
        (MEMOIZE 'F :INVOKE 'F1824557376))
ACL2 !>

We conclude by noting that remove-io-pairs not only removes all I/O pairs for the indicated function symbols from the io-pairs-table, but also unmemoizes those function symbols. By contrast, deinstall-io-pairs leaves the io-pairs-table unchanged, merely unmemoizing the indicated function.