itest-cgen

(defun itest?-extract-assignment
  (a top-vars
    elided-var-map
    counteregp
    state)
  (declare (xargs :stobjs (state)
      :guard (and (symbol-doublet-listp a)
        (implies (consp a) (consp (car a)))
        (symbol-alistp elided-var-map)
        (symbol-listp top-vars)
        (booleanp counteregp))))
  (b* ((top-a (filter-alist-keys a top-vars)) (vals (make-evalable-lst-how (strip-cadrs top-a)
          (get-evalable-printing-abstractions state)))
      (?top-a (list-up-lists (strip-cars top-a)
          vals))
      ((er (list ? top-a)) (get-top-level-assignment a
          top-vars
          t
          elided-var-map
          counteregp
          state))
      (vals (make-evalable-lst-how (strip-cadrs top-a)
          (get-evalable-printing-abstractions state)))
      (top-a (list-up-lists (strip-cars top-a)
          vals)))
    (value top-a)))

(defun itest?-extract-assignments
  (a-lst top-vars
    elided-var-map
    counteregp
    state)
  (declare (xargs :stobjs (state)
      :guard (and (symbol-alist-listp a-lst)
        (symbol-listp top-vars)
        (symbol-alistp elided-var-map)
        (booleanp counteregp))))
  (if (endp a-lst)
    (value nil)
    (b* (((er r) (itest?-extract-assignment (car a-lst)
           top-vars
           elided-var-map
           counteregp
           state)) ((er rs) (itest?-extract-assignments (cdr a-lst)
            top-vars
            elided-var-map
            counteregp
            state)))
      (value (cons r rs)))))

(defun itest?-print-cts/wts
  (s-hist cts-p top-vars state)
  (declare (xargs :stobjs (state)))
  (if (endp s-hist)
    (value nil)
    (b* (((cons ? s-hist-entry%) (car s-hist)) (test-outcomes% (access s-hist-entry% test-outcomes))
        (a-lst (if cts-p
            (access test-outcomes% cts)
            (access test-outcomes% wts)))
        (elide-map (access s-hist-entry% elide-map))
        ((when (endp a-lst)) (itest?-print-cts/wts (cdr s-hist)
            cts-p
            top-vars
            state))
        ((mv & res1 state) (itest?-extract-assignments a-lst
            top-vars
            elide-map
            cts-p
            state))
        ((mv & res2 state) (itest?-print-cts/wts (cdr s-hist)
            cts-p
            top-vars
            state)))
      (value (remove-duplicates (append res1 res2)
          :test 'equal)))))

(defun extract-cgen
  (cgen-state state)
  (declare (xargs :stobjs (state)))
  (b* ((s-hist (cget s-hist)) (gcs% (cget gcs))
      (vl (cget verbosity-level)))
    (case-match gcs%
      (('gcs% (& & . &)
         (& . &)) (b* ((top-term (cget user-supplied-term)) (top-vars (all-vars top-term))
            ((er cts) (itest?-print-cts/wts s-hist
                t
                top-vars
                state))
            ((er wts) (itest?-print-cts/wts s-hist
                nil
                top-vars
                state)))
          (value (list cts wts))))
      (& (value (cw? (normal-output-flag vl)
            "~|ITEST? error: BAD gcs% in cgen-state.~|"))))))