• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Defines
        • Define-sk
        • Error-value-tuples
        • Defmax-nat
        • Defmin-int
        • Deftutorial
        • Extended-formals
        • Defrule
        • Defval
        • Defsurj
        • Defiso
        • Defconstrained-recognizer
        • Deffixer
        • Defmvtypes
        • Defconsts
        • Defthm-unsigned-byte-p
        • Support
          • Extract-keywords
          • Dumb-string-sublis
            • Raise
            • Look-up-return-vals
            • Logic-mode-p
            • Look-up-wrapper-args
            • Look-up-formals
            • Legal-kwds-p
            • Split-///
            • Keyword-legality
            • Getarg+
            • Var-is-stobj-p
            • Look-up-guard
            • Getarg
            • Cons-listp
            • Tuplep
            • Tuple-listp
            • Ends-with-period-p
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Defdata
        • Defrstobj
        • Seq
        • Match-tree
        • Defrstobj
        • With-supporters
        • Def-partial-measure
        • Template-subst
        • Soft
        • Defthm-domain
        • Event-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Support

    Dumb-string-sublis

    Non-recursively applies a list of substring substitutions to a string.

    Earlier key/value pairs take precedence over later ones, and no substitutions are reapplied to the result of other substitutions.

    Definitions and Theorems

    Function: dumb-str-sublis-iter

    (defun dumb-str-sublis-iter (remainder alist x start end len)
     (b*
      (((when (atom remainder))
        (if (or (not (int= start 0))
                (not (int= end len)))
            (subseq x start end)
          x))
       ((cons old-str new-str) (car remainder))
       (loc (search old-str x
                    :start2 start
                    :end2 end))
       ((unless loc)
        (dumb-str-sublis-iter (cdr remainder)
                              alist x start end len))
       (prefix-rw (dumb-str-sublis-iter (cdr remainder)
                                        alist x start loc len))
       (suffix-rw
            (dumb-str-sublis-iter alist alist x (+ loc (length old-str))
                                  end len)))
      (if (and (string-equal prefix-rw "")
               (string-equal suffix-rw ""))
          new-str
        (concatenate 'string
                     prefix-rw new-str suffix-rw))))

    Function: dumb-str-sublis

    (defun dumb-str-sublis (alist str)
      (let ((len (length str)))
        (dumb-str-sublis-iter alist alist str 0 len len)))