		Search-engine friendly clone of the ACL2 documentation.

Matching-functions

Def-match-thms

Prove basic properties about a matching function.

The macro def-match-thms can be used to prove some basic theorems about a new matching function.

Note: typically, you should only want to use this macro if you are defining a new matching function. If you are just using existing matching functions like sin-match-lit to write your own lexer, this isn't what you want.

Form: (def-match-thms name)

This expands into a make-event. The name you give should be the name of some newly defined matching function. We look up the signature of name from the world and try to prove the matching function satisfies the following properties.

Well-Typed. The match is either a non-empty string or nil. Note that there is generally no reason to prove anything about the well-formedness of sin, itself.

Progress. The length of the input stream's contents never increases, and always decreases when text is matched.

Reconstruction. Appending the matched text onto the new input stream's contents yields the original input stream's contents. In other words, the matcher properly matches text from the front of the stream.

Graceful Failure. If there is no match, the stream is unchanged.

Match-Free Failure. (weak matchers only) If the weak matcher fails (i.e., it signals that okp is nil), then the match it returns is also nil.