ACL2s-compute
Run a single-value ACL2 computation from Common Lisp
General form
(acl2s-compute
form ; The form to evaluate. Should return a single value.
: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.
...) ;; Any additional arguments will be passed to ld, except for :ld-error-action
=>
(list erp val)
- Returns
- erp is t if an error occurred during execution of form, and is nil otherwise.
- val is the single value that form evaluated to.
The form argument should be an ACL2 expression that evaluates to a single value. Be careful about symbol packages when using acl2s-compute 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-compute 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-compute will attempt capture all ACL2 printed output during evaluation of form. This temporarily overrides the current capture-output.
Examples
(acl2s-compute '(+ 1 2))
Returns (nil 3)
(acl2s-compute '(+ 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-compute '(append '(1 2) '(3 4)))
Returns (nil (1 2 3 4))
(acl2s-compute '(+ 1 '(1 2)))
Returns (t nil) and prints out a guard violation error message
(acl2s-compute '(mv nil t state))
