|
|
|---|
|
|
|
|---|
Generate a C loop statement from an ACL2 term.
(atc-gen-loop-stmt term gin state) → (mv erp gout)
This is called on loop terms (see user documentation).
The term must be an if. If the test is an mbt, test and `else' branch are ignored, while the `then' branch is recursively processed. Otherwise, the test must be an expression term returning a boolean from which we generate the loop test; the `then' branch must be a statement term, from which we generate the loop body; and the `else' branch must be either a single variable or an mv call on variables, which must be a subset of the function's formals, and from those variables we determine the variables affected by the loop. The statement term in the `then' branch must affect the variables found in the `else' branch. We return the term that represents the loop test, the term that represent the loop body and the variables affected by the loop. The loop test and body are used to generate more modular theorems.
Note that we push a new scope before processing the loop body. This is because the loop body is a block, which opens a new scope in C.
We return a limit that suffices
to execute exec-stmt-while on (the test and body of)
the loop statement, as follows.
We need 1 to get to executing the test,
which is pure and so does not contribute to the overall limit.
If the test is true, we need to add the limit to execute the body.
After that, exec-stmt-while is called recursively,
decrementing the limit:
given that we know that the loop function terminates,
its measure must suffice as the limit.
The loop function decreases the measure by at least 1 (maybe more)
at every recursive call, so the limit does not decrease any faster,
and we will never run out of the limit before the measure runs out.
Thus the measure is an over-approximation for the limit, which is sound.
We also note that the measure refers to the initial call of the function,
while here it would suffice
to take the measure at the first recursive call,
but taking the whole measure is simpler,
and again it is sound to over-appoximate.
Note that we use the measure function for
Function:
(defun atc-gen-loop-stmt (term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (lstmt-ginp gin)))) (let ((__function__ 'atc-gen-loop-stmt)) (declare (ignorable __function__)) (b* (((reterr) (change-lstmt-gout (irr-lstmt-gout) :stmt (make-stmt-while :test (irr-expr) :body (irr-stmt)))) ((lstmt-gin gin) gin) (wrld (w state)) ((mv okp test-term then-term else-term) (fty-check-if-call term)) ((unless okp) (reterr (msg "When generating C loop code for the recursive function ~x0, ~ a term ~x1 that is not an IF has been encountered." gin.fn term))) ((mv mbtp &) (check-mbt-call test-term)) ((when mbtp) (atc-gen-loop-stmt then-term gin state)) ((erp (expr-gout test)) (atc-gen-expr-bool test-term (make-expr-gin :context gin.context :inscope gin.inscope :prec-tags gin.prec-tags :fn gin.fn :fn-guard gin.fn-guard :compst-var gin.compst-var :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid :proofs gin.proofs) state)) (formals (formals+ gin.fn wrld)) ((mv okp affect) (b* (((when (member-eq else-term formals)) (mv t (list else-term))) ((mv okp terms) (fty-check-list-call else-term)) ((when (and okp (subsetp-eq terms formals))) (mv t terms))) (mv nil nil))) ((unless okp) (reterr (msg "The 'else' branch ~x0 of the function ~x1, ~ which should be the non-recursive branch, ~ does not have the required form. ~ See the user documentation." else-term gin.fn))) ((erp (stmt-gout body)) (atc-gen-stmt then-term (make-stmt-gin :context gin.context :var-term-alist nil :typed-formals gin.typed-formals :inscope (cons nil gin.inscope) :loop-flag t :affect affect :fn gin.fn :fn-guard gin.fn-guard :compst-var gin.compst-var :prec-fns gin.prec-fns :prec-tags gin.prec-tags :prec-objs gin.prec-objs :thm-index test.thm-index :names-to-avoid test.names-to-avoid :proofs (and test.thm-name t)) state)) ((unless (type-case body.type :void)) (reterr (raise "Internal error: ~ the loop body ~x0 of ~x1 ~ returns type ~x2." then-term gin.fn body.type))) (body-stmt (make-stmt-compound :items body.items)) (stmt (make-stmt-while :test test.expr :body body-stmt)) ((when (eq gin.measure-for-fn 'quote)) (reterr (raise "Internal error: the measure function is QUOTE."))) (measure-call (pseudo-term-fncall gin.measure-for-fn gin.measure-formals)) (limit (cons 'binary-+ (cons ''1 (cons (cons 'binary-+ (cons body.limit (cons measure-call 'nil))) 'nil))))) (retok (make-lstmt-gout :stmt stmt :test-term test-term :body-term then-term :affect affect :limit-body body.limit :limit-all limit :thm-name nil :thm-index body.thm-index :names-to-avoid body.names-to-avoid)))))
Theorem:
(defthm lstmt-goutp-of-atc-gen-loop-stmt.gout (b* (((mv acl2::?erp ?gout) (atc-gen-loop-stmt term gin state))) (lstmt-goutp gout)) :rule-classes :rewrite)
Theorem:
(defthm stmt-kind-of-atc-gen-loop-stmt (b* (((mv acl2::?erp ?gout) (atc-gen-loop-stmt term gin state))) (equal (stmt-kind (lstmt-gout->stmt gout)) :while)))