other
(in-package "STD")
other
(include-book "std/util/define" :dir :system)
other
(include-book "std/system/acceptable-rewrite-rule-p" :dir :system)
other
(set-state-ok t)
other
(program)
other
(defxdoc define-sk :parents (std/util defun-sk) :short "A very fine alternative to @(tsee defun-sk)." :long "<h3>Introduction</h3> <p>@('define-sk') is an extension of @(see defun-sk) with many @(see define)-like features and other enhancements:</p> <ul> <li>Support for @('define')-style syntax including: extended formals with embedded guards/docs and @('&key')/@('&optional') arguments via macro aliases, @(see xdoc) integration and automatic function signatures, @(':prepwork') and @('///') sections, @(':returns') specifiers, etc.</li> <li>Better support for @(see guard) verification which avoids theory problems and provides smarter handling of @('implies') forms; see @(see define-sk-implies-handling).</li> <li>It automatically infers when using @(':rewrite :direct') is possible, which generally gives you a better theorem for universally quantified functions.</li> </ul> <h5>Example</h5> @({ (define-sk distances-bounded-p ((bound rationalp "Maximum length to allow.") (cluster setp "All nodes to consider.")) :short "Do all nodes in a cluster lie within some certain bound?" (forall ((weaker "Lesser of the two nodes to consider.") (stronger "Greater of the two nodes to consider.")) (implies (and (in lesser cluster) (in greater cluster) (weaker-p weaker stronger)) (<= (distance lesser greater) bound))) /// (defthm sensible-when-sensible-bound-p (implies (and (distances-bounded-p bound cluster) (sensible-bound-p bound)) (sensible-cluster-p cluster)))) }) <h3>Syntax</h3> @({ (define-sk name formals (quantifier extended-vars body) [/// other-events]) ;; optional, starts with the symbol /// }) <p>Where:</p> <ul> <li>The name is just the name of the new quantified function to be defined, as in @(see defun-sk).</li> <li>The @('formals') are a list of @(see std::extended-formals). This could be as simple as a list of variables, but can also specify guards and documentation fragments as in @(see define). The special @('&key')/@('&optional') arguments are allowed. No extra keyword arguments are accepted on individual formals.</li> <li>The @('quantifier') should be either @('forall') or @('exists').</li> <li>The @('extended-vars') are a list of @(see std::extended-formals) that are being quantified over. Like the @('formals'), these can have documentation fragments. Special restrictions: guards are not allowed here and neither are @('&key')/@('&optional') arguments. No additional keyword arguments are accepted for individual extended vars.</li> <li>The @('body') is as in @(see defun-sk).</li> <li>The @('other-events') are as in @(see define); this is just a grouping mechanism that allows you to put related theorems and events here.</li> </ul> <p>Additionally, optional @(':keyword value') arguments may be interspersed anywhere between @('name') and @('///').</p> <h3>Guard Related Features</h3> <p>A common problem when trying to use guard verification with @(see defun-sk) is that @(see implies) isn't lazy, so you won't be able to assume that your hypotheses hold in your conclusion. @('define-sk') tries to help with this by smartly handling @('implies') forms in your function body. See @(see define-sk-implies-handling) for a detailed explanation of the problem.</p> <h5>Guard Options</h5> <dl> <dt>:verify-guards val</dt> <dd>Like @(see define), we try to verify guards by default, but you can avoid this by setting @(':verify-guards nil').</dd> <dt>:guard guard</dt> <dd>Usually it's most convenient to embed your guards within the @(see extended-formals), but the @(':guard') option is sometimes useful for giving additional guards.</dd> <dt>:guard-hints hints</dt> <dt>:guard-debug bool</dt> <dd>These are passed to the guard verification attempt as you would expect.</dd> <dt>:implies mode</dt> <dd>By default we use @(':implies :smart'), which means that uses of @('implies') are automatically converted into @('if') terms in the body. To avoid this, use @(':implies :dumb').</dd> </dl> <h3>Other Keyword Options</h3> <dl> <dt>:enabled val</dt> <dd>By default the quantified function <b>and its @('necc/suff') theorem</b> will both be disabled after the @('///') events are finished. You can control this with @(':enabled'): <ul> <li>@(':enabled :all') -- enable the function and the theorem</li> <li>@(':enable :thm') -- disable the function but enable the theorem</li> <li>@(':enable :fn') -- enable the function but disable the theorem</li> <li>@(':enable nil') -- disable the function and theorem (default)</li> </ul></dd> <dt>:rewrite val</dt> <dd>This is similar to the same option for @(see defun-sk), except that by default we look at your function's body to infer whether @(':rewrite :direct') can be used. If for whatever reason you don't like the rewrite rule that gets generated, you can customize it by adding @(':rewrite <custom-term>').</dd> <dt>:returns spec</dt> <dd>By default we try to prove that your quantified function returns a @(see booleanp). However, note that it is possible to define ``weird'' quantifiers that return non-boolean or multiple values. For instance, here is a quantified function that logically just always returns 0:</dd> @({ (set-ignore-ok t) (defun-sk weird-quantifier (x) (forall elem 0)) (thm (equal (weird-quantifier x) 0)) }) <dd>Similarly, here is a quantified function that actually returns multiple values:</dd> @({ (defun-sk weirder-quantifier (x) (forall elem (mv x x))) (thm (equal (weirder-quantifier x) (mv x x))) }) <dd>If you try to introduce such a function with @('define-sk'), or if your predicate just happens to not return a proper @('t') or @('nil') boolean, then you may need to provide a custom @(':returns') form; see @(see returns-specifiers) for details.</dd> <dt>:strengthen val</dt> <dd>Submits the underlying @(see defchoose) event with the @('strengthen') option.</dd> <dt>:ignore-ok val</dt> <dd>Submits @('(set-ignore-ok val)') before the definition. This option is local to the @('define-sk') and does not affect the @('other-events').</dd> <dt>:irrelevant-formals-ok val</dt> <dd>Submits @('(set-irrelevant-formals-ok val)') before the definition. This option is local to the @('define-sk') and does not affect the @('other-events').</dd> <dt>:parents parents</dt> <dt>:short string</dt> <dt>:long string</dt> <dd>These are @(see defxdoc)-style options for documenting the function. They are passed to a @(see defsection) for this definition.</dd> <dt>:prepwork events</dt> <dd>These are arbitrary events that you want to put before the definition itself. For instance, it might include any local lemmas.</dd> <dt>:progn val</dt> <dd>Normally a @('define-sk') expands to an @('(encapsulate nil ...)'). This means for instance that you can use @(see local) in your @('prepwork'), @('other-events'), to make changes that are local to the @('define-sk') form. In certain special cases, you may want to avoid this use of @('encapsulate') and instead submit the events using @('progn').</dd> <dt>:verbosep val</dt> <dd>By default some output is suppressed, but yu can set @(':verbosep t') to avoid this. This may be useful when debugging failed @('define-sk') forms.</dd> </dl>")
other
(defxdoc define-sk-implies-handling :parents (define-sk) :short "Explanation of the @(':implies :smart') option for @(see define-sk)." :long "<p>By default, the @(see define-sk) macro handles calls of @('implies') in its function's body in a ``smart'' way. Below we explain what problem this special handling is meant to help with and the way it works.</p> <p>Note: you can disable this behavior via @(':implies :dumb').</p> <h3>Sketch of the problem</h3> <p>Consider a quantified function definition like:</p> @({ (defun-sk all-greaterp (min list) (declare (xargs :guard (and (integerp min) (integer-listp list)) :verify-guards nil)) (forall (elem) (implies (member elem list) (< min elem)))) }) <p>Unfortunately, the above produces a lousy @('-necc') theorem that isn't really the rule you usually want:</p> @({ (defthm all-greaterp-necc (implies (not (implies (member elem list) (< min elem))) (not (all-greaterp min list)))) }) <p>We can get a better rule by adding the @(':rewrite :direct') option to the @(see defun-sk). After we do that, we get a better rule:</p> @({ (defthm all-greaterp-necc (implies (all-greaterp min list) (implies (member elem list) (< min elem)))) }) <p>So that's great. The problem comes in when we try to verify the guards of @('all-greaterp'). For that, we need to know that @('elem') is a number when we call @('(< min elem)'). This is obviously true since @('elem') is a member of @('list'), an integer list—except wait, @(see implies) is a real function, so when we call @('(< min elem)'), we haven't yet established that @('elem') is in @('list').</p> <p>To fix this, we might try to rewrite our function to get rid of the @('implies'). For instance, we might write:</p> @({ (defun-sk all-greaterp (min list) (declare (xargs :guard (and (integerp min) (integer-listp list)) :verify-guards nil)) (forall (elem) (if (member elem list) (< min elem) t)) :rewrite :direct) }) <p>But now we run into a different problem: the @('-necc') theorem now ends up looking like this:</p> @({ (defthm all-greaterp-necc (implies (all-greaterp min list) (if (member elem list) (< min elem) t))) }) <p>But this isn't a valid <see topic='@(url acl2::rewrite)'>rewrite</see> rule because of the @(see if) in the conclusion!</p> <p>In short: for guard verification we generally want to use something like @('if') or <see topic='@(url acl2::impliez)'>impliez</see> instead of @('implies'), but to get good rewrite rules we need to use @('implies').</p> <h3>Solution</h3> <p>To try to help with this, @(see define-sk) does something special with @('implies') forms inside the body. In particular, when we submit:</p> @({ (define-sk all-greaterp ((min integerp) (list integer-listp)) (forall (elem) (implies (member elem list) (< min elem)))) }) <p>The @('implies') terms in the resulting @(see defun) for @('all-greaterp') will automatically get expanded into @('if') terms. That is, the real @(see defun) that we submit will look something like this:</p> @({ (defun all-greaterp (min list) (declare ...) (let ((elem (all-greaterp-witness min list))) (if (member elem list) (< min elem) t))) }) <p>This will generally help to make guard verification more straightforward because you'll be able to assume the hyps hold during the conclusion. But note that this rewriting of @('implies') is done only in the function's body, not in the @('-necc') theorem where it would ruin the <see topic='@(url acl2::rewrite)'>rewrite</see> rule.</p> <p>Is this safe? There's of course no logical difference between @('implies') and @('impliez'), but there certainly is a big difference in the execution, viz evaluation order. Fortunately, this difference will not matter for what we are trying to do: we're only changing @('implies') to @('if') in code that follows a call of the @('-witness') function. This code can never be reached in real execution, because calling the @('-witness') function will cause an error. So: logically we aren't changing anything, and this term is never executed anyway, so execution differences don't matter.</p>")
other
(defconst *define-sk-keywords* '(:parents :short :long :prepwork :progn :ignore-ok :irrelevant-formals-ok :verbosep :enabled :verify-guards :guard-hints :guard-debug :guard :implies :returns :rewrite :strengthen :quant-ok :skolem-name :thm-name :classicalp :non-executable :constrain))
other
(def-primitive-aggregate define-sk-guts
(name name-fn
raw-formals
formals
quantifier
bound-vars
raw-body
exec-body
main-def
constrain
macro
returnspecs
kwd-alist
rest-events)
:tag :define-sk-guts)
get-define-sk-guts-alistfunction
(defun get-define-sk-guts-alist (world) (cdr (assoc 'guts-alist (table-alist 'define-sk world))))
extend-define-sk-guts-alistfunction
(defun extend-define-sk-guts-alist (guts) `(table define-sk 'guts-alist (cons (cons ',(STD::DEFINE-SK-GUTS->NAME STD::GUTS) ',STD::GUTS) (get-define-sk-guts-alist world))))
other
(define find-define-sk-guts ((name "This may be either the name of a define-sk function or a macro wrapper for a define-sk.") world) :returns (maybe-guts "A Define-SK guts structure, if the function is found, or NIL if this is not a known Define-SK.") (let ((name-fn (or (cdr (assoc name (table-alist 'define-macro-fns world))) name))) (cdr (assoc name-fn (get-define-sk-guts-alist world)))))
other
(mutual-recursion (defun expand-implies-in-pseudo-term (x) (b* (((when (atom x)) x) ((when (eq (car x) 'quote)) x) (args (expand-implies-in-pseudo-term-list (cdr x))) ((when (eq (car x) 'implies)) (let ((p (first args)) (q (second args))) (list 'if p (list 'if q ''t ''nil) ''t))) ((when (atom (car x))) (cons (car x) args)) ((list lambda formals body) (car x))) (cons (list lambda formals (expand-implies-in-pseudo-term body)) args))) (defun expand-implies-in-pseudo-term-list (x) (if (atom x) x (cons (expand-implies-in-pseudo-term (car x)) (expand-implies-in-pseudo-term-list (cdr x))))))
dumb-expand-implies-in-untranslated-termfunction
(defun dumb-expand-implies-in-untranslated-term (x) (cond ((atom x) x) ((eq (car x) 'quote) x) ((and (eq (car x) 'implies) (true-listp x) (equal (len x) 3)) (let ((p (dumb-expand-implies-in-untranslated-term (second x))) (q (dumb-expand-implies-in-untranslated-term (third x)))) (list 'if p (list 'if q t nil) t))) (t (cons (dumb-expand-implies-in-untranslated-term (car x)) (dumb-expand-implies-in-untranslated-term (cdr x))))))
expand-implies-for-define-skfunction
(defun expand-implies-for-define-sk (raw-body ctx state) "Returns (MV OKP NEW-BODY STATE)" (state-global-let* ((inhibit-output-lst *valid-output-names*)) (b* ((stobjs-out t) (logic-modep t) (known-stobjs t) (wrld (w state)) ((mv er pre-target-term state) (translate raw-body stobjs-out logic-modep known-stobjs ctx wrld state)) ((when (or er (not (pseudo-termp pre-target-term)))) (mv nil raw-body state)) (target-term (expand-implies-in-pseudo-term pre-target-term)) (candidate (dumb-expand-implies-in-untranslated-term raw-body)) ((mv er candidate-trans state) (translate candidate stobjs-out logic-modep known-stobjs ctx wrld state)) ((when (or er (not (pseudo-termp candidate-trans)))) (mv nil raw-body state)) (check-term (expand-implies-in-pseudo-term candidate-trans)) ((unless (equal check-term target-term)) (mv nil raw-body state))) (mv t candidate state))))
other
(encapsulate nil (logic) (local (defmacro trick (x) (substitute 'and 'implies x))) (local (defthm example-of-trick (equal (trick (implies x y)) (and x y)) :rule-classes nil)) (local (make-event (b* ((ctx 'sanity-check) ((mv okp trans state) (expand-implies-for-define-sk '(let ((x 1)) (implies x y)) ctx state)) ((unless (and okp (equal trans '(let ((x 1)) (if x (if y t nil) t))))) (er soft ctx "Example 1 incorrect: got OKP=~x0, Trans=~x1." okp trans)) ((mv okp trans state) (expand-implies-for-define-sk '(let ((x 1)) (trick x y)) ctx state)) ((unless (not okp)) (er soft ctx "Example 2 incorrect: got OKP=~x0, Trans=~x1." okp trans))) (value '(value-triple :success))))))
define-sk-infer-rewrite-modefunction
(defun define-sk-infer-rewrite-mode (body state) "Returns (MV MODE STATE)" (declare (xargs :mode :program :stobjs state)) (b* ((stobjs-out t) (logic-modep t) (known-stobjs t) ((mv er translated-body state) (state-global-let* ((inhibit-output-lst *valid-output-names*)) (translate body stobjs-out logic-modep known-stobjs 'define-sk (w state) state))) ((when er) (mv :default state)) (okp (acceptable-rewrite-rule-p translated-body (ens state) (w state))) ((when (not okp)) (mv :default state))) (mv :direct state)))
other
(encapsulate nil (logic) (local (make-event (b* (((mv mode1 state) (define-sk-infer-rewrite-mode '(implies (atom x) (equal (car x) nil)) state)) ((unless (eq mode1 :direct)) (er soft 'infer-rewrite-mode "sanity check 1 failed")) ((mv mode2 state) (define-sk-infer-rewrite-mode `(if x (integerp y) (consp z)) state)) ((unless (eq mode2 :direct)) (er soft 'infer-rewrite-mode "sanity check 2 failed")) ((mv mode3 state) (define-sk-infer-rewrite-mode ''t state)) ((unless (eq mode3 :default)) (er soft 'infer-rewrite-mode "sanity check 2 failed"))) (value '(value-triple :success))))))
other
(define find-formal-with-non-t-guard (formals) (cond ((atom formals) nil) ((equal (formal->guard (car formals)) t) (find-formal-with-non-t-guard (cdr formals))) (t (car formals))))
other
(define parse-define-sk ((name "User-level name, e.g., FOO instead of FOO-FN.") (args "Everything that comes after the name.") (extra-keywords "Any additional keywords to allow; possibly useful for building tools on top of define-sk.") state) :returns (mv guts state) (b* ((__function__ 'define-sk) (world (w state)) ((unless (symbolp name)) (mv (raise "Expected function name to be a symbol, found ~x0." name) state)) ((mv main-stuff rest-events) (split-/// name args)) ((mv kwd-alist non-keyword-stuff) (extract-keywords name (append extra-keywords *define-sk-keywords*) main-stuff nil)) ((unless (equal (len non-keyword-stuff) 2)) (mv (raise "Error in ~x0: define-sk takes exactly two non-keyword ~ arguments (the formals and quantifier form), found ~x1." name (len non-keyword-stuff)) state)) ((list raw-formals qvb-form) non-keyword-stuff) ((unless (and (consp qvb-form) (or (eq (car qvb-form) 'forall) (eq (car qvb-form) 'exists)))) (mv (raise "Error in ~x0: expected (forall ...) or (exists ...) but ~ found ~x1" name qvb-form) state)) ((unless (tuplep 3 qvb-form)) (mv (raise "Error in ~x0: wrong number of arguments to ~x1: ~x2" name (car qvb-form) qvb-form) state)) ((list quantifier raw-bound-vars raw-body) qvb-form) (raw-bound-vars (cond ((symbolp raw-bound-vars) (list raw-bound-vars)) ((and (consp raw-bound-vars) (consp (cdr raw-bound-vars)) (symbolp (first raw-bound-vars)) (stringp (second raw-bound-vars))) (list raw-bound-vars)) (t raw-bound-vars))) (need-macrop (has-macro-args raw-formals)) (name-fn (cond (need-macrop (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-FN") name)) (t name))) (macro (and need-macrop (make-wrapper-macro name name-fn raw-formals))) (formals (remove-macro-args name raw-formals nil)) (formals (parse-formals name formals nil world)) (formal-names (formallist->names formals)) (formal-guards (remove t (formallist->guards formals))) (stobj-names (formallist->names (formallist-collect-stobjs formals world))) (bound-vars (parse-formals name raw-bound-vars nil world)) (bound-var-names (formallist->names bound-vars)) (bad-bound-var (find-formal-with-non-t-guard bound-vars)) ((when bad-bound-var) (mv (raise "Error in ~x0: bound variables can't have guards but ~x1 ~ has guard ~x2." name (formal->name bad-bound-var) (formal->guard bad-bound-var)) state)) (prepwork (getarg :prepwork nil kwd-alist)) ((unless (true-listp prepwork)) (mv (raise "Error in ~x0: expected :prepwork to be a true-listp, but ~ found ~x1." name prepwork) state)) (implies-mode (getarg :implies :smart kwd-alist)) ((unless (member implies-mode '(:smart :dumb))) (mv (raise "Error in ~x0: unknown :implies mode ~x1 (expected :smart ~ or :dumb)." name implies-mode) state)) (kwd-alist (put-assoc :implies implies-mode kwd-alist)) ((mv ?okp exec-body state) (if (eq implies-mode :smart) (expand-implies-for-define-sk raw-body name state) (mv t raw-body state))) (enabled (getarg :enabled nil kwd-alist)) ((unless (member enabled '(nil :fn :thm :all))) (mv (raise "Error in ~x0: :enabled must be NIL, :FN, :THM, or :ALL, ~ but found ~x1." name enabled) state)) (quant-ok (getarg :quant-ok nil kwd-alist)) (skolem-name (getarg :skolem-name nil kwd-alist)) ((unless (symbolp skolem-name)) (mv (raise "Error in ~x0: :skolem-name must be a symbol; found ~x1." name skolem-name) state)) (skolem-name (or skolem-name (add-suffix name "-WITNESS"))) (kwd-alist (put-assoc :skolem-name skolem-name kwd-alist)) (thm-name (getarg :thm-name nil kwd-alist)) ((unless (symbolp thm-name)) (mv (raise "Error in ~x0: :thm-name must be a symbol; found ~x1." name thm-name) state)) (thm-name (or thm-name (add-suffix name (if (eq quantifier 'exists) "-SUFF" "-NECC")))) (kwd-alist (put-assoc :thm-name thm-name kwd-alist)) (parents (if (assoc :parents kwd-alist) (cdr (assoc :parents kwd-alist)) (get-default-parents world))) (kwd-alist (put-assoc :parents parents kwd-alist)) (rewrite (getarg :rewrite nil kwd-alist)) ((mv rewrite state) (if (and (not rewrite) (not (eq quantifier 'exists))) (define-sk-infer-rewrite-mode raw-body state) (mv rewrite state))) (rewrite (if (and (not (eq quantifier 'exists)) (eq rewrite :direct)) `(implies (,STD::NAME-FN ,@STD::FORMAL-NAMES) ,STD::RAW-BODY) rewrite)) (strengthen (getarg :strengthen nil kwd-alist)) (constrain (getarg :constrain nil kwd-alist)) (witness-dcls nil) (guard (getarg :guard t kwd-alist)) (non-executable (getarg :non-executable (if stobj-names t nil) kwd-alist)) (kwd-alist (put-assoc :non-executable non-executable kwd-alist)) (witness-dcls (append (and stobj-names `((declare (xargs :stobjs ,STD::STOBJ-NAMES)))) (cond ((atom formal-guards) nil) ((atom (cdr formal-guards)) `((declare (xargs :guard ,(CAR STD::FORMAL-GUARDS))))) (t (b* ((sorted-formal-guards (sort-formal-guards formal-guards world))) `((declare (xargs :guard (and . ,STD::SORTED-FORMAL-GUARDS))))))) (and guard `((declare (xargs :guard ,STD::GUARD)))) (and non-executable `((declare (xargs :non-executable ,STD::NON-EXECUTABLE)))) witness-dcls)) (witness-dcls (cons '(declare (xargs :verify-guards nil)) witness-dcls)) (bool-symbol (intern-in-package-of-symbol "BOOL" (pkg-witness (current-package state)))) (returns (getarg :returns `(,STD::BOOL-SYMBOL booleanp :rule-classes :type-prescription) kwd-alist)) (returnspecs (parse-returnspecs name returns world)) (main-def `(defun-sk ,STD::NAME-FN ,STD::FORMAL-NAMES ,@STD::WITNESS-DCLS (,STD::QUANTIFIER ,STD::BOUND-VAR-NAMES ,STD::EXEC-BODY) ,@(AND STD::REWRITE `(:REWRITE ,STD::REWRITE)) ,@(AND STD::STRENGTHEN `(:STRENGTHEN ,STD::STRENGTHEN)) ,@(AND STD::QUANT-OK `(:QUANT-OK ,STD::QUANT-OK)) ,@(AND STD::SKOLEM-NAME `(:SKOLEM-NAME ,STD::SKOLEM-NAME)) ,@(AND STD::THM-NAME `(:THM-NAME ,STD::THM-NAME)) ,@(AND STD::CONSTRAIN `(:CONSTRAIN ,STD::CONSTRAIN)))) (guts (make-define-sk-guts :name name :name-fn name-fn :raw-formals raw-formals :formals formals :quantifier quantifier :bound-vars bound-vars :raw-body raw-body :exec-body exec-body :main-def main-def :constrain constrain :macro macro :returnspecs returnspecs :kwd-alist kwd-alist :rest-events rest-events))) (mv guts state)))
add-macro-aliases-from-define-sk-gutsfunction
(defun add-macro-aliases-from-define-sk-guts (guts) (b* (((define-sk-guts guts) guts)) (and guts.macro `((add-macro-alias ,STD::GUTS.NAME ,STD::GUTS.NAME-FN) (table define-macro-fns ',STD::GUTS.NAME-FN ',STD::GUTS.NAME)))))
other
(define add-define-sk-signature-from-guts
(guts)
(b* (((define-sk-guts guts)))
`(make-event (b* ((current-pkg (f-get-global 'current-package state)) (base-pkg (pkg-witness current-pkg))
(name ',STD::GUTS.NAME)
(all-topics (get-xdoc-table (w state)))
(old-topic (find-topic name all-topics))
((unless old-topic) (value '(value-triple :invisible)))
((mv str state) (make-xdoc-top name
',STD::GUTS.NAME-FN
',STD::GUTS.FORMALS
',STD::GUTS.RETURNSPECS
base-pkg
state))
(event (list 'xdoc-prepend name str)))
(value event)))))
define-sk-events-from-gutsfunction
(defun define-sk-events-from-guts (guts world) (b* (((define-sk-guts guts)) (enabled (getarg :enabled nil guts.kwd-alist)) (prepwork (getarg :prepwork nil guts.kwd-alist)) (short (getarg :short nil guts.kwd-alist)) (long (getarg :long nil guts.kwd-alist)) (parents (getarg :parents nil guts.kwd-alist)) (thm-name (getarg :thm-name nil guts.kwd-alist)) (prognp (getarg :progn nil guts.kwd-alist)) (verify-guards (getarg :verify-guards t guts.kwd-alist)) (guard-hints (getarg :guard-hints nil guts.kwd-alist)) (guard-debug (getarg :guard-debug nil guts.kwd-alist)) (set-ignores (get-set-ignores-from-kwd-alist guts.kwd-alist)) (start-max-absolute-event-number (max-absolute-event-number world))) `(,(IF STD::PROGNP 'STD::DEFSECTION-PROGN 'STD::DEFSECTION) ,STD::GUTS.NAME ,@(AND STD::PARENTS `(:PARENTS ,STD::PARENTS)) ,@(AND STD::SHORT `(:SHORT ,STD::SHORT)) ,@(AND STD::LONG `(:LONG ,STD::LONG)) ,@(AND STD::PREPWORK `((STD::WITH-OUTPUT :STACK :POP (PROGN . ,STD::PREPWORK)))) ,@(AND STD::GUTS.MACRO `((STD::WITH-OUTPUT :STACK :POP ,STD::GUTS.MACRO))) ,@(IF STD::SET-IGNORES `((STD::ENCAPSULATE NIL ,@STD::SET-IGNORES (STD::WITH-OUTPUT :STACK :POP ,STD::GUTS.MAIN-DEF))) `((STD::WITH-OUTPUT :STACK :POP ,STD::GUTS.MAIN-DEF))) ,@(STD::ADD-MACRO-ALIASES-FROM-DEFINE-SK-GUTS STD::GUTS) ,(STD::EXTEND-DEFINE-SK-GUTS-ALIST STD::GUTS) (local (in-theory (enable ,(IF STD::GUTS.CONSTRAIN (STD::ADD-SUFFIX STD::GUTS.NAME "-DEFINITION") STD::GUTS.NAME) ,STD::THM-NAME))) (make-event (let* ((world (w state)) (events (returnspec-thms ',STD::GUTS.NAME ',STD::GUTS.NAME-FN ',STD::GUTS.RETURNSPECS world))) (value (if events `(with-output :stack :pop (progn . ,STD::EVENTS)) '(value-triple :invisible))))) ,@(AND STD::VERIFY-GUARDS `((STD::WITH-OUTPUT :STACK :POP (STD::VERIFY-GUARDS ,STD::GUTS.NAME-FN ,@(AND STD::GUARD-HINTS `(:HINTS ,STD::GUARD-HINTS)) ,@(AND STD::GUARD-DEBUG `(:GUARD-DEBUG ,STD::GUARD-DEBUG)))))) ,@(AND STD::GUTS.REST-EVENTS `((STD::WITH-OUTPUT :STACK :POP (PROGN . ,STD::GUTS.REST-EVENTS)))) ,@(CASE STD::ENABLED (:ALL NIL) (:FN `((STD::IN-THEORY (STD::DISABLE ,STD::THM-NAME)))) (:THM `((STD::IN-THEORY (STD::DISABLE ,(IF STD::GUTS.CONSTRAIN (STD::ADD-SUFFIX STD::GUTS.NAME "-DEFINITION") STD::GUTS.NAME))))) (OTHERWISE `((STD::IN-THEORY (STD::DISABLE ,(IF STD::GUTS.CONSTRAIN (STD::ADD-SUFFIX STD::GUTS.NAME "-DEFINITION") STD::GUTS.NAME) ,STD::THM-NAME))))) ,(STD::ADD-DEFINE-SK-SIGNATURE-FROM-GUTS STD::GUTS) (make-event (list 'value-triple (if (eql ,STD::START-MAX-ABSOLUTE-EVENT-NUMBER (max-absolute-event-number (w state))) :redundant '',STD::GUTS.NAME))))))
define-sk-fnfunction
(defun define-sk-fn (name args state) (declare (xargs :stobjs state)) (b* (((mv guts state) (parse-define-sk name args nil state)) (event (define-sk-events-from-guts guts (w state)))) (value event)))
define-skmacro
(defmacro define-sk (name &rest args) (let* ((verbose-tail (member :verbosep args)) (verbosep (and verbose-tail (cadr verbose-tail)))) `(with-output :stack :push ,@(AND (NOT STD::VERBOSEP) '(:ON (ERROR) :OFF :ALL)) (make-event (define-sk-fn ',STD::NAME ',STD::ARGS state)))))