		Search-engine friendly clone of the ACL2 documentation.

Parser

Reterr-msg

Return an error consisting of a message with information about what was expected and what was found where.

This is used by our lexing and parsing functions to more concisely return more uniform error messages.

This macro assumes that a suitable local macro reterr is in scope (see error-value tuples), which is the case for our lexing and parsing functions. This macro takes as inputs four terms, which must evaluate to messages (i.e. values satisfying msgp). Those are used to form a larger message, in the manner that should be obvious from the body of this macro. Note that the fourth term is optional, in case we want to provide additional information.

For now we also include, at the end of the message, an indication of the ACL2 function that caused the error. This is useful as we are debugging the parser, but we may remove it once the parser is more tested or even verified.

Macro: reterr-msg

(defmacro reterr-msg (&key where expected found extra)
 (cons
  'reterr
  (cons
   (cons
    'msg
    (cons
     '"Expected ~@0 at ~@1; found ~@2 instead.~@3~%~
                 [from function ~x4]~%"
     (cons
      expected
      (cons
       where
       (cons found
             (cons (if extra (cons 'msg
                                   (cons '" ~@0" (cons extra 'nil)))
                     "")
                   '(__function__)))))))
   'nil)))