• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
      • Example-lexer
      • Sin
      • Matching-functions
        • Sin-match-until-lit
        • Sin-match-lit
        • Sin-match-charset*
        • Sin-match-some-lit
        • Sin-match-through-lit
        • Sin-match-everything
        • Def-match-thms
      • Def-sin-progress
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Matching-functions

Sin-match-some-lit

Match any one of several string literals.

Signature

(sin-match-some-lit lits sin) → (mv match sin)

Arguments

lits — The literals to search for, in order.
    Guard (string-listp lits).

sin — The sin stobj.

Returns

match — The first literal in lits that is found at the start of the input stream; nil if none are found.
    Type (or (stringp match) (not match)).

sin — The remainder of the input stream, with the match removed, if applicable.

Since the lits are searched in order, it is often useful to search for longer literals first, e.g., when lexing C operators you might want to search for "++" before "+".

Corner case: like sin-match-lit, we will always fail to match the empty string.

Examples:

(sin-match-some-lit '("applesauce" "apple" "snake")
                    [applesnake])
 -->
("apple" [snake])

(sin-match-some-lit '("applesauce" "apple" "snake")
                    [applesaucesnake])
 -->
("applesauce" [snake])

(sin-match-some-lit '("applesauce" "apple" "snake")
                    [serpent])
 -->
(nil [serpent])

Definitions and Theorems

Function: sin-match-some-lit

(defun sin-match-some-lit (lits sin)
       (declare (xargs :stobjs (sin)))
       (declare (xargs :guard (string-listp lits)))
       (let ((__function__ 'sin-match-some-lit))
            (declare (ignorable __function__))
            (b* (((when (atom lits)) (mv nil sin))
                 ((mv match1 sin)
                  (sin-match-lit (car lits) sin))
                 ((when match1) (mv match1 sin)))
                (sin-match-some-lit (cdr lits) sin))))

Theorem: return-type-of-sin-match-some-lit.match

(defthm return-type-of-sin-match-some-lit.match
        (b* (((mv ?match ?sin)
              (sin-match-some-lit lits sin)))
            (or (stringp match) (not match)))
        :rule-classes :type-prescription)

Theorem: stringp-of-sin-match-some-lit.match

(defthm stringp-of-sin-match-some-lit.match
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (equal (stringp match)
                   (if match t nil))))

Theorem: non-empty-of-sin-match-some-lit.match

(defthm non-empty-of-sin-match-some-lit.match
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (equal (equal match "") nil)))

Theorem: sin-match-some-lit-progress-weak

(defthm sin-match-some-lit-progress-weak
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (<= (len (strin-left new-sin))
                (len (strin-left sin))))
        :rule-classes ((:rewrite) (:linear)))

Theorem: sin-match-some-lit-progress-strong

(defthm sin-match-some-lit-progress-strong
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (implies match
                     (< (len (strin-left new-sin))
                        (len (strin-left sin)))))
        :rule-classes ((:rewrite) (:linear)))

Theorem: sin-match-some-lit-reconstruction

(defthm sin-match-some-lit-reconstruction
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (equal (append (explode match)
                           (strin-left new-sin))
                   (strin-left sin))))

Theorem: sin-match-some-lit-graceful-failure

(defthm sin-match-some-lit-graceful-failure
        (b* (((mv ?match ?new-sin)
              (sin-match-some-lit lits sin)))
            (implies (not match)
                     (equal new-sin sin))))

Theorem: member-of-sin-match-some-lit

(defthm member-of-sin-match-some-lit
        (b* (((mv match ?new-sin)
              (sin-match-some-lit lits sin)))
            (implies match (member match lits))))