		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-collect-fns-in-term

Collect all the functions in a term, in the course of the worklist algorithm.

Signature
(atj-collect-fns-in-term term gen? worklist-gen worklist-chk called-fns collected-gen collected-chk deep$ guards$) → (mv new-worklist-gen new-worklist-chk new-called-fns unsuppported-return-last?)
Arguments: term — Guard (pseudo-termp term).; gen? — Guard (booleanp gen?).; worklist-gen — Guard (symbol-listp worklist-gen).; worklist-chk — Guard (symbol-listp worklist-chk).; called-fns — Guard (symbol-listp called-fns).; collected-gen — Guard (symbol-listp collected-gen).; collected-chk — Guard (symbol-listp collected-chk).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).
Returns: new-worklist-gen — Type (symbol-listp new-worklist-gen), given the guard.; new-worklist-chk — Type (symbol-listp new-worklist-chk), given the guard.; new-called-fns — Type (symbol-listp new-called-fns), given the guard.; unsuppported-return-last? — Type (booleanp unsuppported-return-last?).

See the overview of the worklist algorithm first.

This is called on the defining body of the function removed from the worklist, and recursively on subterms of the defining body.

Besides the term, this function takes as arguments the two worklists and the two collected lists: the -gen suffix stands for `generation', i.e. the functions for which Java code must be generated; the -chk suffix stands for `checking', i.e. the functions that must be just checked. The collected lists are only used to see which of the functions encountered in the term have already been processed by the worklist algorithm. The worklists are updated as appropriate, and eventually returned.

This function also takes an argument flag gen? saying whether we are examining a term from (a function from) the first worklist or a term from a function from (a function from) the second worklist.

Since variables and quoted constants contain no functions, we return the worklists unchanged in these cases.

A term (mbe :logic a :exec b) is translated to (return-last 'acl2::mbe1-raw b a). When :guards is nil, we translate a to Java, but still need to check b for side effects: thus, we recursively descend into a with the current gen? flag, and we recursively descend into b with gen? set to nil. When :guards is t, the treatment of a and b is reversed.

A term (prog2$ a b) is translated to (return-last 'acl2::progn a b) (and progn$ is translated into a nest of prog2$s). Thus, when we encounter this kind of call, when we descend into the argument a we set the gen? flag to nil, while when we descend into the argument b we leave the gen? flag unchanged.

If we encounter a call of return-last of some other form, we immediately return because such other forms are not supported. In this case, the third result of the function is set to t, so that the caller can immediately recognize the situation and cause the algorithm to terminate.

If we encounter a call of anything other than return-last, we recursively process the arguments, propagating any error signaled by the third result.

If the call is of a lambda expression, we conclude by recursively processing the body of the lambda expression.

Otherwise, the call is of a named function (not return-last). We add the function to the appropriate worklist (the exact worklist is determined by the gen? flag), unless it is already there or in a collected list. If gen? is t and the function is already in worklist-chk or collected-chk but not in worklist-gen or collected-gen, we need to add it to worklist-gen nonetheless, because it must eventually end up in collected-gen in order to generate code for it. Thus, if gen? is t, we only check it against worklist-gen and collected-gen, and if we add it to worklist-gen we also remove it from worklist-chk if present there (with remove1 because worklists never have duplicates; if it is not present, no change to worklist-chk occurs), so that the function is not processed again. We do not need to remove the function from collected-chk because, when gen? is t, that collected list is always empty: the reason is that the algorithm first processes worklist-gen completely (during this processing gen? is t), keeping collected-chk empty, and then it processes worklist-chk, and it is during this processing (when gen? is thus nil) that collected-chk gets populated.

We also return a duplicate-free list of the function symbols called by the term for which Java code must be generated.

Theorem: return-type-of-atj-collect-fns-in-term.new-worklist-gen

(defthm return-type-of-atj-collect-fns-in-term.new-worklist-gen
 (implies
   (and (pseudo-termp term)
        (booleanp gen?)
        (symbol-listp worklist-gen)
        (symbol-listp worklist-chk)
        (symbol-listp called-fns)
        (symbol-listp collected-gen)
        (symbol-listp collected-chk)
        (booleanp deep$)
        (booleanp guards$))
   (b*
    (((mv ?new-worklist-gen
          ?new-worklist-chk ?new-called-fns
          ?unsuppported-return-last?)
      (atj-collect-fns-in-term term gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
    (symbol-listp new-worklist-gen)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-term.new-worklist-chk

(defthm return-type-of-atj-collect-fns-in-term.new-worklist-chk
 (implies
   (and (pseudo-termp term)
        (booleanp gen?)
        (symbol-listp worklist-gen)
        (symbol-listp worklist-chk)
        (symbol-listp called-fns)
        (symbol-listp collected-gen)
        (symbol-listp collected-chk)
        (booleanp deep$)
        (booleanp guards$))
   (b*
    (((mv ?new-worklist-gen
          ?new-worklist-chk ?new-called-fns
          ?unsuppported-return-last?)
      (atj-collect-fns-in-term term gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
    (symbol-listp new-worklist-chk)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-term.new-called-fns

(defthm return-type-of-atj-collect-fns-in-term.new-called-fns
 (implies
   (and (pseudo-termp term)
        (booleanp gen?)
        (symbol-listp worklist-gen)
        (symbol-listp worklist-chk)
        (symbol-listp called-fns)
        (symbol-listp collected-gen)
        (symbol-listp collected-chk)
        (booleanp deep$)
        (booleanp guards$))
   (b*
    (((mv ?new-worklist-gen
          ?new-worklist-chk ?new-called-fns
          ?unsuppported-return-last?)
      (atj-collect-fns-in-term term gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
    (symbol-listp new-called-fns)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-term.unsuppported-return-last?

(defthm
   return-type-of-atj-collect-fns-in-term.unsuppported-return-last?
  (b*
    (((mv ?new-worklist-gen
          ?new-worklist-chk ?new-called-fns
          ?unsuppported-return-last?)
      (atj-collect-fns-in-term term gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
    (booleanp unsuppported-return-last?))
  :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-terms.new-worklist-gen

(defthm return-type-of-atj-collect-fns-in-terms.new-worklist-gen
 (implies
  (and (pseudo-term-listp terms)
       (booleanp gen?)
       (symbol-listp worklist-gen)
       (symbol-listp worklist-chk)
       (symbol-listp called-fns)
       (symbol-listp collected-gen)
       (symbol-listp collected-chk)
       (booleanp deep$)
       (booleanp guards$))
  (b*
   (((mv ?new-worklist-gen
         ?new-worklist-chk ?new-called-fns
         ?unsuppported-return-last?)
     (atj-collect-fns-in-terms terms gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
   (symbol-listp new-worklist-gen)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-terms.new-worklist-chk

(defthm return-type-of-atj-collect-fns-in-terms.new-worklist-chk
 (implies
  (and (pseudo-term-listp terms)
       (booleanp gen?)
       (symbol-listp worklist-gen)
       (symbol-listp worklist-chk)
       (symbol-listp called-fns)
       (symbol-listp collected-gen)
       (symbol-listp collected-chk)
       (booleanp deep$)
       (booleanp guards$))
  (b*
   (((mv ?new-worklist-gen
         ?new-worklist-chk ?new-called-fns
         ?unsuppported-return-last?)
     (atj-collect-fns-in-terms terms gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
   (symbol-listp new-worklist-chk)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-terms.new-called-fns

(defthm return-type-of-atj-collect-fns-in-terms.new-called-fns
 (implies
  (and (pseudo-term-listp terms)
       (booleanp gen?)
       (symbol-listp worklist-gen)
       (symbol-listp worklist-chk)
       (symbol-listp called-fns)
       (symbol-listp collected-gen)
       (symbol-listp collected-chk)
       (booleanp deep$)
       (booleanp guards$))
  (b*
   (((mv ?new-worklist-gen
         ?new-worklist-chk ?new-called-fns
         ?unsuppported-return-last?)
     (atj-collect-fns-in-terms terms gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
   (symbol-listp new-called-fns)))
 :rule-classes :rewrite)

Theorem: return-type-of-atj-collect-fns-in-terms.unsuppported-return-last?

(defthm
  return-type-of-atj-collect-fns-in-terms.unsuppported-return-last?
  (b*
   (((mv ?new-worklist-gen
         ?new-worklist-chk ?new-called-fns
         ?unsuppported-return-last?)
     (atj-collect-fns-in-terms terms gen? worklist-gen
                               worklist-chk called-fns collected-gen
                               collected-chk deep$ guards$)))
   (booleanp unsuppported-return-last?))
  :rule-classes :rewrite)

Subtopics

Atj-collect-fns-in-terms