def-error-checker

(in-package "ACL2")

(defxdoc def-error-checker
  :parents (error-checking)
  :short "Generate an error checking function
          and an associated macro abbreviation."
  :long (topstring (p "This macro generates an error checking function
     and an associated macro abbreviation of the following form:")
    (codeblock "(define <name> (<x1> ... <xn>"
      "                (description msgp)"
      "                (error-erp (not (null error-erp))"
      "                           "Flag to return in case of error.")"
      "                (error-val "Value to return in case of error.")"
      "                (ctx "Context for errors.")"
      "                state)"
      "  :returns (mv <erp>"
      "               <val>"
      "               state)"
      "  :mode <mode>"
      "  :verify-guards <verify-guards> ; may be absent"
      "  :parents <parents> ; may be absent"
      "  :short <short> ; may be absent"
      "  :long <long> ; may be absent"
      "  (b* (((unless <condition1>) (er-soft+"
      "                               ctx error-erp error-val . <message1>))"
      "       ..."
      "       ((unless <conditionm>) (er-soft+"
      "                               ctx error-erp error-val . <messagem>)))"
      "    (value <result>))"
      "  :no-function t)"
      ""
      "(defsection <name>$"
      "  :parents (<name>)"
      "  :short "Calls @(tsee <name>) with"
      "          @('ctx') and @('state') as the last two arguments.""
      "  :long "@(def <name>$)""
      "  (defmacro <name>$ (<x1'> ... <xn'> description error-erp error-val)"
      "    `(<name> ,<x1'> ... ,<xn'> description error-erp error-val ctx state)))")
    (p "where each @('<...>'),
     except @('<erp>'), @('<val>'), and @('<x1'>'), ..., @('<xn'>'),
     is supplied as argument to the macro:")
    (ul (li "@('<name>') is the name of the function,
      and, with a @('$') added at the end, the name of the macro.")
      (li "Each @('<xi>') is a symbol or
      an "
        (seetopic "std::extended-formals" "extended formal")
        ".
      Let @('<xi'>') be:
      @('<xi>') if @('<xi>') is a symbol;
      the name of the @('<xi>') extended formal otherwise.")
      (li "@('<erp>') is a "
        (seetopic "std::returns-specifiers"
          "return specifier")
        " that describes the error flag returned
      inside the "
        (seetopic "error-triple" "error triple")
        ".
      This return specifier is:
      @('(erp (implies erp (equal erp error-erp)))')
      if @('<mode>') is @(':logic'); and
      @('(erp "@('nil') or @('error-erp').")')
      if @('<mode>') is @(':program').")
      (li "@('<val>') is a "
        (seetopic "std::returns-specifiers"
          "return specifier")
        " that describes the value returned
      inside the "
        (seetopic "error-triple" "error triple")
        ".
      This return specifier depends on the @('<returns>') argument to the macro
      (see below for the complete list of arguments to the macro)
      and on @('<mode>'):
      if no @('<returns>') argument is supplied and @('<mode>') is @(':logic'),
      then @('<val>') is
      @('(val (and (implies erp (equal val error-val))
                   (implies (and (not erp) error-erp) (not val))))');
      if no @('<returns>') argument is supplied and @('<mode>') is @(':program'),
      then @('<val>') is
      @('(val "@('nil') if @('erp') is @('nil'), otherwise @('error-val').")');
      if a @('<returns>') argument is supplied,
      then @('<val>') is @('<returns>').")
      (li "@('<mode>') is either @(':logic') or @(':program').")
      (li "@('<verify-guards>') is either @('t') or @('nil').
      If @('<verify-guards>') is not supplied as argument,
      @(':verify-guards') is absent.")
      (li "@('<parents>') is a list of parent XDOC topics.
      If @('<parents>') is not supplied as argument, @(':parents') is absent.")
      (li "@('<short>') and @('<long>') are strings that document the function.
      If @('<short>') is not supplied as argument, @(':short') is absent.
      If @('<long>') is not supplied as argument, @(':long') is absent.")
      (li "Each @('<conditionj>') is a term
      whose evaluation checks a condition
      on the @('<x1>'), ..., @('<xn>') arguments.
      The conditions are checked in order.")
      (li "Each @('<messagej>') is a list that consists of
      a "
        (seetopic "fmt" "format string")
        "
      followed by up to 10 terms,
      whose values fill in the placeholders of the format string.
      Generally, one of these terms should be @('description')
      and it should correspond to a @('~@') placeholder
      in the format string,
      which is appropriate for the @(tsee msgp) type of @('description').
      The @('<messagej>') list is inserted into the @(tsee er-soft+) call,
      providing an error message when @('<conditionj>') is not satisfied
      (but the previous conditions are).")
      (li "@('<result>') is a term whose value is returned
      when all the conditions are satisfied."))
    (p "The generated formal arguments
     @('description'), @('error-erp'), and @('error-val')
     and the generated return variables @('erp') and @('val')
     are symbols with those names in the same package as
     the @('<name>') symbol used as the name of the generated function.")
    (p "The macro is called as follows:")
    (codeblock "(def-error-checker <name>"
      "  (<x1> ... <xn>)"
      "  :body ((<condition1> . <message1>) ... (<conditionm> . <messagem>))"
      "  :returns <returns> ; default not used"
      "  :result <result> ; default is nil"
      "  :mode <mode> ; default is :logic"
      "  :verify-guards <verify-guards> ; default not used"
      "  :parents <parents> ; default not used"
      "  :short <short> ; default not used"
      "  :long <long> ; default not used"
      "  )")
    (p "A table keeps track of all the successful calls to this macro,
     for "
      (seetopic "redundant-events" "redundancy")
      " checking.")))

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

(defsection def-error-checker-table
  :short "Table of successful @(tsee def-error-checker) calls."
  :long (topstring-p "This table records these calls as keys, with associated @('nil') values.
    This is used of redundancy checking.")
  (table def-error-checker-calls
    nil
    nil
    :guard (and (pseudo-event-formp key)
      (eq (car key) 'def-error-checker)
      (null val))))

(define def-error-checker-bindings
  ((conditions-messages true-list-listp) (error-erp symbolp "The @('error-erp') formal.")
    (error-val symbolp "The @('error-val') formal."))
  :returns (bindings true-list-listp)
  :short "Generate the @(tsee b*) bindings of the error checking function."
  :long (topstring (p "These are the")
    (codeblock "((unless <conditionj>) (er-soft+ ctx error-erp error-val . <messagej>))")
    (p "bindings,
     but a binder of the form @('(unless (not <condition>))')
     is turned into @('(when <condition>)') to improve readability."))
  (b* (((when (endp conditions-messages)) nil) (condition-message (car conditions-messages))
      (condition (car condition-message))
      (message (cdr condition-message))
      ((mv unless/when condition) (case-match condition
          (('not negated-condition) (mv 'when negated-condition))
          (& (mv 'unless condition))))
      (binding `((,UNLESS/WHEN ,CONDITION) (er-soft+ ctx ,ERROR-ERP ,ERROR-VAL ,@MESSAGE)))
      (bindings (def-error-checker-bindings (cdr conditions-messages)
          error-erp
          error-val)))
    (cons binding bindings)))

(define def-error-checker-x-symbols
  ((xs true-listp))
  :returns (x-symbols true-listp)
  :short "Turn each @('xi') symbol into itself
          and each @('xi') extended formal into its underlying symbol."
  (b* (((when (endp xs)) nil) (x (car xs))
      (x-symbol (if (atom x)
          x
          (car x)))
      (x-symbols (def-error-checker-x-symbols (cdr xs))))
    (cons x-symbol x-symbols)))

(define def-error-checker-fn
  ((name symbolp) (xs true-listp)
    returns
    (returns-supplied-p booleanp)
    (conditions-messages true-list-listp)
    result
    (mode (member-eq mode '(:logic :program)))
    (verify-guards booleanp)
    (verify-guards-supplied-p booleanp)
    (parents (symbol-listp parents))
    (parents-supplied-p booleanp)
    short
    (short-supplied-p booleanp)
    long
    (long-supplied-p booleanp)
    (def-error-checker-call pseudo-event-formp)
    state)
  :returns (function+macro pseudo-event-formp)
  :verify-guards nil
  :short "Generate the function and the macro."
  (b* (((when (assoc-equal def-error-checker-call
          (table-alist 'def-error-checker-calls (w state)))) '(value-triple :redundant)) (function-name name)
      (macro-name (add-suffix name "$"))
      (description (intern-in-package-of-symbol "DESCRIPTION" name))
      (error-erp (intern-in-package-of-symbol "ERROR-ERP" name))
      (error-val (intern-in-package-of-symbol "ERROR-VAL" name))
      (erp (intern-in-package-of-symbol "ERP" name))
      (val (intern-in-package-of-symbol "VAL" name))
      (function `(define ,FUNCTION-NAME
          (,@XS (,DESCRIPTION msgp)
            (,ERROR-ERP "Flag to return in case of error.")
            (,ERROR-VAL "Value to return in case of error.")
            (ctx "Context for errors.")
            state)
          :returns (mv ,(CASE MODE
   (:LOGIC `(,ERP (IMPLIES ,ERP (EQUAL ,ERP ,ERROR-ERP))))
   (:PROGRAM `(,ERP "@('nil') or @('error-erp')."))
   (T (IMPOSSIBLE)))
            ,(IF RETURNS-SUPPLIED-P
     RETURNS
     (CASE MODE
       (:LOGIC
        `(,VAL
          (AND (IMPLIES ,ERP (EQUAL ,VAL ,ERROR-VAL))
               (IMPLIES (AND (NOT ,ERP) ,ERROR-ERP) (NOT ,VAL)))))
       (:PROGRAM
        `(,VAL "@('nil') if @('erp') is @('nil'),
                                   otherwise @('error-val')."))
       (T (IMPOSSIBLE))))
            state)
          :mode ,MODE
          ,@(AND VERIFY-GUARDS-SUPPLIED-P (LIST :VERIFY-GUARDS VERIFY-GUARDS))
          ,@(AND PARENTS-SUPPLIED-P (LIST :PARENTS PARENTS))
          ,@(AND SHORT-SUPPLIED-P (LIST :SHORT SHORT))
          ,@(AND LONG-SUPPLIED-P (LIST :LONG LONG))
          (b* ,(DEF-ERROR-CHECKER-BINDINGS CONDITIONS-MESSAGES ERROR-ERP ERROR-VAL)
            (value ,RESULT))
          :no-function t))
      (x-symbols (def-error-checker-x-symbols xs))
      (macro `(defmacro ,MACRO-NAME
          (,@X-SYMBOLS ,DESCRIPTION ,ERROR-ERP ,ERROR-VAL)
          (list ',FUNCTION-NAME
            ,@X-SYMBOLS
            ,DESCRIPTION
            ,ERROR-ERP
            ,ERROR-VAL
            'ctx
            'state)))
      (section-short (concatenate 'string
          "Calls @(tsee "
          (string-downcase (symbol-name function-name))
          ") with @('ctx') and @('state')"
          " as the last two arguments."))
      (section-long (concatenate 'string
          "@(def "
          (string-downcase (symbol-name macro-name))
          ")"))
      (section `(defsection ,MACRO-NAME
          :parents (,FUNCTION-NAME)
          :short ,SECTION-SHORT
          :long ,SECTION-LONG
          ,MACRO)))
    `(progn ,FUNCTION ,SECTION)))

(defsection def-error-checker-macro-definition
  :short "Definition of the @(tsee def-error-checker) macro."
  :long (topstring-@def "def-error-checker")
  (defmacro def-error-checker
    (&whole def-error-checker-call
      name
      xs
      &key
      body
      (returns 'nil returns-supplied-p)
      (result 'nil)
      (mode ':logic)
      (verify-guards 'nil verify-guards-supplied-p)
      (parents 'nil parents-supplied-p)
      (short '"" short-supplied-p)
      (long '"" long-supplied-p))
    `(make-event (def-error-checker-fn ',NAME
        ',XS
        ',RETURNS
        ',RETURNS-SUPPLIED-P
        ',BODY
        ',RESULT
        ',MODE
        ',VERIFY-GUARDS
        ',VERIFY-GUARDS-SUPPLIED-P
        ',PARENTS
        ',PARENTS-SUPPLIED-P
        ',SHORT
        ',SHORT-SUPPLIED-P
        ',LONG
        ',LONG-SUPPLIED-P
        ',DEF-ERROR-CHECKER-CALL
        state))))