other
(in-package "DEFSTRUCTURE")
other
(include-book "utilities")
other
(program)
other
(defxdoc defstructure :parents (data-structures) :short "Define and characterize a general purpose record structure with typed slots." :long "<p>The on-line documentation only contains examples and a formal syntax description. The complete documentation for DEFSTRUCTURE is a report entitled "DEFSTRUCTURE for ACL2." This report is distributed with the ACL2 release, and is also available from the <a href='http://www.cs.utexas.edu/users/moore/acl2'>ACL2 home page</a>.</p> <p>Examples:</p> @({ (DEFSTRUCTURE SHIP X-POSITION Y-POSITION X-VELOCITY Y-VELOCITY MASS) (DEFSTRUCTURE MC-STATE "The state of the MC68020." (STATUS (:ASSERT (SYMBOLP STATUS) :TYPE-PRESCRIPTION)) (RFILE (:ASSERT (RFILEP RFILE) :REWRITE)) (PC (:ASSERT (LONGWORD-P PC) :REWRITE (:TYPE-PRESCRIPTION (NATURALP PC)))) (CCR (:ASSERT (CCR-P CCR) :REWRITE (:TYPE-PRESCRIPTION (NATURALP CCR)))) (MEM (:ASSERT (MEMORYP MEM) :REWRITE)) (:OPTIONS :GUARDS (:CONC-NAME MC-))) (DEFSTRUCTURE S&ADDR "An MC68020 effective address abstraction." (S (:ASSERT (MC-STATE-P S) :REWRITE)) (LOC (:ASSERT (SYMBOLP LOC) :TYPE-PRESCRIPTION)) (ADDR (:ASSERT ((LAMBDA (LOC ADDR) (CASE LOC ((D A) (RN-NUMBERP ADDR)) ((M I) (LONGWORD-P ADDR)) (OTHERWISE (NULL ADDR)))) LOC ADDR) (:REWRITE (IMPLIES (OR (EQUAL LOC 'D) (EQUAL LOC 'A)) (RN-NUMBERP ADDR))) (:REWRITE (IMPLIES (OR (EQUAL LOC 'M) (EQUAL LOC 'I)) (LONGWORD-P ADDR))))) (:OPTIONS :GUARDS)) (DEFSTRUCTURE V&CVZNX "An MC68020 value abstraction." (V (:ASSERT (LONGWORD-P V) :REWRITE (:TYPE-PRESCRIPTION (NATURALP V)))) (CVZNX (:ASSERT (CCR-P CVZNX) :REWRITE (:TYPE-PRESCRIPTION (NATURALP CVZNX)))) ;; These options make this nothing more than a typed CONS. (:OPTIONS :GUARDS (:REPRESENTATION (V . CVZNX)) (:DO-NOT :TAG))) }) <p>Syntax:</p> @({ DEFSTRUCTURE name [documentation] {slot-and-options}* [option-list] option-list ::= (:OPTIONS [[options]]) options ::= guards-option | verify-guards-option | slot-writers-option | inline-option conc-name-option | set-conc-name-option | keyword-constructor-option | keyword-updater-option | predicate-option | weak-predicate-option | force-option | representation-option | do-not-option | mv-intro-macro-option update-method-option | assertion-lemma-hints-option | predicate-guard-hints-option | prefix-option | {assert-option}* slot-and-options ::= slot-name | (slot-name [[slot-options]]) slot-options ::= default-option | read-only-option | {assert-option}* default-option ::= :DEFAULT | (:DEFAULT) | (:DEFAULT slot-initform) read-only-option ::= :READ-ONLY assert-option ::= (:ASSERT assertion {assertion-rule-descriptor}*) assertion-rule-descriptor ::= rule-token | (rule-token corollary [other-rule-forms]) rule-token ::= NIL | :REWRITE | :LINEAR | :LINEAR-ALIAS | :WELL-FOUNDED-RELATION | :BUILT-IN-CLAUSE | :COMPOUND-RECOGNIZER | :ELIM | :GENERALIZE | :META | :FORWARD-CHAINING | :EQUIVALENCE | :REFINEMENT | :CONGRUENCE | :TYPE-PRESCRIPTION | :DEFINITION | :INDUCTION | :TYPE-SET-INVERTER guards-option ::= :GUARDS verify-guards-option ::= :VERIFY-GUARDS | (:VERIFY-GUARDS) | (:VERIFY-GUARDS T) | (:VERIFY-GUARDS NIL) slot-writers-option ::= :SLOT-WRITERS inline-option ::= :INLINE conc-name-option ::= :CONC-NAME | (:CONC-NAME) | (:CONC-NAME conc-name) set-conc-name-option ::= :SET-CONC-NAME | (:SET-CONC-NAME) | (:SET-CONC-NAME set-conc-name) keyword-constructor-option ::= :KEYWORD-CONSTRUCTOR | (:KEYWORD-CONSTRUCTOR) | (:KEYWORD-CONSTRUCTOR keyword-constructor) keyword-updater-option ::= :KEYWORD-UPDATER | (:KEYWORD-UPDATER) | (:KEYWORD-UPDATER keyword-updater) predicate-option ::= :PREDICATE | (:PREDICATE) | (:PREDICATE predicate) weak-predicate-option ::= :WEAK-PREDICATE | (:WEAK-PREDICATE) | (:WEAK-PREDICATE weak-predicate) force-option ::= :FORCE do-not-option ::= (:DO-NOT [[do-not-options]]) do-not-options ::= :TAG | :READ-WRITE | :WRITE-WRITE representation-option ::= :REPRESENTATION | (:REPRESENTATION) | (:REPRESENTATION representation) representation ::= :LIST | :MV | :DOTTED-LIST | :TREE | template mv-intro-macro-option ::= :MV-INTRO-MACRO | (:MV-INTRO-MACRO) | (:MV-INTRO-MACRO mv-intro-macro) update-method-option ::= :UPDATE-METHOD | (:UPDATE-METHOD) | (:UPDATE-METHOD update-method) update-method ::= :HEURISTIC | :SET | :COPY assertion-lemma-hints-option ::= :ASSERTION-LEMMA-HINTS | (:ASSERTION-LEMMA-HINTS) | (:ASSERTION-LEMMA-HINTS hints) predicate-guard-hints-option ::= :PREDICATE-GUARD-HINTS | (:PREDICATE-GUARD-HINTS) | (:PREDICATE-GUARD-HINTS hints) prefix-option ::= :PREFIX | (:PREFIX) | (:PREFIX prefix) }) <p>Arguments and Values:</p> @({ assertion -- a slots-assertion. corollary -- a slots-assertion. conc-name -- a string-designator. documentation -- a string; not evaluated. hints -- an acl2-hints. keyword-constructor -- a symbol. keyword-updater -- a symbol. name -- a symbol. mv-intro-macro -- a symbol. other-rule-forms -- Some acl2-rule-forms. predicate -- a symbol. prefix -- a string-designator. read-write-lemma -- a symbol. set-conc-name -- a string-designator. slot-initform -- a form; not evaluated. slot-name -- a valid-slot-name. tag -- a symbol. template -- A slots-template. weak-predicate -- a symbol. write-write-lemma -- a symbol. }) <p>Definitions:</p> @({ acl2-hints -- any form valid as the hints argument of defthm. See the documentation for HINTS in the ACL2 documentation. acl2-rule-forms -- Any forms that would be valid in an ACL2 rule-classes form, except for the rule class itself, or a corollary and formula. See the documentation for the DEFSTRUCTURE assertion theory in the DEFSTRUCTURE document,and the ACL2 documentations for RULE-CLASSES. slots-assertion -- DEFSTRUCTURE assertions are covered in the DEFSTRUCTURE document. slots-template -- A cons tree whose flattened form (by DEFSTRUCTURE::FLATTEN) is a permutation of the list of slot names of the structure. string-designator -- a character, string or symbol, it designates the string obtained by (STRING STRING-DESIGNATOR) except that by convention the symbol NIL designates the empty string. valid-slot-name -- Any symbol valid for use as a formal parameter of a function. This is any symbol not in the "keyword" package, neither T nor NIL, neither beginning nor ending with `*', and not beginning with `&'. In addition, no slot-name may be the same as the structure name, and all slot-names must have unique print names, i.e., it is illegal to duplicate slot names, and it is illegal to use symbols from different packages that have the same print name. })")
acons-upmacro
(defmacro acons-up (&rest forms) (cond ((null forms) 'nil) (t `(acons$ ,(CAAR DEFSTRUCTURE::FORMS) ,(CADAR DEFSTRUCTURE::FORMS) (acons-up ,@(CDR DEFSTRUCTURE::FORMS))))))
bomb-frommacro
(defmacro bomb-from (where fmt &rest args) `(er hard ,DEFSTRUCTURE::WHERE ,DEFSTRUCTURE::FMT ,@DEFSTRUCTURE::ARGS))
bombmacro
(defmacro bomb (fmt &rest args) `(bomb-from 'defstructure ,DEFSTRUCTURE::FMT ,@DEFSTRUCTURE::ARGS))
other
(mutual-recursion (defun mlambda-fn-lst (args list) (cond ((atom list) nil) (t (cons (mlambda-fn args (car list)) (mlambda-fn-lst args (cdr list)))))) (defun mlambda-fn (args form) (declare (xargs :guard (symbol-listp args))) (cond ((atom form) (cond ((member form args) form) (t (list 'quote form)))) ((eq (car form) 'quote) (list 'quote form)) (t (cons 'list (cons (list 'quote (car form)) (mlambda-fn-lst args (cdr form))))))))
mlambdamacro
(defmacro mlambda (args form) "A macro lambda that doesn't substitute function symbols or quoted constants." (declare (xargs :guard (symbol-listp args))) (mlambda-fn args form))
ncarsfunction
(defun ncars (n l) "The 1st n CARs of l." (cond ((= n 0) nil) ((null l) nil) (t (cons (car l) (ncars (- n 1) (cdr l))))))
foldfunction
(defun fold (args) "Folds a list into a somewhat balanced tree." (cond ((null args) nil) ((null (cdr args)) (car args)) (t (cons (fold (ncars (truncate (length args) 2) args)) (fold (nthcdr (truncate (length args) 2) args))))))
flattenfunction
(defun flatten (args) "An `improper' list flattener. NIL is always flattened away." (cond ((atom args) (cond ((null args) nil) (t (list args)))) (t (append (flatten (car args)) (flatten (cdr args))))))
dotifyfunction
(defun dotify (l) "Make the last CONS of l a `dotted pair' if possible." (cond ((atom l) l) ((atom (cdr l)) l) ((atom (cdr (cdr l))) (cond ((null (cdr (cdr l))) (cons (car l) (cadr l))) (t l))) (t (cons (car l) (dotify (cdr l))))))
duplicates-equalfunction
(defun duplicates-equal (lst) (cond ((atom lst) nil) ((member-equal (car lst) (cdr lst)) (add-to-set-equal (car lst) (duplicates-equal (cdr lst)))) (t (duplicates-equal (cdr lst)))))
keywordifyfunction
(defun keywordify (string-designator) (intern-in-package-of-symbol (string string-designator) :keyword))
other
(defloop keywordify-list
(l)
(for ((x in l))
(collect (keywordify x))))
keywordify-treefunction
(defun keywordify-tree (tree) (cond ((atom tree) (cond ((not tree) nil) ((not (symbolp tree)) (bomb-from 'keywordify-tree "Bug. ~p0" tree)) (t (keywordify tree)))) (t (cons (keywordify-tree (car tree)) (keywordify-tree (cdr tree))))))
other
(defloop keywordp-listp
(l)
(for ((x in l))
(always (keywordp x))))
other
(defloop list-all
(l)
(for ((x in l))
(collect (list x))))
other
(defloop map-string
(l)
(for ((x in l))
(collect (string x))))
other
(defloop remove-strings (l) (for ((x in l)) (unless (stringp x) (collect x))))
x-or-car-xfunction
(defun x-or-car-x (x) (if (atom x) x (car x)))
other
(defloop map-x-or-car-x
(l)
(for ((x in l))
(collect (x-or-car-x x))))
x-or-cadr-xfunction
(defun x-or-cadr-x (x) (declare (xargs :guard (or (atom x) (and (consp x) (consp (cdr x)))))) (if (atom x) x (cadr x)))
other
(defloop map-x-or-cadr-x
(l)
(for ((x in l))
(collect (x-or-cadr-x x))))
designated-stringfunction
(defun designated-string (string-designator) (cond ((null string-designator) "") (t (string string-designator))))
lambda-function-pfunction
(defun lambda-function-p (x) (and (true-listp x) (equal (length x) 3) (equal (first x) 'lambda) (true-listp (second x))))
other
(mutual-recursion (defun assertion-termp (term) (cond ((atom term) t) ((eq (car term) 'quote) t) (t (and (or (symbolp (car term)) (lambda-function-p (car term))) (assertion-termp-list (cdr term)))))) (defun assertion-termp-list (l) (cond ((atom l) (null l)) (t (and (assertion-termp (car l)) (assertion-termp-list (cdr l)))))))
other
(mutual-recursion (defun reason-for-not-assertion-termp (term) (cond ((atom term) nil) ((eq (car term) 'quote) nil) (t (if (or (symbolp (car term)) (lambda-function-p (car term))) (reason-for-not-assertion-termp-list (cdr term)) (msg "the CAR of ~p0 is neither a symbol nor a LAMBDA function." term))))) (defun reason-for-not-assertion-termp-list (l) (cond ((atom l) (or (null l) (msg "it contains an `improper' list terminated by the atom ~ ~p0." l))) (t (or (reason-for-not-assertion-termp (car l)) (reason-for-not-assertion-termp-list (cdr l)))))))
other
(mutual-recursion (defun free-vars1 (term ans) "A free variable is a symbol that is not a constant, i.e., it excludes T, NIL, and *CONST* etc." (cond ((atom term) (if (and (symbolp term) (not (eq (legal-variable-or-constant-namep term) 'constant))) (add-to-set-eq term ans) ans)) ((eq (car term) 'quote) ans) (t (free-vars1-lst (cdr term) ans)))) (defun free-vars1-lst (terms ans) (cond ((atom terms) ans) (t (free-vars1-lst (cdr terms) (free-vars1 (car terms) ans))))))
other
(mutual-recursion (defun subst-expr (new old term) (cond ((equal term old) new) ((atom term) term) ((eq (car term) 'quote) term) (t (cons (car term) (subst-expr-lst new old (cdr term)))))) (defun subst-expr-lst (new old args) (cond ((null args) nil) (t (cons (subst-expr new old (car args)) (subst-expr-lst new old (cdr args)))))))
subst-expr-allfunction
(defun subst-expr-all (term new-list old-list) (cond ((atom old-list) term) (t (subst-expr-all (subst-expr (car new-list) (car old-list) term) (cdr new-list) (cdr old-list)))))
other
(logic)
other
(defthm open-mv-nth (implies (syntaxp (and (consp n) (eq (car n) 'quote))) (equal (mv-nth n l) (if (zp n) (car l) (mv-nth (1- n) (cdr l))))) :hints (("Goal" :in-theory (enable mv-nth))))
other
(in-theory (disable open-mv-nth))
other
(program)
other
(defconst *db-fields* '(:acl2-count-lemma :assertions :assertion-lemma :assertion-lemma-hints :conc-name :constructor-call :definition-theory :doc :elimination-lemma :force :guards :inline :intro-macro :keyword-constructor :keyword-slot-names :keyword-updater :lemma-theory :lift-if-lemma :mv-intro-macro :name :predicate :predicate-call :predicate-constructor-lemma :predicate-slot-writers-lemma :predicate-guard-hints :predicate-weak-predicate-lemma :prefix :read-lemma :read-only :read-write :read-write-lemma :representation :required-slot-names :set-conc-name :slot-names :tag :template :update-method :value-variable :value-variable1 :verify-guards :weak-predicate :weak-predicate-call :weak-predicate-constructor-lemma :weak-predicate-slot-writers-lemma :write-lemma :write-write :write-write-lemma))
other
(defconst *db-slot-fields* '(:assertions :default :default-specified :reader :reader-call :read-only :writer :writer-call))
other
(defconst *function-names* `(:name :predicate :weak-predicate))
other
(defconst *slot-function-names* '(:reader :writer))
other
(defconst *macro-names* '(:keyword-constructor :keyword-updater))
other
(defconst *lemma-names* '(:acl2-count-lemma :assertion-lemma :elimination-lemma :lift-if-lemma :predicate-constructor-lemma :predicate-slot-writers-lemma :predicate-weak-predicate-lemma :read-lemma :read-write-lemma :weak-predicate-constructor-lemma :weak-predicate-slot-writers-lemma :write-lemma :write-write-lemma))
db-fnfunction
(defun db-fn (key form db) (let ((pair (assoc key db))) (cond (pair (cdr pair)) (t (bomb-from 'db-fn "Key not present at runtime: ~p0." form)))))
db-slot-fnfunction
(defun db-slot-fn (slot key form db) (let ((pair (assoc-equal (cons slot key) db))) (cond (pair (cdr pair)) (t (bomb-from 'db-slot-fn "Key not present at runtime: ~p0." form)))))
dbmacro
(defmacro db (&whole form &rest args) (case (length args) (1 (cond ((not (member (car args) *db-fields*)) (bomb-from 'db "Unrecognized field: ~p0" form)) (t `(db-fn ,(CAR DEFSTRUCTURE::ARGS) ',DEFSTRUCTURE::FORM db)))) (2 (cond ((not (member (cadr args) *db-slot-fields*)) (bomb-from 'db "Unrecognized slot field: ~p0" form)) (t `(db-slot-fn ,(CAR DEFSTRUCTURE::ARGS) ,(CADR DEFSTRUCTURE::ARGS) ',DEFSTRUCTURE::FORM db)))) (t (bomb-from "DB coded with wrong # of args: ~p0" form))))
acons-dbmacro
(defmacro acons-db (&rest forms) "Acons up a list of (<keyword> <value>) pairs, evaluting each successive form in the context of the new DB." (cond ((null forms) 'db) (t (cond ((not (member (caar forms) *db-fields*)) (bomb-from 'acons-db "Unrecognized field: ~p0" (caar forms))) (t `(let ((db (acons$ ,(CAAR DEFSTRUCTURE::FORMS) ,(CADAR DEFSTRUCTURE::FORMS) db))) (acons-db ,@(CDR DEFSTRUCTURE::FORMS))))))))
append-dbmacro
(defmacro append-db (&rest forms) "APPEND new sublists to DB, evaluting each sucessive form in the context of the new DB." (cond ((null forms) 'db) (t `(let ((db (append ,(CAR DEFSTRUCTURE::FORMS) db))) (append-db ,@(CDR DEFSTRUCTURE::FORMS))))))
extend-dbmacro
(defmacro extend-db (&rest forms) "Evaluate each form in the context of the DB that successive forms created." (cond ((null forms) 'db) (t `(let ((db ,(CAR DEFSTRUCTURE::FORMS))) (extend-db ,@(CDR DEFSTRUCTURE::FORMS))))))
other
(defloop db-let-fn
(fields)
(for ((field in fields))
(collect (cond ((symbolp field) `(,DEFSTRUCTURE::FIELD (db ,(DEFSTRUCTURE::KEYWORDIFY DEFSTRUCTURE::FIELD))))
((and (consp field)
(consp (cdr field))
(symbolp (cadr field))) `(,(CADR DEFSTRUCTURE::FIELD) (db ,(CAR DEFSTRUCTURE::FIELD)
,(DEFSTRUCTURE::KEYWORDIFY (CADR DEFSTRUCTURE::FIELD)))))
(t (bomb-from 'db-let-fn
"Illegal field: ~p0"
field))))))
db-letmacro
(defmacro db-let (fields &rest forms) "This macro is a shorthand way to bind fields of the DB to the like-named variable. A field can be a field name, or (slot field)." `(let ,(DEFSTRUCTURE::DB-LET-FN DEFSTRUCTURE::FIELDS) ,@DEFSTRUCTURE::FORMS))
other
(defloop map-slots-db
(slot-names key
db)
"Return a list in SLOT order of the indicated key."
(for ((slot in
slot-names))
(collect (db-slot-fn slot
key
`(map-slots-db on
,DEFSTRUCTURE::SLOT
,DEFSTRUCTURE::KEY)
db))))
other
(defloop map-if-slots-db
(slot-names key
db)
"Return a list in SLOT order of the indicated key if non-NIL."
(for ((slot in
slot-names))
(append (let ((val (db-slot-fn slot
key
`(map-if-slots-db on
,DEFSTRUCTURE::SLOT
,DEFSTRUCTURE::KEY)
db)))
(if val
(list val)
nil)))))
other
(defrec assertion (assertion bound-slots subst-assertion slot rules) nil)
other
(defrec rule (assertion rule-class) nil)
other
(defloop required-slot-names (slot-names db) "A slot is required by the constructor macro if no default was specified." (for ((slot in slot-names)) (unless (db slot :default-specified) (collect (keywordify slot)))))
make-corollaryfunction
(defun make-corollary (assertion db) "Create the :COROLLARY rule for the assertion." (let* ((force (db :force)) (predicate-call (db :predicate-call)) (hyp (if force `(force ,DEFSTRUCTURE::PREDICATE-CALL) predicate-call))) `(implies ,DEFSTRUCTURE::HYP ,(DEFSTRUCTURE::ACCESS DEFSTRUCTURE::ASSERTION DEFSTRUCTURE::ASSERTION :SUBST-ASSERTION))))
make-prefix-namemacro
(defmacro make-prefix-name (&rest names) `(pack-intern (db :name) (db :prefix) ,@DEFSTRUCTURE::NAMES))
make-templatefunction
(defun make-template (db) "Using the :SLOT-NAMES, :REPRESENTATION, and :TAG, make a template for function generation. If the structure is tagged, the tag is always added as the CAR. We know that the :TAG is a symbol, and that the :REPRSENTATION is of the proper form." (db-let (representation slot-names tag) (let ((template (case representation ((:mv :list) slot-names) (:dotted-list (dotify slot-names)) (:tree (fold slot-names)) (t representation)))) (if tag (cons tag template) template))))
other
(defloop reader-names (slot-names db) (for ((slot in slot-names)) (collect (db-let (name conc-name) (cons (cons slot :reader) (pack-intern name conc-name slot))))))
other
(defloop writer-names (slot-names db) "Generate the writer name, setting to NIL if either the slot or the structure as a whole is :READ-ONLY." (for ((slot in slot-names)) (collect (db-let (name set-conc-name (slot read-only)) (cons (cons slot :writer) (if (or read-only (db :read-only)) nil (pack-intern name set-conc-name slot)))))))
other
(defloop reader-calls (slot-names db) "Create a symbolic access form for a slot. The default access form for slot A of structure FOO looks like (FOO-A FOO)." (for ((slot in slot-names)) (collect (db-let (name) (cons (cons slot :reader-call) `(,(DEFSTRUCTURE::DB DEFSTRUCTURE::SLOT :READER) ,DEFSTRUCTURE::NAME))))))
other
(defloop writer-calls (slot-names db) "Create a symbolic update form for a slot. The default update form for slot A of structure FOO with slots A, B, and C looks like (SET-FOO-A FOOABC FOO)." (for ((slot in slot-names)) (collect (db-let (name value-variable (slot writer)) (cons (cons slot :writer-call) (if writer `(,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE ,DEFSTRUCTURE::NAME) nil))))))
guard-declarationfunction
(defun guard-declaration (guard verifyp db) "If :GUARDS was specified, declare a guard and verify based on :VERIFY-GUARDS. Note that the default is :DEFAULT." (db-let (guards verify-guards) (if guards (list `(declare (xargs :guard ,DEFSTRUCTURE::GUARD ,@(COND ((OR (NULL DEFSTRUCTURE::VERIFYP) (NULL DEFSTRUCTURE::VERIFY-GUARDS)) '(:VERIFY-GUARDS NIL)) ((EQ DEFSTRUCTURE::VERIFY-GUARDS T) '(:VERIFY-GUARDS T)))))) nil)))
constructor-bodyfunction
(defun constructor-body (template) "Use the template to create a large CONS expression that creates the new tuple. The elements of the template are the argument names." (cond ((atom template) template) (t `(cons ,(DEFSTRUCTURE::CONSTRUCTOR-BODY (CAR DEFSTRUCTURE::TEMPLATE)) ,(DEFSTRUCTURE::CONSTRUCTOR-BODY (CDR DEFSTRUCTURE::TEMPLATE))))))
template-costfunction
(defun template-cost (template) (cond ((atom template) 0) (t (+ 1 (template-cost (car template)) (template-cost (cdr template))))))
other
(defloop acl2-countify-slots
(slots)
(for ((slot in slots))
(collect `(acl2-count ,DEFSTRUCTURE::SLOT))))
constructorfunction
(defun constructor (db) "If :REPRESENTATION is :MV, create an MV macro. Else create a function or macro under control of the :INLINE option. For tagged structures the tag is in the constructor-body as a free variable, so we need to bind it." (db-let (name acl2-count-lemma constructor-call slot-names representation tag doc template inline) (cond ((eq representation :mv) (list " ; The constructor is defined as a macro that expands into an MV form for ; every slot. " `(defmacro ,DEFSTRUCTURE::NAME ,DEFSTRUCTURE::SLOT-NAMES ,@(IF DEFSTRUCTURE::DOC (LIST DEFSTRUCTURE::DOC) NIL) (cons 'mv (list ,@DEFSTRUCTURE::SLOT-NAMES))))) (inline (list " ; The constructor is defined as a macro that accepts every slot. " (if tag `(defmacro ,DEFSTRUCTURE::NAME ,DEFSTRUCTURE::SLOT-NAMES ,@(IF DEFSTRUCTURE::DOC (LIST DEFSTRUCTURE::DOC) NIL) (let ((,DEFSTRUCTURE::TAG '',DEFSTRUCTURE::TAG)) (mlambda (,DEFSTRUCTURE::TAG ,@DEFSTRUCTURE::SLOT-NAMES) ,(DEFSTRUCTURE::CONSTRUCTOR-BODY DEFSTRUCTURE::TEMPLATE)))) `(defmacro ,DEFSTRUCTURE::NAME ,DEFSTRUCTURE::SLOT-NAMES ,@(IF DEFSTRUCTURE::DOC (LIST DEFSTRUCTURE::DOC) NIL) (mlambda ,DEFSTRUCTURE::SLOT-NAMES ,(DEFSTRUCTURE::CONSTRUCTOR-BODY DEFSTRUCTURE::TEMPLATE)))))) (t (list " ; The constructor is defined as a function that accepts every slot. " (if tag `(defun ,DEFSTRUCTURE::NAME ,DEFSTRUCTURE::SLOT-NAMES ,@(IF DEFSTRUCTURE::DOC (LIST DEFSTRUCTURE::DOC) NIL) ,@(DEFSTRUCTURE::GUARD-DECLARATION T T DEFSTRUCTURE::DB) (let ((,DEFSTRUCTURE::TAG ',DEFSTRUCTURE::TAG)) ,(DEFSTRUCTURE::CONSTRUCTOR-BODY DEFSTRUCTURE::TEMPLATE))) `(defun ,DEFSTRUCTURE::NAME ,DEFSTRUCTURE::SLOT-NAMES ,@(IF DEFSTRUCTURE::DOC (LIST DEFSTRUCTURE::DOC) NIL) ,@(DEFSTRUCTURE::GUARD-DECLARATION T T DEFSTRUCTURE::DB) ,(DEFSTRUCTURE::CONSTRUCTOR-BODY DEFSTRUCTURE::TEMPLATE))) " ; This lemma justifies recursion on any slot of the structure. It is ; unlikely to be used unless the structure is itself recursive. " `(defthm ,DEFSTRUCTURE::ACL2-COUNT-LEMMA (equal (acl2-count ,DEFSTRUCTURE::CONSTRUCTOR-CALL) (+ ,(DEFSTRUCTURE::TEMPLATE-COST DEFSTRUCTURE::TEMPLATE) ,@(DEFSTRUCTURE::ACL2-COUNTIFY-SLOTS DEFSTRUCTURE::SLOT-NAMES)))))))))
weak-predicate-bodyfunction
(defun weak-predicate-body (template tree) "Traverse the template, creating CONSP and NULL expressions wherever needed. It is necessary for the read/write lemmas that if the template contains a NULL entry, that entry must be NULL in every shell. This is initialized with tree = <structure-name> which is the formal parameter of the weak predicate." (cond ((atom template) (cond ((null template) (list `(null ,DEFSTRUCTURE::TREE))))) (t (append (list `(consp ,DEFSTRUCTURE::TREE)) (weak-predicate-body (car template) `(car ,DEFSTRUCTURE::TREE)) (weak-predicate-body (cdr template) `(cdr ,DEFSTRUCTURE::TREE))))))
reader-bodyfunction
(defun reader-body (slot template tree) "Write a CA/DR form to get slot from a structure. Tree is initialized with the structure name, which is the formal parameter of the reader." (declare (xargs :guard (symbolp slot))) (cond ((atom template) (cond ((eq slot template) tree))) (t (or (reader-body slot (car template) `(car ,DEFSTRUCTURE::TREE)) (reader-body slot (cdr template) `(cdr ,DEFSTRUCTURE::TREE))))))
weak-predicatefunction
(defun weak-predicate (db) "This is the predicate on the `structure' of the structure. If the structure is named, then we include a test that the CAR of the structure is the correct name. We also write a lemma that shows when the constructor function satisfies this predicate." (db-let (weak-predicate weak-predicate-constructor-lemma constructor-call name template tag inline) (let* ((wp-body (weak-predicate-body template name)) (body (cond ((null template) (list `(null ,DEFSTRUCTURE::NAME))) ((atom template) (list `(declare (ignore ,DEFSTRUCTURE::NAME)) t)) (tag (list `(and ,@DEFSTRUCTURE::WP-BODY (eq (car ,DEFSTRUCTURE::NAME) ',DEFSTRUCTURE::TAG)))) (t (list `(and ,@DEFSTRUCTURE::WP-BODY)))))) (list* " ; This predicate defines the `structure' of the structure, and is used as a ; weak guard on the readers and writers (if defined). " `(defun ,DEFSTRUCTURE::WEAK-PREDICATE (,DEFSTRUCTURE::NAME) ,@(DEFSTRUCTURE::GUARD-DECLARATION T T DEFSTRUCTURE::DB) ,@DEFSTRUCTURE::BODY) (if inline nil (list " ; The weak-predicate is satisfied by any explicit reference of the ; constructor. We also store this information as a :BUILT-IN-CLAUSE " `(defthm ,DEFSTRUCTURE::WEAK-PREDICATE-CONSTRUCTOR-LEMMA (equal (,DEFSTRUCTURE::WEAK-PREDICATE ,DEFSTRUCTURE::CONSTRUCTOR-CALL) t) :rule-classes ((:rewrite) (:built-in-clause :corollary (,DEFSTRUCTURE::WEAK-PREDICATE ,DEFSTRUCTURE::CONSTRUCTOR-CALL))))))))))
other
(defloop map-access-assertion-assertion
(assertions)
(for ((assertion in
assertions))
(collect (access assertion
assertion
:assertion))))
other
(defloop slot-assertions (slot-names db) (for ((slot in slot-names)) (append (db-let ((slot assertions)) (map-access-assertion-assertion assertions)))))
other
(defloop map-access-assertion-subst-assertion
(assertions)
(for ((assertion in
assertions))
(collect (access assertion
assertion
:subst-assertion))))
other
(defloop slot-subst-assertions (slot-names db) (for ((slot in slot-names)) (append (db-let ((slot assertions)) (map-access-assertion-subst-assertion assertions)))))
predicate-bodyfunction
(defun predicate-body (db) "The predicate body is a conjunction of the weak predicate, and all assertions about the slots." (db-let (weak-predicate-call slot-names assertions) `(and ,DEFSTRUCTURE::WEAK-PREDICATE-CALL ,@(DEFSTRUCTURE::REMOVE-DUPLICATES-EQUAL (APPEND (DEFSTRUCTURE::SLOT-SUBST-ASSERTIONS DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB) (DEFSTRUCTURE::MAP-ACCESS-ASSERTION-SUBST-ASSERTION DEFSTRUCTURE::ASSERTIONS))) t)))
predicate-assertions-explicitfunction
(defun predicate-assertions-explicit (db) "The predicate, as the set of assertions for explicit instances of the constructor." (db-let (slot-names assertions) (let ((assertions (remove-duplicates-equal (append (slot-assertions slot-names db) (map-access-assertion-assertion assertions))))) (cond (assertions `(and ,@DEFSTRUCTURE::ASSERTIONS t)) (t 't)))))
predicatefunction
(defun predicate (db) (db-let (predicate name predicate-call weak-predicate-call constructor-call predicate-weak-predicate-lemma predicate-constructor-lemma inline) (list* " ; This is the predicate, which contains the weak predicate and every ; assertion made about the slots of the structure. The final T guarantees ; that all DEFSTRUCTURE predicates are Boolean. " `(defun ,DEFSTRUCTURE::PREDICATE (,DEFSTRUCTURE::NAME) ,@(DEFSTRUCTURE::GUARD-DECLARATION T NIL DEFSTRUCTURE::DB) ,(DEFSTRUCTURE::PREDICATE-BODY DEFSTRUCTURE::DB)) (if inline nil (list " ; This lemma shows that the predicate includes the weak predicate, as ; :REWRITE, :FORWARD-CHAINING, and :BUILT-IN-CLAUSE rules. Note that the ; :REWRITE rule is sometimes implicated in thrashing in conjunction with the ; normalization lemmas. " `(defthm ,DEFSTRUCTURE::PREDICATE-WEAK-PREDICATE-LEMMA (implies ,DEFSTRUCTURE::PREDICATE-CALL ,DEFSTRUCTURE::WEAK-PREDICATE-CALL) :rule-classes (:forward-chaining :rewrite :built-in-clause)) " ; This lemma rewrites the predicate on an explicit reference of ; the constructor. " `(defthm ,DEFSTRUCTURE::PREDICATE-CONSTRUCTOR-LEMMA (equal (,DEFSTRUCTURE::PREDICATE ,DEFSTRUCTURE::CONSTRUCTOR-CALL) ,(DEFSTRUCTURE::PREDICATE-ASSERTIONS-EXPLICIT DEFSTRUCTURE::DB))))))))
other
(defloop default-alist (slot-names db) (for ((slot in slot-names)) (collect (cons (keywordify slot) (db slot :default)))))
other
(defloop keyword-constructor-body (args keyword-slot-names default-alist) (for ((keyword-slot in keyword-slot-names)) (collect (let ((tail (assoc-keyword keyword-slot args))) (if tail (cadr tail) (cdr (assoc keyword-slot default-alist)))))))
keyword-slot-checkerfunction
(defun keyword-slot-checker (macro-name form args keyword-slot-names) "Check keyword argument list for basic syntax and either bomb or return NIL." (cond ((not (keyword-value-listp args)) (bomb-from macro-name "The argument list in the macro invocation ~p0 ~ does not match the syntax of a keyword argument ~ list because ~@1." form (reason-for-non-keyword-value-listp args))) ((not (subsetp (evens args) keyword-slot-names)) (bomb-from macro-name "The argument list in the macro invocation ~p0 is not ~ a valid keyword argument list because it contains the ~ ~#1~[keyword~/keywords~] ~&1, which ~#1~[is~/are~] ~ not the keyword ~#1~[form~/forms~] of any of the ~ slot names ~&2." form (set-difference-equal (evens args) keyword-slot-names) keyword-slot-names)) (t nil)))
keyword-constructor-fnfunction
(defun keyword-constructor-fn (form args name keyword-constructor default-alist keyword-slot-names required-slot-names) (cond ((keyword-slot-checker keyword-constructor form args keyword-slot-names)) ((not (subsetp required-slot-names (evens args))) (bomb-from keyword-constructor "The argument list in the macro invocation ~p0 is not ~ valid does not specify a value for the required ~ ~#1~[keyword~/keywords~] ~&1. ~ Any slot which has no :DEFAULT option at ~ DEFSTRUCTURE time must be specified in every ~ invocation of the constructor macro." form (set-difference-equal required-slot-names (evens args)) keyword-slot-names)) (t `(,DEFSTRUCTURE::NAME ,@(DEFSTRUCTURE::KEYWORD-CONSTRUCTOR-BODY DEFSTRUCTURE::ARGS DEFSTRUCTURE::KEYWORD-SLOT-NAMES DEFSTRUCTURE::DEFAULT-ALIST)))))
keyword-constructorfunction
(defun keyword-constructor (db) (db-let (name keyword-constructor slot-names keyword-slot-names required-slot-names) (if keyword-constructor (list " ; This is the keyword constructor macro. It will expand into a call of the ; constructor, with appropriate defaulting. " `(defmacro ,DEFSTRUCTURE::KEYWORD-CONSTRUCTOR (&whole form &rest args) (keyword-constructor-fn form args ',DEFSTRUCTURE::NAME ',DEFSTRUCTURE::KEYWORD-CONSTRUCTOR ',(DEFSTRUCTURE::DEFAULT-ALIST DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB) ',DEFSTRUCTURE::KEYWORD-SLOT-NAMES ',DEFSTRUCTURE::REQUIRED-SLOT-NAMES))) nil)))
other
(defloop reader-definitions (slot-names db) (for ((slot in slot-names)) (collect (db-let ((slot reader) name weak-predicate-call template inline) (if inline `(defmacro ,DEFSTRUCTURE::READER (,DEFSTRUCTURE::NAME) (mlambda (,DEFSTRUCTURE::NAME) ,(DEFSTRUCTURE::READER-BODY DEFSTRUCTURE::SLOT DEFSTRUCTURE::TEMPLATE DEFSTRUCTURE::NAME))) `(defun ,DEFSTRUCTURE::READER (,DEFSTRUCTURE::NAME) ,@(DEFSTRUCTURE::GUARD-DECLARATION DEFSTRUCTURE::WEAK-PREDICATE-CALL T DEFSTRUCTURE::DB) ,(DEFSTRUCTURE::READER-BODY DEFSTRUCTURE::SLOT DEFSTRUCTURE::TEMPLATE DEFSTRUCTURE::NAME)))))))
readersfunction
(defun readers (db) "Define the reader functions" (db-let (slot-names) (if slot-names (cons " ; These are the `readers' for the structure. " (reader-definitions slot-names db)) nil)))
other
(defconst *binding-variable* '|x|)
other
(defconst *binding-variable1* '|y|)
writer-bodyfunction
(defun writer-body (slot template var tree) "Write a CONS form to put a new slot into a structure, given the slot, the structure template, a variable name (a formal parameter) and the `tree'." (declare (xargs :guard (symbolp slot))) (cond ((atom template) (cond ((eq slot template) var))) (t (let ((car-side (writer-body slot (car template) var `(car ,DEFSTRUCTURE::TREE))) (cdr-side (writer-body slot (cdr template) var `(cdr ,DEFSTRUCTURE::TREE)))) (cond (car-side `(cons ,DEFSTRUCTURE::CAR-SIDE ,(COND ((NULL (CDR DEFSTRUCTURE::TEMPLATE)) NIL) (T `(CDR ,DEFSTRUCTURE::TREE))))) (cdr-side `(cons (car ,DEFSTRUCTURE::TREE) ,DEFSTRUCTURE::CDR-SIDE)))))))
writer-macro-fnfunction
(defun writer-macro-fn (bind slot template value name) (if bind `(let ((,DEFSTRUCTURE::*BINDING-VARIABLE* (check-vars-not-free (,DEFSTRUCTURE::*BINDING-VARIABLE*) ,DEFSTRUCTURE::NAME))) ,(DEFSTRUCTURE::WRITER-BODY DEFSTRUCTURE::SLOT DEFSTRUCTURE::TEMPLATE DEFSTRUCTURE::VALUE DEFSTRUCTURE::*BINDING-VARIABLE*)) (writer-body slot template value name)))
other
(defloop writer-definitions (slot-names db) (for ((slot in slot-names)) (append (db-let ((slot writer) name weak-predicate-call template value-variable inline) (if writer (if inline (list `(defmacro ,DEFSTRUCTURE::WRITER (,DEFSTRUCTURE::VALUE-VARIABLE ,DEFSTRUCTURE::NAME) (writer-macro-fn (not (atom ,DEFSTRUCTURE::NAME)) ',DEFSTRUCTURE::SLOT ',DEFSTRUCTURE::TEMPLATE ,DEFSTRUCTURE::VALUE-VARIABLE ,DEFSTRUCTURE::NAME))) (list `(defun ,DEFSTRUCTURE::WRITER (,DEFSTRUCTURE::VALUE-VARIABLE ,DEFSTRUCTURE::NAME) ,@(DEFSTRUCTURE::GUARD-DECLARATION DEFSTRUCTURE::WEAK-PREDICATE-CALL T DEFSTRUCTURE::DB) ,(DEFSTRUCTURE::WRITER-BODY DEFSTRUCTURE::SLOT DEFSTRUCTURE::TEMPLATE DEFSTRUCTURE::VALUE-VARIABLE DEFSTRUCTURE::NAME)))) nil)))))
writersfunction
(defun writers (db) "Define the writer functions." (db-let (slot-names read-only) (if read-only nil (cons " ; These are the `writers' for the structure. " (writer-definitions slot-names db)))))
other
(defloop keyword-writer-map (slot-names db) (for ((slot in slot-names)) (collect (db-let ((slot writer)) (cons (keywordify slot) writer)))))
other
(defloop keyword-reader-map (slot-names db) (for ((slot in slot-names)) (collect (db-let ((slot reader)) (cons (keywordify slot) reader)))))
other
(defloop read-only-keyword-slots (slot-names db) (for ((slot in slot-names)) (when (db slot :read-only) (collect (keywordify slot)))))
slot-costfunction
(defun slot-cost (slot template accum) "Compute the cost of reading (CAR/CDR) and writing (CONS) a slot." (cond ((atom template) (cond ((eq slot template) accum) (t nil))) (t (or (slot-cost slot (car template) (1+ accum)) (slot-cost slot (cdr template) (1+ accum))))))
set-costfunction
(defun set-cost (slots template) (cond ((atom slots) 0) (t (+ (slot-cost (car slots) template 0) (set-cost (cdr slots) template)))))
set-heuristicfunction
(defun set-heuristic (keyword-set-slots template) (let* ((keyword-template (keywordify-tree template)) (set-cost (set-cost keyword-set-slots keyword-template))) (<= set-cost (template-cost keyword-template))))
set-updatefunction
(defun set-update (args keyword-writer-map struct) (cond ((atom args) struct) (t `(,(CDR (ASSOC (CAR DEFSTRUCTURE::ARGS) DEFSTRUCTURE::KEYWORD-WRITER-MAP)) ,(CADR DEFSTRUCTURE::ARGS) ,(DEFSTRUCTURE::SET-UPDATE (CDDR DEFSTRUCTURE::ARGS) DEFSTRUCTURE::KEYWORD-WRITER-MAP DEFSTRUCTURE::STRUCT)))))
other
(defloop copy-update-fn (keyword-slot-names args keyword-reader-map struct check) (for ((keyword-slot in keyword-slot-names)) (collect (let ((assigned? (assoc-keyword keyword-slot args))) (if assigned? (if check `(check-vars-not-free (,DEFSTRUCTURE::*BINDING-VARIABLE*) ,(CADR DEFSTRUCTURE::ASSIGNED?)) (cadr assigned?)) `(,(CDR (ASSOC DEFSTRUCTURE::KEYWORD-SLOT DEFSTRUCTURE::KEYWORD-READER-MAP)) ,DEFSTRUCTURE::STRUCT))))))
other
(defloop all-slots-assigned-p (keyword-slot-names args) (for ((keyword-slot in keyword-slot-names)) (always (assoc-keyword keyword-slot args))))
copy-updatefunction
(defun copy-update (name keyword-slot-names args keyword-reader-map struct) "If all slots are assigned (equivalent to a constructor call), or the updated thing is an atom (variable symbol), then we can simply do the copy. Otherwise, bind the struct to a temp and then do the copy." (if (or (atom struct) (all-slots-assigned-p keyword-slot-names args)) `(,DEFSTRUCTURE::NAME ,@(DEFSTRUCTURE::COPY-UPDATE-FN DEFSTRUCTURE::KEYWORD-SLOT-NAMES DEFSTRUCTURE::ARGS DEFSTRUCTURE::KEYWORD-READER-MAP DEFSTRUCTURE::STRUCT NIL)) `(let ((,DEFSTRUCTURE::*BINDING-VARIABLE* ,DEFSTRUCTURE::STRUCT)) (,DEFSTRUCTURE::NAME ,@(DEFSTRUCTURE::COPY-UPDATE-FN DEFSTRUCTURE::KEYWORD-SLOT-NAMES DEFSTRUCTURE::ARGS DEFSTRUCTURE::KEYWORD-READER-MAP DEFSTRUCTURE::*BINDING-VARIABLE* T)))))
inline-update-fnfunction
(defun inline-update-fn (args template tree check) "Write a CONS form to update slots from args, given the structure template and tree." (cond ((atom template) (cond ((null template) (mv nil nil)) (t (let* ((keyword-slot (keywordify template)) (found (assoc-keyword keyword-slot args)) (val (cadr found))) (cond (found (mv t (cond (check `(check-vars-not-free (,DEFSTRUCTURE::*BINDING-VARIABLE*) ,DEFSTRUCTURE::VAL)) (t val)))) (t (mv nil tree))))))) (t (mv-let (car-found car-result) (inline-update-fn args (car template) `(car ,DEFSTRUCTURE::TREE) check) (mv-let (cdr-found cdr-result) (inline-update-fn args (cdr template) `(cdr ,DEFSTRUCTURE::TREE) check) (cond ((not (or car-found cdr-found)) (mv nil tree)) (t (mv t `(cons ,(COND (DEFSTRUCTURE::CAR-FOUND DEFSTRUCTURE::CAR-RESULT) (T `(CAR ,DEFSTRUCTURE::TREE))) ,(COND (DEFSTRUCTURE::CDR-FOUND DEFSTRUCTURE::CDR-RESULT) ((NULL (CDR DEFSTRUCTURE::TEMPLATE)) NIL) (T `(CDR ,DEFSTRUCTURE::TREE))))))))))))
inline-updatefunction
(defun inline-update (args template struct keyword-slot-names) (let ((bind (and (not (atom struct)) (not (all-slots-assigned-p keyword-slot-names args))))) (mv-let (found form) (inline-update-fn args template (if bind *binding-variable* struct) bind) (declare (ignore found)) (cond (bind `(let ((,DEFSTRUCTURE::*BINDING-VARIABLE* ,DEFSTRUCTURE::STRUCT)) ,DEFSTRUCTURE::FORM)) (t form)))))
keyword-updater-fnfunction
(defun keyword-updater-fn (form struct args name keyword-updater keyword-slot-names read-only-keyword-slots update-method template keyword-reader-map keyword-writer-map) (cond ((keyword-slot-checker keyword-updater form args keyword-slot-names)) ((intersection-eq (evens args) read-only-keyword-slots) (bomb-from keyword-updater "The argument list in the macro invocation ~p0 is not ~ valid because it specifies ~#1~[a~/an~] update for the ~ ~#1~[slot~/slots~] ~&1 which ~#1~[is a~/are~] ~ :READ-ONLY ~#1~[slot~/slots~]." form (intersection-eq (evens args) read-only-keyword-slots))) (t (let* ((keyword-set-slots (evens args)) (method (if (eq update-method :heuristic) (if (set-heuristic keyword-set-slots template) :set :copy) update-method))) (case method (:set (set-update args keyword-writer-map struct)) (:copy (copy-update name keyword-slot-names args keyword-reader-map struct)) (:inline (inline-update args template struct keyword-slot-names)) (t (bomb-from 'keyword-updater-fn "Illegal method: ~p0." method)))))))
keyword-updaterfunction
(defun keyword-updater (db) (db-let (keyword-updater name keyword-slot-names slot-names update-method template) (if keyword-updater (list " ; This is the macro that provides for updates of multiple slots of a ; structure. " `(defmacro ,DEFSTRUCTURE::KEYWORD-UPDATER (&whole form struct &rest args) (keyword-updater-fn form struct args ',DEFSTRUCTURE::NAME ',DEFSTRUCTURE::KEYWORD-UPDATER ',DEFSTRUCTURE::KEYWORD-SLOT-NAMES ',(DEFSTRUCTURE::READ-ONLY-KEYWORD-SLOTS DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB) ',DEFSTRUCTURE::UPDATE-METHOD ',DEFSTRUCTURE::TEMPLATE ',(DEFSTRUCTURE::KEYWORD-READER-MAP DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB) ',(DEFSTRUCTURE::KEYWORD-WRITER-MAP DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB)))) nil)))
other
(defloop read-lemma-body (slot-names db) (for ((slot in slot-names)) (collect (db-let ((slot reader) constructor-call) `(equal (,DEFSTRUCTURE::READER ,DEFSTRUCTURE::CONSTRUCTOR-CALL) ,DEFSTRUCTURE::SLOT)))))
read-lemmafunction
(defun read-lemma (db) (db-let (slot-names read-lemma) (if read-lemma (list " ; This lemma simplifies reads of an explicit constructor. " `(defthm ,DEFSTRUCTURE::READ-LEMMA (and ,@(DEFSTRUCTURE::READ-LEMMA-BODY DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB)))) nil)))
other
(defloop write-lemma-body (slot-names db) (for ((slot in slot-names)) (unless (db slot :read-only) (collect (db-let ((slot writer) constructor-call value-variable) `(equal (,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE ,DEFSTRUCTURE::CONSTRUCTOR-CALL) ,(SUBST DEFSTRUCTURE::VALUE-VARIABLE DEFSTRUCTURE::SLOT DEFSTRUCTURE::CONSTRUCTOR-CALL)))))))
write-lemmafunction
(defun write-lemma (db) (db-let (slot-names write-lemma) (if write-lemma (list " ; This lemma simplifies writes of an explicit constructor. " `(defthm ,DEFSTRUCTURE::WRITE-LEMMA (and ,@(DEFSTRUCTURE::WRITE-LEMMA-BODY DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB)))) nil)))
other
(defloop lift-if-writers
(slots test
left
right
db)
(for ((slot in slots))
(when (db slot :writer)
(collect (db-let (value-variable (slot writer))
`(equal (,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
(if ,DEFSTRUCTURE::TEST
,DEFSTRUCTURE::LEFT
,DEFSTRUCTURE::RIGHT))
(if ,DEFSTRUCTURE::TEST
(,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::LEFT)
(,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::RIGHT))))))))
other
(defloop lift-if-readers
(slots test
left
right
db)
(for ((slot in slots))
(collect (db-let ((slot reader))
`(equal (,DEFSTRUCTURE::READER (if ,DEFSTRUCTURE::TEST
,DEFSTRUCTURE::LEFT
,DEFSTRUCTURE::RIGHT))
(if ,DEFSTRUCTURE::TEST
(,DEFSTRUCTURE::READER ,DEFSTRUCTURE::LEFT)
(,DEFSTRUCTURE::READER ,DEFSTRUCTURE::RIGHT)))))))
lift-if-lemma-fnfunction
(defun lift-if-lemma-fn (slots test left right db) (append (lift-if-readers slots test left right db) (lift-if-writers slots test left right db)))
lift-if-lemmafunction
(defun lift-if-lemma (db) (db-let (name lift-if-lemma slot-names) (let ((test (pack-intern name name "-TEST")) (left (pack-intern name name "-LEFT")) (right (pack-intern name name "-RIGHT"))) (if lift-if-lemma (list " ; This lemma lifts IF through calls of the slot accessors. " `(defthm ,DEFSTRUCTURE::LIFT-IF-LEMMA (and ,@(DEFSTRUCTURE::LIFT-IF-LEMMA-FN DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::TEST DEFSTRUCTURE::LEFT DEFSTRUCTURE::RIGHT DEFSTRUCTURE::DB)))) nil))))
elimination-lemmafunction
(defun elimination-lemma (db) (db-let (elimination-lemma slot-names name force weak-predicate-call) (if elimination-lemma (list " ; This is the :ELIM lemma for the constructor. " `(defthm ,DEFSTRUCTURE::ELIMINATION-LEMMA (implies ,(IF DEFSTRUCTURE::FORCE `(DEFSTRUCTURE::FORCE ,DEFSTRUCTURE::WEAK-PREDICATE-CALL) DEFSTRUCTURE::WEAK-PREDICATE-CALL) (equal (,DEFSTRUCTURE::NAME ,@(DEFSTRUCTURE::MAP-SLOTS-DB DEFSTRUCTURE::SLOT-NAMES :READER-CALL DEFSTRUCTURE::DB)) ,DEFSTRUCTURE::NAME)) :rule-classes (:rewrite :elim))) nil)))
other
(defloop weak-predicate-slot-writers-lemma-fn (weak-predicate writer-calls) (for ((call in writer-calls)) (collect `(,DEFSTRUCTURE::WEAK-PREDICATE ,DEFSTRUCTURE::CALL))))
other
(defloop normalization-rhs
(slot-names written-slot
db)
(for ((slot in
slot-names))
(collect (db-let (value-variable (slot reader)
name)
(cond ((eq slot written-slot) value-variable)
(t `(,DEFSTRUCTURE::READER ,DEFSTRUCTURE::NAME)))))))
other
(defloop map-access-assertion-bound-slots
(assertions)
(for ((assertion in
assertions))
(collect (access assertion
assertion
:bound-slots))))
other
(defloop map-subst-assertions
(assertions slot
value-variable)
(for ((assertion in
assertions))
(collect (subst-expr-all assertion
(list value-variable)
(list slot)))))
other
(defloop all-bound-slots-fn (slot-names db) (for ((slot in slot-names)) (append (map-access-assertion-bound-slots (db slot :assertions)))))
all-bound-slotsfunction
(defun all-bound-slots (slot-names db) (append (map-access-assertion-bound-slots (db :assertions)) (all-bound-slots-fn slot-names db)))
simple-slot-pfunction
(defun simple-slot-p (slot db) (db-let ((slot assertions) slot-names) (and (equal (remove-duplicates-equal (map-access-assertion-bound-slots assertions)) (list (list slot))) (not (member slot (flatten (all-bound-slots (remove slot slot-names) db)))))))
other
(defloop predicate-slot-writers-lemma-fn (predicate slot-names all-slot-names db) (for ((slot in slot-names)) (unless (db slot :read-only) (collect (db-let (name predicate-call weak-predicate-call value-variable (slot writer-call)) (if (not (simple-slot-p slot db)) `(implies ,DEFSTRUCTURE::WEAK-PREDICATE-CALL (equal (,DEFSTRUCTURE::PREDICATE ,DEFSTRUCTURE::WRITER-CALL) (,DEFSTRUCTURE::PREDICATE (,DEFSTRUCTURE::NAME ,@(DEFSTRUCTURE::NORMALIZATION-RHS DEFSTRUCTURE::ALL-SLOT-NAMES DEFSTRUCTURE::SLOT DEFSTRUCTURE::DB))))) (let* ((slot-assertions-assertions (map-access-assertion-assertion (db slot :assertions))) (subst-assertions (map-subst-assertions slot-assertions-assertions slot value-variable))) `(implies ,DEFSTRUCTURE::PREDICATE-CALL (iff (,DEFSTRUCTURE::PREDICATE ,DEFSTRUCTURE::WRITER-CALL) ,(IF DEFSTRUCTURE::SUBST-ASSERTIONS (COND ((CDR DEFSTRUCTURE::SUBST-ASSERTIONS) `(AND ,@DEFSTRUCTURE::SUBST-ASSERTIONS)) (T (CAR DEFSTRUCTURE::SUBST-ASSERTIONS))) 'T))))))))))
slot-writers-lemmasfunction
(defun slot-writers-lemmas (db) (db-let (weak-predicate-slot-writers-lemma weak-predicate-call weak-predicate predicate-slot-writers-lemma predicate slot-names) (append (if weak-predicate-slot-writers-lemma (list " ; This lemma backchains the weak predicate through the slot writers. " `(defthm ,DEFSTRUCTURE::WEAK-PREDICATE-SLOT-WRITERS-LEMMA (implies ,DEFSTRUCTURE::WEAK-PREDICATE-CALL (and ,@(DEFSTRUCTURE::WEAK-PREDICATE-SLOT-WRITERS-LEMMA-FN DEFSTRUCTURE::WEAK-PREDICATE (DEFSTRUCTURE::MAP-IF-SLOTS-DB DEFSTRUCTURE::SLOT-NAMES :WRITER-CALL DEFSTRUCTURE::DB)))))) nil) (if predicate-slot-writers-lemma (list " ; This lemma proves the predicate on a slot writer call. For simple slots ; whose assertions (if any) only mention the slot itself one need only prove ; the assertion about the new slot. For more complex slot assertions, or if ; the structure as a whole has an assertion, it is necessary to normalize ; the slot writer call to an explicit instance of the constructor. " `(defthm ,DEFSTRUCTURE::PREDICATE-SLOT-WRITERS-LEMMA (and ,@(DEFSTRUCTURE::PREDICATE-SLOT-WRITERS-LEMMA-FN DEFSTRUCTURE::PREDICATE DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB)))) nil))))
other
(defloop read-write-conjuncts1
(slot-names write-slot
db)
(for ((read-slot in
slot-names))
(collect (db-let (value-variable (read-slot reader)
(write-slot writer)
name)
(cond ((eq read-slot write-slot) `(equal (,DEFSTRUCTURE::READER (,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::NAME))
,DEFSTRUCTURE::VALUE-VARIABLE))
(t `(equal (,DEFSTRUCTURE::READER (,DEFSTRUCTURE::WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::NAME))
(,DEFSTRUCTURE::READER ,DEFSTRUCTURE::NAME))))))))
other
(defloop read-write-conjuncts
(slot-names all-slot-names
db)
(for ((write-slot in
slot-names))
(unless (db write-slot :read-only)
(append (read-write-conjuncts1 all-slot-names
write-slot
db)))))
read-write-lemmafunction
(defun read-write-lemma (db) (db-let (read-write-lemma slot-names) (if read-write-lemma (list " ; This lemma normalizes symbolic reads of symbolic writes by `pushing' ; reads though nested writes until either 1) a symbolic write of the read ; slot is detected, or 2) something unrecognized is found. " `(defthm ,DEFSTRUCTURE::READ-WRITE-LEMMA (and ,@(DEFSTRUCTURE::READ-WRITE-CONJUNCTS DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::SLOT-NAMES DEFSTRUCTURE::DB)))) nil)))
other
(defloop write-write-conjuncts1
(deep-slot template
db)
(for ((shallow-slot in
template))
(unless (db shallow-slot :read-only)
(collect (db-let (value-variable value-variable1
name)
(let ((deep-writer (db deep-slot :writer)) (shallow-writer (db shallow-slot :writer)))
(if (eq deep-slot shallow-slot)
`(equal (,DEFSTRUCTURE::DEEP-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
(,DEFSTRUCTURE::DEEP-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE1
,DEFSTRUCTURE::NAME))
(,DEFSTRUCTURE::DEEP-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::NAME))
`(equal (,DEFSTRUCTURE::DEEP-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
(,DEFSTRUCTURE::SHALLOW-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE1
,DEFSTRUCTURE::NAME))
(,DEFSTRUCTURE::SHALLOW-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE1
(,DEFSTRUCTURE::DEEP-WRITER ,DEFSTRUCTURE::VALUE-VARIABLE
,DEFSTRUCTURE::NAME))))))))))
other
(defloop write-write-conjuncts (template db) (for ((slot in template)) (unless (db slot :read-only) (append (write-write-conjuncts1 slot template db)))))
write-write-lemmafunction
(defun write-write-lemma (db) (db-let (write-write-lemma template tag) (if write-write-lemma (let ((template (reverse (flatten (if tag (cdr template) template))))) (list " ; This lemma normalizes multiple nested writes of a structure by pushing ; writes for `deep' slots through writes to `shallow' slots, and reducing ; redundant writes to the same slot to a single write. " `(defthm ,DEFSTRUCTURE::WRITE-WRITE-LEMMA (and ,@(DEFSTRUCTURE::WRITE-WRITE-CONJUNCTS DEFSTRUCTURE::TEMPLATE DEFSTRUCTURE::DB))))) nil)))
other
(defloop map-rules-for-rule-classes
(rules)
(for ((rule in rules))
(collect (access rule
rule
:rule-class))))
other
(defloop map-assertions-for-rule-classes
(assertions)
(for ((assertion in
assertions))
(append (map-rules-for-rule-classes (access assertion
assertion
:rules)))))
other
(defloop map-slot-assertions-for-rule-classes (slot-names db) (for ((slot in slot-names)) (append (db-let ((slot assertions)) (map-assertions-for-rule-classes assertions)))))
all-rule-classesfunction
(defun all-rule-classes (db) (db-let (assertions slot-names) (append (map-slot-assertions-for-rule-classes slot-names db) (map-assertions-for-rule-classes assertions))))
naked-proofsfunction
(defun naked-proofs (db) (db-let (assertion-lemma predicate predicate-call predicate-guard-hints assertion-lemma-hints guards verify-guards) (if (or assertion-lemma (and guards verify-guards)) (append (list `(local (in-theory (enable ,DEFSTRUCTURE::PREDICATE)))) (and guards verify-guards (list " ; The guard verification for the predicate is performed here since it may ; need the current environment. If it does not prove then you may need some ; hints. Any :PREDICATE-GUARD-HINTS option to DEFSTRUCTURE will be attached ; to this lemma. " `(verify-guards ,DEFSTRUCTURE::PREDICATE ,@(AND DEFSTRUCTURE::PREDICATE-GUARD-HINTS (LIST :HINTS DEFSTRUCTURE::PREDICATE-GUARD-HINTS))))) (and assertion-lemma (list " ; This lemma captures all assertions about the structure. This lemma is not ; guaranteed to prove. If it does not prove than you may have to provide ; some :HINTS. Any :ASSERTION-LEMMA-HINTS option to DEFSTRUCTURE will be ; attached to this lemma. Be sure that you have not specified ; unsatisfiable assertions. " `(defthm ,DEFSTRUCTURE::ASSERTION-LEMMA (implies ,DEFSTRUCTURE::PREDICATE-CALL ,(DEFSTRUCTURE::PREDICATE-BODY DEFSTRUCTURE::DB)) :rule-classes ,(DEFSTRUCTURE::ALL-RULE-CLASSES DEFSTRUCTURE::DB) ,@(AND DEFSTRUCTURE::ASSERTION-LEMMA-HINTS (LIST :HINTS DEFSTRUCTURE::ASSERTION-LEMMA-HINTS)))))) nil)))
mv-intro-macro-case-bodyfunction
(defun mv-intro-macro-case-body (readers form n) (cond ((atom readers) nil) (t (cons `(,DEFSTRUCTURE::N (,(CAR DEFSTRUCTURE::READERS) ,DEFSTRUCTURE::FORM)) (mv-intro-macro-case-body (cdr readers) form (1+ n))))))
mv-intro-macro-fnfunction
(defun mv-intro-macro-fn (name form event-name readers) (let* ((event-name (if event-name event-name (pack-intern (car form) name "-MV-INTRO-" (car form)))) (n (car (unique-symbols 1 'mv-intro-macro-n (flatten form)))) (mv-nth-form `(mv-nth ,DEFSTRUCTURE::N ,DEFSTRUCTURE::FORM))) `(defthm ,DEFSTRUCTURE::EVENT-NAME (equal ,DEFSTRUCTURE::MV-NTH-FORM (case ,DEFSTRUCTURE::N ,@(DEFSTRUCTURE::MV-INTRO-MACRO-CASE-BODY DEFSTRUCTURE::READERS DEFSTRUCTURE::FORM 0) (t (hide ,DEFSTRUCTURE::MV-NTH-FORM)))) :hints (("Goal" :in-theory '(zp open-mv-nth ,@DEFSTRUCTURE::READERS) :expand (hide ,DEFSTRUCTURE::MV-NTH-FORM))))))
mv-intro-macrofunction
(defun mv-intro-macro (db) (db-let (name slot-names mv-intro-macro) (if mv-intro-macro (list " ; This macro generates a lemma that will rewrite MV-NTH applied to any form ; as a call of the appropriate reader for this MV structure. " `(defmacro ,DEFSTRUCTURE::MV-INTRO-MACRO (form &key event-name) (declare (xargs :guard (and form (symbol-listp form) (symbolp event-name)))) (mv-intro-macro-fn ',DEFSTRUCTURE::NAME form event-name ',(DEFSTRUCTURE::MAP-SLOTS-DB DEFSTRUCTURE::SLOT-NAMES :READER DEFSTRUCTURE::DB)))) nil)))
definition-theoryfunction
(defun definition-theory (db) (db-let (name weak-predicate predicate definition-theory slot-names representation inline) (if inline nil (list " ; This theory consists of all :DEFINITION runes associated with the ; constructor, predicates, and slot readers/writers. Only the ; :TYPE-PRESCRIPTIONS and :EXECUTABLE-COUNTERPARTS remain ENABLEd. " `(deftheory ,DEFSTRUCTURE::DEFINITION-THEORY '(,@(IF (EQ DEFSTRUCTURE::REPRESENTATION :MV) NIL (LIST DEFSTRUCTURE::NAME)) ,DEFSTRUCTURE::WEAK-PREDICATE ,DEFSTRUCTURE::PREDICATE ,@(DEFSTRUCTURE::MAP-IF-SLOTS-DB DEFSTRUCTURE::SLOT-NAMES :READER DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::MAP-IF-SLOTS-DB DEFSTRUCTURE::SLOT-NAMES :WRITER DEFSTRUCTURE::DB))) `(in-theory (disable ,DEFSTRUCTURE::DEFINITION-THEORY))))))
other
(defloop lemma-theory-names (lemma-names db) (for ((lemma-key in lemma-names)) (append (let ((lemma-name (db-fn lemma-key `(lemma-theory ,DEFSTRUCTURE::LEMMA-KEY) db))) (if lemma-name (list lemma-name) nil)))))
lemma-theoryfunction
(defun lemma-theory (db) (db-let (lemma-theory inline) (if inline nil (list " ; This theory lists every lemma generated by this DEFSTRUCTURE. These are ; normally to remain ENABLEd. " `(deftheory ,DEFSTRUCTURE::LEMMA-THEORY '(,@(DEFSTRUCTURE::LEMMA-THEORY-NAMES DEFSTRUCTURE::*LEMMA-NAMES* DEFSTRUCTURE::DB)))))))
other
(defconst *update-methods* '(:heuristic :set :copy))
other
(defconst *keyword-representations* '(:list :mv :dotted-list :tree))
other
(defconst *options* '(:assert :assertion-lemma-hints :conc-name :do-not :force :guards :mv-intro-macro :keyword-constructor :keyword-updater :predicate :predicate-guard-hints :prefix :inline :read-write-lemma :representation :set-conc-name :slot-writers :weak-predicate :update-method :verify-guards :write-write-lemma))
other
(defconst *duplicate-options* '(:assert :do-not))
other
(defconst *do-not-options* '(:tag :read-write :write-write))
other
(defconst *slot-options* '(:default :read-only :assert))
other
(defconst *duplicate-slot-options* '(:assert))
other
(defconst *rule-tokens* '(:built-in-clause :compound-recognizer :congruence :definition :elim :equivalence :forward-chaining :generalize :induction :linear :linear-alias :meta nil :refinement :rewrite :type-prescription :type-set-inverter :well-founded-relation))
check-assertionfunction
(defun check-assertion (assertion slot context db) "Check the assertion for syntax, and return an ASSERTION record containing the assertion, its bound slots, its substitution, and its associated slot." (db-let (slot-names) (cond ((not (assertion-termp assertion)) (bomb "Assertions are required to satisfy DEFSTRUCTURE::ASSERTION-TERMP, ~ and ~p0 does not because ~@1." assertion (reason-for-not-assertion-termp assertion))) (t (let* ((bound-slots (free-vars assertion)) (err (cond ((not (subsetp bound-slots slot-names)) (msg "is not a subset of the slot names ~p0." slot-names)) ((and slot (not (member slot bound-slots))) (msg "does not contain the current slot ~p0." slot))))) (if err (bomb "The putative assertion ~p0 in the context ~p1 is not ~ a valid assertion because the free variable list of the ~ assertion (as defined by DEFSTRUCTURE::FREE-VARS), ~p2, ~ ~@3 If you feel that this message is incorrect, ~ then restate your assertion as a LAMBDA function ~ and try again." assertion context bound-slots err) (make assertion :assertion assertion :bound-slots bound-slots :subst-assertion (subst-expr-all assertion (map-slots-db bound-slots :reader-call db) bound-slots) :slot slot :rules nil)))))))
parse-rulefunction
(defun parse-rule (rule default-assertion context slot db) "Check rule syntax and return a RULE record." (let ((rule-token (if (atom rule) rule (car rule)))) (if (or (not (symbolp rule-token)) (not (member rule-token *rule-tokens*))) (bomb "The putative rule descriptor ~p0 in the context ~ ~p1 is not valid because ~#2~[it~/its CAR~] ~ is not one of the allowable rule tokens ~v3." rule context (if (equal rule rule-token) 0 1) *rule-tokens*) (cond ((or (atom rule) (null (cdr rule))) (make rule :assertion default-assertion :rule-class `(,DEFSTRUCTURE::RULE-TOKEN :corollary ,(DEFSTRUCTURE::MAKE-COROLLARY DEFSTRUCTURE::DEFAULT-ASSERTION DEFSTRUCTURE::DB)))) ((not (true-listp rule)) (bomb "The putative atomic rule descriptor ~p0 in the context ~ ~p1 is not valid because it is not a true list." rule context)) (t (let ((assertion (check-assertion (second rule) slot rule db))) (make rule :assertion assertion :rule-class (append `(,DEFSTRUCTURE::RULE-TOKEN :corollary ,(DEFSTRUCTURE::MAKE-COROLLARY DEFSTRUCTURE::ASSERTION DEFSTRUCTURE::DB)) (rest (rest rule))))))))))
other
(defloop parse-rule-list
(rule-list default-assertion
context
slot
db)
(for ((rule in
rule-list))
(collect (parse-rule rule
default-assertion
context
slot
db))))
other
(defloop parse-assert-options
(assert-options slot
db)
"Traverse the assert-options (which *only* consist of :ASSERT options),
and check the syntax and collect a list of ASSERTION records."
(for ((option in
assert-options))
(collect (if (or (atom option)
(atom (rest option))
(not (true-listp option)))
(bomb "The :ASSERT option ~p0 needs an assertion and optional ~
rule-descriptors, or it is not a true list.")
(let* ((assertion (check-assertion (second option)
slot
option
db)) (rule-list (parse-rule-list (rest (rest option))
assertion
option
slot
db)))
(change assertion
assertion
:rules rule-list))))))
other
(defloop parse-slot-options (slots db) "We know that the slot is either a valid symbol, or a CONS whose CAR is a valid symbol. Check all of the rest of the syntax and return an extension to be APPENDed to the DB." (for ((slot-and-options in slots)) (append (let* ((slot-name (if (symbolp slot-and-options) slot-and-options (car slot-and-options))) (options (if (symbolp slot-and-options) nil (cdr slot-and-options)))) (acons-up ((cons slot-name :read-only) (get-option-as-flag 'defstructure :read-only options)) ((cons slot-name :default-specified) (get-option-entry :default options)) ((cons slot-name :default) (get-option-argument 'defstructure :default options :form nil nil)) ((cons slot-name :assertions) (parse-assert-options (get-option-entries :assert options) slot-name db)))))))
get-string-designatorfunction
(defun get-string-designator (key options default) (designated-string (get-option-argument 'defstructure key options :string-designator default default)))
get-symbolfunction
(defun get-symbol (key options default) (get-option-argument 'defstructure key options :symbol default default))
other
(defloop parse-do-not-options (do-not-options) "We allow any number of :DO-NOT options. We return an alist to append to the DB that resets the defaults." (for ((options on do-not-options)) (append (let ((do-nots (get-option-subset 'defstructure :do-not options *do-not-options* nil))) (pairlis$ do-nots (make-list (length do-nots) :initial-element nil))))))
get-representationfunction
(defun get-representation (options slot-names) "The :REPRESENTATION has a special syntax." (let ((opt (get-option-entry :representation options)) (default :list)) (cond (opt (cond ((consp opt) (cond ((null (cdr opt)) default) (t (if (and (true-listp opt) (null (cddr opt)) (or (member (cadr opt) *keyword-representations*) (let ((l (flatten (cadr opt)))) (and (subsetp l slot-names) (subsetp slot-names l) (equal (length l) (length slot-names)))))) (cadr opt) (bomb "The :REPRESENTATION option descriptor must be either ~ :REPRESENTATION, (:REPRESENTATION), ~ or (:REPRESENTATION representation), where ~ representation is either one of ~v0, or a CONS ~ tree which when flattened according to ~ DEFSTRUCTURE::FLATTEN yields a permutation of the ~ slot names ~p1, but ~p2 is not." *keyword-representations* slot-names opt))))) (t default))) (t default))))
parse-defstructurefunction
(defun parse-defstructure (name doc-and-slots) "Parse the DEFSTRUCTURE arguments, returning the DB" (let* ((name (if (and name (symbolp name)) name (bomb "The <name> argument of DEFSTRUCTURE must be a ~ non-NIL symbol, but ~p0 is not." name))) (doc (if (stringp (car doc-and-slots)) (car doc-and-slots) nil)) (slots-and-options (if doc (cdr doc-and-slots) doc-and-slots)) (last-car (car (last slots-and-options))) (options? (and (consp last-car) (eq (car last-car) :options))) (options (if options? (cdr last-car) nil)) (slots (if options? (butlast slots-and-options 1) slots-and-options)) (slot-names (map-x-or-car-x slots))) (extend-db nil (acons-db (:name name) (:doc doc) (:slot-names slot-names) (:guards (get-option-as-flag 'defstructure :guards options)) (:verify-guards (get-option-member 'defstructure :verify-guards options '(t nil) :default :default)) (:inline (get-option-as-flag 'defstructure :inline options)) (:conc-name (get-string-designator :conc-name options (concatenate 'string (string name) "-"))) (:set-conc-name (get-string-designator :set-conc-name options (concatenate 'string "SET-" (string name) "-"))) (:keyword-constructor (get-symbol :keyword-constructor options (pack-intern name "MAKE-" name))) (:keyword-updater (get-symbol :keyword-updater options (pack-intern name "UPDATE-" name))) (:predicate (get-symbol :predicate options (pack-intern name name "-P"))) (:weak-predicate (get-symbol :weak-predicate options (pack-intern name "WEAK-" name "-P"))) (:force (get-option-as-flag 'defstructure :force options)) (:representation (get-representation options slot-names)) (:read-only (let ((slot-writers (get-option-as-flag 'defstructure :slot-writers options))) (cond ((and slot-writers (eq (db :representation) :mv)) (bomb ":MV structures can't have :SLOT-WRITERS.")) (t (not slot-writers))))) (:mv-intro-macro (if (eq (db :representation) :mv) (get-symbol :mv-intro-macro options (pack-intern name name "-INTRO")) (let ((entry (get-option-entry :mv-intro-macro options))) (if (and entry (or (atom entry) (atom (cdr entry)) (cadr entry))) (bomb "The :MV-INTRO-MACRO option is illegal unless the ~ (:REPRESENTATION :MV) option is chosen.") nil)))) (:update-method (let* ((default (if (db :read-only) :copy :heuristic)) (method (get-option-member 'defstructure :update-method options *update-methods* default default))) (if (and (db :read-only) (not (eq method :copy))) (bomb "The only valid :UPDATE-METHOD for structures without ~ :SLOT-WRITERS is :COPY.") (if (db :inline) :inline method)))) (:assertion-lemma-hints (get-option-argument 'defstructure :assertion-lemma-hints options :form nil nil)) (:predicate-guard-hints (get-option-argument 'defstructure :predicate-guard-hints options :form nil nil)) (:prefix (get-string-designator :prefix options "DEFS-")) (:tag name) (:read-write t) (:write-write t)) (append-db (parse-do-not-options (get-option-entries :do-not options))) (acons-db (:value-variable (car (unique-symbols 2 (pack-intern name "VALUE") (cons name slot-names)))) (:value-variable1 (cadr (unique-symbols 2 (pack-intern name "VALUE") (cons name slot-names)))) (:predicate-call `(,(DEFSTRUCTURE::DB :PREDICATE) ,DEFSTRUCTURE::NAME))) (append-db (reader-names slot-names db) (reader-calls slot-names db)) (acons-db (:assertions (parse-assert-options (get-option-entries :assert options) nil db))) (append-db (parse-slot-options slots db)))))
other
(defloop nullify-lemmas
(lemma-names)
(for ((lemma in
lemma-names))
(collect (cons lemma nil))))
prepare-for-code-genfunction
(defun prepare-for-code-gen (db) (db-let (slot-names representation name predicate read-only tag read-write write-write weak-predicate inline set-conc-name) (cond ((and (eq representation :mv) (< (len slot-names) 2) (bomb "An :MV structure must have at least 2 slots in order ~ to be valid according to the syntax of Acl2, but ~ the current structure has ~#0~[one slot~/no slots~]." slot-names))) ((not weak-predicate) (bomb "You have apparently tried to suppress the generation of the weak predicate on the structure, which is currently illegal.")) ((not predicate) (bomb "You have apparently tried to suppress the generation of the predicate on the structure, which is currently illegal.")) (t (extend-db (acons-db (:keyword-slot-names (keywordify-list slot-names)) (:required-slot-names (required-slot-names slot-names db)) (:read-only (or read-only (equal (read-only-keyword-slots slot-names db) (db :keyword-slot-names)) (eq representation :mv))) (:tag (if (eq representation :mv) nil tag)) (:template (make-template db))) (db-let (read-only keyword-updater) (extend-db (acons-db (:constructor-call `(,DEFSTRUCTURE::NAME ,@DEFSTRUCTURE::SLOT-NAMES)) (:acl2-count-lemma (if (eq representation :mv) nil (make-prefix-name "ACL2-COUNT-" name))) (:weak-predicate-call `(,DEFSTRUCTURE::WEAK-PREDICATE ,DEFSTRUCTURE::NAME)) (:weak-predicate-constructor-lemma (make-prefix-name weak-predicate "-" name)) (:predicate-weak-predicate-lemma (make-prefix-name predicate "-INCLUDES-" weak-predicate)) (:predicate-constructor-lemma (make-prefix-name predicate "-" name)) (:keyword-updater (if (or (eq representation :mv) (not slot-names)) nil keyword-updater)) (:read-lemma (if slot-names (make-prefix-name "READ-" name) nil)) (:write-lemma (if (or read-only (not slot-names)) nil (make-prefix-name "WRITE-" name))) (:lift-if-lemma (if slot-names (make-prefix-name name "-LIFT-IF") nil)) (:elimination-lemma (if (or (eq representation :mv) (not slot-names)) nil (make-prefix-name "ELIMINATE-" name))) (:weak-predicate-slot-writers-lemma (if (and slot-names (not read-only)) (make-prefix-name weak-predicate "-" set-conc-name) nil)) (:predicate-slot-writers-lemma (if (and slot-names (not read-only)) (make-prefix-name predicate "-" set-conc-name) nil)) (:read-write-lemma (if (and read-write (not read-only) slot-names) (make-prefix-name "READ-WRITE-" name) nil)) (:write-write-lemma (if (and write-write (not read-only) slot-names) (make-prefix-name "WRITE-WRITE-" name) nil)) (:assertion-lemma (if (and predicate (all-rule-classes db)) (make-prefix-name name "-ASSERTIONS") nil)) (:definition-theory (make-prefix-name name "-DEFINITION-THEORY")) (:lemma-theory (make-prefix-name name "-LEMMA-THEORY"))) (append-db (writer-names slot-names db) (writer-calls slot-names db) (if inline (nullify-lemmas *lemma-names*) nil)))))))))
capsulemacro
(defmacro capsule (&rest args) "Remove documentation strings and recast as an ENCAPSULATE." `(encapsulate nil ,@(DEFSTRUCTURE::REMOVE-STRINGS DEFSTRUCTURE::ARGS)))
other
(encapsulate nil (logic) (deftheory minimal-theory-for-defstructure (append *expandable-boot-strap-non-rec-fns* (list-all *built-in-executable-counterparts*) '(iff car-cons cdr-cons car-cdr-elim eqlablep mv-nth zp true-listp open-mv-nth o< acl2-count (:type-prescription acl2-count) integer-abs))))
defstructuremacro
(defmacro defstructure (name &rest doc-and-slots) (let ((db (prepare-for-code-gen (parse-defstructure name doc-and-slots)))) (db-let (inline guards) `(progn (capsule " ; We define the structure and all of the events (except the assertion theory) ; in the absoulte minimum theory possible in order to expedite the proofs ; and guarantee that they will always work. If you ever find a case where ; one of these proof fails (except due to user syntax errors) please ; report it as a bug in DEFSTRUCTURE. " (local (in-theory (theory 'minimal-theory-for-defstructure))) ,@(DEFSTRUCTURE::CONSTRUCTOR DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::WEAK-PREDICATE DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::READERS DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::WRITERS DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::PREDICATE DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::KEYWORD-CONSTRUCTOR DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::KEYWORD-UPDATER DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::SLOT-WRITERS-LEMMAS DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::READ-WRITE-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::WRITE-WRITE-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::READ-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::WRITE-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::LIFT-IF-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::ELIMINATION-LEMMA DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::MV-INTRO-MACRO DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::DEFINITION-THEORY DEFSTRUCTURE::DB)) ,@(IF (AND INLINE (NOT DEFSTRUCTURE::GUARDS)) NIL (LIST `(DEFSTRUCTURE::CAPSULE ,@(DEFSTRUCTURE::NAKED-PROOFS DEFSTRUCTURE::DB) ,@(DEFSTRUCTURE::LEMMA-THEORY DEFSTRUCTURE::DB))))))))