fty-set

(in-package "FTY")

(include-book "centaur/fty/database" :dir :system)

(include-book "centaur/fty/fty-parseutils" :dir :system)

(include-book "std/lists/list-defuns" :dir :system)

(include-book "std/osets/top" :dir :system)

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

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

(defxdoc defset
  :parents (fty-extensions fty std/osets)
  :short "Generate a <see topic='@(url fty::fty)'>fixtype</see>
          of <see topic='@(url set::std/osets)'>osets</see>
          whose elements have a specified fixtype."
  :long (topstring (h3 "Introduction")
    (p "This is analogous to
     @(tsee fty::deflist),
     @(tsee fty::defalist), and
     @(tsee fty::defomap).
     Besides the fixtype itself,
     this macro also generates some theorems about the fixtype.
     Future versions of this macro may generate more theorems, as needed.")
    (p "Aside from the recognizer, fixer, and equivalence for the fixtype,
     this macro does not generate any operations on the typed osets.
     Instead, the "
      (seetopic "acl2::std/osets" "generic oset operations")
      " can be used on typed osets.
     This macro generates theorems about
     the use of these generic operations on typed osets.")
    (p "Future versions of this macro may be modularized to provide
     a ``sub-macro'' that generates only the recognizer and theorems about it,
     without the fixtype (and without the fixer and equivalence),
     similarly to @(tsee std::deflist) and @(tsee std::defalist).
     That sub-macro could be called @('set::defset').")
    (h3 "General Form")
    (codeblock "(defset type"
      "        :elt-type ..."
      "        :elementp-of-nil ..."
      "        :pred ..."
      "        :fix ..."
      "        :equiv ..."
      "        :measure ..."
      "        :parents ..."
      "        :short ..."
      "        :long ..."
      "  )")
    (h3 "Inputs")
    (desc "@('type')"
      (p "The name of the new fixtype."))
    (desc "@(':elt-type')"
      (p "The (existing) fixtype of the elements of the new set fixtype."))
    (desc "@(':elementp-of-nil')"
      (p "Specifies whether @('nil') is in the element fixtype @(':elt-type').
      It must be @('t'), @('nil'), or @(':unknown') (the default).
      When @('t') or @('nil'), slightly better theorems are generated."))
    (desc "@(':pred')
     <br/>
     @(':fix')
     <br/>
     @(':equiv')"
      (p "The name of the recognizer, fixer, and equivalence for the new fixtype.")
      (p "The defaults are @('type') followed by
      @('-p'), @('-fix'), and @('-equiv')."))
    (desc "@(':parents')
     <br/>
     @(':short')
     <br/>
     @(':long')"
      (p "These are used to generate XDOC documentation
      for the topic @('name').")
      (p "If any of these is not supplied, the corresponding component
      is omitted from the generated XDOC topic."))
    (p "This macro currently does not perform a thorough validation of its inputs.
     Erroneous inputs may result in failures of the generated events.
     Errors should be easy to diagnose,
     also since this macro has a very simple and readable implementation.
     Future versions of this macro
     should perform more thorough input validation.")
    (h3 "Generated Events")
    (p "The following are generated, inclusive of XDOC documentation:")
    (ul (li "The recognizer, the fixer, the equivalence, and the fixtype.")
      (li "Several theorems about the recognizer, fixer, and equivalence."))
    (p "See the implementation, which uses a readable backquote notation,
     for details.")))

(defxdoc defset-implementation
  :parents (defset)
  :short "Implementation of @(tsee defset).")

(program)

(define check-flexset-already-defined
  (pred kwd-alist
    our-fixtypes
    ctx
    state)
  (declare (ignorable kwd-alist))
  (b* (((when (< 1 (len our-fixtypes))) nil) (existing-formals (fgetprop pred 'formals t (w state)))
      (already-defined (not (eq existing-formals t)))
      (- (and already-defined
          (cw "NOTE: Using existing definition of ~x0.~%"
            pred)))
      (- (or (not already-defined)
          (eql (len existing-formals) 1)
          (er hard?
            ctx
            "~x0 is already defined in an incompatible manner: it ~
                   should take exactly 1 input, but its formals are ~x1"
            pred
            existing-formals))))
    already-defined))

(define check-flexset-fix-already-defined
  (fix kwd-alist
    our-fixtypes
    ctx
    state)
  (declare (ignorable kwd-alist))
  (b* (((when (< 1 (len our-fixtypes))) nil) (fix$inline (add-suffix fix *inline-suffix*))
      (existing-formals (fgetprop fix$inline
          'formals
          t
          (w state)))
      (already-defined (not (eq existing-formals t)))
      (- (and already-defined
          (cw "NOTE: Using existing definition of ~x0.~%"
            fix)))
      (- (or (not already-defined)
          (eql (len existing-formals) 1)
          (er hard?
            ctx
            "~x0 is already defined in an incompatible manner: it ~
                   should take exactly 1 input, but its formals are ~x1"
            fix
            existing-formals))))
    already-defined))

(defconst *flexset-keywords*
  '(:pred :fix :equiv :count :elt-type :measure :measure-debug :xvar :elementp-of-nil :parents :short :long :no-count))

(define parse-flexset
  (x xvar
    our-fixtypes
    fixtypes
    state)
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed flexset: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist rest) (extract-keywords name
          *flexset-keywords*
          pre-///
          nil))
      (kwd-alist (append kwd-alist
          (table-alist 'defset-defaults (w state))))
      ((when rest) (raise "Malformed flexset: ~x0: after kind should be a keyword/value set."
          name))
      (elt-type (getarg :elt-type nil kwd-alist))
      ((unless (and (symbolp elt-type) elt-type)) (raise "Bad flexset ~x0: Element type must be a symbol"
          name))
      ((mv elt-type
         elt-fix
         elt-equiv
         recp) (get-pred/fix/equiv (getarg :elt-type nil kwd-alist)
          our-fixtypes
          fixtypes))
      (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))
      (elementp-of-nil (getarg :elementp-of-nil :unknown 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))
      (already-defined (check-flexset-already-defined pred
          kwd-alist
          our-fixtypes
          'defset
          state))
      (fix-already-defined (check-flexset-fix-already-defined fix
          kwd-alist
          our-fixtypes
          'defset
          state)))
    (make-flexset :name name
      :pred pred
      :fix fix
      :equiv equiv
      :count count
      :elt-type elt-type
      :elt-fix elt-fix
      :elt-equiv elt-equiv
      :elementp-of-nil elementp-of-nil
      :measure measure
      :kwd-alist (if post-///
        (cons (cons :///-events post-///) kwd-alist)
        kwd-alist)
      :xvar xvar
      :recp recp
      :already-definedp already-defined
      :fix-already-definedp fix-already-defined)))

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

(define flexset-collect-fix/pred-pairs
  (x)
  (b* (((flexset x)))
    (and x.elt-type
      x.elt-fix
      (list (cons x.elt-fix x.elt-type)))))

(define flexset-predicate-def
  (x)
  (b* (((flexset x)) (type-ref (concatenate 'string
          "@(tsee "
          (string-downcase (symbol-package-name x.name))
          "::"
          (string-downcase (symbol-name x.name))
          ")"))
      (y (intern-in-package-of-symbol "Y" x.pred))
      (a (intern-in-package-of-symbol "A" x.pred))
      (booleanp-of-pred (packn-pos (list 'booleanp-of x.pred) x.pred))
      (setp-when-pred (packn-pos (list 'setp-when- x.pred) x.pred))
      (elt-type-of-head-when-pred (packn-pos (list x.elt-type '-of-head-when- x.pred)
          x.pred))
      (pred-of-tail-when-pred (packn-pos (list x.pred '-of-tail-when- x.pred)
          x.pred))
      (pred-of-insert (packn-pos (list x.pred '-of-insert) x.pred))
      (elt-type-when-in-pred-binds-free-xvar (packn-pos (list x.elt-type
            '-when-in-
            x.pred
            '-binds-free-
            x.xvar)
          x.pred))
      (not-in-pred-when-not-elt-type (packn-pos (list 'not-in-
            x.pred
            '-when-not-
            x.elt-type)
          x.pred))
      (pred-of-intersect (packn-pos (list x.pred '-of-intersect)
          x.pred))
      (pred-of-union (packn-pos (list x.pred '-of-union) x.pred))
      (pred-of-difference (packn-pos (list x.pred '-of-difference)
          x.pred))
      (pred-of-delete (packn-pos (list x.pred '-of-delete) x.pred)))
    (if x.already-definedp
      '(progn)
      `(define ,FTY::X.PRED
        (,FTY::X.XVAR)
        :parents (,FTY::X.NAME)
        :short ,(CONCATENATE 'STRING "Recognizer for " FTY::TYPE-REF ".")
        ,@(IF FTY::X.MEASURE
      `(:MEASURE ,FTY::X.MEASURE)
      NIL)
        (if (atom ,FTY::X.XVAR)
          (null ,FTY::X.XVAR)
          (and (,FTY::X.ELT-TYPE (car ,FTY::X.XVAR))
            (or (null (cdr ,FTY::X.XVAR))
              (and (consp (cdr ,FTY::X.XVAR))
                (fast-<< (car ,FTY::X.XVAR) (cadr ,FTY::X.XVAR))
                (,FTY::X.PRED (cdr ,FTY::X.XVAR))))))
        :no-function t
        ///
        (defrule ,FTY::BOOLEANP-OF-PRED
          (booleanp (,FTY::X.PRED ,FTY::X.XVAR)))
        (defrule ,FTY::SETP-WHEN-PRED
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            (setp ,FTY::X.XVAR))
          :induct t
          :enable setp
          :rule-classes (:rewrite))
        (defrule ,FTY::ELT-TYPE-OF-HEAD-WHEN-PRED
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            ,(COND
  ((EQ FTY::X.ELEMENTP-OF-NIL T) `(,FTY::X.ELT-TYPE (SET::HEAD ,FTY::X.XVAR)))
  ((EQ FTY::X.ELEMENTP-OF-NIL NIL)
   `(EQUAL (,FTY::X.ELT-TYPE (SET::HEAD ,FTY::X.XVAR))
           (NOT (SET::EMPTYP ,FTY::X.XVAR))))
  (T
   `(FTY::IMPLIES (NOT (SET::EMPTYP ,FTY::X.XVAR))
     (,FTY::X.ELT-TYPE (SET::HEAD ,FTY::X.XVAR))))))
          :enable (head emptyp))
        (defrule ,FTY::PRED-OF-TAIL-WHEN-PRED
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            (,FTY::X.PRED (tail ,FTY::X.XVAR)))
          :enable tail)
        (defrule ,FTY::PRED-OF-INSERT
          (equal (,FTY::X.PRED (insert ,FTY::A ,FTY::X.XVAR))
            (and (,FTY::X.ELT-TYPE ,FTY::A)
              (,FTY::X.PRED (sfix ,FTY::X.XVAR))))
          :induct t
          :enable (insert emptyp
            head
            tail
            setp
            sfix))
        (defrule ,FTY::ELT-TYPE-WHEN-IN-PRED-BINDS-FREE-XVAR
          (implies (and (in ,FTY::A ,FTY::X.XVAR)
              (,FTY::X.PRED ,FTY::X.XVAR))
            (,FTY::X.ELT-TYPE ,FTY::A))
          :induct t
          :enable (in head))
        (defruled ,FTY::NOT-IN-PRED-WHEN-NOT-ELT-TYPE
          (implies (and (,FTY::X.PRED ,FTY::X.XVAR)
              (not (,FTY::X.ELT-TYPE ,FTY::A)))
            (not (in ,FTY::A ,FTY::X.XVAR))))
        (defrule ,FTY::PRED-OF-UNION
          (equal (,FTY::X.PRED (union ,FTY::X.XVAR ,FTY::Y))
            (and (,FTY::X.PRED (sfix ,FTY::X.XVAR))
              (,FTY::X.PRED (sfix ,FTY::Y))))
          :induct t
          :enable (union emptyp setp head tail sfix))
        (defrule ,FTY::PRED-OF-INTERSECT
          (implies (or (,FTY::X.PRED ,FTY::X.XVAR) (,FTY::X.PRED ,FTY::Y))
            (,FTY::X.PRED (intersect ,FTY::X.XVAR ,FTY::Y)))
          :induct t
          :enable intersect)
        (defrule ,FTY::PRED-OF-DIFFERENCE
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            (,FTY::X.PRED (difference ,FTY::X.XVAR ,FTY::Y)))
          :induct t
          :enable difference)
        (defrule ,FTY::PRED-OF-DELETE
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            (,FTY::X.PRED (delete ,FTY::A ,FTY::X.XVAR)))
          :induct t
          :enable delete)))))

(define flexset-fix-def
  (x flagp)
  (b* (((flexset x)) (pred-of-fix (packn-pos (list x.pred '-of- x.fix)
          x.name))
      (fix-when-pred (packn-pos (list x.fix '-when- x.pred)
          x.name))
      (emptyp-fix (packn-pos (list 'emptyp- x.fix) x.name))
      (emptyp-of-fix (packn-pos (list 'emptyp-of- x.fix) x.pred)))
    (if x.fix-already-definedp
      '(progn)
      `(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 usual @(see fty::fty) set fixing function.")
        :long ,(FTY::CAT "<p>In the logic, we apply @(see? "
  (XDOC::FULL-ESCAPE-SYMBOL FTY::X.ELT-FIX)
  ") to each member of the x.  In the execution, none of
                    that is actually necessary and this is just an inlined
                    identity function.</p>")
        ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
        ,@(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME))
        :progn t
        (mbe :logic (if (,FTY::X.PRED ,FTY::X.XVAR)
            ,FTY::X.XVAR
            nil)
          :exec ,FTY::X.XVAR)
        :no-function t
        ///
        (defrule ,FTY::PRED-OF-FIX
          (,FTY::X.PRED (,FTY::X.FIX ,FTY::X.XVAR)))
        (defrule ,FTY::FIX-WHEN-PRED
          (implies (,FTY::X.PRED ,FTY::X.XVAR)
            (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR)))
        (defrule ,FTY::EMPTYP-FIX
          (implies (or (emptyp ,FTY::X.XVAR)
              (not (,FTY::X.PRED ,FTY::X.XVAR)))
            (emptyp (,FTY::X.FIX ,FTY::X.XVAR))))
        (defruled ,FTY::EMPTYP-OF-FIX
          (equal (emptyp (,FTY::X.FIX ,FTY::X.XVAR))
            (or (not (,FTY::X.PRED ,FTY::X.XVAR))
              (emptyp ,FTY::X.XVAR))))))))

(define flexset-fix-postevents
  (x)
  :ignore-ok t
  :irrelevant-formals-ok t
  nil)

(define flexset-fix-when-pred-thm
  (x flagp)
  (b* (((flexset x)) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
            "-WHEN-"
            (symbol-name x.pred))
          x.fix)))
    (if flagp
      `(defthm ,FTY::FOO-FIX-WHEN-FOO-P
        t
        :flag ,FTY::X.NAME
        :skip t)
      '(progn))))

(defun flexset-count
  (x types)
  (b* (((flexset x)) ((unless x.count) nil)
      (eltcount (flextypes-find-count-for-pred x.elt-type
          types)))
    `((define ,FTY::X.COUNT
       ((,FTY::X.XVAR ,FTY::X.PRED))
       :returns (count natp
         :rule-classes :type-prescription :hints ('(:expand (,FTY::X.COUNT ,FTY::X.XVAR)
            :in-theory (disable ,FTY::X.COUNT))))
       :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
       (if (or (emptyp ,FTY::X.XVAR)
           (not (,FTY::X.PRED ,FTY::X.XVAR)))
         1
         (+ 1
           ,@(AND FTY::ELTCOUNT `((,FTY::ELTCOUNT (SET::HEAD ,FTY::X.XVAR))))
           (,FTY::X.COUNT (tail ,FTY::X.XVAR))))))))

(defun flexset-count-post-events
  (x types)
  (b* (((flexset x)) ((unless x.count) nil)
      (eltcount (flextypes-find-count-for-pred x.elt-type
          types))
      (foo-count-of-insert (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-INSERT")
          x.count))
      (foo-count-of-head (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-HEAD")
          x.count))
      (foo-count-of-tail (intern-in-package-of-symbol (cat (symbol-name x.count) "-OF-TAIL")
          x.count))
      (foo-count-when-emptyp (intern-in-package-of-symbol (cat (symbol-name x.count) "-WHEN-EMPTYP")
          x.count))
      (foo-count-when-not-emptyp (intern-in-package-of-symbol (cat (symbol-name x.count) "-WHEN-NOT-EMPTYP")
          x.count)))
    `((defthm ,FTY::FOO-COUNT-WHEN-EMPTYP
       (implies (emptyp ,FTY::X.XVAR)
         (equal (,FTY::X.COUNT ,FTY::X.XVAR) 1))
       :hints (("Goal" :in-theory (enable ,FTY::X.COUNT)))) (defthm ,FTY::FOO-COUNT-WHEN-NOT-EMPTYP
        (implies (and (not (emptyp ,FTY::X.XVAR))
            (,FTY::X.PRED ,FTY::X.XVAR))
          (equal (,FTY::X.COUNT ,FTY::X.XVAR)
            (+ 1
              ,@(AND FTY::ELTCOUNT `((,FTY::ELTCOUNT (SET::HEAD ,FTY::X.XVAR))))
              (,FTY::X.COUNT (tail ,FTY::X.XVAR)))))
        :hints (("Goal" :in-theory (enable ,FTY::X.COUNT))))
      ,@(AND FTY::ELTCOUNT
       `((FTY::DEFTHM ,FTY::FOO-COUNT-OF-HEAD
          (FTY::IMPLIES
           (AND (NOT (FTY::EMPTYP ,FTY::X.XVAR)) (,FTY::X.PRED ,FTY::X.XVAR))
           (< (,FTY::ELTCOUNT (SET::HEAD ,FTY::X.XVAR))
              (,FTY::X.COUNT ,FTY::X.XVAR)))
          :RULE-CLASSES :LINEAR)))
      (defthm ,FTY::FOO-COUNT-OF-TAIL
        (implies (and (not (emptyp ,FTY::X.XVAR))
            (,FTY::X.PRED ,FTY::X.XVAR))
          (< (,FTY::X.COUNT (tail ,FTY::X.XVAR))
            (,FTY::X.COUNT ,FTY::X.XVAR)))
        :rule-classes :linear :hints (("Goal" :in-theory (enable ,FTY::X.COUNT))))
      (defthm ,FTY::FOO-COUNT-OF-INSERT
        (implies (and (,FTY::X.PRED b)
            (,FTY::X.ELT-TYPE a)
            (not (in a b)))
          ,(IF FTY::ELTCOUNT
     `(EQUAL (,FTY::X.COUNT (SET::INSERT FTY::A FTY::B))
             (+ 1 (,FTY::ELTCOUNT FTY::A) (,FTY::X.COUNT FTY::B)))
     `(> (,FTY::X.COUNT (SET::INSERT FTY::A FTY::B)) (,FTY::X.COUNT FTY::B))))
        :hints (("Goal" :in-theory (enable (:i weak-insert-induction))
           :induct (weak-insert-induction a b)))
        :rule-classes :linear))))