		Search-engine friendly clone of the ACL2 documentation.

Regex

Regex-get

Lookup a string in the regular expression alist.

Signature
(regex-get str alist) → key-value-pair
Arguments: str — String to lookup.
Guard (stringp str).; alist — Alistp where keys are regular expressions in string form and the values are of an unspecified type.
Guard (string-keyed-alist-p alist).
Returns: key-value-pair — Matching regular expression paired with its value. Nil if no entry is found. Note that this is an exact match, which is different from the functionality of grep, which returns substrings that match.
Type (equal (consp key-value-pair) (if key-value-pair t nil)), given the guard.

Warning: this is likely to be a pretty slow way of doing things -- but we currently have no experimental evidence that indicates whether this performance is unacceptable. If you're looking for a place to suspect of bad performance, this could be a good place to start.

It is likely that the user will want to use regex-get to implement a function that returns a value of a specific type. Here, we show a couple events that we needed to provide to prove that our wrapper for regex-get returns an acl2-number-listp. We expect that users in similar situations will need comparable lemmas. Such composability is similar to the approach available and documented in the book defexec/other-apps/records/records.

We now begin our approach. First we setup an alist to serve as our regex dictionary:

(include-book "std/util/defalist" :dir :system)

(std::defalist dictionary-p (x)
  :key (stringp x)
  :val (acl2-number-listp x)
  :true-listp t)

Next we establish two lemmas that help us specify the return type for what will be our use of regex-get:

(include-book "projects/regex/regex-ui" :dir :system)

(defthm dictionary-p-is-string-keyed-alist-p
  (implies (dictionary-p x)
           (string-keyed-alist-p x))
  :hints (("Goal" :in-theory (enable string-keyed-alist-p))))

(defthm regex-get-of-dictionary-p-returns-terminal-list-p
  (implies (and (stringp x)
                (dictionary-p dict))
           (acl2-number-listp (cdr (regex-get x dict))))
  :hints (("Goal" :in-theory (enable regex-get))))

Which enables ACL2 to admit our lookup function:

(include-book "std/util/define" :dir :system)

(define dictionary-lookup ((key stringp)
                           (dictionary dictionary-p))
  :returns (ans (acl2-number-listp ans)
                "The list of integers associated with the given key"
                :hyp :fguard)
  (let ((val (regex-get key dictionary)))
    (if (consp val)
        (cdr val)
      nil))) ; return value in the atom case is chosen by user

Definitions and Theorems

Function: regex-get

(defun regex-get (str alist)
  (declare (xargs :guard (and (stringp str)
                              (string-keyed-alist-p alist))))
  (let ((__function__ 'regex-get))
    (declare (ignorable __function__))
    (if (atom alist)
        nil
      (mv-let (err whole substrs)
              (do-regex-match str (caar alist)
                              (parse-options 'ere nil nil nil nil))
        (declare (ignore substrs))
        (cond (err (er hard? 'regex-get err))
              ((equal str whole) (car alist))
              (t (regex-get str (cdr alist))))))))

Theorem: return-type-of-regex-get

(defthm return-type-of-regex-get
  (implies (and (force (stringp str))
                (force (string-keyed-alist-p alist)))
           (b* ((key-value-pair (regex-get str alist)))
             (equal (consp key-value-pair)
                    (if key-value-pair t nil))))
  :rule-classes :rewrite)