		Search-engine friendly clone of the ACL2 documentation.

Mapping

Make-mapping

Basic constructor macro for mapping structures.

Syntax

(make-mapping [:name <name>] 
              [:key-name <key-name>] 
              [:key-type <key-type>] 
              [:value-name <value-name>] 
              [:value-type <value-type>])

This is the usual way to construct mapping structures. It simply conses together a structure with the specified fields.

This macro generates a new mapping structure from scratch. See also change-mapping, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-mapping

(defmacro make-mapping (&rest args)
  (std::make-aggregate 'mapping
                       args
                       '((:name)
                         (:key-name)
                         (:key-type)
                         (:value-name)
                         (:value-type))
                       'make-mapping
                       nil))

Function: mapping

(defun mapping (name key-name key-type value-name value-type)
  (declare (xargs :guard (and (identifierp name)
                              (identifierp key-name)
                              (finalize-typep key-type)
                              (identifierp value-name)
                              (finalize-typep value-type))))
  (declare (xargs :guard t))
  (let ((__function__ 'mapping))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (identifier-fix name)
                    :exec name))
         (key-name (mbe :logic (identifier-fix key-name)
                        :exec key-name))
         (key-type (mbe :logic (finalize-type-fix key-type)
                        :exec key-type))
         (value-name (mbe :logic (identifier-fix value-name)
                          :exec value-name))
         (value-type (mbe :logic (finalize-type-fix value-type)
                          :exec value-type)))
      (cons :mapping (list (cons 'name name)
                           (cons 'key-name key-name)
                           (cons 'key-type key-type)
                           (cons 'value-name value-name)
                           (cons 'value-type value-type))))))