		Search-engine friendly clone of the ACL2 documentation.

Struct-operations

Op-struct-make

Leo struct construction operation.

Signature
(op-struct-make name valmap env) → result
Arguments: name — Guard (identifierp name).; valmap — Guard (value-mapp valmap).; env — Guard (struct-denvp env).
Returns: result — Type (value-resultp result).

Given the name (identifier) of a struct type and a value map (from identifiers to values), we return the corresponding value provided that the type map corresponding to the value map is the one associated to the struct type name in the dynamic struct environment. It is an error if it differs, or if the struct type is not in the environment.

Definitions and Theorems

Function: op-struct-make

(defun op-struct-make (name valmap env)
  (declare (xargs :guard (and (identifierp name)
                              (value-mapp valmap)
                              (struct-denvp env))))
  (let ((__function__ 'op-struct-make))
    (declare (ignorable __function__))
    (b* ((cinfo (get-struct-dinfo name env))
         ((unless cinfo)
          (reserrf (list :struct-not-found (identifier-fix name))))
         (tymap (type-map-of-value-map valmap))
         ((unless (equal tymap (struct-dinfo->components cinfo)))
          (reserrf (list :struct-mistype
                         :required (struct-dinfo->components cinfo)
                         :supplied tymap))))
      (make-value-struct :type name
                         :components valmap))))

Theorem: value-resultp-of-op-struct-make

(defthm value-resultp-of-op-struct-make
  (b* ((result (op-struct-make name valmap env)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-struct-make-of-identifier-fix-name

(defthm op-struct-make-of-identifier-fix-name
  (equal (op-struct-make (identifier-fix name)
                         valmap env)
         (op-struct-make name valmap env)))

Theorem: op-struct-make-identifier-equiv-congruence-on-name

(defthm op-struct-make-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (op-struct-make name valmap env)
                  (op-struct-make name-equiv valmap env)))
  :rule-classes :congruence)

Theorem: op-struct-make-of-value-map-fix-valmap

(defthm op-struct-make-of-value-map-fix-valmap
  (equal (op-struct-make name (value-map-fix valmap)
                         env)
         (op-struct-make name valmap env)))

Theorem: op-struct-make-value-map-equiv-congruence-on-valmap

(defthm op-struct-make-value-map-equiv-congruence-on-valmap
  (implies (value-map-equiv valmap valmap-equiv)
           (equal (op-struct-make name valmap env)
                  (op-struct-make name valmap-equiv env)))
  :rule-classes :congruence)

Theorem: op-struct-make-of-struct-denv-fix-env

(defthm op-struct-make-of-struct-denv-fix-env
  (equal (op-struct-make name valmap (struct-denv-fix env))
         (op-struct-make name valmap env)))

Theorem: op-struct-make-struct-denv-equiv-congruence-on-env

(defthm op-struct-make-struct-denv-equiv-congruence-on-env
  (implies (struct-denv-equiv env env-equiv)
           (equal (op-struct-make name valmap env)
                  (op-struct-make name valmap env-equiv)))
  :rule-classes :congruence)