		Search-engine friendly clone of the ACL2 documentation.

Atc-types

Type-to-maker

Turn a type into a term that makes (evaluates to) it.

Signature
(type-to-maker type) → term
Arguments: type — Guard (typep type).
Returns: term — A term.

This is somewhat meta.

Definitions and Theorems

Function: type-to-maker

(defun type-to-maker (type)
 (declare (xargs :guard (typep type)))
 (let ((__function__ 'type-to-maker))
  (declare (ignorable __function__))
  (type-case
      type
      :void '(type-void)
      :char '(type-char)
      :schar '(type-schar)
      :uchar '(type-uchar)
      :sshort '(type-sshort)
      :ushort '(type-ushort)
      :sint '(type-sint)
      :uint '(type-uint)
      :slong '(type-slong)
      :ulong '(type-ulong)
      :sllong '(type-sllong)
      :ullong '(type-ullong)
      :struct
      (cons 'type-struct
            (cons (cons 'ident
                        (cons (ident->name (type-struct->tag type))
                              'nil))
                  'nil))
      :pointer
      (cons 'make-type-pointer
            (cons ':to
                  (cons (type-to-maker (type-pointer->to type))
                        'nil)))
      :array (cons 'make-type-array
                   (cons ':of
                         (cons (type-to-maker (type-array->of type))
                               (cons ':size
                                     (cons (type-array->size type)
                                           'nil))))))))

Theorem: type-to-maker-of-type-fix-type

(defthm type-to-maker-of-type-fix-type
  (equal (type-to-maker (type-fix type))
         (type-to-maker type)))

Theorem: type-to-maker-type-equiv-congruence-on-type

(defthm type-to-maker-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (type-to-maker type)
                  (type-to-maker type-equiv)))
  :rule-classes :congruence)