Guard-obligation
The guard proof obligation
See verify-guards, and see guard for a discussion of
guards. Guard-obligation is a low-level function for use in system
programs, not typically appropriate for most ACL2 users. A corresponding
user-level utility is verify-guards-formula; also see guard-formula-utilities for related utilities.
Example Forms:
(guard-obligation 'foo nil t t 'top-level state)
(guard-obligation '(if (consp x) (foo (car x)) t) nil nil t 'my-fn state)
General Forms:
(guard-obligation name rrp guard-debug guard-simplify ctx state)
(guard-obligation term rrp guard-debug guard-simplify ctx state)
where the first argument is either the name of a function or theorem or is
a non-variable term that may be in untranslated form; rrp (``return
redundant p'') is non-nil when it is permissible to return a value of
'redundant in the first (name) case (and is irrelevant in the term case);
guard-debug is typically nil but may be t (see guard-debug); guard-simplify is typically t but may be
:limited (see verify-guards); ctx is a context (typically, a
symbol used in error and warning messages); and state references the
ACL2 state.
If you want to obtain the formula but you don't care about the so-called
``tag tree'':
(mv-let (erp val)
(guard-obligation x nil guard-debug guard-simplify 'top-level state)
(if erp
( .. code for handling error case, e.g., name is undefined .. )
(let ((cl-set (cadr val))) ; to be proved for guard verification
( .. code using cl-set, which is a list of clauses,
implicitly conjoined, each of which is viewed as
a disjunction .. ))))
The form (guard-obligation x rrp guard-debug guard-simplify ctx state)
evaluates to a pair (mv erp val), where erp is nil unless there
is an error. (Actually, this is a context-message pair; see the source code's
``Essay on Context-message Pairs''for relevant information.) Suppose erp
is nil. Then val is the keyword :redundant if the
corresponding verify-guards event would be redundant and rrp is
not nil; see redundant-events. Otherwise, val is a tuple
(list* names cl-set ttree), where: names is (cons :term xt) if
x is not a variable, where xt is the translated form of x; and
otherwise is a list containing x along with, if x is defined in a
mutual-recursion, any other functions defined in the same mutual-recursion nest; cl-set is a list of lists of terms, viewed as a
conjunction of clauses (each viewed (as a disjunction); and ttree
is an assumption-free tag-tree that justifies cl-set. (The notion of
``tag-tree'' may probably be ignored except for system developers.)
Guard-obligation is typically used for function names or non-variable
terms, but as for verify-guards, it may also be applied to theorem
names.
See the source code for verify-guards-formula for an example of how
to use guard-obligation.
