		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat-from-stat1

Turn a stat1 value into a stat value.

Signature
(stat-from-stat1 stat1) → stat
Arguments: stat1 — Guard (stat1p stat1).
Returns: stat — Type (statp stat).

A transformation that generates the stobj definition from stat could also generate this conversion function.

This is not quite executable, because it calls the non-executable stat1->memory.

Definitions and Theorems

Function: stat-from-stat1

(defun stat-from-stat1 (stat1)
  (declare (xargs :stobjs (stat1)))
  (declare (xargs :guard (stat1p stat1)))
  (let ((__function__ 'stat-from-stat1))
    (declare (ignorable __function__))
    (make-stat :xregs (stat1->xregs stat1)
               :pc (stat1->pc stat1)
               :memory (stat1->memory stat1)
               :error (stat1->error stat1))))

Theorem: statp-of-stat-from-stat1

(defthm statp-of-stat-from-stat1
  (b* ((stat (stat-from-stat1 stat1)))
    (statp stat))
  :rule-classes :rewrite)