ACL2s-query
Run a multiple-value ACL2 computation from Common Lisp
General form
(acl2s-query
form ; The form to evaluate. Should evaluate to an error triple.
:quiet <bool> ; Optional. Whether or not to suppress all ACL2 printed output. Defaults to nil.
:capture-output <bool> ; Optional. Whether or not to capture all ACL2 printed output. Defaults to nil.
:prover-step-limit <integer> ; Optional. Sets the prover step limit. Defaults to what ACL2 would have used
; for a top-level evaluation (see set-prover-step-limit).
...) ; Any additional arguments will be passed to ld, except for :ld-error-action
=>
(list erp val)
- Returns
- erp is the first value of the error triple that form evaluated to, or nil if an error occurred while evaluating form.
- val is the second value of the error triple that form evaluated to.
The form argument should be an ACL2 expression that evaluates to an ACL2::error-triple. form should also not change the state of the ACL2 world with respect to events. Be careful about symbol packages when using acl2s-query when inside a different package - you may need to fully specify the name of an ACL2 function when calling it. See ACL2s-interface-symbol-package-tips for more information.
When the :quiet option is set to t, acl2s-query will attempt to suppress all ACL2 printed output during evaluation of form. This temporarily overrides the current quiet-mode.
When the :capture-output option is set to t, acl2s-query will attempt capture all ACL2 printed output during evaluation of form. This temporarily overrides the current capture-output.
acl2s-query evaluates form inside of a ACL2::with-prover-step-limit, where the step-limit is set to the value provided to :prover-step-limit, or ACL2's set prover-step-limit if that option is not provided. See ACL2::set-prover-step-limit for more information about the prover step-limit. If you don't want to limit the number of prover steps permitted for an event, set :prover-step-limit to nil.
Examples
(acl2s-query '(value (+ 1 2)))
Returns (nil 3)
(acl2s-query '(thm (implies (natp x) (integerp x))))
Returns (nil :invisible)
(acl2s-query '(mv nil t state))
Returns (nil t)
(acl2s-query '(value (+ 1 2)) :quiet nil :ld-pre-eval-print t)
Returns (nil 3), does not attempt to suppress any ACL2 printed output, and passes
:ld-pre-eval-print t to
ACL2::ld
(acl2s-query '(trans-eval '(+ 1 2) 'my-ctx state nil))
Returns (nil ((nil) . 3)). See
ACL2::trans-eval for more information
about trans-eval's return value.
(acl2s-query '(test? (implies (integerp x) (natp x))))
Returns (t nil)
