defconstrained-recognizer

(in-package "STD")

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

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

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

(defxdoc defconstrained-recognizer
  :parents (std/util)
  :short "Introduce a constrained recognizer."
  :long (topstring (h3 "Introduction")
    (p "ACL2 support the introduction of
     arbitrary consistency-preserving constrained functions
     via @(tsee encapsulate).
     The @('defconstrained-recognizer') macro abbreviates @(tsee encapsulate)s
     to introduce certain common kinds of constrained recognizers.")
    (p "This macro currently provides just a few options.
     More will be added as the need for them arises.")
    (h3 "General Form")
    (codeblock "(defconstrained-recognizer name"
      "                           :nonempty ..."
      "  )")
    (h3 "Inputs")
    (desc "@('name')"
      (p "The name of the recognizer."))
    (desc "@(':nonempty')"
      (p "Determines whether the recognizer is constrained be non-empty or not,
      and if so it provides the name of a witness function
      for the non-emptiness of the recognizer.")
      (p "It must be one of the following:")
      (ul (li "A symbol that is not @('nil').
       In this case, the recognizer is constrained to be non-empty,
       by introducing, besides the recognizer,
       also a nullary function, whose name is this input,
       constrained to satisfy the recognizer.")
        (li "@('nil') (the default).
       In this case, the recognizer is not constrained to be non-empty,
       i.e. it may be empty or non-empty.
       No constrained nullary function is introduced in this case.")))
    (h3 "Generated Events")
    (p "This macro generates an @(tsee encapsulate)
     that introduces the following functions
     with the following constraining theorems.")
    (desc "@('name')"
      (p "The recognizer, a unary function.")
      (p "Its executable counterpart is disabled."))
    (desc "@('booleanp-of-name')"
      (p "A rewrite and type prescription rule
      saying that the recognizer returns a boolean:")
      (codeblock "(defthm booleanp-of-name"
        "  (booleanp (name x))"
        "  :rule-classes (:rewrite :type-prescription))"))
    (desc "@('nonempty')"
      (p "A nullary function witnessing the non-emptiness of the recognizer.")
      (p "This is generated exactly when @(':nonempty') is not @('nil')."))
    (desc "@('name-of-nonempty')"
      (codeblock "(defthm name-of-nonempty"
        "  (name (nonempty)))")
      (p "This is generated exactly when @(':nonempty') is not @('nil')."))))

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

(define defconstrained-recognizer-fn
  (name nonempty)
  :returns (event maybe-pseudo-event-formp)
  :short "Event generated by @(tsee defconstrained-recognizer)."
  (b* (((unless (symbolp name)) (raise "The NAME input must be a symbol, ~
                but it is ~x0 instead."
         name)) ((unless (symbolp nonempty)) (raise "The :NONEMPTY input must be a symbol, ~
                but it is ~x0 instead."
          nonempty))
      (pkg (symbol-package-name name))
      (pkg (if (equal pkg *main-lisp-package-name*)
          "ACL2"
          pkg))
      (pkg-witness (pkg-witness pkg))
      (x (intern-in-package-of-symbol "X" pkg-witness))
      (name-sig `((,STD::NAME *) => *))
      (nonempty-sig? (and nonempty (list `((,STD::NONEMPTY) => *))))
      (name-def `(local (defun ,STD::NAME (,STD::X) (declare (ignore ,STD::X)) t)))
      (nonempty-def? (and nonempty
          (list `(local (defun ,STD::NONEMPTY nil nil)))))
      (booleanp-of-name `(defthm ,(PACKN-POS (LIST 'STD::BOOLEANP-OF- STD::NAME) STD::PKG-WITNESS)
          (booleanp (,STD::NAME ,STD::X))
          :rule-classes (:rewrite :type-prescription)))
      (name-of-nonempty? (and nonempty
          (list `(defthm ,(PACKN-POS (LIST STD::NAME 'STD::-OF- STD::NONEMPTY) STD::PKG-WITNESS)
              (,STD::NAME (,STD::NONEMPTY)))))))
    `(encapsulate nil
      (logic)
      (encapsulate (,STD::NAME-SIG ,@STD::NONEMPTY-SIG?)
        ,STD::NAME-DEF
        ,@STD::NONEMPTY-DEF?
        ,STD::BOOLEANP-OF-NAME
        ,@STD::NAME-OF-NONEMPTY?))))

(defsection defconstrained-recognizer-definition
  :short "Definition of the @(tsee defconstrained-recognizer) macro."
  :long (topstring-@def "defconstrained-recognizer")
  (defmacro defconstrained-recognizer
    (name &key nonempty)
    `(make-event (defconstrained-recognizer-fn ',STD::NAME
        ',STD::NONEMPTY))))