• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • 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
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Mailing-lists
        • Interfacing-tools
      • 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
        • 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)))