|
|
|---|
|
|
|
|---|
Define and characterize a general purpose record structure with typed slots.
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 ACL2 home page.
Examples:
(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)))
Syntax:
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)
Arguments and Values:
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.
Definitions:
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.