		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-let

Check if a term may be a let statement term.

Signature
(atc-check-let term) → (mv yes/no var val body wrapper?)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; var — Type (symbolp var).; val — Type (pseudo-termp val).; body — Type (pseudo-termp body).; wrapper? — Type (symbolp wrapper?).

The forms of these terms are described in the user documentation.

Here we recognize and decompose statement terms that are lets. In translated form, (let ((var val)) body) is ((lambda (var) body) val). However, if body has other free variables in addition to var, those appear as both formal parameters and actual arguments, e.g. ((lambda (var x y) rest<var,x,y>) val x y): this is because ACL2 translated terms have all closed lambda expressions, so ACL2 adds formal parameters and actual arguments to make that happen. Here, we must remove them in order to get the ``true'' let. This is done via a system utility.

We also return the declar or assign wrapper, if present; nil if absent.

Definitions and Theorems

Function: atc-check-let

(defun atc-check-let (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'atc-check-let))
    (declare (ignorable __function__))
    (b* (((acl2::fun (no))
          (mv nil nil nil nil nil))
         ((mv okp formals body actuals)
          (fty-check-lambda-call term))
         ((when (not okp)) (no))
         ((mv formals actuals)
          (fty-remove-equal-formals-actuals formals actuals))
         ((unless (and (list-lenp 1 formals)
                       (list-lenp 1 actuals)))
          (no))
         (var (first formals))
         (possibly-wrapped-val (first actuals))
         ((unless (pseudo-term-case possibly-wrapped-val :fncall))
          (mv t var possibly-wrapped-val body nil))
         ((pseudo-term-fncall possibly-wrapped-val)
          possibly-wrapped-val)
         ((unless (member-eq possibly-wrapped-val.fn
                             '(declar assign)))
          (mv t var possibly-wrapped-val body nil))
         ((unless (list-lenp 1 possibly-wrapped-val.args))
          (no)))
      (mv t var (first possibly-wrapped-val.args)
          body possibly-wrapped-val.fn))))

Theorem: booleanp-of-atc-check-let.yes/no

(defthm booleanp-of-atc-check-let.yes/no
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-let.var

(defthm symbolp-of-atc-check-let.var
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (symbolp var))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-let.val

(defthm pseudo-termp-of-atc-check-let.val
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (pseudo-termp val))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-let.body

(defthm pseudo-termp-of-atc-check-let.body
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (pseudo-termp body))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-let.wrapper?

(defthm symbolp-of-atc-check-let.wrapper?
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (symbolp wrapper?))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-let-val

(defthm pseudo-term-count-of-atc-check-let-val
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (implies yes/no
             (< (pseudo-term-count val)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-let-body

(defthm pseudo-term-count-of-atc-check-let-body
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (implies yes/no
             (< (pseudo-term-count body)
                (pseudo-term-count term))))
  :rule-classes :linear)

Theorem: pseudo-term-count-of-atc-check-let

(defthm pseudo-term-count-of-atc-check-let
  (b* (((mv ?yes/no ?var ?val ?body ?wrapper?)
        (atc-check-let term)))
    (implies yes/no
             (< (+ (pseudo-term-count val)
                   (pseudo-term-count body))
                (pseudo-term-count term))))
  :rule-classes :linear)