defsurj

(in-package "ACL2")

(defxdoc+ defsurj-implementation
  :parents (defsurj)
  :short "Implementation of @(tsee defsurj)."
  :long (topstring (p "We implement @(tsee defsurj) as a thin wrapper of @(tsee defmapping).
     We also provide a programmatic interface
     to retrieve surjective mappings from the "
      (seetopic "defmapping-table" "@('defmapping') table")
      "."))
  :order-subtopics t
  :default-parent t)

(define defsurj-lookup
  ((name symbolp) (wrld plist-worldp))
  :returns (info? "A @(tsee maybe-defmapping-infop).")
  :verify-guards nil
  :short "Return the information for the @(tsee defsurj) specified by name,
          or @('nil') if there is no @(tsee defsurj) with that name."
  :long (topstring-p "This is a wrapper of @(tsee defmapping-lookup)
    that makes sure that the @($\alpha$) conversion is a surjection
    (and also that the right inverse @($\beta$) conversion is an injection),
    i.e. that it has the @(':alpha-of-beta') theorem.
    It causes an error if that is not the case.")
  (b* ((info (defmapping-lookup name wrld)) ((when (not info)) nil)
      ((when (not (defmapping-info->alpha-of-beta info))) (raise "The mapping ~x0 does not have the :ALPHA-OF-BETA theorem."
          name)))
    info))

(defsection defsurj-macro-definition
  :short "Definition of the @(tsee defsurj) macro."
  :long (topstring (p "We call @(tsee defmapping-fn),
     passing @('t') as @(':alpha-of-beta-thm')
     and @('nil') as @(':beta-of-alpha-thm').
     Furthermore, we set the context to reference @(tsee defsurj).")
    (@def "defsurj"))
  (defmacro defsurj
    (&whole call
      name
      doma
      domb
      alpha
      beta
      &key
      (unconditional 'nil)
      (guard-thms 't)
      (thm-names 'nil)
      (thm-enable 'nil)
      (hints 'nil)
      (print ':result)
      (show-only 'nil))
    `(make-event-terse (defmapping-fn ',NAME
        ',DOMA
        ',DOMB
        ',ALPHA
        ',BETA
        nil
        t
        ',GUARD-THMS
        ',UNCONDITIONAL
        ',THM-NAMES
        ',THM-ENABLE
        ',HINTS
        ',PRINT
        ',SHOW-ONLY
        ',CALL
        (cons 'defsurj ',NAME)
        state)
      :suppress-errors ,(NOT PRINT))))