|
|
|---|
|
|
|
|---|
A user-level function to extract guards from a definition body.
This function takes a definition body, that is, a list of forms valid as the body of a DEFUN, and returns a guard for the DEFUN that consists of all guards specified either by (DECLARE (XARGS ... :GUARD g ...)) or (DECLARE (TYPE ...)) forms in body. This function is designed to be used by macros that create function definitions and lemmas that may depend on the guards of the newly defined function. The guard will be returned as a conjunction: either T, NIL (?) a single conjunct, or (AND . conjuncts) where conjuncts is a list of the conjuncts.
Restrictions on the form of macros in Acl2 make it impossible for a macro to query the ACL2 database to determine any property of a function, including its guards. Therefore we provide this function which parses function bodies and extracts the guards from the source text of a function.
This is a `fail-safe' procedure. If any syntax errors are encountered during guard parsing, those illegal guard specifications are simply ignored, under the assumption that when the function is finally submitted to Acl2 that Acl2's more powerful error checking facilities will uncover and report the errors to the user. Thus this routine may return garbage, but it shouldn't crash!
Function:
(defun get-guards-from-body (body) (untranslate (conjoin (get-guards-from-body1 body)) nil nil))