• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
      • Fresh-logical-name-with-$s-suffix
      • Irrelevant-formals-info
      • Std/system/function-queries
      • Std/system/term-queries
        • Check-mv-let-call
        • Term-possible-numbers-of-results
        • Check-user-term
        • Check-nary-lambda-call
        • Check-lambda-call
        • All-vars-open
        • Dumb-occur-var-open
        • Check-user-lambda
        • Check-if-call
        • One-way-unify$
        • Check-unary-lambda-call
        • Guard-verified-fnsp
        • All-non-gv-ffn-symbs
        • All-non-gv-exec-ffn-symbs
        • Check-fn-call
        • Guard-verified-exec-fnsp
        • Check-list-call
        • Check-or-call
        • Check-and-call
        • All-program-ffn-symbs
        • Lambda-guard-verified-fnsp
        • All-free/bound-vars
        • Check-mbt$-call
        • If-tree-leaf-terms
        • Check-not-call
        • Check-mbt-call
        • Term-guard-obligation
        • All-pkg-names
        • All-vars-in-untranslated-term
        • Std/system/all-fnnames
        • Lambda-logic-fnsp
        • Lambda-guard-verified-exec-fnsp
        • All-lambdas
        • Lambda-closedp
        • Std/system/all-vars
      • Std/system/term-transformations
      • Std/system/enhanced-utilities
      • Install-not-normalized-event
      • Install-not-normalized-event-lst
      • Std/system/term-function-recognizers
      • Genvar$
      • Std/system/event-name-queries
      • Pseudo-tests-and-call-listp
      • Maybe-pseudo-event-formp
      • Add-suffix-to-fn-or-const
      • Chk-irrelevant-formals-ok
      • Table-alist+
      • Pseudo-tests-and-callp
      • Add-suffix-to-fn-or-const-lst
      • Known-packages+
      • Add-suffix-to-fn-lst
      • Unquote-term
      • Event-landmark-names
      • Add-suffix-lst
      • Std/system/theorem-queries
      • Unquote-term-list
      • Std/system/macro-queries
      • Pseudo-command-landmark-listp
      • Install-not-normalized$
      • Pseudo-event-landmark-listp
      • Known-packages
      • Std/system/partition-rest-and-keyword-args
      • Rune-enabledp
      • Rune-disabledp
      • Included-books
      • Std/system/pseudo-event-formp
      • Std/system/plist-worldp-with-formals
      • Std/system/w
      • Std/system/geprops
      • Std/system/arglistp
      • Std/system/constant-queries
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/system/term-queries

Check-mv-let-call

Check if a term is a (translated) call of mv-let.

Signature

(check-mv-let-call term) 
  → 
(mv yes/no mv-var vars indices hides mv-term body-term)

Arguments

term — Guard (pseudo-termp term).

Returns

yes/no — Type (booleanp yes/no).

mv-var — Type (symbolp mv-var), given the guard.

vars — Type (symbol-listp vars), given the guard.

indices — Type (nat-listp indices).

hides — Type (boolean-listp hides).

mv-term — Type (pseudo-termp mv-term), given the guard.

body-term — Type (pseudo-termp body-term), given the guard.

In translated form, (mv-let (var1 ... varn) mv-term body-term) is

((lambda (mv)
         ((lambda (var1 ... varn) body-term-trans)
          (mv-nth '0 mv)
          ...
          (mv-nth 'n-1 mv)))
 mv-term-trans)

where mv-term-trans and body-term-trans are the translations of mv-term and body-term.

This utility checks if a translated term has the form above; it also checks that mv does not occur free in body-term (via dumb-occur-var-open for greater flexibility). If all these checks pass, it returns t as first result, and additionally the variable mv, the list (var1 ... varn), the term mv-term-trans, and the term body-term-trans. If the input term does not have that form, this utility returns nil for each result.

If the input term has the form above, it is not necessarily the result of translating mv-let. It could be the translation of (let ((mv mv-term)) (let ((var1 (mv-nth 0 mv)) ... (varn (mv-nth n-1 mv))) mv-body)) instead; it depends on whether mv-term is single-valued or multi-valued, and also on whether the term is translated for execution or not. However, the result of translating mv-let necessarily has the form above.

Note, however, that lambda expressions are always closed in translated terms directly obtained from untranslated terms. ACL2 accomplishes this closure by adding formal parameters to the lambda expressions for the otherwise free variables, and adding actual arguments identical to those variables; see remove-trivial-vars. This means that the lambda expressions above may have extra variables. To ``correct'' for this, before examining the two lambda expressions, we remove all their formal parameters that are identical to the corresponding arguments, via remove-trivial-vars's auxiliary function remove-equal-formals-actuals, which does exactly that. We do not use remove-trivial-vars because that one removes the trivial variables at all levels, while here we only want to remove the ones from the two lambda expressions being examined.

Note also that, due to this lambda expression closure, the mv variable is not always the symbol `mv': if that symbol happens to be a free variable, ACL2's translation picks a different symbol for the first formal argument of the outer lambda expression above. For instance,

:trans (let ((mv 0)) (mv-let (x y) (f mv) (list x y mv)))

produces a translated term with the symbol `mv0' as the variable bound to the multiple value. This is why this utility returns this variable as one of its results.

In translated terms directly obtained from untranslated terms, mv-lets always have (mv-nth i ...) calls for all contiguous indices i from 0 to the number of mv-let-bound variables minus 1, corresponding to all the bound variables (0-based). However, if a term is subjected to transformations like remove-unused-vars, some of those mv-nth calls may disappear (if they are not used in the body of the mv-let). Thus, for wider usability, this utility does not require all the mv-nth calls to be present. It only requires calls with strictly increasing indices, allowing gaps. The ordered list of indices actually present is returned, so that a caller can indipendently check that there are no gaps, if the term is not supposed to have any such gaps.

An additional complication derives from the fact that mv-let allows the declaration of ignored variables within, e.g. (mv-let (x y z) (mv 1 2 3) (declare (ignore x y)) z). In translated terms, this manifests in the addition of hide around the mv-nth terms, which in this example is

((lambda (mv)
         ((lambda (x y z) z)
          (hide (mv-nth '0 mv))
          (hide (mv-nth '1 mv))
          (mv-nth '2 mv)))
 (cons '1 (cons '2 (cons '3 'nil))))

This utility takes this possibility into account, and returns, as an additional result, a list of booleans, of the same length as variables and indices, that says whether the corresponding mv-nth is wrapped by hide or not. This way, the utility returns all the information about the term, which the caller may use as desired.

mv-let also support the declaration of ignorable variables. But these declarations do not introduce any hide wrapper or other change into the translated term.

This utility is a left inverse of make-mv-let-call.

Definitions and Theorems

Function: check-mv-let-call-aux

(defun check-mv-let-call-aux (terms min-index mv-var)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (natp min-index)
                              (symbolp mv-var))))
  (let ((__function__ 'check-mv-let-call-aux))
    (declare (ignorable __function__))
    (b* (((when (endp terms)) (mv t nil nil))
         (term (car terms))
         ((mv hide term)
          (if (and (true-listp term)
                   (consp term)
                   (consp (cdr term))
                   (atom (cddr term))
                   (eq (car term) 'hide))
              (mv t (cadr term))
            (mv nil term)))
         ((unless (and (true-listp term)
                       (consp term)
                       (consp (cdr term))
                       (consp (cddr term))
                       (atom (cdddr term))))
          (mv nil nil nil))
         ((unless (eq (car term) 'mv-nth))
          (mv nil nil nil))
         (index-term (cadr term))
         ((unless (eq (caddr term) mv-var))
          (mv nil nil nil))
         ((unless (quotep index-term))
          (mv nil nil nil))
         (index (unquote index-term))
         ((unless (natp index)) (mv nil nil nil))
         ((unless (>= index min-index))
          (mv nil nil nil))
         ((mv yes/no indices hides)
          (check-mv-let-call-aux (cdr terms)
                                 (1+ index)
                                 mv-var))
         ((unless yes/no) (mv nil nil nil)))
      (mv t (cons index indices)
          (cons hide hides)))))

Theorem: booleanp-of-check-mv-let-call-aux.yes/no

(defthm booleanp-of-check-mv-let-call-aux.yes/no
  (b* (((mv ?yes/no ?indices ?hides)
        (check-mv-let-call-aux terms min-index mv-var)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: nat-listp-of-check-mv-let-call-aux.indices

(defthm nat-listp-of-check-mv-let-call-aux.indices
  (b* (((mv ?yes/no ?indices ?hides)
        (check-mv-let-call-aux terms min-index mv-var)))
    (nat-listp indices))
  :rule-classes :rewrite)

Theorem: boolean-listp-of-check-mv-let-call-aux.hides

(defthm boolean-listp-of-check-mv-let-call-aux.hides
  (b* (((mv ?yes/no ?indices ?hides)
        (check-mv-let-call-aux terms min-index mv-var)))
    (boolean-listp hides))
  :rule-classes :rewrite)

Theorem: len-of-check-mv-let-call-aux.indices

(defthm len-of-check-mv-let-call-aux.indices
  (b* (((mv ?yes/no ?indices ?hides)
        (check-mv-let-call-aux terms min-index mv-var)))
    (implies yes/no
             (equal (len indices) (len terms)))))

Theorem: len-of-check-mv-let-call-aux.hides

(defthm len-of-check-mv-let-call-aux.hides
  (b* (((mv ?yes/no ?indices ?hides)
        (check-mv-let-call-aux terms min-index mv-var)))
    (implies yes/no
             (equal (len hides) (len terms)))))

Function: check-mv-let-call

(defun check-mv-let-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'check-mv-let-call))
    (declare (ignorable __function__))
    (b* (((when (variablep term))
          (mv nil nil nil nil nil nil nil))
         ((when (fquotep term))
          (mv nil nil nil nil nil nil nil))
         ((unless (flambda-applicationp term))
          (mv nil nil nil nil nil nil nil))
         (outer-lambda-expr (ffn-symb term))
         (formals (lambda-formals outer-lambda-expr))
         (actuals (fargs term))
         ((mv list-mv list-mv-term)
          (remove-equal-formals-actuals formals actuals))
         ((unless (and (consp list-mv)
                       (not (consp (cdr list-mv)))))
          (mv nil nil nil nil nil nil nil))
         (mv-var (car list-mv))
         ((unless (and (consp list-mv-term)
                       (not (consp (cdr list-mv-term)))))
          (mv nil nil nil nil nil nil nil))
         (mv-term (car list-mv-term))
         (inner-lambda-expr-call (lambda-body outer-lambda-expr))
         ((when (variablep inner-lambda-expr-call))
          (mv nil nil nil nil nil nil nil))
         ((when (fquotep inner-lambda-expr-call))
          (mv nil nil nil nil nil nil nil))
         ((unless (flambda-applicationp inner-lambda-expr-call))
          (mv nil nil nil nil nil nil nil))
         (inner-lambda-expr (ffn-symb inner-lambda-expr-call))
         (formals (lambda-formals inner-lambda-expr))
         (actuals (fargs inner-lambda-expr-call))
         ((mv vars mv-nths)
          (remove-equal-formals-actuals formals actuals))
         (body-term (lambda-body inner-lambda-expr))
         ((when (dumb-occur-var-open mv-var body-term))
          (mv nil nil nil nil nil nil nil))
         ((mv okp indices hides)
          (check-mv-let-call-aux mv-nths 0 mv-var))
         ((unless okp)
          (mv nil nil nil nil nil nil nil)))
      (mv t mv-var
          vars indices hides mv-term body-term))))

Theorem: booleanp-of-check-mv-let-call.yes/no

(defthm booleanp-of-check-mv-let-call.yes/no
  (b* (((mv ?yes/no ?mv-var ?vars
            ?indices ?hides ?mv-term ?body-term)
        (check-mv-let-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-check-mv-let-call.mv-var

(defthm symbolp-of-check-mv-let-call.mv-var
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (symbolp mv-var)))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-check-mv-let-call.vars

(defthm symbol-listp-of-check-mv-let-call.vars
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (symbol-listp vars)))
  :rule-classes :rewrite)

Theorem: nat-listp-of-check-mv-let-call.indices

(defthm nat-listp-of-check-mv-let-call.indices
  (b* (((mv ?yes/no ?mv-var ?vars
            ?indices ?hides ?mv-term ?body-term)
        (check-mv-let-call term)))
    (nat-listp indices))
  :rule-classes :rewrite)

Theorem: boolean-listp-of-check-mv-let-call.hides

(defthm boolean-listp-of-check-mv-let-call.hides
  (b* (((mv ?yes/no ?mv-var ?vars
            ?indices ?hides ?mv-term ?body-term)
        (check-mv-let-call term)))
    (boolean-listp hides))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-mv-let-call.mv-term

(defthm pseudo-termp-of-check-mv-let-call.mv-term
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (pseudo-termp mv-term)))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-check-mv-let-call.body-term

(defthm pseudo-termp-of-check-mv-let-call.body-term
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (pseudo-termp body-term)))
  :rule-classes :rewrite)

Theorem: len-of-check-mv-let-call.indices/vars

(defthm len-of-check-mv-let-call.indices/vars
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (implies yes/no
                      (equal (len indices) (len vars))))))

Theorem: len-of-check-mv-let-call.hides/vars

(defthm len-of-check-mv-let-call.hides/vars
  (implies (and (pseudo-termp term))
           (b* (((mv ?yes/no ?mv-var ?vars
                     ?indices ?hides ?mv-term ?body-term)
                 (check-mv-let-call term)))
             (implies yes/no
                      (equal (len hides) (len vars))))))

Theorem: acl2-count-of-check-mv-let-call.mv-term

(defthm acl2-count-of-check-mv-let-call.mv-term
  (b* (((mv ?yes/no ?mv-var ?vars
            ?indices ?hides ?mv-term ?body-term)
        (check-mv-let-call term)))
    (implies yes/no
             (< (acl2-count mv-term)
                (acl2-count term))))
  :rule-classes :linear)

Theorem: acl2-count-of-check-mv-let-call.body-term

(defthm acl2-count-of-check-mv-let-call.body-term
  (b* (((mv ?yes/no ?mv-var ?vars
            ?indices ?hides ?mv-term ?body-term)
        (check-mv-let-call term)))
    (implies yes/no
             (< (acl2-count body-term)
                (acl2-count term))))
  :rule-classes :linear)