type-extract-cp

(in-package "SMT")

(include-book "std/util/bstar" :dir :system)

(include-book "xdoc/top" :dir :system)

(include-book "std/util/define" :dir :system)

(include-book "hint-please")

(include-book "hint-interface")

(include-book "extractor")

(include-book "type-hyp")

(defsection type-extract-cp
  :parents (verified)
  :short "Verified clause-processor for extracting type declarations"
  (defevaluator ev-extract
    ev-lst-extract
    ((not x) (if x
        y
        z)
      (implies x y)
      (hint-please hint)))
  (def-join-thms ev-extract)
  (define type-extract-helper
    ((cl pseudo-term-listp) (smtlink-hint smtlink-hint-p)
      state)
    :mode :program (b* ((cl (pseudo-term-list-fix cl)) (smtlink-hint (smtlink-hint-fix smtlink-hint))
        ((smtlink-hint h) smtlink-hint)
        (g (disjoin cl))
        ((mv type-decl-list g/type) (smt-extract g h.fty-info h.abs))
        ((mv err type-decl-list-translated) (translate-cmp `(list ,@SMT::TYPE-DECL-LIST)
            t
            t
            nil
            'type-extract-cp->type-extract-helper
            (w state)
            (default-state-vars t)))
        ((when err) (er hard?
            'type-extract-cp->type-extract-helper
            "Error ~
    translating form: ~@0"
            `(list ,@SMT::TYPE-DECL-LIST))))
      (change-smtlink-hint h
        :expanded-g/type g/type
        :type-decl-list type-decl-list-translated)))
  (define type-extract-fn
    ((cl pseudo-term-listp) (smtlink-hint t))
    :returns (subgoal-lst pseudo-term-list-listp)
    (b* (((unless (pseudo-term-listp cl)) nil) ((unless (smtlink-hint-p smtlink-hint)) (list cl))
        ((smtlink-hint h) smtlink-hint)
        (g (disjoin cl))
        (type-decl-list h.type-decl-list)
        (g/type h.expanded-g/type)
        (next-cp (cdr (assoc-equal 'type-extract
              *smt-architecture*)))
        ((if (null next-cp)) (list cl))
        (the-hint `(:clause-processor (,SMT::NEXT-CP clause ',SMT::H)))
        (cl0 `((hint-please ',SMT::THE-HINT) (not (type-hyp (hide ,SMT::TYPE-DECL-LIST) ':type))
            ,SMT::G/TYPE))
        (cl1 `((hint-please '(:in-theory (enable type-hyp)
               :expand ((:free (x) (hide x))))) (not (implies (type-hyp (hide ,SMT::TYPE-DECL-LIST) ':type)
                ,SMT::G/TYPE))
            ,SMT::G)))
      `(,SMT::CL0 ,SMT::CL1)))
  (defmacro type-extract-cp
    (clause hint)
    `(type-extract-fn clause
      (type-extract-helper ,SMT::CLAUSE
        ,SMT::HINT
        state)))
  (local (in-theory (enable type-extract-fn
        type-hyp
        hint-please
        hide)))
  (defthm correctness-of-type-extract-cp
    (implies (and (pseudo-term-listp cl)
        (alistp b)
        (ev-extract (conjoin-clauses (type-extract-fn cl smtlink-hint))
          b))
      (ev-extract (disjoin cl) b))
    :rule-classes :clause-processor))