fty-transsum

(in-package "FTY")

(include-book "fty-parseutils")

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

(set-state-ok t)

(program)

(define some-flextranssum-member-recursivep
  (x)
  (if (atom x)
    nil
    (or (flextranssum-member->recp (car x))
      (some-flextranssum-member-recursivep (cdr x)))))

(defun flextranssum-memberlist->tags
  (x)
  (if (atom x)
    nil
    (append (flextranssum-member->tags (car x))
      (flextranssum-memberlist->tags (cdr x)))))

(define infer-possible-tags-from-flextype
  ((ctx "Context for error messages.") (member-name "Name of the transsum member we are inferring tags for.")
    (x "The top-level flextype object for member-name."))
  (cond ((eq (tag x) :sum) (b* (((flexsum x)))
        (if (or (eq x.typemacro 'deftagsum)
            (eq x.typemacro 'defprod))
          (flexprods->kinds x.prods)
          (er hard?
            ctx
            "Can't infer tags for ~x0: not supported: ~x1."
            member-name
            x.typemacro))))
    ((eq (tag x) :transsum) (flextranssum-memberlist->tags (flextranssum->members x)))
    (t (er hard?
        ctx
        "Can't infer tags for ~x0: unsupported flextype ~x1."
        member-name
        (tag x)))))

(define infer-possible-tags-from-typename
  ((ctx "Context for error messages.") (member-type "Name of the member type.")
    (table "The whole flextypes database."))
  (b* (((mv ?flextypes-obj this-type) (search-deftypes-table member-type table)) ((unless this-type) (er hard?
          ctx
          "Type ~x0 not found in the flextypes table."
          member-type)))
    (infer-possible-tags-from-flextype ctx
      member-type
      this-type)))

(defconst *transsum-keywords*
  '(:pred :fix :equiv :case :count :kind :measure :measure-debug :xvar :no-count :parents :short :long :inline :layout :base-case-override :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :enable-rules :verbosep))

(define parse-transsum-member
  ((ctx "Context for error messages.") (x "User-level member name.")
    (our-fixtypes "Fixtypes for the new types we're currently defining.")
    (fixtypes "Existing fixtypes that have already been defined previously.")
    (table "The whole flextypes database."))
  :returns (member "A flextranssum-member.")
  (b* (((unless (symbolp x)) (er hard?
         ctx
         "invalid transsum member: ~x0"
         x)) (name (b* ((fixtype (or (find-fixtype x our-fixtypes)
               (find-fixtype x fixtypes))) ((unless fixtype) (er hard?
                ctx
                "not a known type for transsum member: ~x0"
                x)))
          (fixtype->name fixtype)))
      ((mv pred fix equiv recp) (get-pred/fix/equiv name
          our-fixtypes
          fixtypes))
      ((when recp) (er hard?
          ctx
          "mutually recursive transsum members aren't supported: ~x0"
          x))
      (tags (infer-possible-tags-from-typename ctx
          name
          table)))
    (make-flextranssum-member :name name
      :pred pred
      :fix fix
      :equiv equiv
      :tags tags
      :recp recp)))

(define parse-transsum-members
  (ctx x our-fixtypes fixtypes table)
  :returns (members)
  (if (atom x)
    (if x
      (er hard?
        ctx
        "deftranssum members should be nil-terminated; found ~
                 final cdr ~x0.~%"
        x)
      nil)
    (cons (parse-transsum-member ctx
        (car x)
        our-fixtypes
        fixtypes
        table)
      (parse-transsum-members ctx
        (cdr x)
        our-fixtypes
        fixtypes
        table))))

(define parse-transsum
  (x xvar
    our-fixtypes
    fixtypes
    state)
  (declare (ignorable state))
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed transsum: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist other-args) (extract-keywords name
          *transsum-keywords*
          pre-///
          nil))
      (kwd-alist (append kwd-alist
          (table-alist 'deftranssum-defaults
            (w state))))
      ((when (atom other-args)) (raise "Malformed transsum ~x0: no members list."
          name))
      ((unless (eql (len other-args) 1)) (raise "Malformed transsum ~x0: too many arguments."
          name))
      (members (parse-transsum-members name
          (first other-args)
          our-fixtypes
          fixtypes
          (get-flextypes (w state))))
      ((unless (consp members)) (raise "Malformed transsum ~x0: no members." name))
      (pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
            name)
          kwd-alist))
      (fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
            name)
          kwd-alist))
      (equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
            name)
          kwd-alist))
      (case (getarg! :case (intern-in-package-of-symbol (cat (symbol-name name) "-CASE")
            name)
          kwd-alist))
      (kind (getarg! :kind (intern-in-package-of-symbol (cat (symbol-name name) "-KIND")
            name)
          kwd-alist))
      (inline (get-deftypes-inline-opt *inline-defaults*
          kwd-alist))
      (count (flextype-get-count-fn name kwd-alist))
      (xvar (or (getarg :xvar xvar kwd-alist)
          (car (find-symbols-named-x (getarg :measure nil kwd-alist)))
          (intern-in-package-of-symbol "X" name)))
      (measure (getarg! :measure `(acl2-count ,FTY::XVAR)
          kwd-alist))
      (kwd-alist (if post-///
          (cons (cons :///-events post-///) kwd-alist)
          kwd-alist)))
    (make-flextranssum :name name
      :pred pred
      :fix fix
      :equiv equiv
      :case case
      :kind kind
      :count count
      :members members
      :measure measure
      :xvar xvar
      :inline inline
      :kwd-alist kwd-alist
      :recp (some-flextranssum-member-recursivep members))))

(define dts-member-implies-sum-thm
  (x member)
  (b* (((flextranssum x)) ((flextranssum-member member))
      (foo-p-when-subfoo-p (intern-in-package-of-symbol (cat (symbol-name x.pred)
            "-WHEN-"
            (symbol-name member.pred))
          x.pred)))
    `(defthm ,FTY::FOO-P-WHEN-SUBFOO-P
      (implies (,FTY::MEMBER.PRED ,FTY::X.XVAR)
        (,FTY::X.PRED ,FTY::X.XVAR))
      :hints (("Goal" :in-theory (enable* ,FTY::X.PRED tag-reasoning)))
      :rule-classes ((:rewrite :backchain-limit-lst 1)))))

(define dts-member-implies-sum-thms
  (x members)
  (if (atom members)
    nil
    (cons (dts-member-implies-sum-thm x (car members))
      (dts-member-implies-sum-thms x (cdr members)))))

(define dts-tag-equalities
  (xvar tags)
  (if (atom tags)
    nil
    (cons `(equal (tag ,FTY::XVAR) ,(CAR FTY::TAGS))
      (dts-tag-equalities xvar (cdr tags)))))

(define dts-tag-inequalities
  (xvar tags)
  (if (atom tags)
    nil
    (cons `(not (equal (tag ,FTY::XVAR) ,(CAR FTY::TAGS)))
      (dts-tag-inequalities xvar (cdr tags)))))

(define dts-by-tag-thm
  (x member)
  (b* (((flextranssum x)) ((flextranssum-member member))
      (subfoo-p-by-tag-when-foo-p (intern-in-package-of-symbol (cat (symbol-name member.pred)
            "-BY-TAG-WHEN-"
            (symbol-name x.pred))
          x.name)))
    `((defthm ,FTY::SUBFOO-P-BY-TAG-WHEN-FOO-P
       (implies (and (or . ,(FTY::DTS-TAG-EQUALITIES FTY::X.XVAR FTY::MEMBER.TAGS))
           (,FTY::X.PRED ,FTY::X.XVAR))
         (,FTY::MEMBER.PRED ,FTY::X.XVAR))
       :hints (("Goal" :in-theory (enable ,FTY::X.PRED)))
       :rule-classes ((:rewrite :backchain-limit-lst 1))) (add-to-ruleset tag-reasoning
        '(,FTY::SUBFOO-P-BY-TAG-WHEN-FOO-P)))))

(define dts-by-tag-thms
  (x members)
  (if (atom members)
    nil
    (append (dts-by-tag-thm x (car members))
      (dts-by-tag-thms x (cdr members)))))

(define dts-when-invalid-tag-thms
  (x)
  (b* (((flextranssum x)) (foo-p-when-invalid-tag (intern-in-package-of-symbol (cat (symbol-name x.pred) "-WHEN-INVALID-TAG")
          x.name))
      (all-tags (flextranssum-memberlist->tags x.members)))
    `((defthm ,FTY::FOO-P-WHEN-INVALID-TAG
       (implies (and . ,(FTY::DTS-TAG-INEQUALITIES FTY::X.XVAR FTY::ALL-TAGS))
         (not (,FTY::X.PRED ,FTY::X.XVAR)))
       :hints (("Goal" :in-theory (enable* ,FTY::X.PRED tag-reasoning)))
       :rule-classes ((:rewrite :backchain-limit-lst 0))) (add-to-ruleset tag-reasoning
        '(,FTY::FOO-P-WHEN-INVALID-TAG)))))

(define dts-fwd-thms
  (x)
  (b* (((flextranssum x)) (foo-p-when-invalid-tag (intern-in-package-of-symbol (cat (symbol-name x.pred) "-WHEN-INVALID-TAG")
          x.name))
      (tag-when-foo-p-forward (intern-in-package-of-symbol (cat "TAG-WHEN-" (symbol-name x.pred) "-FORWARD")
          x.name))
      (all-tags (flextranssum-memberlist->tags x.members)))
    `((defthm ,FTY::TAG-WHEN-FOO-P-FORWARD
       (implies (,FTY::X.PRED ,FTY::X.XVAR)
         (or . ,(FTY::DTS-TAG-EQUALITIES FTY::X.XVAR FTY::ALL-TAGS)))
       :hints (("Goal" :by ,FTY::FOO-P-WHEN-INVALID-TAG))
       :rule-classes ((:forward-chaining))) (add-to-ruleset tag-reasoning
        '(,FTY::TAG-WHEN-FOO-P-FORWARD)))))

(define flextranssum-pred-cases
  (members xvar)
  (b* (((when (atom members)) (raise "never get here")) ((flextranssum-member x1) (car members))
      ((when (atom (cdr members))) (list `(otherwise (,FTY::X1.PRED ,FTY::XVAR)))))
    (cons `(,FTY::X1.TAGS (,FTY::X1.PRED ,FTY::XVAR))
      (flextranssum-pred-cases (cdr members) xvar))))

(define flextranssum-predicate-def
  (x)
  (b* (((flextranssum x)) (consp-when-foop (intern-in-package-of-symbol (cat "CONSP-WHEN-" (symbol-name x.pred))
          x.name)))
    `(define ,FTY::X.PRED
      (,FTY::X.XVAR)
      :parents (,FTY::X.NAME)
      :progn t
      :short ,(STR::CAT "Recognizer for @(see " (XDOC::FULL-ESCAPE-SYMBOL FTY::X.NAME) ").")
      :measure ,FTY::X.MEASURE
      ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
      (case (tag ,FTY::X.XVAR)
        ,@(FTY::FLEXTRANSSUM-PRED-CASES FTY::X.MEMBERS FTY::X.XVAR))
      ///
      (defthm ,FTY::CONSP-WHEN-FOOP
        (implies (,FTY::X.PRED ,FTY::X.XVAR)
          (consp ,FTY::X.XVAR))
        :rule-classes :compound-recognizer)
      ,@(FTY::DTS-MEMBER-IMPLIES-SUM-THMS FTY::X FTY::X.MEMBERS)
      ,@(FTY::DTS-BY-TAG-THMS FTY::X FTY::X.MEMBERS)
      ,@(FTY::DTS-WHEN-INVALID-TAG-THMS FTY::X)
      ,@(FTY::DTS-FWD-THMS FTY::X))))

(define flextranssum-fix-cases
  (members xvar)
  (b* (((when (atom members)) (raise "never get here")) ((flextranssum-member x1) (car members))
      ((when (atom (cdr members))) (list `(otherwise (,FTY::X1.FIX ,FTY::XVAR)))))
    (cons `(,FTY::X1.TAGS (,FTY::X1.FIX ,FTY::XVAR))
      (flextranssum-fix-cases (cdr members) xvar))))

(define flextranssum-fix-def
  (x flagp)
  (b* (((flextranssum x)))
    `(define ,FTY::X.FIX
      ((,FTY::X.XVAR ,FTY::X.PRED))
      :parents (,FTY::X.NAME)
      :short ,(FTY::CAT "@(call " (XDOC::FULL-ESCAPE-SYMBOL FTY::X.FIX)
  ") is a @(see fty::fty) fixing function.")
      :long "<p>Note that in the execution this is just an inline identity function.</p>"
      :measure ,FTY::X.MEASURE
      ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
      ,@(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME))
      :returns (newx ,FTY::X.PRED
        :hints (("Goal" :in-theory (enable* ,FTY::X.PRED tag-reasoning)
           :expand ((,FTY::X.FIX ,FTY::X.XVAR)))))
      :verify-guards nil
      :progn t
      :inline t
      (mbe :logic (case (tag ,FTY::X.XVAR)
          ,@(FTY::FLEXTRANSSUM-FIX-CASES FTY::X.MEMBERS FTY::X.XVAR))
        :exec ,FTY::X.XVAR)
      ///)))

(define flextranssum-fix-postevents
  (x)
  (b* (((flextranssum x)) (tag-when-foo-p-forward (intern-in-package-of-symbol (cat "TAG-WHEN-" (symbol-name x.pred) "-FORWARD")
          x.name))
      (tag-of-foo-fix-forward (intern-in-package-of-symbol (cat "TAG-OF-" (symbol-name x.fix) "-FORWARD")
          x.name))
      (all-tags (flextranssum-memberlist->tags x.members)))
    `((defthm ,FTY::TAG-OF-FOO-FIX-FORWARD
       (or ,@(FTY::DTS-TAG-EQUALITIES `(,FTY::X.FIX ,FTY::X.XVAR) FTY::ALL-TAGS))
       :rule-classes ((:forward-chaining :trigger-terms ((tag (,FTY::X.FIX ,FTY::X.XVAR)))))
       :hints (("Goal" :in-theory (theory 'minimal-theory)
          :use ((:instance ,FTY::TAG-WHEN-FOO-P-FORWARD
             (,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR))))))) (add-to-ruleset tag-reasoning
        '(,FTY::TAG-OF-FOO-FIX-FORWARD)))))

(define flextranssum-count
  (x types)
  (declare (ignorable types))
  (b* (((flextranssum x)) ((unless x.count) nil))
    `((define ,FTY::X.COUNT
       ((,FTY::X.XVAR ,FTY::X.PRED))
       :returns (count natp :rule-classes :type-prescription)
       :measure (let ((,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
         ,FTY::X.MEASURE)
       ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
       :verify-guards nil
       :progn t
       (bozo-implement-flextranssum-count ,FTY::X.NAME)))))

(define flextranssum-count-post-events
  (x types)
  (declare (ignorable types))
  (b* (((flextranssum x)) ((unless x.count) nil))
    nil))

(define flextranssum-fns
  (x)
  (b* (((flextranssum x) x))
    (list x.pred x.fix)))

(define flextranssum-fix-when-pred-thm
  (x flagp)
  (b* (((flextranssum x)) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
            "-WHEN-"
            (symbol-name x.pred))
          x.fix)))
    `(defthm ,FTY::FOO-FIX-WHEN-FOO-P
      (implies (,FTY::X.PRED ,FTY::X.XVAR)
        (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR))
      :hints ('(:expand ((,FTY::X.PRED ,FTY::X.XVAR) (,FTY::X.FIX ,FTY::X.XVAR))
         :in-theory (disable ,FTY::X.FIX ,FTY::X.PRED))) . ,(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME)))))

(defun flextranssum-members-collect-fix-pred-pairs
  (members)
  (b* (((when (atom members)) nil) ((flextranssum-member x1) (car members)))
    (cons (cons x1.fix x1.pred)
      (flextranssum-members-collect-fix-pred-pairs (cdr members)))))

(defun flextranssum-collect-fix/pred-pairs
  (x)
  (flextranssum-members-collect-fix-pred-pairs (flextranssum->members x)))