|
|
|---|
|
|
|
|---|
Core macro for writing recursive-descent parsers, used throughout VL's parsing routines.
(defparser name (x y) [:guard (blah x y)] [:verify-guards { t, nil }] [:count { weak, strong, strong-on-value }] [:result (blah-blah val)] [:resultp-of-nil { t, nil }] [:true-listp { t, nil }] [:fails { never, gracefully }] [:result-hints (("Goal" ...))] [(declare ...)] [(declare ...)] <body> ;; usually (seq tokens pstate ...) ) <p>Such an event always introduces:</p> <ul> <li>A macro, (foo x y), that just calls (foo-fn x y tokstream).</li> <li>A function, (foo-fn x y tokstream), that implicitly binds the variable __function__ to 'foo and otherwise has the given bodies and declares, with the :guard thrown in if that is provided.</li> <li>An add-macro-alias so foo can be used in place of foo-fn in enables and disables.</li> <li>An untranslate-pattern so that (foo-fn x y tokstream) is displayed as (foo x y) during theorems.</li. </ul> <p>In addition to these events, several theorems may be generated depending upon the optional keyword arguments given above. In particular, if any of the following keywords are provided, then some theorems will be generated:</p> @({ result, resultp-of-nil, true-listp, count, fails
The RESULT theorem will forcibly assume (vl-tokenlist-p tokens), and you can also sort of assume that no error has occurred (the actual rule we produce is influenced by the RESULTP-OF-NIL setting). All you have to say is the property you want to establish, targetting the variable VAL.
The TRUE-LISTP flag may be set when foo unconditionally returns a true-listp, and is only used to generate a type-prescription rule for foo.
The FAILS keyword can be used to introduce a theorem about the failure behavior of a parsing function. Recall that we have standardized upon the (mv err val tokens) format for all of our parsing functions. We say that our functions fail GRACEFULLY if, whenever they return a non-nil err, the val returned is nil. Almost all of our functions fail gracefully, and we can sometimes exploit this fact along with resultp-of-nil to create stronger rewrite rules for the result theorem. Another common paradigm is a parser that NEVER fails -- e.g., perhaps it is for an "optional" production or for "zero or more occurrences" of something.
The COUNT theorem is used to create a theorem about (len tokens). In practice, most parsers have a STRONG count-decreasing behavior, which is to say that they always decrease the length on success. But functions which never fail, such as "match zero or more" parsers, usually have a weaker property which we call STRONG-ON-VALUE, which means that whenever the value they return is non-nil, the count decreases. We also allow for WEAK count theorems, which just say the count never increases, but these do not occur very frequently.