		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-matrix

Retrieve the matrix of a function introduced via defun-sk, in untranslated form.

Signature
(defun-sk-matrix fn wrld) → matrix
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: matrix — A pseudo-termp.

If fn is defined (i.e. :constrain is nil or absent), then after translation, the (unnormalized) body of fn should have the form (return-last 'progn (throw-nonexec-error ...) core) if fn is non-executable (i.e. it fn is introduced via defun-nx in the encapsulate), or just core otherwise. core should have one of the following forms, where arg1, ..., argN are the formal arguments of fn, and matrix is the translated matrix:

```
((lambda (bvar) matrix) (witness arg1 ... argN))
```
if there is just one bound variable bvar, as resulting from the translation of the let.

((lambda (mv argN ... arg1)
        ((lambda (bvar1 ... bvarM argN ... arg1) matrix)
         (mv-nth '0 mv) ... (mv-nth 'M-1 mv) argN ... arg1))
(witness arg1 ... argN) arg1 ... argN)

if there are M > 1 bound variables, as resulting from the translation of the mv-let.

If instead fn is constrained (i.e. :constrain is not nil), the generated definition theorem for fn should have the form (equal (fn arg1 ... argN) core), with arg1, ..., argN and core as above.

Note that here we consider a function to be defined if it has an unnormalized body (via ubody). Certain program-mode functions may be defined without having an unnormalized body; however, defun-sk functions should always be in logic mode.

Use defun-sk-imatrix to retrieve the matrix in untranslated form.

Definitions and Theorems

Function: defun-sk-matrix

(defun defun-sk-matrix (fn wrld)
 (declare (xargs :guard (and (plist-worldp wrld)
                             (defun-sk-namep fn wrld))))
 (let ((__function__ 'defun-sk-matrix))
  (declare (ignorable __function__))
  (b* ((core (if (ubody fn wrld)
                 (b* ((body (ubody fn wrld)))
                   (if (non-executablep fn wrld)
                       (car (last body))
                     body))
               (b* ((def-thm (defun-sk-definition-name fn wrld)))
                 (third (thm-formula def-thm wrld))))))
   (if
    (= 1 (len (defun-sk-bound-vars fn wrld)))
    (case-match core
     (((& & matrix) . &) matrix)
     (&
      (raise
       "Internal error: ~
                     the translated definiens ~x0 ~
                     of the DEFUN-SK function ~x1 ~
                     is malformed."
       core fn)))
    (case-match core
     (((& & ((& & matrix) . &)) . &) matrix)
     (&
      (raise
       "Internal error: ~
                   the translated definiens ~x0 ~
                   of the DEFUN-SK function ~x1 ~
                   is malformed."
       core fn)))))))