Lookup a string in the regular expression alist.
(regex-get str alist) → key-value-pair
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
(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))))))))