|
|
|---|
|
|
|
|---|
Define a new alist type, and a theory of the alist type.
Examples:(defalist symbol-to-integer-alistp (l) "Recognizes an alist mapping symbols to integers." (symbolp . integerp)) (defalist symbol-to-bnatural-alistp (l lub) "Recognizes an alists mapping symbols to naturals bounded by lub." (symbolp . (lambda (x) (bnaturalp x lub)))) (defalist symbol-alistp (l) "Define an alist theory alists from an unspecified domain type to symbols." ((lambda (x) t) . symbolp) (:options :omit-defun (:range-type symbol-listp))) (defalist string-to-integer-alistp (l) "Recognizes an alist mapping strings to integers. Produce a minimal theory, and store the BINDING-EQUAL lemma as a :TYPE-PRESCRIPTION." (stringp . integerp) (:options (:theory nth put) (:binding-equal-rule-classes :type-prescription) (:domain-type string-listp) (:range-type integer-listp)))
Syntax:
DEFALIST name arglist [documentation] {declaration}* type-pair [option-list]
option-list ::= (:OPTIONS <<!options>>)
options ::= !binding-equal-rule-classes-option |
!omit-defun-option |
!theory-option |
!domain-type-option |
!range-type-option |
!theory-name-option
theory-option ::= (:THEORY <<!alist-functions>>)
theory-name-option ::= (:THEORY-NAME theory-name)
alist-functions ::= acons | alistp | all-bindings-equal| all-bound?-equal | append |
assoc-equal | bind-all-equal | bind-equal | bind-pairs-equal |
binding-equal | bound?-equal | collect-bound-equal | domain |
domain-restrict-equal | pairlis$ | range | rembind-all-equal |
rembind-equal
binding-equal-rule-classes-option ::= (:BINDING-EQUAL-RULE-CLASSES rule-classes)
omit-defun-option ::= :OMIT-DEFUN
Arguments and Values:
arglist -- an argument list satisfying ACL2::ARGLISTP, and containing exactly one symbol whose `print-name' is "L". declaration -- any valid declaration. documentation -- a string; not evaluated. name -- a symbol. theory-name -- any symbol that is a legal name for a deftheory event. type-pair -- A pair (d . r) where d and r are either a function symbol or a one argument LAMBDA function or the constant T. d designates a predicate to be applied to each element of the domain of the alist, and r designates a predicate to be applied to each element of the range of the alist. T means no type restriction. rule-classes -- any form legal as an argument to the :RULE-CLASSES keyword of DEFTHM. Acl2-theory-expression -- Any legal Acl2 theory expression
DEFALIST defines a recognizer for association lists whose pairs map keys of a given type to values of a given type, and by default creates an extensive theory for alists of the newly defined type.
To define an alist type with DEFALIST you must supply a name for the alist recognizer, an argument list for the recognizer, and predicate designator for elements of the alist's range. The name may be any symbol. The argument list must be valid as a functional argument list, and must contain exactly one symbol whose `print-name'is "L". By convention this is the alist argument recognized by the function defined by DEFALIST.
The type of the domain and range of the alist is given by a pair (d . r) where d identifies the type of an element of the alist's domain, and r specifies the type of an element of the alist's range. Either of these may be specified by a symbol which names a one-argument function (or macro) which tests the elements of the domain and range of L. Either of d and r may also be specified as a single-argument LAMBDA function. Finally, either of d and r may be specified as the constant t, indicating no type constraint.
Any number of other arguments to the alist functions may be supplied, but only the L argument will change in the recursive structure of the recognizer.
Note that DEFALIST does not create any guards for L or any other argument. Guards may be specified in the usual way since any number of DECLARE forms may preceed the predicate specification in the DEFALIST form. Bear in mind that if you are defining a function to be used as a guard, then you are advised to consider what impact guarding the arguments of the function may have on its utility. In general the most useful guard functions are those that are guard-free.
By default, DEFALIST creates an extensive theory for the recognized alists. This theory contains appropriate lemmas for all of the alist functions appearing in the `alist-functions' syntax description above. One can select a subset of this theory to be generated by using the :THEORY option (see below). DEFALIST always creates a :FORWARD-CHAINING rule from the recognizer to ALISTP.
DEFALIST also creates a DEFTHEORY event that lists all of the lemmas created by the DEFALIST. The name of the theory is formed by concatenating the function name and the string "-THEORY", and INTERNing the resulting string in the package of the function name.
DEFALIST options are specified with a special :OPTIONS list systax. If present, the :OPTIONS list must appear as the last form in the body of the DEFALIST.