Map a list of type specifiers to a type specifier sequence in the language definition.
(ldm-type-spec-list tyspecs) → (mv erp tyspecseq)
The language definition only supports certain type specifier sequences. This mapping function recognizes the lists of type specifiers that correspond to the ones supported in the language definition.
Function:
(defun ldm-type-spec-list (tyspecs) (declare (xargs :guard (type-spec-listp tyspecs))) (declare (xargs :guard (type-spec-list-unambp tyspecs))) (let ((__function__ 'ldm-type-spec-list)) (declare (ignorable __function__)) (b* (((reterr) (c::tyspecseq-void)) (tyspecs (type-spec-list-fix tyspecs))) (cond ((equal tyspecs (list (type-spec-void))) (retok (c::tyspecseq-void))) ((equal tyspecs (list (type-spec-char))) (retok (c::tyspecseq-char))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-char))) (retok (c::tyspecseq-schar))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-char))) (retok (c::tyspecseq-uchar))) ((equal tyspecs (list (type-spec-short))) (retok (c::make-tyspecseq-sshort :signed nil :int nil))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-short))) (retok (c::make-tyspecseq-sshort :signed t :int nil))) ((equal tyspecs (list (type-spec-short) (type-spec-int))) (retok (c::make-tyspecseq-sshort :signed nil :int t))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-short) (type-spec-int))) (retok (c::make-tyspecseq-sshort :signed t :int t))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-short))) (retok (c::make-tyspecseq-ushort :int nil))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-short) (type-spec-int))) (retok (c::make-tyspecseq-ushort :int t))) ((equal tyspecs (list (type-spec-int))) (retok (c::make-tyspecseq-sint :signed nil :int t))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)))) (retok (c::make-tyspecseq-sint :signed t :int nil))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-int))) (retok (c::make-tyspecseq-sint :signed t :int t))) ((equal tyspecs (list (type-spec-unsigned))) (retok (c::make-tyspecseq-uint :int nil))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-int))) (retok (c::make-tyspecseq-uint :int t))) ((equal tyspecs (list (type-spec-long))) (retok (c::make-tyspecseq-slong :signed nil :int nil))) ((equal tyspecs (list (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-slong :signed nil :int t))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long))) (retok (c::make-tyspecseq-slong :signed t :int nil))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-slong :signed t :int t))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-long))) (retok (c::make-tyspecseq-ulong :int nil))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-ulong :int t))) ((equal tyspecs (list (type-spec-long) (type-spec-long))) (retok (c::make-tyspecseq-sllong :signed nil :int nil))) ((equal tyspecs (list (type-spec-long) (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-sllong :signed nil :int t))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-long))) (retok (c::make-tyspecseq-sllong :signed t :int nil))) ((equal tyspecs (list (type-spec-signed (keyword-uscores-none)) (type-spec-long) (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-sllong :signed t :int t))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-long))) (retok (c::make-tyspecseq-ullong :int nil))) ((equal tyspecs (list (type-spec-unsigned) (type-spec-long) (type-spec-long) (type-spec-int))) (retok (c::make-tyspecseq-ullong :int t))) ((equal tyspecs (list (type-spec-bool))) (retok (c::tyspecseq-bool))) ((equal tyspecs (list (type-spec-float))) (retok (c::make-tyspecseq-float :complex nil))) ((equal tyspecs (list (type-spec-float) (type-spec-complex))) (retok (c::make-tyspecseq-float :complex t))) ((equal tyspecs (list (type-spec-double))) (retok (c::make-tyspecseq-double :complex nil))) ((equal tyspecs (list (type-spec-double) (type-spec-complex))) (retok (c::make-tyspecseq-double :complex t))) ((equal tyspecs (list (type-spec-long) (type-spec-double))) (retok (c::make-tyspecseq-ldouble :complex nil))) ((equal tyspecs (list (type-spec-long) (type-spec-double) (type-spec-complex))) (retok (c::make-tyspecseq-ldouble :complex t))) ((and (consp tyspecs) (endp (cdr tyspecs)) (type-spec-case (car tyspecs) :struct)) (b* ((tyspec (car tyspecs)) (ident (check-strunispec-no-members (type-spec-struct->unwrap tyspec))) ((when (not ident)) (reterr (msg "Unsupported type specifier ~x0 that is ~ a structure specifier with members." tyspec))) ((erp ident1) (ldm-ident ident))) (retok (c::make-tyspecseq-struct :tag ident1)))) ((and (consp tyspecs) (endp (cdr tyspecs)) (type-spec-case (car tyspecs) :union)) (b* ((tyspec (car tyspecs)) (ident (check-strunispec-no-members (type-spec-union->unwrap tyspec))) ((when (not ident)) (reterr (msg "Unsupported type specifier ~x0 that is ~ a union specifier with members." tyspec))) ((erp ident1) (ldm-ident ident))) (retok (c::make-tyspecseq-union :tag ident1)))) ((and (consp tyspecs) (endp (cdr tyspecs)) (type-spec-case (car tyspecs) :enum)) (b* ((tyspec (car tyspecs)) (ident (check-enumspec-no-list (type-spec-enum->unwrap tyspec))) ((when (not ident)) (reterr (msg "Unsupported type specifier ~x0 that is ~ an enumeration specifier with enumerators." tyspec))) ((erp ident1) (ldm-ident ident))) (retok (c::make-tyspecseq-enum :tag ident1)))) ((and (consp tyspecs) (endp (cdr tyspecs)) (type-spec-case (car tyspecs) :typedef)) (b* ((tyspec (car tyspecs)) (ident (type-spec-typedef->name tyspec)) ((erp ident1) (ldm-ident ident))) (retok (c::make-tyspecseq-typedef :name ident1)))) (t (reterr (msg "Unsupported type specifier sequence ~x0." tyspecs)))))))
Theorem:
(defthm tyspecseqp-of-ldm-type-spec-list.tyspecseq (b* (((mv acl2::?erp ?tyspecseq) (ldm-type-spec-list tyspecs))) (c::tyspecseqp tyspecseq)) :rule-classes :rewrite)
Theorem:
(defthm ldm-type-spec-list-of-type-spec-list-fix-tyspecs (equal (ldm-type-spec-list (type-spec-list-fix tyspecs)) (ldm-type-spec-list tyspecs)))
Theorem:
(defthm ldm-type-spec-list-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (ldm-type-spec-list tyspecs) (ldm-type-spec-list tyspecs-equiv))) :rule-classes :congruence)