		Search-engine friendly clone of the ACL2 documentation.

Translation

Translate-to-ACL2-fn

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

Signature
(translate-to-acl2-fn top/tops ctx state) → (mv erp event state)
Returns: event — A pseudo-event-formp.

This is called by translate-to-ACL2, which is the entry point of the translation from Syntheto to 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 semnantics). 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: translate-to-acl2-fn

(defun translate-to-acl2-fn (top/tops ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'translate-to-acl2-fn))
  (declare (ignorable __function__))
  (b*
   (((er tops)
     (cond
      ((toplevelp top/tops)
       (value (list top/tops)))
      ((toplevel-listp top/tops)
       (value top/tops))
      (t
       (er
        soft ctx
        "The input must be ~
                            a Syntheto top-level construct ~
                            or a list of them, ~
                            but it is ~x0 instead."
        top/tops))))
    (tstate (get-trans-state (w state)))
    (old-tops (trans-state->tops tstate))
    (ctxt (make-context :tops old-tops))
    ((mv err? obligs)
     (check-toplevel-list tops ctxt))
    ((when err?)
     (er soft ctx
         "Static semantic failure:~%~x0" err?))
    (- (cw "Proof obligations:~%~x0~%" obligs))
    (tstate (extend-trans-state-list tops tstate))
    (table-event (cons 'set-trans-state
                       (cons tstate 'nil)))
    (logical-events (d-->s-toplevel-list tops)))
   (value (cons 'progn
                (cons table-event logical-events))))))