		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Named-captures-bindings

Signature
(named-captures-bindings args matchresult !) → *

Definitions and Theorems

Function: named-captures-bindings

(defun named-captures-bindings (args matchresult !)
 (declare (xargs :guard t))
 (let ((__function__ 'named-captures-bindings))
  (declare (ignorable __function__))
  (b*
   (((when (atom args)) nil)
    (arg (car args))
    (fn (if ! 'matchresult->captured-substr!
          'matchresult->captured-substr))
    ((when (symbolp arg))
     (cons
      (cons
          arg
          (cons (cons fn
                      (cons (str::downcase-string (symbol-name arg))
                            (cons matchresult 'nil)))
                'nil))
      (named-captures-bindings (cdr args)
                               matchresult !))))
   (case-match arg
    ((var name)
     (cons (cons var
                 (cons (cons fn (cons name (cons matchresult 'nil)))
                       'nil))
           (named-captures-bindings (cdr args)
                                    matchresult !)))
    (& (er hard? 'named-captures-bindings
           "Bad capture element: ~x0" arg))))))