deffixer

(in-package "STD")

(include-book "std/system/maybe-pseudo-event-formp" :dir :system)

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

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

(include-book "xdoc/defxdoc-plus" :dir :system)

(defxdoc deffixer
  :parents (std/util)
  :short "Introduce a fixer for a predicate."
  :long (topstring (h3 "Introduction")
    (p "Given a unary predicate,
     a fixer (i.e. fixing function) for the predicate
     can be defined in a standard way.
     This macro automates this.")
    (p "This macro may be extended
     to accommodate variations in the definition of fixers.")
    (h3 "General Form")
    (codeblock "(deffixer name"
      "          :pred ..."
      "          :param ..."
      "          :body-fix ..."
      "          :parents ..."
      "          :short ..."
      "          :long ..."
      "  )")
    (h3 "Inputs")
    (desc "@('name')"
      (p "A symbol that specifies the name of the fixer."))
    (desc "@(':pred')"
      (p "A symbol that names a unary predicate.
      This is the predicate that the fixer is for."))
    (desc "@(':param')"
      (p "The formal parameter to use for the fixer.")
      (p "If not supplied, it defaults to @('x'),
      in the same package as @('name')."))
    (desc "@(':body-fix')"
      (p "A term that defines the value of the fixer
      when the argument is not in the predicate.
      Its only free variables, if any,
      must be just the parameter of the fixer (see @(':param')).
      It must be the case that this term satisfies the predicate
      when the parameter of the fixer does not."))
    (desc (list "@(':parents')" "@(':short')" "@(':long')")
      (p "These, if present, are added to
      the XDOC topic generated for the fixer."))
    (h3 "Generated Events")
    (desc "@('name')"
      (p "The fixer, with the predicate as guard and the following body:")
      (codeblock "(mbe :logic (if (pred param) param body-fix)"
        "     :exec param)"))
    (desc "@('pred-of-name')"
      (p "A rewrite rule asserting that the fixer always satisfies the predicate:")
      (codeblock "(pred (name param))"))
    (desc "@('pred-when-name')"
      (p "A rewrite rule asserting that the fixer rewrites to the parameter
      when the predicate holds:")
      (codeblock "(implies (pred param)"
        "         (equal (name param)"
        "                param))"))
    (p "The above items are generated in a @(tsee define) for the fixer.")))

(defxdoc+ deffixer-implementation
  :parents (deffixer)
  :short "Implementation of @(tsee deffixer)."
  :order-subtopics t
  :default-parent t)

(define deffixer-fn
  (name pred
    param
    body-fix
    parents
    (parents-supplied-p booleanp)
    short
    (short-supplied-p booleanp)
    long
    (long-supplied-p booleanp))
  :returns (event maybe-pseudo-event-formp)
  :short "Event generated by @(tsee deffixer)."
  (b* (((unless (symbolp name)) (raise "The NAME input must be a symbol, ~
                but it is ~x0 instead."
         name)) ((unless (symbolp pred)) (raise "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
          pred))
      ((unless (symbolp param)) (raise "The :PARAM input must be a symbol, ~
                but it is ~x0 instead."
          param))
      (pkg (symbol-package-name name))
      (pkg (if (equal pkg *main-lisp-package-name*)
          "ACL2"
          pkg))
      (pkg-witness (pkg-witness pkg))
      (param (or param
          (intern-in-package-of-symbol "X" pkg-witness)))
      (fixed-param (packn-pos (list 'fixed- param) pkg-witness))
      (name-when-pred-thm `(defrule ,(PACKN-POS (LIST STD::NAME 'STD::-WHEN- STD::PRED) STD::PKG-WITNESS)
          (implies (,STD::PRED ,STD::PARAM)
            (equal (,STD::NAME ,STD::PARAM) ,STD::PARAM))))
      (name-fn `(define ,STD::NAME
          ((,STD::PARAM ,STD::PRED))
          :returns (,STD::FIXED-PARAM ,STD::PRED)
          ,@(AND STD::PARENTS-SUPPLIED-P (LIST :PARENTS STD::PARENTS))
          ,@(AND STD::SHORT-SUPPLIED-P (LIST :SHORT STD::SHORT))
          ,@(AND STD::LONG-SUPPLIED-P (LIST :LONG STD::LONG))
          (mbe :logic (if (,STD::PRED ,STD::PARAM)
              ,STD::PARAM
              ,STD::BODY-FIX)
            :exec ,STD::PARAM)
          :no-function t
          ///
          ,STD::NAME-WHEN-PRED-THM)))
    `(encapsulate nil (logic) ,STD::NAME-FN)))

(defsection deffixer-macro-definition
  :short "Definition of the @(tsee deffixer) macro."
  :long (topstring-@def "deffixer")
  (defmacro deffixer
    (name &key
      pred
      param
      body-fix
      (parents 'nil parents-supplied-p)
      (short 'nil short-supplied-p)
      (long 'nil long-supplied-p))
    `(make-event (deffixer-fn ',STD::NAME
        ',STD::PRED
        ',STD::PARAM
        ',STD::BODY-FIX
        ',STD::PARENTS
        ,STD::PARENTS-SUPPLIED-P
        ,STD::SHORT
        ,STD::SHORT-SUPPLIED-P
        ,STD::LONG
        ,STD::LONG-SUPPLIED-P))))