		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Create-var

Create a variable in a computation state.

Signature
(create-var var val compst) → result
Arguments: var — Guard (identp var).; val — Guard (valuep val).; compst — Guard (compustatep compst).
Returns: result — Type (compustate-resultp result).

If there are no frames, we add the variable to the static storage; otherwise, we add the variable to the top scope of the top frame. The variable comes with a value. If there is already a variable with the same name (in the static storage or in the top scope of the top frame), we return an error: C disallows variable redefinition. However, there may well be a variable with the same in a different scope: in this case, the new variable hides the other one.

Prior to storing the value, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: create-var

(defun create-var (var val compst)
 (declare (xargs :guard (and (identp var)
                             (valuep val)
                             (compustatep compst))))
 (let ((__function__ 'create-var))
   (declare (ignorable __function__))
   (b*
    ((var (ident-fix var))
     ((when (equal (compustate-frames-number compst)
                   0))
      (b* ((static (compustate->static compst))
           (pair (omap::assoc var static))
           ((when (consp pair))
            (error (list :var-redefinition var)))
           (new-static
                (omap::update var (remove-flexible-array-member val)
                              static))
           (new-compst (change-compustate compst
                                          :static new-static)))
        new-compst))
     (frame (top-frame compst))
     (scopes (frame->scopes frame))
     (scope (car scopes))
     (pair (omap::assoc var scope))
     ((when (consp pair))
      (error (list :var-redefinition var)))
     (new-scope (omap::update var (remove-flexible-array-member val)
                              scope))
     (new-scopes (cons new-scope (cdr scopes)))
     (new-frame (change-frame frame :scopes new-scopes))
     (new-compst (push-frame new-frame (pop-frame compst))))
    new-compst)))

Theorem: compustate-resultp-of-create-var

(defthm compustate-resultp-of-create-var
  (b* ((result (create-var var val compst)))
    (compustate-resultp result))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-create-var

(defthm compustate-frames-number-of-create-var
  (b* ((?result (create-var var val compst)))
    (implies (compustatep result)
             (equal (compustate-frames-number result)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-create-var

(defthm compustate-scopes-numbers-of-create-var
  (implies (> (compustate-frames-number compst) 0)
           (b* ((?result (create-var var val compst)))
             (implies (compustatep result)
                      (equal (compustate-scopes-numbers result)
                             (compustate-scopes-numbers compst))))))

Theorem: create-var-of-ident-fix-var

(defthm create-var-of-ident-fix-var
  (equal (create-var (ident-fix var) val compst)
         (create-var var val compst)))

Theorem: create-var-ident-equiv-congruence-on-var

(defthm create-var-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (create-var var val compst)
                  (create-var var-equiv val compst)))
  :rule-classes :congruence)

Theorem: create-var-of-value-fix-val

(defthm create-var-of-value-fix-val
  (equal (create-var var (value-fix val) compst)
         (create-var var val compst)))

Theorem: create-var-value-equiv-congruence-on-val

(defthm create-var-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (create-var var val compst)
                  (create-var var val-equiv compst)))
  :rule-classes :congruence)

Theorem: create-var-of-compustate-fix-compst

(defthm create-var-of-compustate-fix-compst
  (equal (create-var var val (compustate-fix compst))
         (create-var var val compst)))

Theorem: create-var-compustate-equiv-congruence-on-compst

(defthm create-var-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (create-var var val compst)
                  (create-var var val compst-equiv)))
  :rule-classes :congruence)