other
(in-package "PRIMES")
other
(include-book "projects/numbers/euclid" :dir :system)
other
(include-book "kestrel/utilities/pack" :dir :system)
other
(include-book "kestrel/utilities/defmacrodoc" :dir :system)
other
(include-book "kestrel/strings-light/downcase" :dir :system)
other
(include-book "std/util/add-io-pairs" :dir :system)
other
(include-book "xdoc/constructors" :dir :system)
other
(in-theory (disable (:e primep)))
other
(defund defprime-fn
(name number
pratt-cert
existing-prime-name
evisc
doc
parents
short
long
wrld)
(declare (xargs :guard (and (symbolp name)
(if existing-prime-name
(eq :none number)
(posp number))
(if existing-prime-name
(eq :none pratt-cert)
(true-listp pratt-cert))
(booleanp evisc)
(booleanp doc)
(or (eq nil parents)
(eq :auto parents)
(symbol-listp parents))
(or (eq nil short)
(eq :auto short)
(stringp short))
(or (eq nil long)
(eq :auto long)
(stringp long))
(symbolp existing-prime-name)
(plist-worldp wrld))))
(b* ((defprime-alist (table-alist 'defprime-table wrld)) ((when (not (alistp defprime-alist))) (er hard?
'defprime
"Ill-formed defprime-alist: ~x0."
defprime-alist))
((when (and existing-prime-name
(not (assoc-eq existing-prime-name
defprime-alist)))) (er hard?
'defprime
"No existing prime found for name ~x0."
existing-prime-name))
(number (if existing-prime-name
(cdr (assoc-eq existing-prime-name
defprime-alist))
number))
((when (not (natp number))) (er hard?
'defprime
"Bad value for existing prime: ~x0."
number))
((when (and (not doc)
(or (not (eq :auto parents))
(not (eq :auto short))
(not (eq :auto long))))) (er hard?
'defprime
"Since the :doc argument is nil, :parents, :short, and :long should not be supplied."))
(defconst-name (pack-in-package-of-symbol name '* name '*))
(pratt-cert-defconst-name (pack-in-package-of-symbol name
'*
name
'-pratt-cert*))
(parents (if (eq nil parents)
nil
(if (eq :auto parents)
'(:parents (number-theory))
`(:parents ,PRIMES::PARENTS))))
(short (if (eq nil short)
nil
(if (eq :auto short)
'(:short "A prime defined by @(tsee defprime).")
`(:short ,PRIMES::SHORT))))
(long (if (eq nil long)
nil
(if (eq :auto long)
`(:long ,(CONCATENATE 'STRING "<p>The value of "
(STRING-DOWNCASE-GEN (SYMBOL-NAME PRIMES::NAME)) " is "
(NAT-TO-STRING NUMBER) ".</p>"))
`(:long ,PRIMES::LONG)))))
`(encapsulate nil
,@(AND (NOT PRIMES::EXISTING-PRIME-NAME)
'((PRIMES::LOCAL
(PRIMES::INCLUDE-BOOK "projects/numbers/pratt" :DIR :SYSTEM))))
(local (in-theory (disable (:e primep))))
(defconst ,PRIMES::DEFCONST-NAME ,NUMBER)
(defund ,PRIMES::NAME
nil
(declare (xargs :guard t))
,PRIMES::DEFCONST-NAME)
(defmacro ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::EVISCERATE- PRIMES::NAME)
nil
`(table evisc-table
,,NUMBER
,,(CONCATENATE 'STRING "#.*" (SYMBOL-NAME PRIMES::NAME) "*")))
(defmacro ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::UNEVISCERATE- PRIMES::NAME)
nil
`(table evisc-table ,,NUMBER nil))
,@(AND PRIMES::EVISC
`((,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::EVISCERATE-
PRIMES::NAME))))
(defconst ,PRIMES::PRATT-CERT-DEFCONST-NAME
',PRIMES::PRATT-CERT)
(defthm ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::PRIMEP-OF- PRIMES::NAME
'PRIMES::-CONSTANT)
(primep ,PRIMES::DEFCONST-NAME)
,@(IF PRIMES::EXISTING-PRIME-NAME
`(:HINTS
(("Goal" :USE
(:INSTANCE
,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::EXISTING-PRIME-NAME
'PRIMES::PRIMEP-OF- PRIMES::EXISTING-PRIME-NAME
'PRIMES::-CONSTANT))
:IN-THEORY NIL)))
`(:HINTS
(("Goal" :IN-THEORY (PRIMES::ENABLE (:E DM::CERTIFY-PRIME)) :USE
(:INSTANCE DM::CERTIFICATION-THEOREM
(PRIMES::P ,PRIMES::DEFCONST-NAME)
(PRIMES::C ,PRIMES::PRATT-CERT-DEFCONST-NAME)))))))
(defthm ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::PRIMEP-OF- PRIMES::NAME)
(primep (,PRIMES::NAME))
:hints (("Goal" :in-theory '(,PRIMES::NAME)
:use (:instance ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME 'PRIMES::PRIMEP-OF- PRIMES::NAME
'PRIMES::-CONSTANT)))))
(local (in-theory (disable (:e ,PRIMES::NAME))))
(defthm ,(PACK-IN-PACKAGE-OF-SYMBOL PRIMES::NAME PRIMES::NAME 'PRIMES::-LINEAR)
(= (,PRIMES::NAME) ,PRIMES::DEFCONST-NAME)
:rule-classes ((:linear :trigger-terms ((,PRIMES::NAME))))
:hints (("Goal" :in-theory (enable (:e ,PRIMES::NAME)))))
,@(AND (NOT PRIMES::EXISTING-PRIME-NAME)
`((ADD-IO-PAIRS (((PRIMES::PRIMEP (,PRIMES::NAME)) T)))))
,@(AND PRIMES::DOC
`((PRIMES::DEFXDOC ,PRIMES::NAME ,@PRIMES::PARENTS ,@PRIMES::SHORT
,@PRIMES::LONG)))
(table defprime-table
',PRIMES::NAME
,NUMBER))))
other
(defmacrodoc defprime
(name number
pratt-cert
&key
(evisc 't)
(parents ':auto)
(short ':auto)
(long ':auto)
(doc 't))
`(make-event (defprime-fn ',PRIMES::NAME
',NUMBER
',PRIMES::PRATT-CERT
nil
',PRIMES::EVISC
,PRIMES::DOC
',PRIMES::PARENTS
,PRIMES::SHORT
,PRIMES::LONG
(w state)))
:parents (number-theory)
:short "Introduce a prime and related machinery."
:args ((name "Name of the prime to introduce, a symbol.") (number "Numeric value of the prime, a natural number.")
(pratt-cert "Pratt certificate for the prime.")
(evisc "Whether to print occurrences of the prime using its symbolic name.")
(doc "Whether to generate xdoc for the prime.")
(parents "Xdoc :parents for the prime.")
(short "Xdoc :short description for the prime.")
(long "Xdoc :long section for the prime."))
:description (topstring (p "Defprime generates, for a prime named FOO:")
(ul (li "A constant, *FOO*, representing the prime.")
(li "A theorem that *FOO* is prime.")
(li "A 0-ary function, FOO, representing the prime. This is disabled but its :executable-counterpart is not (disable the :executable-counterpart to prevent execution during proofs).")
(li "A theorem that the function FOO always returns a prime.")
(li "A :linear rule stating that the function FOO is equal to the prime (i.e., its integer value).")
(li "A utility, eviscerate-FOO, to cause the prime to be printed using a symbolic name. This is in turn invoked by defprime to turn on evisceration, unless the :evisc argument is nil.")
(li "A utility, uneviscerate-FOO, to turn off the evisceration mentioned just above.")
(li "A constant, *FOO-pratt-cert*, for the Pratt certificate supplied for FOO.")
(li "A @(tsee defxdoc) form for the prime, using the supplied :short, :long, and :parents, or suitable defaults for each.")
(li "A call of @(tsee acl2::add-io-pairs) to cause primep to be fast when called on the prime.")
(li "A @(tsee table) event that records the call of defprime."))))
other
(defmacrodoc defprime-alias
(name existing-prime-name
&key
(evisc 't)
(parents ':auto)
(short ':auto)
(long ':auto)
(doc 't))
`(make-event (defprime-fn ',PRIMES::NAME
',:NONE
':none
',PRIMES::EXISTING-PRIME-NAME
',PRIMES::EVISC
,PRIMES::DOC
',PRIMES::PARENTS
,PRIMES::SHORT
,PRIMES::LONG
(w state)))
:parents (number-theory)
:short "Introduce an alias of an existing prime introduced with defprime."
:args ((name "Name of the prime to introduce, a symbol.") (existing-prime-name "Name of the existing prime, a symbol.")
(evisc "Whether to print occurrences of the prime using its symbolic name.")
(doc "Whether to generate xdoc for the prime.")
(parents "Xdoc :parents for the prime.")
(short "Xdoc :short description for the prime.")
(long "Xdoc :long section for the prime."))
:description "Defprime-alias generates all of the things generated by @(tsee defprime), except that it omits the call to @(tsee acl2::add-io-pairs), since that has already been done for the existing prime, which has the same numeric value as the new prime.")