ACL2s-event
Install an ACL2 event from Common Lisp
General form
(acl2s-event
form ; The form to evaluate. Should return 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 ; Optional. Sets the prover step limit. Defaults to what ACL2 would have used
; for a top-level evaluation (see acl2::set-prover-step-limit).
...) ; Any additional arguments will be passed to ld, except for :ld-error-action.
=>
(list erp nil)
- Returns
- erp is `nil` if ld indicates that the form was successfully evaluated.
The form argument should be an ACL2 expression that evaluates to an ACL2::error-triple. Be careful about symbol packages when using acl2s-event 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-event 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-event will attempt capture all ACL2 printed output during evaluation of form. This temporarily overrides the current capture-output.
acl2s-event 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-event '(definec f (x :int) :int (* x x)))
Returns (nil nil), and defines the function
f in the ACL2 world.
(acl2s-event '(definec g (x :int) :int (* 5 x)) :quiet t)
Returns (nil nil), and defines the function
g in the ACL2 world. Tries to suppresses all ACL2 printed output during this process.
(acl2s-event '(defthm triangle-inequality
(implies (and (natp x) (natp y))
(>= (+ (abs x) (abs y)) (abs (+ x y)))))
:prover-step-limit 200)
Returns (t nil), indicating that the
defthm did not successfully execute. This is because the
defthm was limited to 200 prover steps, and more prover steps than that are required to prove it.
(acl2s-event '(defthm triangle-inequality
(implies (and (natp x) (natp y))
(>= (+ (abs x) (abs y)) (abs (+ x y)))))
:prover-step-limit 1000)
Returns (nil nil), and defines the theorem
triangle-inequality in the ACL2 world. It limits the
defthm call to 1000 prover steps.
