• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
        • Acre-internals
          • Regex
            • Regex-case
            • Regex-p
            • Regex-equiv
            • Regex-zerolength
            • Regex-repeat
              • Make-regex-repeat
                • Regex-repeat->pat
                • Regex-repeat->max
                • Regex-repeat->min
                • Change-regex-repeat
              • Regex-group
              • Regex-charset
              • Regex-case-sens
              • Regex-kind
              • Regex-reverse-pref
              • Regex-no-backtrack
              • Regex-exact
              • Regex-disjunct
              • Regex-concat
              • Regex-backref
              • Regex-start
              • Regex-end
              • Regexlist
              • Regex-fix
              • Regex-count
            • Match-string-at
            • Matchstatelist-measure
            • Parse-primitive
            • Matches-remove-zero-length
            • Parse-repeatop
            • Parse-repeatbase
            • Matchstatelist-in-bounds
            • Parse-range
            • Parse-charset-set
            • Parse-charset-atom
            • Match-regex-locs
            • Parse-octal-charcode
            • Parse-k-backref
            • Parse-g-backref
            • Matchstatelist-all-have-backref
            • Parse-repeatmod
            • Parse-charset-elem
            • Parse-charset-aux
            • Parse-hex-charcode
            • Parse-charset
            • Matchstatelist-indices-lte
            • Matchstatelist-indices-gte
            • Match-exact
            • Matches-add-backref
            • Matchresult
            • Preproc-legible-aux
            • Maybe-backref
            • Match-charset
            • Undup-equiv
            • Find-substr
            • Maybe-backref-extract-substr
            • Matchstatelist-min-index
            • Matchstate-in-bounds
            • Match-add-backref
            • Undup
            • Backref-alist-in-bounds
            • Backref
            • Matchstate
            • Matchresult->matched-substr
            • Matchresult->captured-substr!
            • Matchresult->captured-substr
            • Maybe-backref-in-bounds
            • Matchmode
            • Backref-extract-substr
            • Charset-range
            • Matchstate-measure
            • Backref-in-bounds
            • Rev-keys
            • Parse-regex
            • Undup-exec
            • Get-charset
            • Regex-concat2
            • Preproc-legible
            • Matchresult-in-bounds
            • Regex-disjunct2
            • Backref-alist
            • Named-captures-bindings
            • Captures-bindings
            • Matchstatelist
            • Charset-char-regex
            • Repeatmod-p
          • Parse-and-match-regex
          • Match-regex
          • Parse
          • Matchresult->matchedp
          • Match
        • Milawa
        • Smtlink
        • Abnf
        • Vwsim
        • Isar
        • Wp-gen
        • Dimacs-reader
        • Pfcs
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Regex-repeat

    Make-regex-repeat

    Basic constructor macro for regex-repeat structures.

    Syntax
    (make-regex-repeat [:pat <pat>] 
                       [:min <min>] 
                       [:max <max>]) 
    

    This is the usual way to construct regex-repeat structures. It simply conses together a structure with the specified fields.

    This macro generates a new regex-repeat structure from scratch. See also change-regex-repeat, which can "change" an existing structure, instead.

    Definition

    This is an ordinary make- macro introduced by defprod.

    Macro: make-regex-repeat

    (defmacro make-regex-repeat (&rest args)
      (std::make-aggregate 'regex-repeat
                           args '((:pat) (:min) (:max))
                           'make-regex-repeat
                           nil))

    Function: regex-repeat

    (defun regex-repeat (pat min max)
      (declare (xargs :guard (and (regex-p pat)
                                  (natp min)
                                  (maybe-natp max))))
      (declare (xargs :guard t))
      (let ((__function__ 'regex-repeat))
        (declare (ignorable __function__))
        (b* ((pat (mbe :logic (regex-fix pat) :exec pat))
             (min (mbe :logic (nfix min) :exec min))
             (max (mbe :logic (maybe-natp-fix max)
                       :exec max)))
          (cons :repeat (list pat min max)))))