Filtering...

basetypes

books/centaur/fty/basetypes

Included Books

defs pos-fix list-defuns fixtype equiv
other
(in-package "ACL2")
include-book
(include-book "std/basic/defs" :dir :system)
include-book
(include-book "std/basic/pos-fix" :dir :system)
include-book
(include-book "std/lists/list-defuns" :dir :system)
include-book
(include-book "fixtype")
local
(local (include-book "std/lists/equiv" :dir :system))
*defbasetype-keys*constant
(defconst *defbasetype-keys* '(:name :fix :topic))
defbasetype-fnfunction
(defun defbasetype-fn
  (equiv pred keys)
  (declare (xargs :mode :program))
  (b* ((__function__ 'defbasetype-fn) ((mv kwd-alist args) (extract-keywords __function__
          *defbasetype-keys*
          keys
          nil))
      ((when args) (raise "Bad args: ~x0" args))
      (pkg (if (equal (symbol-package-name pred) "COMMON-LISP")
          'foo
          pred))
      (typename (or (getarg :name nil kwd-alist)
          (b* ((predname (symbol-name pred)) (len (length predname))
              (p? (char predname (- len 1)))
              ((unless (eql p? #\P)) pred)
              (dash? (char predname (- len 2)))
              (newlen (- len
                  (if (eql dash? #\-)
                    2
                    1))))
            (intern-in-package-of-symbol (subseq predname 0 newlen) pkg))))
      (fix (or (getarg :fix nil kwd-alist)
          (intern-in-package-of-symbol (concatenate 'string (symbol-name typename) "-FIX")
            pkg)))
      (topic (getarg :topic typename kwd-alist)))
    `(deffixtype ,TYPENAME
      :pred ,PRED
      :fix ,FIX
      :equiv ,EQUIV
      :define t
      :topic ,TOPIC)))
defbasetypemacro
(defmacro defbasetype
  (equiv pred &rest keys)
  (defbasetype-fn equiv pred keys))
other
(defbasetype bit-equiv bitp :fix bfix :topic bitp)
other
(defbasetype nat-equiv natp :fix nfix :topic natp)
other
(defbasetype int-equiv
  integerp
  :fix ifix
  :name int
  :topic integerp)
other
(defbasetype rational-equiv
  rationalp
  :fix rfix
  :topic rationalp)
other
(defbasetype number-equiv
  acl2-numberp
  :fix fix
  :topic acl2-numberp)
other
(deffixtype true-list
  :pred true-listp
  :fix list-fix
  :equiv list-equiv
  :topic true-listp)
local
(local (in-theory (enable streqv)))
other
(deffixtype string
  :pred stringp
  :fix str-fix
  :equiv streqv
  :topic stringp)
other
(defsection true-p
  :parents (basetypes)
  :short "@(call true-p) recognizes only the symbol @('t')."
  (defun true-p (x) (declare (xargs :guard t)) (eq x t)))
other
(defsection true-fix
  :parents (basetypes)
  :short "@(call true-fix) ignores its argument and unconditionally returns @('t')."
  (defun true-fix
    (x)
    (declare (xargs :guard t)
      (ignore x))
    t))
other
(defsection true-equiv
  :parents (basetypes)
  :short "@(call true-equiv) is a ``degenerate'' equivalence for @(see true-p) objects."
  :long "<p>Because of the way @(see true-fix) works, this is always just true.</p>"
  (local (set-default-hints '('(:in-theory (enable true-fix true-p)))))
  (deffixtype true
    :pred true-p
    :fix true-fix
    :equiv true-equiv
    :define t
    :topic true-p))
other
(defsection symbol-fix
  :parents (basetypes symbolp)
  :short "@(call symbol-fix) is a fixing function for @(see symbolp); it is the
identity for symbols and coerces non-symbols to @('acl2::||'), i.e., the empty
symbol in the ACL2 package."
  :long "<p>Unfortunately it's not currently possible to come up with a good
symbol-fixing function that induces the proper congruences for both @(see
symbol-name) and @(see symbol-package-name).  This definition at least gives us
a congruence for @(see symbol-name).</p>

<p>BOZO consider adding a symbolp guard, inlining it, and turning it into an
identity function for execution.</p>"
  (defund symbol-fix
    (x)
    (declare (xargs :guard t))
    (if (symbolp x)
      x
      '))
  (local (in-theory (enable symbol-fix)))
  (defthm symbolp-of-symbol-fix
    (symbolp (symbol-fix x))
    :rule-classes :type-prescription)
  (defthm symbol-fix-when-symbolp
    (implies (symbolp x) (equal (symbol-fix x) x))))
other
(defsection symbol-equiv
  :parents (basetypes symbolp)
  :short "@(call symbol-equiv) recognizes symbols that are identical under
@(see symbol-fix)."
  (local (in-theory (enable symbol-fix)))
  (defbasetype symbol-equiv symbolp :topic symbolp)
  (defcong symbol-equiv equal (symbol-name x) 1))
other
(defsection pos-equiv
  :parents (basetypes posp)
  :short "@(call pos-equiv) is equality for positive numbers, i.e., equality up
to @(see pos-fix)."
  (defbasetype pos-equiv posp :fix pos-fix :topic posp))
other
(defsection lposfix
  :parents (basetypes posp)
  :short "@(call lposfix) is logically identical to @(call pos-fix), but its
guard requires that @('x') is a @(see posp) and, in the execution, it's just a
no-op that returns @('x')."
  (defun-inline lposfix
    (x)
    (declare (xargs :guard (posp x)))
    (mbe :logic (pos-fix x) :exec x)))
other
(deffixtype character
  :pred characterp
  :fix char-fix
  :equiv chareqv)
other
(defsection any-p
  :parents (basetypes)
  :short "@(call any-p) is always true; i.e., it recognizes any ACL2 object."
  :long "<p>This is a ``degenerate'' recognizer which is sometimes useful for
@(see fty).  For instance, it allows you to have fields within a @(see
fty::defprod) that are completely unconstrained, which may be especially useful
when you are in the early stages of development and haven't yet thought much
about types.</p>"
  (defun-inline any-p
    (x)
    (declare (xargs :guard t)
      (ignore x))
    t))
other
(deffixtype any
  :pred any-p
  :fix identity
  :equiv equal
  :topic any-p)
other
(defsection bool-fix
  :parents (basetypes booleanp)
  :short "@(call bool-fix) is a fixing function for Booleans; it coerces any
non-@('nil') symbol to @('t')."
  :long "<p>BOZO: could consider putting a @(see booleanp) guard here.</p>"
  (defund-inline bool-fix
    (x)
    (declare (xargs :guard t))
    (and x t))
  (local (in-theory (enable bool-fix)))
  (defthm booleanp-of-bool-fix
    (booleanp (bool-fix x))
    :rule-classes :type-prescription)
  (defthm bool-fix-when-booleanp
    (implies (booleanp x) (equal (bool-fix x) x)))
  (deffixtype bool
    :pred booleanp
    :fix bool-fix
    :equiv iff
    :topic booleanp)
  (defcong iff equal (bool-fix x) 1)
  (defthm bool-fix-under-iff (iff (bool-fix x) x)))
maybe-natp-when-natptheorem
(defthm maybe-natp-when-natp
  (implies (natp x) (maybe-natp x)))
natp-when-maybe-natptheorem
(defthmd natp-when-maybe-natp
  (implies (and (maybe-natp x) (double-rewrite x)) (natp x)))
other
(defsection maybe-natp-fix
  :parents (basetypes maybe-natp)
  :short "@(call maybe-natp-fix) is the identity for @(see maybe-natp)s, or
  coerces any invalid object to @('nil')."
  :long "<p>Performance note.  In the execution this is just an inlined
  identity function, i.e., it should have zero runtime cost.</p>"
  (defund-inline maybe-natp-fix
    (x)
    (declare (xargs :guard (maybe-natp x)))
    (mbe :logic (if x
        (nfix x)
        nil)
      :exec x))
  (local (in-theory (enable maybe-natp-fix)))
  (defthm maybe-natp-of-maybe-natp-fix
    (maybe-natp (maybe-natp-fix x))
    :rule-classes (:rewrite :type-prescription))
  (defthm maybe-natp-fix-when-maybe-natp
    (implies (maybe-natp x) (equal (maybe-natp-fix x) x)))
  (defthm maybe-natp-fix-under-iff (iff (maybe-natp-fix x) x))
  (defthm maybe-natp-fix-under-nat-equiv
    (nat-equiv (maybe-natp-fix x) x)
    :hints (("Goal" :in-theory (enable maybe-natp-fix)))))
other
(defsection maybe-nat-equiv
  :parents (basetypes maybe-natp)
  :short "@('(maybe-natp-equiv x y)') is an equivalence relation for @(see
  maybe-natp)s, i.e., equality up to @(see maybe-natp-fix)."
  :long "<p>Performance note.  In the execution, this is just an inlined call
  of @(see eql).</p>"
  (deffixtype maybe-nat
    :pred maybe-natp
    :fix maybe-natp-fix
    :equiv maybe-nat-equiv
    :define t
    :inline t
    :equal eql
    :topic maybe-natp))
maybe-posp-when-posptheorem
(defthm maybe-posp-when-posp
  (implies (posp x) (maybe-posp x)))
posp-when-maybe-posptheorem
(defthmd posp-when-maybe-posp
  (implies (and (maybe-posp x) (double-rewrite x)) (posp x)))
other
(defsection maybe-posp-fix
  :parents (basetypes maybe-posp)
  :short "@(call maybe-posp-fix) is the identity for @(see maybe-posp)s, or
  coerces any non-@(see posp) to @('nil')."
  :long "<p>Performance note.  In the execution this is just an inlined
  identity function, i.e., it should have zero runtime cost.</p>"
  (defund-inline maybe-posp-fix
    (x)
    (declare (xargs :guard (maybe-posp x)))
    (mbe :logic (if x
        (pos-fix x)
        nil)
      :exec x))
  (local (in-theory (enable maybe-posp-fix)))
  (defthm maybe-posp-of-maybe-posp-fix
    (maybe-posp (maybe-posp-fix x))
    :rule-classes (:rewrite :type-prescription))
  (defthm maybe-posp-fix-when-maybe-posp
    (implies (maybe-posp x) (equal (maybe-posp-fix x) x)))
  (defthm maybe-posp-fix-under-iff (iff (maybe-posp-fix x) x))
  (defthm maybe-posp-fix-under-pos-equiv
    (pos-equiv (maybe-posp-fix x) x)
    :hints (("Goal" :in-theory (enable maybe-posp-fix)))))
other
(defsection maybe-pos-equiv
  :parents (basetypes maybe-posp)
  :short "@('(maybe-posp-equiv x y)') is an equivalence relation for @(see
  maybe-posp)s, i.e., equality up to @(see maybe-posp-fix)."
  :long "<p>Performance note.  In the execution, this is just an inlined call
  of @(see eql).</p>"
  (deffixtype maybe-pos
    :pred maybe-posp
    :fix maybe-posp-fix
    :equiv maybe-pos-equiv
    :define t
    :inline t
    :equal eql
    :topic maybe-posp))
maybe-bitp-when-bitptheorem
(defthm maybe-bitp-when-bitp
  (implies (bitp x) (maybe-bitp x)))
bitp-when-maybe-bitptheorem
(defthmd bitp-when-maybe-bitp
  (implies (and (maybe-bitp x) (double-rewrite x)) (bitp x))
  :hints (("Goal" :in-theory (e/d (maybe-bitp) nil))))
other
(defsection maybe-bit-fix
  :parents (basetypes maybe-bitp)
  :short "@(call maybe-bit-fix) is the identity for @(see maybe-bitp)s, or
  coerces any non-@(see bitp) to @('nil')."
  :long "<p>Performance note.  In the execution this is just an inlined
  identity function, i.e., it should have zero runtime cost.</p>"
  (defund-inline maybe-bit-fix
    (x)
    (declare (xargs :guard (maybe-bitp x)
        :guard-hints (("Goal" :in-theory (e/d (maybe-bitp) nil)))))
    (mbe :logic (if x
        (bfix x)
        nil)
      :exec x))
  (local (in-theory (enable maybe-bitp maybe-bit-fix)))
  (defthm maybe-bitp-of-maybe-bit-fix
    (maybe-bitp (maybe-bit-fix x))
    :rule-classes (:rewrite :type-prescription))
  (defthm maybe-bit-fix-when-maybe-bitp
    (implies (maybe-bitp x) (equal (maybe-bit-fix x) x)))
  (defthm maybe-bit-fix-under-iff (iff (maybe-bit-fix x) x))
  (defthm maybe-bit-fix-under-bit-equiv
    (bit-equiv (maybe-bit-fix x) x)
    :hints (("Goal" :in-theory (enable maybe-bit-fix)))))
other
(defsection maybe-bit-equiv
  :parents (basetypes maybe-bitp)
  :short "@('(maybe-bitp-equiv x y)') is an equivalence relation for @(see
  maybe-bitp)s, i.e., equality up to @(see maybe-bit-fix)."
  :long "<p>Performance note.  In the execution, this is just an inlined call
  of @(see eql).</p>"
  (deffixtype maybe-bit
    :pred maybe-bitp
    :fix maybe-bit-fix
    :equiv maybe-bit-equiv
    :define t
    :inline t
    :equal eql
    :topic maybe-bitp))
maybe-integerp-when-integerptheorem
(defthm maybe-integerp-when-integerp
  (implies (integerp x) (maybe-integerp x)))
integerp-when-maybe-integerptheorem
(defthmd integerp-when-maybe-integerp
  (implies (and (maybe-integerp x) (double-rewrite x))
    (integerp x)))
other
(defsection maybe-integerp-fix
  :parents (basetypes maybe-integerp)
  :short "@(call maybe-integerp-fix) is the identity for @(see maybe-integerp)s, or
  coerces any invalid object to @('nil')."
  :long "<p>Performance note.  In the execution this is just an inlined
  identity function, i.e., it should have zero runtime cost.</p>"
  (defund-inline maybe-integerp-fix
    (x)
    (declare (xargs :guard (maybe-integerp x)))
    (mbe :logic (if x
        (ifix x)
        nil)
      :exec x))
  (local (in-theory (enable maybe-integerp-fix)))
  (defthm maybe-integerp-of-maybe-integerp-fix
    (maybe-integerp (maybe-integerp-fix x))
    :rule-classes (:rewrite :type-prescription))
  (defthm maybe-integerp-fix-when-maybe-integerp
    (implies (maybe-integerp x)
      (equal (maybe-integerp-fix x) x)))
  (defthm maybe-integerp-fix-under-iff
    (iff (maybe-integerp-fix x) x))
  (defthm maybe-integerp-fix-under-int-equiv
    (int-equiv (maybe-integerp-fix x) x)
    :hints (("Goal" :in-theory (enable maybe-integerp-fix)))))
other
(defsection maybe-integer-equiv
  :parents (basetypes maybe-integerp)
  :short "@('(maybe-integerp-equiv x y)') is an equivalence relation for @(see
  maybe-integerp)s, i.e., equality up to @(see maybe-integerp-fix)."
  :long "<p>Performance note.  In the execution, this is just an inlined call
  of @(see eql).</p>"
  (deffixtype maybe-integer
    :pred maybe-integerp
    :fix maybe-integerp-fix
    :equiv maybe-integer-equiv
    :define t
    :inline t
    :equal eql
    :topic maybe-integerp))
make-basetypes-table-rcharsfunction
(defun make-basetypes-table-rchars
  (table acc)
  (declare (xargs :mode :program))
  (b* (((when (atom table)) acc) ((fixtype type) (cdar table))
      (row (concatenate 'string
          "<tr><td><sf>"
          (string-downcase (symbol-name type.name))
          "</sf></td>"
          "<td>@(see |"
          (symbol-package-name type.pred)
          "|::|"
          (symbol-name type.pred)
          "|)</td>"
          "<td>@(see |"
          (symbol-package-name type.fix)
          "|::|"
          (symbol-name type.fix)
          "|)</td>"
          "<td><tt>"
          (string-downcase (symbol-name type.equiv))
          "</tt></td>"
          "</tr>"))
      (acc (revappend (coerce row 'list) acc))
      (acc (cons #\
 acc)))
    (make-basetypes-table-rchars (cdr table) acc)))
other
(make-event (let* ((types (cdar (table-alist 'fixtypes (w state)))) (rows (reverse (coerce (make-basetypes-table-rchars (reverse types) nil)
            'string))))
    `(defxdoc basetypes
      :parents (fty)
      :short "A book that associates many built-in ACL2 predicates with
suitable fixing functions and equivalence relations, for use in the @(see
fty::fty-discipline)."
      :long (concatenate 'string
        "<p>The @('centaur/fty/basetypes') book provides basic support for
using many built-in ACL2 types with the FTY discipline.  It introduces any
necessary fixing functions and equivalences, and then sets up @(see
fty::deffixtype) associations between the recognizers, fixing functions, and
equivalence relations for the following types.</p>

<p>See also @(see fty::baselists), which sets up similar support for various
built-in list recognizers like @(see character-listp), etc.</p>

<table>
<tr><th>Type Name</th> <th>Recognizer</th> <th>Fix</th> <th>Equiv</th></tr>"
        ,ROWS
        "</table>

<p>Note: all of these associations are made in the ACL2 package.</p>
"))))