• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
            • Ex-args
            • Expand
            • Expand-measure
            • Ex-outs
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Function-expansion

Expand

Signature

(expand expand-args fty-info abs state) → expanded-result

Arguments

expand-args — Guard (ex-args-p expand-args).

fty-info — Guard (fty-info-alist-p fty-info).

abs — Guard (symbol-listp abs).

Returns

expanded-result — Type (ex-outs-p expanded-result).

Definitions and Theorems

Function: expand

(defun expand (expand-args fty-info abs state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (ex-args-p expand-args)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'expand))
  (declare (ignorable acl2::__function__))
  (b*
   ((expand-args (ex-args-fix expand-args))
    (fty-info (fty-info-alist-fix fty-info))
    ((ex-args a) expand-args)
    ((unless (consp a.term-lst))
     (make-ex-outs :expanded-term-lst nil
                   :expanded-fn-lst a.expand-lst))
    ((cons term rest) a.term-lst)
    ((if (symbolp term))
     (b* ((rest-res (expand (change-ex-args a :term-lst rest)
                            fty-info abs state))
          ((ex-outs o) rest-res))
       (make-ex-outs
            :expanded-term-lst (cons term o.expanded-term-lst)
            :expanded-fn-lst o.expanded-fn-lst)))
    ((if (equal (car term) 'quote))
     (b* ((rest-res (expand (change-ex-args a :term-lst rest)
                            fty-info abs state))
          ((ex-outs o) rest-res))
       (make-ex-outs
            :expanded-term-lst (cons term o.expanded-term-lst)
            :expanded-fn-lst o.expanded-fn-lst)))
    ((cons fn-call fn-actuals) term)
    ((if (pseudo-lambdap fn-call))
     (b*
      ((lambda-formals (lambda-formals fn-call))
       (body-res
        (expand
             (change-ex-args a
                             :term-lst (list (lambda-body fn-call)))
             fty-info abs state))
       ((ex-outs b) body-res)
       (lambda-body (car b.expanded-term-lst))
       (actuals-res
            (expand (change-ex-args a
                                    :term-lst fn-actuals
                                    :expand-lst b.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs ac) actuals-res)
       (lambda-actuals ac.expanded-term-lst)
       ((unless (mbt (equal (len lambda-formals)
                            (len lambda-actuals))))
        (make-ex-outs :expanded-term-lst a.term-lst
                      :expanded-fn-lst a.expand-lst))
       (lambda-fn
          (cons (cons 'lambda
                      (cons lambda-formals (cons lambda-body 'nil)))
                lambda-actuals))
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs
           :expanded-term-lst (cons lambda-fn r.expanded-term-lst)
           :expanded-fn-lst r.expanded-fn-lst)))
    ((unless (mbt (symbolp fn-call)))
     (make-ex-outs :expanded-term-lst a.term-lst
                   :expanded-fn-lst a.expand-lst))
    (fn (hons-get fn-call a.fn-lst))
    ((unless fn)
     (b*
      (((unless (function-symbolp fn-call (w state)))
        (prog2$ (er hard? 'smt-goal-generator=>expand
                    "Should be a function call: ~q0"
                    fn-call)
                (make-ex-outs :expanded-term-lst a.term-lst
                              :expanded-fn-lst a.expand-lst)))
       (basic-function (member-equal fn-call *smt-basics*))
       (flex? (fncall-of-flextype fn-call fty-info))
       (abs? (member-equal fn-call abs))
       (lvl-item (assoc-equal fn-call a.fn-lvls))
       (extract-res (meta-extract-formula fn-call state))
       ((if (equal fn-call 'return-last))
        (b*
         ((actuals-res
               (expand (change-ex-args a
                                       :term-lst (last fn-actuals))
                       fty-info abs state))
          ((ex-outs ac) actuals-res)
          (rest-res
             (expand (change-ex-args a
                                     :term-lst rest
                                     :expand-lst ac.expanded-fn-lst)
                     fty-info abs state))
          ((ex-outs r) rest-res))
         (make-ex-outs
              :expanded-term-lst (cons (car ac.expanded-term-lst)
                                       r.expanded-term-lst)
              :expanded-fn-lst r.expanded-fn-lst)))
       ((if (or basic-function
                flex? abs? (<= a.wrld-fn-len 0)
                (and lvl-item (zp (cdr lvl-item)))
                (equal extract-res ''t)))
        (b*
         ((actuals-res
               (expand (change-ex-args a :term-lst fn-actuals)
                       fty-info abs state))
          ((ex-outs ac) actuals-res)
          (rest-res
             (expand (change-ex-args a
                                     :term-lst rest
                                     :expand-lst ac.expanded-fn-lst)
                     fty-info abs state))
          ((ex-outs r) rest-res))
         (make-ex-outs :expanded-term-lst
                       (cons (cons fn-call ac.expanded-term-lst)
                             r.expanded-term-lst)
                       :expanded-fn-lst r.expanded-fn-lst)))
       (formals (formals fn-call (w state)))
       ((unless (symbol-listp formals))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "formals get a list that's not a symbol-listp for ~q0, the formals are ~q1"
          fn-call formals)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       ((unless (true-listp extract-res))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "meta-extract-formula returning a non-true-listp for ~q0The extracted result is ~q1"
          fn-call extract-res)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       (body (nth 2 extract-res))
       ((unless (pseudo-termp body))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "meta-extract-formula returning a non-pseudo-term for ~q0The body is ~q1"
          fn-call body)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       (updated-expand-lst (if (assoc-equal term a.expand-lst)
                               a.expand-lst
                             (cons (cons term term) a.expand-lst)))
       (body-res
        (expand
         (change-ex-args a
                         :term-lst (list body)
                         :fn-lvls (cons (cons fn-call '0) a.fn-lvls)
                         :wrld-fn-len (1- a.wrld-fn-len)
                         :expand-lst updated-expand-lst)
         fty-info abs state))
       ((ex-outs b) body-res)
       (expanded-lambda-body (car b.expanded-term-lst))
       (expanded-lambda
            (cons 'lambda
                  (cons formals
                        (cons expanded-lambda-body 'nil))))
       (actuals-res
            (expand (change-ex-args a
                                    :term-lst fn-actuals
                                    :expand-lst b.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs ac) actuals-res)
       (expanded-term-list ac.expanded-term-lst)
       ((unless (equal (len formals)
                       (len expanded-term-list)))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "You called your function with the wrong number of actuals: ~q0"
          term)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst ac.expanded-fn-lst)))
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs :expanded-term-lst
                    (cons (cons expanded-lambda expanded-term-list)
                          r.expanded-term-lst)
                    :expanded-fn-lst r.expanded-fn-lst)))
    (lvl-item (assoc-equal fn-call a.fn-lvls))
    ((unless lvl-item)
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "Function ~q0 exists in the definition list but not in the levels list?"
       fn-call)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    ((if (zp (cdr lvl-item)))
     (b*
      ((actuals-res (expand (change-ex-args a :term-lst fn-actuals)
                            fty-info abs state))
       ((ex-outs ac) actuals-res)
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs
        :expanded-term-lst (cons (cons fn-call ac.expanded-term-lst)
                                 r.expanded-term-lst)
        :expanded-fn-lst r.expanded-fn-lst)))
    (new-fn-lvls (update-fn-lvls fn-call a.fn-lvls))
    ((func f) (cdr fn))
    (extract-res (meta-extract-formula fn-call state))
    ((unless (true-listp extract-res))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "meta-extract-formula returning a non-true-listp for ~q0The extracted result is ~q1"
       fn-call extract-res)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    (body (nth 2 extract-res))
    ((unless (pseudo-termp body))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "meta-extract-formula returning a non-pseudo-term for ~q0The body is ~q1"
       fn-call body)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    (updated-expand-lst (if (assoc-equal term a.expand-lst)
                            a.expand-lst
                          (cons (cons term term) a.expand-lst)))
    (formals f.flattened-formals)
    (body-res
         (expand (change-ex-args a
                                 :term-lst (list body)
                                 :fn-lvls new-fn-lvls
                                 :expand-lst updated-expand-lst)
                 fty-info abs state))
    ((ex-outs b) body-res)
    (expanded-lambda-body (car b.expanded-term-lst))
    (expanded-lambda (cons 'lambda
                           (cons formals
                                 (cons expanded-lambda-body 'nil))))
    (actuals-res
         (expand (change-ex-args a
                                 :term-lst fn-actuals
                                 :expand-lst b.expanded-fn-lst)
                 fty-info abs state))
    ((ex-outs ac) actuals-res)
    (expanded-term-list ac.expanded-term-lst)
    ((unless (equal (len formals)
                    (len expanded-term-list)))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "You called your function with the wrong number of actuals: ~q0"
       term)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst ac.expanded-fn-lst)))
    (rest-res
         (expand (change-ex-args a
                                 :term-lst rest
                                 :expand-lst ac.expanded-fn-lst)
                 fty-info abs state))
    ((ex-outs r) rest-res))
   (make-ex-outs :expanded-term-lst
                 (cons (cons expanded-lambda expanded-term-list)
                       r.expanded-term-lst)
                 :expanded-fn-lst r.expanded-fn-lst))))

Theorem: ex-outs-p-of-expand

(defthm ex-outs-p-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (ex-outs-p expanded-result))
  :rule-classes :rewrite)

Theorem: pseudo-term-alistp-of-expand

(defthm pseudo-term-alistp-of-expand
 (b* ((expanded-result (expand expand-args fty-info abs state)))
  (implies
   (ex-args-p expand-args)
   (pseudo-term-alistp (ex-outs->expanded-fn-lst expanded-result))))
 :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-expand

(defthm pseudo-term-listp-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (implies (ex-args-p expand-args)
             (pseudo-term-listp
                  (ex-outs->expanded-term-lst expanded-result))))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-car-of-expand

(defthm pseudo-termp-of-car-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (implies
         (ex-args-p expand-args)
         (pseudo-termp
              (car (ex-outs->expanded-term-lst expanded-result)))))
  :rule-classes :rewrite)

Theorem: len-of-expand

(defthm len-of-expand
 (b* ((expanded-result (expand expand-args fty-info abs state)))
  (implies (ex-args-p expand-args)
           (equal (len (ex-outs->expanded-term-lst expanded-result))
                  (len (ex-args->term-lst expand-args)))))
 :rule-classes :rewrite)