callback

(defun let-binding->dep-graph-alst
  (vt-lst ans)
  "Walk down the var-term list vt-lst and add edges.
   Build graph alist in ans"
  (if (endp vt-lst)
    ans
    (b* (((list var term) (car vt-lst)) (fvars (all-vars term)))
      (let-binding->dep-graph-alst (cdr vt-lst)
        (union-entry-in-adj-list var
          fvars
          ans)))))

(defun get-ordered-alst
  (keys alst ans)
  (declare (xargs :guard (and (true-listp keys)
        (alistp ans)
        (alistp alst))))
  "accumulate entries of alist in ans in the order of keys"
  (if (endp keys)
    ans
    (let ((at (assoc-equal (car keys) alst)))
      (if at
        (get-ordered-alst (cdr keys)
          alst
          (append ans (list at)))
        (get-ordered-alst (cdr keys)
          alst
          ans)))))

(defun do-let*-ordering
  (vt-lst debug-flag)
  (declare (xargs :guard (symbol-alistp vt-lst)
      :mode :program))
  (b* ((vars (union-eq (all-vars1-lst (strip-cars vt-lst) nil)
         (all-vars1-lst (strip-cdrs vt-lst) nil))) (dep-g (let-binding->dep-graph-alst vt-lst
          (make-empty-adj-list vars)))
      (sorted-vars (approximate-topological-sort dep-g
          debug-flag)))
    (get-ordered-alst (reverse sorted-vars)
      vt-lst
      nil)))

(defun get-dest-elim-replaced-terms
  (elim-sequence)
  (if (endp elim-sequence)
    nil
    (let* ((elt (car elim-sequence)) (rhs (nth 1 elt))
        (lhs (nth 2 elt)))
      (cons (list rhs lhs)
        (get-dest-elim-replaced-terms (cdr elim-sequence))))))

(defun collect-replaced-terms
  (hist ans)
  (declare (xargs :mode :program))
  (if (endp hist)
    ans
    (b* ((h (car hist)) (ttree (access history-entry h :ttree))
        (proc (access history-entry h :processor)))
      (cond ((eq proc 'generalize-clause) (let ((ans1 (list-up-lists (tagged-object 'terms ttree)
                 (tagged-object 'variables ttree))))
            (collect-replaced-terms (cdr hist)
              (append ans1 ans))))
        ((eq proc 'eliminate-destructors-clause) (let* ((elim-sequence (tagged-object 'elim-sequence ttree)) (ans1 (get-dest-elim-replaced-terms elim-sequence)))
            (collect-replaced-terms (cdr hist)
              (append ans1 ans))))
        (t (let* ((binding-lst (tagged-object 'binding-lst ttree)) (ans1 (list-up-lists (strip-cars binding-lst)
                  (strip-cdrs binding-lst))))
            (collect-replaced-terms (cdr hist)
              (append ans1 ans))))))))

(defun cgen-search-clause
  (cl name
    ens
    hist
    elim-elided-var-map
    cgen-state
    vl
    ctx
    state)
  "helper function for test-checkpoint. It basically sets up
   everything for the call to csearch."
  (declare (xargs :stobjs (state) :mode :program))
  (b* ((type-alist (get-acl2-type-alist-fn cl
         ens
         state)) (vars (all-vars1-lst cl 'nil))
      ((mv hyps concl) (clause-mv-hyps-concl cl))
      ((mv hyps concl state) (if (and (consp cl)
            (null (cdr cl))
            (consp (car cl))
            (eq (caar cl) 'implies))
          (partition-into-hyps-concl-and-preprocess (car cl)
            "cgen-search-clause"
            state)
          (mv hyps concl state)))
      (elided-var-map (append (collect-replaced-terms hist nil)
          elim-elided-var-map))
      (- (cw? (verbose-stats-flag vl)
          "~|CEgen/Verbose: Search clause with elide-map ~x0. ~|"
          elided-var-map))
      (ord-elide-map (do-let*-ordering elided-var-map
          (system-debug-flag vl)))
      (tau-interval-alist (tau-interval-alist-clause cl
          vars
          ens))
      ((mv erp cgen-state state) (cgen-search-fn name
          hyps
          concl
          type-alist
          tau-interval-alist
          ord-elide-map
          (eq (default-defun-mode (w state))
            :program)
          cgen-state
          ctx
          state)))
    (mv erp cgen-state state)))

(defun all-functions-definedp-lst
  (fns wrld)
  "are all the functions used in fns executable?"
  (declare (xargs :verify-guards nil
      :guard (and (symbol-listp fns)
        (plist-worldp wrld))))
  (if (endp fns)
    t
    (and (logical-namep (car fns) wrld)
      (all-functions-definedp-lst (cdr fns)
        wrld))))

(defun unsupported-fns
  (fns wrld)
  "gather functions that
1. take stobjs as args
2. constrained (encapsulate) and no attachment"
  (if (endp fns)
    nil
    (let* ((fn (car fns)) (constrainedp (acl2-getprop fn
            'constrainedp
            wrld
            :default nil))
        (att (acl2-getprop fn
            'attachment
            wrld
            :default nil)))
      (if (or (or-list (stobjs-in fn wrld))
          (and constrainedp (null att)))
        (cons fn
          (unsupported-fns (cdr fns) wrld))
        (unsupported-fns (cdr fns) wrld)))))

(defun cgen-exceptional-functions
  (terms vl wrld)
  "return (mv all-execp unsupportedp)"
  (declare (xargs :verify-guards nil
      :guard (pseudo-term-listp terms)))
  (b* ((fns (all-functions-lst terms)) (all-execp (all-functions-definedp-lst fns wrld))
      (- (cw? (and (not all-execp) (verbose-flag vl))
          "~|CEgen/Note: Skipping testing completely, since not all functions in this conjecture are defined.~%"))
      (unsupportedp (consp (unsupported-fns fns wrld)))
      (- (cw? (and unsupportedp (verbose-flag vl))
          "~|CEgen/Note: Skipping testing completely, since some functions in this conjecture either take stobj arguments or are constrained without an attachment.~%")))
    (mv all-execp unsupportedp)))

(defun not-equivalid-p
  (processor-hist)
  "proof has wandered into non-equi-valid path"
  (intersection-eq processor-hist
    '(fertilize-clause generalize-clause
      eliminate-irrelevance-clause)))

(defun update-cgen-state-givens/callback
  (term ctx vl state)
  "update cgen-state fields user-supplied-term,top-vt-alist etc from test-checkpoint"
  (b* ((cgen-state (@ cgen-state)) (cgen-state (cput top-ctx ctx))
      (cgen-state (cput user-supplied-term term))
      (cgen-state (cput displayed-goal term))
      ((mv hyp concl) (mv (get-hyp term)
          (get-concl term)))
      (hyps (if (eq hyp 't)
          'nil
          (expand-assumptions-1 hyp)))
      (vars (vars-in-dependency-order hyps
          concl
          vl
          (w state)))
      (d-typ-al (dumb-type-alist-infer (cons (cgen-dumb-negate-lit concl) hyps)
          vars
          vl
          (w state)))
      (cgen-state (cput top-vt-alist d-typ-al))
      (- (cw? (system-debug-flag vl)
          "~|CEgen/Sysdebug: update-gcs%-top-level : ~x0 dumb top vt-alist: ~x1 ~|"
          term
          d-typ-al)))
    cgen-state))

(defun test-checkpoint-h1
  (id cl
    cl-list
    processor
    pspv
    hist
    ctx
    state)
  "?: This function is a callback called via an override hint +
backtrack no-op hint combination.  On SUBGOALS that are not
checkpoints it is a no-op. On checkpoints it calls the main
cgen/testing procedure.

Note that this (observer) hint combination means that when this
callback function is called, that particular processor had a HIT and
resulted in one or more subgoals, each of which will fall on top of
the waterfall like in a Escher drawing.

RETURN either (mv t nil state) or (mv nil nil state) i.e as a hint it
is a no-op with the following exception.  If the processor is
generalize and a counterexample was found to the generalized subgoal,
then it returns (value '(:do-not '(acl2::generalize)
                                :no-thanks t))

"
  (b* ((vl (acl2s-defaults :get verbosity-level)) (backtrack? (acl2s-defaults :get backtrack-bad-generalizations))
      ((unless (and (f-boundp-global 'cgen-state state)
           (cgen-state-p (@ cgen-state)))) (prog2$ (cw? (debug-flag vl)
            "~|CEgen/Debug: test-checkpoint -- cgen-state malformed; skip cgen/testing...~%")
          (value nil)))
      ((mv all-execp unsupportedp) (cgen-exceptional-functions cl
          vl
          (w state)))
      ((unless all-execp) (value nil))
      ((when unsupportedp) (value nil))
      (hist-len (len hist))
      (- (cw? (debug-flag vl)
          "test-checkpoint : id = ~x0 processor = ~x1 ctx = ~x2 hist-len = ~x3~|"
          id
          processor
          ctx
          hist-len))
      ((unless (member-eq processor
           '(preprocess-clause settled-down-clause
             eliminate-destructors-clause
             fertilize-clause
             generalize-clause
             eliminate-irrelevance-clause
             push-clause))) (value nil))
      (name (string-for-tilde-@-clause-id-phrase id))
      ((when (and (eq processor 'preprocess-clause)
           (not (equal name "Goal")))) (value nil))
      (wrld (w state))
      (cgen-state (@ cgen-state))
      (pspv-user-supplied-term (access prove-spec-var pspv :user-supplied-term))
      (- (cw? (debug-flag vl)
          "~| pspv-ust: ~x0 curr ust: ~x1 ctx:~x2 cgen-state.ctx:~x3~%"
          pspv-user-supplied-term
          (cget user-supplied-term)
          ctx
          (cget top-ctx)))
      ((unless (implies (and (not (eq (cget user-supplied-term) :undefined))
             (not (eq (car (cget top-ctx)) :user-defined)))
           (equal ctx (cget top-ctx)))) (prog2$ (cw? (verbose-flag vl)
            "~|Cgen/Note: We encountered a new goal ctx ~x0, in the course of testing ctx ~x1. ~
Nested testing not allowed! Skipping testing of new goal...~%"
            ctx
            (cget top-ctx))
          (value nil)))
      (user-supplied-term (cget user-supplied-term))
      ((unless (implies (not (eq user-supplied-term :undefined))
           (equal user-supplied-term
             pspv-user-supplied-term))) (prog2$ (cw? (verbose-flag vl)
            "~|Cgen/Note: We encountered a new goal ~x0, in the course of testing ~x1. ~
Nested testing not allowed! Skipping testing of new goal...~%"
            (prettyify-clause (list pspv-user-supplied-term)
              nil
              wrld)
            (prettyify-clause (list user-supplied-term)
              nil
              wrld))
          (value nil)))
      (cgen-state (if (eq (cget user-supplied-term) :undefined)
          (update-cgen-state-givens/callback pspv-user-supplied-term
            ctx
            vl
            state)
          cgen-state))
      (- (cw? (verbose-stats-flag vl)
          "~%~%~|Cgen/Note: @Checkpoint Subgoal-name:~x0 Processor:~x1~|"
          name
          processor))
      (ens (access rewrite-constant
          (access prove-spec-var pspv :rewrite-constant)
          :current-enabled-structure))
      ((mv & cgen-state state) (cgen-search-clause cl
          name
          ens
          hist
          'nil
          cgen-state
          vl
          ctx
          state))
      (processor-hist (cons processor (cget processor-hist)))
      (cgen-state (cput processor-hist processor-hist))
      (abo? (not-equivalid-p processor-hist))
      (- (cw? (and (debug-flag vl) abo?)
          "~|Cgen/Debug: Top-level cts/wts cannot be constructed now ... ~x0 in ~x1~%"
          name
          ctx))
      (state (f-put-global 'cgen-state
          cgen-state
          state))
      (gcs% (cget gcs)))
    (if (or (cget stopping-condition-p)
        (and (> (access gcs% cts) 0)
          (or abo? (eq processor 'push-clause))))
      (mv t nil state)
      (if (and backtrack?
          (equal processor 'generalize-clause))
        (b* ((gen-cl (car cl-list)) (type-alist (get-acl2-type-alist gen-cl))
            ((mv h c) (clause-mv-hyps-concl gen-cl))
            (vars (vars-in-dependency-order h
                c
                vl
                wrld))
            (vt-alist (make-weakest-type-alist vars))
            (tau-interval-alist (tau-interval-alist-clause gen-cl vars))
            (temp-cgen-state (list (cons 'params (cget params))
                (cons 'gcs *initial-gcs%*)
                (cons 'top-ctx ctx)
                (cons 'top-vt-alist vt-alist)))
            ((mv erp res state) (cgen-search-local name
                h
                c
                type-alist
                tau-interval-alist
                nil
                *initial-test-outcomes%*
                *initial-gcs%*
                temp-cgen-state
                ctx
                state))
            ((when erp) (value nil))
            ((list & test-outcomes% &) res)
            (num-cts-found (access test-outcomes% |#cts|)))
          (value (if (> num-cts-found 0)
              (progn$ (cw? (not (f-get-global 'gag-mode state))
                  "~| Generalized subgoal: ~x0~|"
                  (prettyify-clause gen-cl nil (w state)))
                (cw? (not (f-get-global 'gag-mode state))
                  "~| Counterexample found: ~x0 ~|"
                  (car (access test-outcomes% cts)))
                (cw? (not (f-get-global 'gag-mode state))
                  "~| Bad generalization! Backtracking...~|")
                '(:do-not '(generalize) :no-thanks t))
              nil)))
        (value nil)))))

(defun test-checkpoint
  (id cl
    cl-list
    processor
    pspv
    hist
    ctx
    state)
  (declare (xargs :stobjs (state) :mode :program))
  (b* ((debug-enable (f-get-global 'debugger-enable state)) (state (f-put-global 'debugger-enable :never state))
      ((mv erp val state) (test-checkpoint-h1 id
          cl
          cl-list
          processor
          pspv
          hist
          ctx
          state))
      (state (f-put-global 'debugger-enable
          debug-enable
          state)))
    (mv erp val state)))

(defun init-cgen-state/event
  (params start-time top-ctx)
  (declare (xargs :guard (and (cgen-params-p params)
        (rationalp start-time)
        (allowed-cgen-event-ctx-p top-ctx))))
  (list (cons 'params params)
    (cons 'user-supplied-term :undefined)
    (cons 'displayed-goal :undefined)
    (cons 'start-time start-time)
    (cons 'gcs *initial-gcs%*)
    (cons 'top-ctx top-ctx)))

(defun compute-event-ctx
  (ctx-form)
  (cond ((atom ctx-form) ctx-form)
    ((mem-tree 'thm ctx-form) 'thm)
    ((mem-tree 'defthm ctx-form) 'defthm)
    ((mem-tree 'verify-guards ctx-form) 'verify-guards)
    ((mem-tree 'defun-ctx ctx-form) 'defuns)
    (t ctx-form)))

(defun initialize-event-user-cgen
  (ctx-form body state)
  (declare (xargs :stobjs state
      :mode :program :verify-guards nil))
  (declare (ignorable body))
  (b* (((unless (and (f-boundp-global 'cgen-state state)
          (f-boundp-global 'event-ctx state))) state) (vl (acl2s-defaults :get verbosity-level))
      (ctx (compute-event-ctx ctx-form))
      ((unless (allowed-cgen-event-ctx-p ctx)) (prog2$ (cw? (> vl 8)
            "~|CEgen/Warning: initialize-event -- ctx ~x0 ignored...~%"
            ctx)
          state))
      ((mv start state) (read-run-time state))
      (cgen-state (init-cgen-state/event (acl2s-defaults-alist)
          start
          :undefined))
      (- (cw? (debug-flag vl)
          "~|CEgen/Note: CGEN-STATE initialized for ~x0~%"
          ctx-form))
      (state (f-put-global 'cgen-state
          cgen-state
          state))
      (state (f-put-global 'event-ctx
          ctx-form
          state)))
    state))

(defun finalize-event-user-cgen
  (ctx-form body state)
  (declare (xargs :mode :program :verify-guards nil
      :stobjs state))
  (declare (ignorable body))
  (b* (((unless (and (f-boundp-global 'cgen-state state)
          (f-boundp-global 'event-ctx state))) state) (vl (acl2s-defaults :get verbosity-level))
      (event-ctx (@ event-ctx))
      ((unless (equal event-ctx ctx-form)) (prog2$ (cw? (> vl 8)
            "~|CEgen/Warning: finalize-event -- ignore non-top event...~%")
          state))
      (state (f-put-global 'event-ctx nil state))
      ((mv end state) (read-run-time state))
      (cgen-state (@ cgen-state))
      (cgen-state (cput end-time end))
      (state (f-put-global 'cgen-state
          cgen-state
          state))
      (gcs% (cget gcs))
      (ctx (compute-event-ctx ctx-form))
      (print-summary-p (and (cget print-cgen-summary)
          (allowed-cgen-event-ctx-p ctx)))
      (- (cw? (system-debug-flag vl)
          "~|CEgen/SysDebug: Exiting event with gcs% : ~x0. ~ ctx: ~x1 print-cgen-summ : ~x2 ~%"
          gcs%
          ctx
          (cget print-cgen-summary)))
      ((mv & & state) (if print-summary-p
          (print-testing-summary cgen-state
            ctx
            state)
          (value nil)))
      (- (cw? (debug-flag vl)
          "~|CEgen/Note: CGEN-STATE finalized for ctx ~x0~%"
          ctx))
      (state (f-put-global 'cgen-state nil state)))
    state))

(defun initialize-event-user-cgen-gv
  (ctx body state)
  (declare (xargs :mode :program :stobjs state :guard t))
  (ec-call (initialize-event-user-cgen ctx
      body
      state)))

(defun finalize-event-user-cgen-gv
  (ctx body state)
  (declare (xargs :mode :program :guard t :stobjs state))
  (ec-call (finalize-event-user-cgen ctx
      body
      state)))