		Search-engine friendly clone of the ACL2 documentation.

Defdata-attach

Attach/modify metadata for a defdata type

Examples:

(defdata-attach pos :enumerator nth-small-pos-testing)

(defdata-attach imem :enum/acc imem-custom-enum2)

General Form:

(defdata-attach typename 
     [:enum/test enum-fn]
     [:equiv eq-rel]
     [:equiv-fixer eq-fix-fn]
     [:constraint ... ]
     [:sampling constant-list]
     [overridable metadata]
     )

Defdata-attach can be used to attach custom test enumerators for certain types. This provides a method to customize Cgen's test data generation capability for certain scenarios.

(Advanced) Type refinement : User can attach rules that specify (to Cgen) how to refine/expand a variable of this type when certain additional constraints match (or subterm-match). For those who are familar with dest-elim rules, the :rule field has a similar form. For example:

(defdata-attach imemory
         :constraint (mget a x) ;x is the variable of this type
         :constraint-variable x
         :rule (implies (and (natp a) ;additional hyps
                             (instp x.a)
                             (imemoryp x1))
                        (equal x (mset a x.a x1))) ;refine/expand
         :meta-precondition (or (variablep a)
                                (fquotep a))
         :match-type :subterm-match)

Warning: Other optional keyword arguments are currently unsupported and the use of :override-ok can be unsound.