		Search-engine friendly clone of the ACL2 documentation.

Syntheto

Process-syntheto-toplevel-fn

Translate a Syntheto top-level construct, or a list of them, into corresponding ACL2 events and execute them, returning a list of outcomes.

Signature
(process-syntheto-toplevel-fn top/tops state) → (mv * * state)

This is the entry point for the translation from Syntheto to ACL2 and processing in ACL2.

We ensure that the input is a top-level construct or a list of them.

We retrieve the existing (i.e. old) top-level constructs from the current translation state. We wrap them into a context and we check that the input satisfies the static semantics (this wrapping is a bit awkward, and we will eliminate it after we make some planned improvements to the static semantics). If the static semantic checks succeed, we generate an event to extend the translation state with the input.

This is just a start: there is, of course, much more to do here. In particular, we need to generate ACL2 events corresponding to the input Syntheto top-level constructs. We are also curently ignoring the type obligations generated by the static semantics checks: these should be turned into ACL2 theorems, and used to generate proofs for the other events (e.g. guard proofs for function definitions).

Definitions and Theorems

Function: process-syntheto-toplevel-fn

(defun process-syntheto-toplevel-fn (top/tops state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'process-syntheto-toplevel-fn))
  (declare (ignorable __function__))
  (b*
   (((mv er tops)
     (cond ((toplevelp top/tops)
            (mv nil (list top/tops)))
           ((toplevel-listp top/tops)
            (mv nil top/tops))
           (t (mv t nil))))
    ((when er)
     (value
      (make-outcome-unexpected-failure
        :message "Expected a toplevel or toplevel-list argument.")))
    (tstate (get-trans-state (w state)))
    (old-tops (trans-state->tops tstate))
    (ctxt (make-context :tops old-tops))
    (tstate (extend-trans-state-list tops tstate))
    (table-event (cons 'set-trans-state
                       (cons tstate 'nil)))
    (state (acl2::submit-event-quiet table-event state))
    ((mv events outcomes state)
     (generate-and-process-acl2-events tops ctxt state))
    (new-tops (tops-from-transform-outcomes outcomes))
    (tstate (extend-trans-state-list new-tops tstate))
    (table-event (cons 'set-trans-state
                       (cons tstate 'nil)))
    (events (if (endp events)
                events
              (append events (list table-event))))
    (final-outcome
         (if (endp outcomes)
             (make-outcome-unexpected-failure
                  :message "Shouldn't happen: No actual outcomes!")
           (car (last outcomes))))
    (make-final-outcome-form (outcome--make-myself final-outcome)))
   (value
    (cons
     'progn
     (append
        events
        (cons (cons 'value-triple
                    (cons (cons 'quote
                                (cons make-final-outcome-form 'nil))
                          'nil))
              'nil)))))))