other
(in-package "STD")
other
(include-book "deflist-base")
other
(include-book "std/alists/abstract" :dir :system)
other
(defxdoc defalist :parents (std/util) :short "Introduce a recognizer for a typed association list (alist)." :long "<p>Defalist allows you to quickly introduce a recognizer for a typed association list (e.g., @('string-nat-alistp')) and proves basic theorems about it.</p> <p>Unlike many ACL2 alist recognizers, the recognizers introduced by defalist <b>do not</b>, by default, imply @('(alistp x)'), but they do imply something like @('(cons-listp x)'). That is,</p> <ul> <li>We require that each element is a cons, but</li> <li>We do not require the alists to be nil-terminated.</li> </ul> <p>Not requiring @('nil') termination has some advantages. It plays well with @(see acl2::equivalence) relations like @(see list-equiv) and @(see acl2::alist-equiv). It also allows you to use features of @(see acl2::fast-alists) such as "size hints" and "alist names" (see @(see hons-acons) for details).</p> <p>But there is also a disadvantage. Namely, it may be difficult to operate on a defalist using traditional alist functions, whose @(see guard)s require @(see alistp). Fortunately, there are generally good alternatives to these traditional functions with no such requirement, e.g.,:</p> <ul> <li>@(see acons) → @(see hons-acons) or ordinary @(see cons)es.</li> <li>@(see assoc) → @(see hons-get) for fast alists, or @(see hons-assoc-equal) for ordinary alists</li> <li>@(see strip-cars) → @(see alist-keys)</li> <li>@(see strip-cdrs) → @(see alist-vals)</li> </ul> <p>General form:</p> @({ (defalist name formals &key key ; required val ; required guard ; t by default verify-guards ; t by default keyp-of-nil ; :unknown by default valp-of-nil ; :unknown by default true-listp ; nil by default mode ; current defun-mode by default already-definedp ; nil by default parents ; nil by default short ; nil by default long ; nil by default ) }) <p>For example,</p> @({ (defalist string-nat-alistp (x) :key (stringp x) :val (natp x)) }) <p>introduces a new function, @('string-nat-alistp'), that recognizes alists whose keys are strings and whose values are natural numbers. It also proves many theorems about this new function.</p> <p>Note that <b>x</b> is treated in a special way: it refers to the whole alist in the formals and guards, but refers to individual keys or values in the @(':key') and @(':val') positions. This is similar to how @(see deflist), @(see defprojection), and @(see defmapappend) handle @('x').</p> <h3>Usage and Arguments</h3> <p>Let @('pkg') be the package of @('name'). All functions, theorems, and variables are created in this package. One of the formals must be @('pkg::x'), and this argument represents the alist to check. Otherwise, the only restriction on the formals is that you may not use the names @('pkg::a'), @('pkg::n'), or @('pkg::y'), because we use these variables in the theorems we generate.</p> <p>The @(':key') and @(':val') arguments are required and should be simple function calls involving some subset of the formals. The basic idea is that you write @('x') for the particular key or value that is being inspected.</p> <p>The optional @(':guard') and @(':verify-guards') are given to the @('defund') event that we introduce. In other words, these are the guards that will be used for the list recognizer, not the element recognizer.</p> <p>The optional @(':true-listp') argument can be used to make the new recognizer "strict" and only accept alists that are @('nil')-terminated; by default the recognizer will be "loose" and will not pay attention to the final <tt>cdr</tt>. See @(see strict-list-recognizers) for further discussion.</p> <p>The optional @(':keyp-of-nil') (similarly @(':valp-of-nil')) keywords can be used when @('(key-recognizer nil ...)') (similarly @('(val-recognzier nil ...)')) is always known to be @('t') or @('nil'). When it is provided, @('defalist') can generate slightly better theorems.</p> <p>The optional @(':already-definedp') keyword can be set if you have already defined the function. This can be used to generate all of the ordinary @('defalist') theorems without generating a @('defund') event, and is useful when you are dealing with mutually recursive recognizers.</p> <p>The optional @(':mode') keyword can be set to @(':program') to introduce the recognizer in program mode. In this case, no theorems are introduced.</p> <p>The optional @(':parents'), @(':short'), and @(':long') keywords are as in @(see defxdoc). Typically you only need to specify @(':parents'), perhaps implicitly with @(see xdoc::set-default-parents), and suitable documentation will be automatically generated for @(':short') and @(':long'). If you don't like this documentation, you can supply your own @(':short') and/or @(':long') to override it.</p>")
other
(program)
other
(set-state-ok t)
defalist-deflist-instantiate-table-thmsfunction
(defun defalist-deflist-instantiate-table-thms (name formals key val kwd-alist x world) (b* ((table (table-alist 'listp-rules world)) (element `(and (consp ,STD::X) ,@(AND (NOT (EQ STD::KEY T)) `((,(CAR STD::KEY) . ,(SUBST `(CAR ,STD::X) STD::X (CDR STD::KEY))))) ,@(AND (NOT (EQ STD::VAL T)) `((,(CAR STD::VAL) . ,(SUBST `(CDR ,STD::X) STD::X (CDR STD::VAL))))))) (kwd-alist `((:negatedp) (:elementp-of-nil) . ,STD::KWD-ALIST)) (fn-subst (deflist-substitution name formals element kwd-alist x)) (req-alist (deflist-requirement-alist kwd-alist formals element))) (deflist-instantiate-table-thms-aux table element name formals kwd-alist x req-alist fn-subst world)))
defalist-substitutionfunction
(defun defalist-substitution (name formals key val kwd-alist x) (b* ((key-negatedp (getarg :key-negatedp nil kwd-alist)) (val-negatedp (getarg :val-negatedp nil kwd-alist)) (true-listp (getarg :true-listp nil kwd-alist))) `((keytype-p ,(IF STD::KEY-NEGATEDP `(LAMBDA (,STD::X) (NOT ,STD::KEY)) `(LAMBDA (,STD::X) ,STD::KEY))) (non-keytype-p ,(IF STD::KEY-NEGATEDP `(LAMBDA (,STD::X) ,STD::KEY) `(LAMBDA (,STD::X) (NOT ,STD::KEY)))) (valtype-p ,(IF STD::VAL-NEGATEDP `(LAMBDA (,STD::X) (NOT ,STD::VAL)) `(LAMBDA (,STD::X) ,STD::VAL))) (non-valtype-p ,(IF STD::VAL-NEGATEDP `(LAMBDA (,STD::X) ,STD::VAL) `(LAMBDA (,STD::X) (NOT ,STD::VAL)))) (keyval-alist-p (lambda (,STD::X) (,STD::NAME . ,STD::FORMALS))) (keyval-alist-final-cdr-p ,(IF STD::TRUE-LISTP 'NOT '(LAMBDA (STD::X) T))))))
defalist-requirement-alistfunction
(defun defalist-requirement-alist (kwd-alist formals key val) (b* ((key-negatedp (getarg :key-negatedp nil kwd-alist)) (val-negatedp (getarg :val-negatedp nil kwd-alist)) (key-simple (simple-fncall-p-hack key)) (val-simple (simple-fncall-p-hack val)) (true-listp (getarg :true-listp nil kwd-alist)) (keyp-of-nil (getarg :keyp-of-nil :unknown kwd-alist)) (valp-of-nil (getarg :valp-of-nil :unknown kwd-alist)) (single-var (eql (len formals) 1)) (cheap (getarg :cheap nil kwd-alist))) `((keytype-p-of-nil . ,(EQ STD::KEYP-OF-NIL (NOT STD::KEY-NEGATEDP))) (not-keytype-p-of-nil . ,(EQ STD::KEYP-OF-NIL STD::KEY-NEGATEDP)) (valtype-p-of-nil . ,(EQ STD::VALP-OF-NIL (NOT STD::VAL-NEGATEDP))) (not-valtype-p-of-nil . ,(EQ STD::VALP-OF-NIL STD::VAL-NEGATEDP)) (key-negatedp . ,STD::KEY-NEGATEDP) (val-negatedp . ,STD::VAL-NEGATEDP) (keytype-simple . ,STD::KEY-SIMPLE) (valtype-simple . ,STD::VAL-SIMPLE) (true-listp . ,STD::TRUE-LISTP) (single-var . ,STD::SINGLE-VAR) (cheap . ,STD::CHEAP))))
other
(mutual-recursion (defun defalist-thmbody-subst (body key val name formals x key-negatedp val-negatedp) (if (atom body) body (case (car body) (keytype-p (if (eq key t) t (let ((call (cons (car key) (subst (cadr body) x (cdr key))))) (if key-negatedp (list 'not call) call)))) (non-keytype-p (if (eq key t) nil (let ((call (cons (car key) (subst (cadr body) x (cdr key))))) (if key-negatedp call (list 'not call))))) (valtype-p (if (eq val t) t (let ((call (cons (car val) (subst (cadr body) x (cdr val))))) (if val-negatedp (list 'not call) call)))) (non-valtype-p (if (eq val t) nil (let ((call (cons (car val) (subst (cadr body) x (cdr val))))) (if val-negatedp call (list 'not call))))) (keyval-alist-p (cons name (subst (cadr body) x formals))) (t (if (symbolp (car body)) (cons (car body) (defalist-thmbody-list-subst (cdr body) key val name formals x key-negatedp val-negatedp)) (defalist-thmbody-list-subst body key val name formals x key-negatedp val-negatedp)))))) (defun defalist-thmbody-list-subst (body key val name formals x key-negatedp val-negatedp) (if (atom body) body (cons (defalist-thmbody-subst (car body) key val name formals x key-negatedp val-negatedp) (defalist-thmbody-list-subst (cdr body) key val name formals x key-negatedp val-negatedp)))))
defalist-thmname-substfunction
(defun defalist-thmname-subst (thmname name key val) (b* ((thmname (symbol-name thmname)) (keyp (and (consp key) (car key))) (valp (and (consp val) (car val))) (subst-list `(("KEYVAL-ALIST-P" . ,(SYMBOL-NAME STD::NAME)) ("KEYVAL-ALIST" . ,(SYMBOL-NAME STD::NAME)) ,@(AND (CONSP STD::KEY) `(("KEYTYPE-P" . ,(SYMBOL-NAME STD::KEYP)) ("KEYTYPE" . ,(SYMBOL-NAME STD::KEYP)))) ,@(AND (CONSP STD::VAL) `(("VALTYPE-P" . ,(SYMBOL-NAME STD::VALP)) ("VALTYPE" . ,(SYMBOL-NAME STD::VALP))))))) (intern-in-package-of-symbol (dumb-str-sublis subst-list thmname) name)))
defalist-ruleclasses-substfunction
(defun defalist-ruleclasses-subst (rule-classes key val name formals x key-negatedp val-negatedp) (b* (((when (atom rule-classes)) rule-classes) (class (car rule-classes)) ((when (atom class)) (cons class (defalist-ruleclasses-subst (cdr rule-classes) key val name formals x key-negatedp val-negatedp))) (corollary-look (assoc-keyword :corollary (cdr class))) ((unless corollary-look) (cons class (defalist-ruleclasses-subst (cdr rule-classes) key val name formals x key-negatedp val-negatedp))) (prefix (take (- (len class) (len corollary-look)) class)) (corollary-term (defalist-thmbody-subst (cadr corollary-look) key val name formals x key-negatedp val-negatedp))) (cons (append prefix `(:corollary ,STD::COROLLARY-TERM . ,(CDDR STD::COROLLARY-LOOK))) (defalist-ruleclasses-subst (cdr rule-classes) key val name formals x key-negatedp val-negatedp))))
defalist-instantiatefunction
(defun defalist-instantiate (table-entry key val name formals kwd-alist x req-alist fn-subst world) (b* (((cons inst-thm alist) table-entry) ((when (not alist)) nil) (alist (and (not (eq alist t)) alist)) (req-look (assoc :requirement alist)) (req-ok (or (not req-look) (generic-eval-requirement (cadr req-look) req-alist))) ((unless req-ok) nil) (thmname-base (let ((look (assoc :name alist))) (if look (cadr look) inst-thm))) (thmname (defalist-thmname-subst thmname-base name key val)) (body (let ((look (assoc :body alist))) (if look (cadr look) (fgetprop inst-thm 'untranslated-theorem nil world)))) ((when (not body)) (er hard? 'defalist-instantiate "Bad defalist table entry: ~x0~%" inst-thm)) (rule-classes (b* ((cheap-look (and (getarg :cheap nil kwd-alist) (assoc :cheap-rule-classes alist))) ((when cheap-look) (cadr cheap-look)) (look (assoc :rule-classes alist))) (if look (cadr look) (fgetprop inst-thm 'classes nil world)))) (key-negatedp (getarg :key-negatedp nil kwd-alist)) (val-negatedp (getarg :val-negatedp nil kwd-alist)) (rule-classes (defalist-ruleclasses-subst rule-classes key val name formals x key-negatedp val-negatedp)) (disable (cdr (assoc :disable alist))) (defthm/defthmd (if disable 'defthmd 'defthm))) `((,STD::DEFTHM/DEFTHMD ,STD::THMNAME ,(STD::DEFALIST-THMBODY-SUBST STD::BODY STD::KEY STD::VAL STD::NAME STD::FORMALS STD::X STD::KEY-NEGATEDP STD::VAL-NEGATEDP) :hints (("goal" :use ((:functional-instance ,STD::INST-THM . ,STD::FN-SUBST)))) :rule-classes ,STD::RULE-CLASSES))))
defalist-instantiate-table-thms-auxfunction
(defun defalist-instantiate-table-thms-aux (table key val name formals kwd-alist x req-alist fn-subst world) (if (atom table) nil (append (defalist-instantiate (car table) key val name formals kwd-alist x req-alist fn-subst world) (defalist-instantiate-table-thms-aux (cdr table) key val name formals kwd-alist x req-alist fn-subst world))))
defalist-instantiate-table-thmsfunction
(defun defalist-instantiate-table-thms (name formals key val kwd-alist x world) (b* ((table (table-alist 'alistp-rules world)) (fn-subst (defalist-substitution name formals key val kwd-alist x)) (req-alist (defalist-requirement-alist kwd-alist formals key val))) (defalist-instantiate-table-thms-aux table key val name formals kwd-alist x req-alist fn-subst world)))
defalist-fnfunction
(defun defalist-fn (name formals kwd-alist other-events state) (declare (xargs :mode :program)) (b* (((unless (symbolp name)) (er hard 'deflist "Name must be a symbol, but is ~x0." name)) (mksym-package-symbol name) (world (w state)) (x (intern-in-package-of-symbol "X" name)) (a (intern-in-package-of-symbol "A" name)) (n (intern-in-package-of-symbol "N" name)) (y (intern-in-package-of-symbol "Y" name)) ((unless (and (symbol-listp formals) (no-duplicatesp formals))) (er hard 'defalist "The formals must be a list of unique symbols, but the ~ formals are ~x0." formals)) ((unless (member x formals)) (er hard 'defalist "The formals must contain X, but are ~x0.~%" formals)) ((when (or (member a formals) (member n formals) (member y formals))) (er hard 'defalist "As a special restriction, formals may not mention a, n, ~ or y, but the formals are ~x0." formals)) (key (getarg :key t kwd-alist)) ((unless (or (eq key t) (and (consp key) (symbolp (car key))))) (er hard 'defalist "The key recognizer must be a function applied ~ to the formals, but is ~x0." key)) (keyp (if (eq key t) t (car key))) (key-formals (if (eq key t) nil (cdr key))) (val (getarg :val t kwd-alist)) ((unless (or (eq val t) (and (consp val) (symbolp (car val))))) (er hard 'defalist "The value recognizer must be a function applied ~ to the formals, but is ~x0." val)) (valp (if (eq val t) t (car val))) (val-formals (if (eq val t) nil (cdr val))) (keyp-of-nil (if (eq key t) t (getarg :keyp-of-nil :unknown kwd-alist))) ((unless (member keyp-of-nil '(t nil :unknown))) (er hard? 'defalist "keyp-of-nil must be a boolean or :unknown.")) (valp-of-nil (if (eq val t) t (getarg :valp-of-nil :unknown kwd-alist))) ((unless (member valp-of-nil '(t nil :unknown))) (er hard? 'defalist "valp-of-nil must be a boolean or :unknown.")) (true-listp (getarg :true-listp nil kwd-alist)) (guard (getarg :guard t kwd-alist)) (verify-guards (getarg :verify-guards t kwd-alist)) ((unless (booleanp verify-guards)) (er hard 'defalist ":verify-guards must be a boolean, but is ~x0." verify-guards)) (mode (getarg :mode (default-defun-mode world) kwd-alist)) ((unless (or (eq mode :logic) (eq mode :program))) (er hard 'defalist ":mode must be one of :logic or :program, but is ~x0." mode)) (already-definedp (getarg :already-definedp nil kwd-alist)) ((unless (or (eq mode :logic) (not already-definedp))) (er hard 'defalist ":mode :program and already-definedp cannot be used together.")) (short (getarg :short nil kwd-alist)) (long (getarg :long nil kwd-alist)) (parents-p (assoc :parents kwd-alist)) (squelch-docs-p (and already-definedp (not short) (not long) (not (cdr parents-p)))) (parents (and (not squelch-docs-p) (if parents-p (cdr parents-p) (or (get-default-parents world) '(undocumented))))) (short (and (not squelch-docs-p) (or short (and parents (concatenate 'string "@(call " (full-escape-symbol name) ") recognizes association lists where every key satisfies @(see? " (full-escape-symbol keyp) ") and each value satisfies @(see? " (full-escape-symbol valp) ")."))))) (long (and (not squelch-docs-p) (or long (and parents (concatenate 'string "<p>This is an ordinary @(see std::defalist).</p>" "@(def " (full-escape-symbol name) ")"))))) (rest (append (getarg :rest nil kwd-alist) other-events)) (def (if already-definedp nil `((defund ,STD::NAME (,@STD::FORMALS) (declare (xargs :guard ,STD::GUARD :verify-guards ,STD::VERIFY-GUARDS :mode ,STD::MODE :normalize nil)) (if (consp ,STD::X) (and (consp (car ,STD::X)) ,@(AND (NOT (EQ STD::KEY T)) `((,STD::KEYP ,@(SUBST `(CAAR ,STD::X) STD::X STD::KEY-FORMALS)))) ,@(AND (NOT (EQ STD::VAL T)) `((,STD::VALP ,@(SUBST `(CDAR ,STD::X) STD::X STD::VAL-FORMALS)))) (,STD::NAME ,@(SUBST `(CDR ,STD::X) STD::X STD::FORMALS))) ,(IF STD::TRUE-LISTP `(NULL ,STD::X) T)))))) ((when (eq mode :program)) `(defsection ,STD::NAME ,@(AND (OR STD::SQUELCH-DOCS-P STD::PARENTS-P STD::PARENTS) `(:PARENTS ,STD::PARENTS)) ,@(AND STD::SHORT `(:SHORT ,STD::SHORT)) ,@(AND STD::LONG `(:LONG ,STD::LONG)) ,@(AND STD::SQUELCH-DOCS-P '(:NO-XDOC-OVERRIDE T)) (program) ,@STD::DEF ,@REST)) (theory-hack (getarg :theory-hack nil kwd-alist)) (events `((logic) (logic) (set-inhibit-warnings "theory" "free" "non-rec") (local (encapsulate nil ,@(AND (NOT (EQ STD::KEY T)) `((STD::LOCAL (STD::DEFTHM ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::KEYP 'STD::-FOR- STD::NAME 'STD::-KEY-LEMMA) (OR (EQUAL (,STD::KEYP ,@STD::KEY-FORMALS) T) (EQUAL (,STD::KEYP ,@STD::KEY-FORMALS) NIL)) :RULE-CLASSES NIL)))) ,@(AND (NOT (EQ STD::VAL T)) `((STD::LOCAL (STD::DEFTHM ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::VALP 'STD::-FOR- STD::NAME 'STD::-VAL-LEMMA) (OR (EQUAL (,STD::VALP ,@STD::VAL-FORMALS) T) (EQUAL (,STD::VALP ,@STD::VAL-FORMALS) NIL)) :RULE-CLASSES NIL)))) ,@(AND (NOT (EQ STD::KEYP-OF-NIL :UNKNOWN)) (NOT (EQ STD::KEY T)) `((STD::LOCAL (STD::DEFTHM ,(STD::MKSYM STD::KEYP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-KEY-LEMMA) (EQUAL (,STD::KEYP ,@(SUBST ''NIL STD::X STD::KEY-FORMALS)) ',STD::KEYP-OF-NIL) :RULE-CLASSES NIL)))) ,@(AND (NOT (EQ STD::VALP-OF-NIL :UNKNOWN)) (NOT (EQ STD::VAL T)) `((STD::LOCAL (STD::DEFTHM ,(STD::MKSYM STD::VALP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-VAL-LEMMA) (EQUAL (,STD::VALP ,@(SUBST ''NIL STD::X STD::VAL-FORMALS)) ',STD::VALP-OF-NIL) :RULE-CLASSES NIL)))) (local (in-theory nil)) ,@(AND (NOT (EQ STD::KEY T)) `((STD::DEFTHM ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::KEYP 'STD::-FOR- STD::NAME 'STD::-KEY) (OR (EQUAL (,STD::KEYP ,@STD::KEY-FORMALS) T) (EQUAL (,STD::KEYP ,@STD::KEY-FORMALS) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :BY ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::KEYP 'STD::-FOR- STD::NAME 'STD::-KEY-LEMMA)))))) ,@(AND (NOT (EQ STD::VAL T)) `((STD::DEFTHM ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::VALP 'STD::-FOR- STD::NAME 'STD::-VAL) (OR (EQUAL (,STD::VALP ,@STD::VAL-FORMALS) T) (EQUAL (,STD::VALP ,@STD::VAL-FORMALS) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :BY ,(STD::MKSYM 'STD::BOOLEANP-OF- STD::VALP 'STD::-FOR- STD::NAME 'STD::-VAL-LEMMA)))))) ,@(AND (NOT (EQ STD::KEYP-OF-NIL :UNKNOWN)) (NOT (EQ STD::KEY T)) `((STD::MAYBE-DEFTHM-AS-REWRITE ,(STD::MKSYM STD::KEYP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-KEY) (EQUAL (,STD::KEYP ,@(SUBST ''NIL STD::X STD::KEY-FORMALS)) ',STD::KEYP-OF-NIL) :HINTS (("Goal" :BY ,(STD::MKSYM STD::KEYP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-KEY-LEMMA)))))) ,@(AND (NOT (EQ STD::VALP-OF-NIL :UNKNOWN)) (NOT (EQ STD::VAL T)) `((STD::MAYBE-DEFTHM-AS-REWRITE ,(STD::MKSYM STD::VALP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-VAL) (EQUAL (,STD::VALP ,@(SUBST ''NIL STD::X STD::VAL-FORMALS)) ',STD::VALP-OF-NIL) :HINTS (("Goal" :BY ,(STD::MKSYM STD::VALP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-VAL-LEMMA)))))))) ,@STD::DEF (local (in-theory (theory 'minimal-theory))) (local (in-theory (disable (:executable-counterpart tau-system)))) (local (in-theory (enable ,STD::NAME ,@(AND (NOT (EQ STD::KEY T)) `(,(STD::MKSYM 'STD::BOOLEANP-OF- STD::KEYP 'STD::-FOR- STD::NAME 'STD::-KEY))) ,@(AND (NOT (EQ STD::VAL T)) `(,(STD::MKSYM 'STD::BOOLEANP-OF- STD::VALP 'STD::-FOR- STD::NAME 'STD::-VAL))) (:type-prescription ,STD::NAME)))) (local (enable-if-theorem ,(STD::MKSYM STD::KEYP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-KEY))) (local (enable-if-theorem ,(STD::MKSYM STD::VALP 'STD::-OF-NIL-FOR- STD::NAME 'STD::-VAL))) ,@STD::THEORY-HACK ,@(STD::DEFALIST-DEFLIST-INSTANTIATE-TABLE-THMS STD::NAME STD::FORMALS STD::KEY STD::VAL STD::KWD-ALIST STD::X STD::WORLD) ,@(STD::DEFALIST-INSTANTIATE-TABLE-THMS STD::NAME STD::FORMALS STD::KEY STD::VAL STD::KWD-ALIST STD::X STD::WORLD)))) `(defsection ,STD::NAME ,@(AND (OR STD::SQUELCH-DOCS-P STD::PARENTS-P STD::PARENTS) `(:PARENTS ,STD::PARENTS)) ,@(AND STD::SHORT `(:SHORT ,STD::SHORT)) ,@(AND STD::LONG `(:LONG ,STD::LONG)) ,@(AND STD::SQUELCH-DOCS-P '(:NO-XDOC-OVERRIDE T)) (encapsulate nil . ,STD::EVENTS) . ,(AND REST `((STD::VALUE-TRIPLE (STD::CW "Defalist: submitting /// events.~%")) (STD::WITH-OUTPUT :STACK :POP (PROGN (STD::LOCAL (STD::IN-THEORY (STD::ENABLE ,STD::NAME))) . ,REST)))))))
other
(defconst *defalist-valid-keywords* '(:key :val :cheap :guard :verify-guards :guard-debug :guard-hints :already-definedp :keyp-of-nil :valp-of-nil :mode :parents :short :long :true-listp :rest :verbosep :theory-hack))
defalistmacro
(defmacro defalist (name formals &rest args) (b* ((__function__ 'defalist) ((unless (symbolp name)) (raise "Name must be a symbol.")) (ctx (list 'defalist name)) ((mv main-stuff other-events) (split-/// ctx args)) ((mv kwd-alist extra-args) (extract-keywords ctx *defalist-valid-keywords* main-stuff nil)) ((when extra-args) (raise "Wrong number of non-keyword arguments to defalist.")) (verbosep (getarg :verbosep nil kwd-alist))) `(with-output :stack :push ,@(IF STD::VERBOSEP NIL '(:GAG-MODE T :OFF (SUMMARY OBSERVATION PROVE PROOF-TREE EVENT))) (make-event `(progn ,(STD::DEFALIST-FN ',STD::NAME ',STD::FORMALS ',STD::KWD-ALIST ',STD::OTHER-EVENTS STD::STATE) (value-triple '(defalist ,',STD::NAME)))))))