		Search-engine friendly clone of the ACL2 documentation.

Types

Ldm-type

Map a type in type to a type in the language definition.

Signature
(ldm-type type) → (mv erp type1)
Arguments: type — Guard (typep type).
Returns: type1 — Type (c::typep type1).

This function can be regarded as an extension of the collection of ldm- functions in mapping-to-language-definition. The supported types are the same as discussed in type-formalp.

Definitions and Theorems

Function: ldm-type

(defun ldm-type (type)
  (declare (xargs :guard (typep type)))
  (b* (((reterr) (c::type-void)))
    (type-case type :void (retok (c::type-void))
               :char (retok (c::type-char))
               :schar (retok (c::type-schar))
               :uchar (retok (c::type-uchar))
               :sshort (retok (c::type-sshort))
               :ushort (retok (c::type-ushort))
               :sint (retok (c::type-sint))
               :uint (retok (c::type-uint))
               :slong (retok (c::type-slong))
               :ulong (retok (c::type-ulong))
               :sllong (retok (c::type-sllong))
               :ullong (retok (c::type-ullong))
               :float
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :double
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :ldouble
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :floatc
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :doublec
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :ldoublec
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :bool
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :struct
               (if type.tag? (b* (((erp tag) (ldm-ident type.tag?)))
                               (retok (c::type-struct tag)))
                 (reterr (msg "Type ~x0 not supported."
                              (type-fix type))))
               :union
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :enum
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :array
               (reterr (msg "Type ~x0 not supported."
                            (type-fix type)))
               :pointer
               (b* (((erp refd-type) (ldm-type type.to)))
                 (retok (c::make-type-pointer :to refd-type)))
               :function (reterr (msg "Type ~x0 not supported."
                                      (type-fix type)))
               :unknown (reterr (msg "Type ~x0 not supported."
                                     (type-fix type))))))

Theorem: typep-of-ldm-type.type1

(defthm typep-of-ldm-type.type1
  (b* (((mv acl2::?erp ?type1)
        (ldm-type type)))
    (c::typep type1))
  :rule-classes :rewrite)

Theorem: ldm-type-when-type-formalp

(defthm ldm-type-when-type-formalp
  (implies (type-formalp type)
           (b* (((mv acl2::?erp ?type1)
                 (ldm-type type)))
             (not erp))))

Theorem: ldm-type-of-type-fix-type

(defthm ldm-type-of-type-fix-type
  (equal (ldm-type (type-fix type))
         (ldm-type type)))

Theorem: ldm-type-type-equiv-congruence-on-type

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