		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmtlist-compile-top

Signature
(svstmtlist-compile-top x &key sclimit (nb-delayp 't)) → (mv ok warnings final-st constraints blk-masks nonblk-masks)
Arguments: x — Guard (svstmtlist-p x).; sclimit — Guard (natp sclimit).
Returns: warnings — Type (vl-warninglist-p warnings).; final-st — Type (svstate-p final-st).; constraints — Type (constraintlist-p constraints).; blk-masks — Type (4vmask-alist-p blk-masks).; nonblk-masks — Type (4vmask-alist-p nonblk-masks).

Definitions and Theorems

Function: svstmtlist-compile-top-fn

(defun svstmtlist-compile-top-fn (x sclimit nb-delayp)
 (declare (xargs :guard (and (svstmtlist-p x) (natp sclimit))))
 (let ((__function__ 'svstmtlist-compile-top))
  (declare (ignorable __function__))
  (b*
   (((mv ok
         warnings st jst blk-masks nonblk-masks)
     (svstmtlist-compile x (make-svstate)
                         sclimit nb-delayp nil nil nil))
    ((svjumpstate jst))
    (final-st
     (svstate-fork
          (svstate-merge-branches jst.returncond jst.returnst st))))
   (svjumpstate-free jst)
   (svstate-free st)
   (mv ok warnings final-st jst.constraints
       blk-masks nonblk-masks))))

Theorem: vl-warninglist-p-of-svstmtlist-compile-top.warnings

(defthm vl-warninglist-p-of-svstmtlist-compile-top.warnings
  (b* (((mv vl::?ok vl::?warnings ?final-st
            ?constraints ?blk-masks ?nonblk-masks)
        (svstmtlist-compile-top-fn x sclimit nb-delayp)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: svstate-p-of-svstmtlist-compile-top.final-st

(defthm svstate-p-of-svstmtlist-compile-top.final-st
  (b* (((mv vl::?ok vl::?warnings ?final-st
            ?constraints ?blk-masks ?nonblk-masks)
        (svstmtlist-compile-top-fn x sclimit nb-delayp)))
    (svstate-p final-st))
  :rule-classes :rewrite)

Theorem: constraintlist-p-of-svstmtlist-compile-top.constraints

(defthm constraintlist-p-of-svstmtlist-compile-top.constraints
  (b* (((mv vl::?ok vl::?warnings ?final-st
            ?constraints ?blk-masks ?nonblk-masks)
        (svstmtlist-compile-top-fn x sclimit nb-delayp)))
    (constraintlist-p constraints))
  :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-svstmtlist-compile-top.blk-masks

(defthm 4vmask-alist-p-of-svstmtlist-compile-top.blk-masks
  (b* (((mv vl::?ok vl::?warnings ?final-st
            ?constraints ?blk-masks ?nonblk-masks)
        (svstmtlist-compile-top-fn x sclimit nb-delayp)))
    (4vmask-alist-p blk-masks))
  :rule-classes :rewrite)

Theorem: 4vmask-alist-p-of-svstmtlist-compile-top.nonblk-masks

(defthm 4vmask-alist-p-of-svstmtlist-compile-top.nonblk-masks
  (b* (((mv vl::?ok vl::?warnings ?final-st
            ?constraints ?blk-masks ?nonblk-masks)
        (svstmtlist-compile-top-fn x sclimit nb-delayp)))
    (4vmask-alist-p nonblk-masks))
  :rule-classes :rewrite)

Theorem: vars-of-svstmtlist-compile-top

(defthm vars-of-svstmtlist-compile-top
 (b* (((mv vl::?ok vl::?warnings ?final-st
           ?constraints ?blk-masks ?nonblk-masks)
       (svstmtlist-compile-top-fn x sclimit nb-delayp)))
   (implies
        (and (svarlist-addr-p (svstmtlist-vars x))
             ok)
        (and (svarlist-addr-p (svstate-vars final-st))
             (svarlist-addr-p (constraintlist-vars constraints))))))

Theorem: svstmtlist-compile-top-fn-of-svstmtlist-fix-x

(defthm svstmtlist-compile-top-fn-of-svstmtlist-fix-x
  (equal (svstmtlist-compile-top-fn (svstmtlist-fix x)
                                    sclimit nb-delayp)
         (svstmtlist-compile-top-fn x sclimit nb-delayp)))

Theorem: svstmtlist-compile-top-fn-svstmtlist-equiv-congruence-on-x

(defthm svstmtlist-compile-top-fn-svstmtlist-equiv-congruence-on-x
 (implies
      (svstmtlist-equiv x x-equiv)
      (equal (svstmtlist-compile-top-fn x sclimit nb-delayp)
             (svstmtlist-compile-top-fn x-equiv sclimit nb-delayp)))
 :rule-classes :congruence)

Theorem: svstmtlist-compile-top-fn-of-nfix-sclimit

(defthm svstmtlist-compile-top-fn-of-nfix-sclimit
  (equal (svstmtlist-compile-top-fn x (nfix sclimit)
                                    nb-delayp)
         (svstmtlist-compile-top-fn x sclimit nb-delayp)))

Theorem: svstmtlist-compile-top-fn-nat-equiv-congruence-on-sclimit

(defthm svstmtlist-compile-top-fn-nat-equiv-congruence-on-sclimit
 (implies
      (nat-equiv sclimit sclimit-equiv)
      (equal (svstmtlist-compile-top-fn x sclimit nb-delayp)
             (svstmtlist-compile-top-fn x sclimit-equiv nb-delayp)))
 :rule-classes :congruence)