|
|
|---|
|
|
|
|---|
Translate to ACL2 and Syntheto top-level construct or a list of them.
This is the entry point of the translation from Syntheto to ACL2. The argument is evaluated, and it must evaluate to a Syntheto top-level construct or to a list of them; this is checked by the function called by this macro. The function returns events that are submitted to ACL2 by this macro. The events update the translation state table and generate ACL2 counterparts of the Syntheto construct(s).
Macro:
(defmacro process-syntheto-toplevel (top/tops) (cons 'make-event (cons (cons 'process-syntheto-toplevel-fn (cons top/tops '(state))) 'nil)))