support

(in-package "STD")

(include-book "xdoc/top" :dir :system)

(include-book "std/util/bstar" :dir :system)

(defxdoc support
  :parents (std/util)
  :short "Miscellaneous supporting functions used by the @(see std/util) library.")

(defsection tuplep
  :parents (support)
  :short "@(call tuplep) recognizes nil-terminated @('n')-tuples."
  (defun tuplep
    (n x)
    (declare (xargs :guard (natp n)))
    (mbe :logic (and (true-listp x)
        (equal (len x) n))
      :exec (and (true-listp x) (eql (length x) n)))))

(defsection tuple-listp
  :parents (support)
  :short "@(call tuple-listp) recognizes a list of nil-terminated @('n')-tuples."
  (defun tuple-listp
    (n x)
    (declare (xargs :guard (natp n)))
    (if (consp x)
      (and (tuplep n (car x))
        (tuple-listp n (cdr x)))
      t)))

(defsection cons-listp
  :parents (support)
  :short "@(call cons-listp) is like @(see alistp) but does not require the
list to be nil-terminated."
  (defun cons-listp
    (x)
    (declare (xargs :guard t))
    (if (consp x)
      (and (consp (car x)) (cons-listp (cdr x)))
      t)))

(defsection raise
  :parents (support define er)
  :short "Shorthand for causing hard errors."
  :long "<p>@(call raise) is equivalent to @('(er hard? ...)'), but it
automatically fills in the function name using @('__function__').</p>

<p>This only works in contexts where @('__function__') is bound, e.g., the body
of a @(see define) or within a @(see defconsts) form.  In these contexts,
rather than write something like:</p>

@({
 (er hard? __function__ "bad input value ~x0~%" x)
})

<p>You can just write:</p>

@({
 (raise "bad input value ~x0~%" x)
})

<p>Logically @('raise') just returns @('nil').</p>

@(def raise)"
  (defmacro raise
    (&rest args)
    `(er hard? __function__ . ,STD::ARGS)))

(defsection legal-kwds-p
  :parents (support)
  :short "List of legal keywords for extract-keywords."
  :long "<p>Recognizes a list where each element is either a symbol a singleton
list containing a symbol.  In @(see extract-keywords), a bare symbol is a legal
keyword and a symbol in a singleton list is a keyword that can occur multiple
times in an argument list.</p>"
  (defun legal-kwds-p
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      (eq x nil)
      (and (or (symbolp (car x))
          (and (consp (car x))
            (symbolp (caar x))
            (not (cdar x))))
        (legal-kwds-p (cdr x))))))

(defsection keyword-legality
  :parents (support)
  :short "Check whether x is a legal keyword"
  :long "<p>Returns :single if x is allowed to occur once in the argument
list, :multiple if it is allowed to occur more than once, and NIL if not
allowed.</p>"
  (defun keyword-legality
    (x legals)
    (declare (xargs :guard (and (symbolp x) (legal-kwds-p legals))))
    (cond ((atom legals) nil)
      ((eq x (car legals)) :single)
      ((and (consp (car legals))
         (eq x (caar legals))) :multiple)
      (t (keyword-legality x (cdr legals))))))

(local (defthm alistp-of-remove1-assoc-equal
    (implies (alistp alist)
      (alistp (remove1-assoc-equal key alist)))))

(defsection extract-keywords
  :parents (support)
  :short "Extract legal keyword/value pairs from an argument list."
  :long "<p>If a keyword occurs as a singleton list in legal-kwds, it may have
mulitple occurrences in the args, and the result stored in the kwd-alist will
be a list of the arguments to the occurrences.  For example:</p>
@({
 (extract-keywords 'foo '((:bar)) '(:bar x :bar y) nil)
 })
<p>produces @('((:bar y x))') as its keyword alist result.</p>"
  (defun extract-keywords
    (ctx legal-kwds args kwd-alist)
    "Returns (mv kwd-alist other-args)"
    (declare (xargs :guard (and (legal-kwds-p legal-kwds)
          (alistp kwd-alist))))
    (b* ((__function__ 'extract-keywords) ((when (atom args)) (mv kwd-alist args))
        (arg1 (first args))
        ((unless (keywordp arg1)) (b* (((mv kwd-alist other-args) (extract-keywords ctx
                 legal-kwds
                 (cdr args)
                 kwd-alist)))
            (mv kwd-alist (cons arg1 other-args))))
        (legality (keyword-legality arg1 legal-kwds))
        ((unless legality) (raise (concatenate 'string
              "~x0: invalid keyword ~x1."
              (if legal-kwds
                "  Valid keywords: ~&2."
                "  No keywords are valid here."))
            ctx
            arg1
            legal-kwds)
          (mv nil nil))
        ((when (atom (rest args))) (raise "~x0: keyword ~x1 has no argument."
            ctx
            arg1)
          (mv nil nil))
        ((when (and (not (eq legality :multiple))
             (assoc arg1 kwd-alist))) (raise "~x0: multiple occurrences of keyword ~x1."
            ctx
            arg1)
          (mv nil nil))
        (value (second args))
        (kwd-alist (if (eq legality :multiple)
            (acons arg1
              (cons value (cdr (assoc arg1 kwd-alist)))
              (remove1-assoc arg1 kwd-alist))
            (acons arg1 value kwd-alist))))
      (extract-keywords ctx
        legal-kwds
        (cddr args)
        kwd-alist))))

(defsection getarg
  :parents (support)
  :short "Get a value from the keyword-value alist produced by @(see
extract-keywords), with default-value support."
  (defun getarg
    (arg default alist)
    (declare (xargs :guard (and (eqlablep arg) (alistp alist))))
    (b* ((look (assoc arg alist)))
      (if look
        (cdr look)
        default))))

(defsection getarg+
  :parents (support)
  :short "Get a value from the keyword-value alist produced by @(see
extract-keywords), with default-value support, and additionally return a flag
saying whether the key was bound.  Returns (mv value boundp)."
  (defun getarg+
    (arg default alist)
    (declare (xargs :guard (and (eqlablep arg) (alistp alist))))
    (b* ((look (assoc arg alist)))
      (if look
        (mv (cdr look) t)
        (mv default nil)))))

(defun assigns-for-getargs
  (args alist lazyp)
  (declare (xargs :mode :program))
  (if (atom args)
    nil
    (append (let ((arg (car args)))
        (case-match arg
          ((var default boundp) (b* (((mv basevar ?ign) (decode-varname-for-patbind var)) (key (intern-in-package-of-symbol (symbol-name basevar)
                    :key)))
              (if (and lazyp
                  (consp default)
                  (not (eq (car default) 'quote)))
                `((,BOUNDP (assoc ,STD::KEY ,STD::ALIST)) (,STD::VAR (if boundp
                      (cdr boundp)
                      ,STD::DEFAULT)))
                `(((mv ,STD::VAR ,BOUNDP) (getarg+ ,STD::KEY ,STD::DEFAULT ,STD::ALIST))))))
          ((var default) (b* (((mv basevar ?ign) (decode-varname-for-patbind var)) (key (intern-in-package-of-symbol (symbol-name basevar)
                    :key)))
              (if (and lazyp
                  (consp default)
                  (not (eq (car default) 'quote)))
                `((,STD::VAR (let ((tmp-look (assoc ,STD::KEY ,STD::ALIST)))
                     (if tmp-look
                       (cdr tmp-look)
                       (check-vars-not-free (tmp-look) ,STD::DEFAULT)))))
                `((,STD::VAR (getarg ,STD::KEY ,STD::DEFAULT ,STD::ALIST))))))
          (var (b* (((mv basevar ?ign) (decode-varname-for-patbind var)) (key (intern-in-package-of-symbol (symbol-name basevar)
                    :key)))
              `((,STD::VAR (getarg ,STD::KEY nil ,STD::ALIST)))))))
      (assigns-for-getargs (cdr args)
        alist
        lazyp))))

(def-b*-binder getargs
  :short "@(see b*) binder for getargs on a keyword alist."
  :long "<p>Usage:</p>
@({
    (b* (((getargs :lazyp t
                   a
                   (b b-default-term)
                   (c c-default-term cp)
                   d)
          alst))
      form)
})

<p>is equivalent to</p>

@({
    (b* ((a (getarg :a nil alst))
         (b (getarg :b b-default-term alst))
         ((mv c cp) (getarg+ :c c-default-term alst))
         (d (getarg :d nil alist)))
      form)
})"
  :body (b* (((mv kwd-alist args) (extract-keywords 'getargs
         '(:lazyp)
         args
         nil)) (lazyp (cdr (assoc :lazyp kwd-alist))))
    (mv-let (pre-bindings name rest)
      (if (and (consp (car forms)) (not (eq (caar forms) 'quote)))
        (mv `((?tmp-for-getargs ,(CAR FORMS)))
          'tmp-for-getargs
          `(check-vars-not-free (tmp-for-getargs) ,REST-EXPR))
        (mv nil (car forms) rest-expr))
      `(b* (,@STD::PRE-BINDINGS . ,(STD::ASSIGNS-FOR-GETARGS STD::ARGS STD::NAME STD::LAZYP))
        ,REST))))

(defun keys-for-getargs
  (args)
  (declare (xargs :mode :program))
  (if (atom args)
    nil
    (b* ((arg (car args)) (var (if (consp arg)
            (car arg)
            arg))
        ((mv basevar ?ign) (decode-varname-for-patbind var))
        (key (intern-in-package-of-symbol (symbol-name basevar)
            :key)))
      (cons key (keys-for-getargs (cdr args))))))

(def-b*-binder extract-keyword-args
  :short "@(see b*) binder for getargs on a keyword alist."
  :long "<p>Usage:</p>
@({
    (b* (((extract-keyword-args
            :other-args other-args-var
            :allowed-keys allowed-keys-term
            :kwd-alist kwd-alist-var
            :defaults default-kwd-alist
            :ctx context
            :lazyp lazyp
             a
            (b b-default-term)
            (c c-default-term cp)
            d)
          args))
      form)
})

<p>is equivalent to</p>

@({
    (b* (((mv kwd-alist-var other-args-var)
          (extract-keywords context
               (append '(:a :b :c :d) allowed-keys-term) ;; allowed keys
                args nil))
         ((getargs :lazyp lazyp
             a
            (b b-default-term)
            (c c-default-term cp)
            d)
          (append kwd-alist-var default-kwd-alist)))
      form)
})"
  :body (b* (((mv keywords args) (extract-keywords 'extract-keyword-args
         '(:lazyp :other-args :kwd-alist :ctx :allowed-keys :defaults)
         args
         nil)) ((getargs lazyp
         allowed-keys
         (other-args '?other-args)
         (kwd-alist '?kwd-alist)
         (ctx '__function__)
         (defaults nil)) keywords)
      (getarg-keys (keys-for-getargs args))
      ((mv kwd-alist-var ?ign) (decode-varname-for-patbind kwd-alist))
      ((mv pre-bindings name rest) (if (and (consp (car forms)) (not (eq (caar forms) 'quote)))
          (mv `((?tmp-for-extract-keyword-args ,(CAR FORMS)))
            'tmp-for-extract-keyword-args
            `(check-vars-not-free (tmp-for-extract-keyword-args)
              ,REST-EXPR))
          (mv nil (car forms) rest-expr))))
    `(b* (,@STD::PRE-BINDINGS ((mv ,STD::KWD-ALIST ,STD::OTHER-ARGS) (extract-keywords ,STD::CTX
            ,(IF STD::ALLOWED-KEYS
     (IF STD::GETARG-KEYS
         `(APPEND ',STD::GETARG-KEYS ,STD::ALLOWED-KEYS)
         STD::ALLOWED-KEYS)
     `',STD::GETARG-KEYS)
            ,STD::NAME
            nil))
        ((getargs :lazyp ,STD::LAZYP . ,STD::ARGS) ,(IF STD::DEFAULTS
     `(APPEND ,STD::KWD-ALIST-VAR ,STD::DEFAULTS)
     STD::KWD-ALIST-VAR)))
      ,REST)))

(defsection split-///
  :parents (support)
  :short "Split an argument list into pre- and post-@('///') contents."
  (defun split-///
    (ctx x)
    "Returns (mv pre-/// post-///)"
    (declare (xargs :guard t))
    (b* ((__function__ 'split-///) ((when (not x)) (mv nil nil))
        ((when (atom x)) (raise "~x0: expected nil-terminated arguments but found ~x1."
            ctx
            x)
          (mv nil nil))
        ((when (eq (car x) '///)) (mv nil (cdr x)))
        ((mv pre post) (split-/// ctx (cdr x))))
      (mv (cons (car x) pre) post)))
  (defthmd true-listp-of-split-///.pre-///
    (true-listp (mv-nth 0 (split-/// ctx x))))
  (defthm true-listp-of-split-///.post-///
    (implies (true-listp x)
      (true-listp (mv-nth 1 (split-/// ctx x)))))
  (in-theory (disable split-///)))

(defsection ends-with-period-p
  :parents (support)
  :short "Determines if a string ends with a period."
  (defun ends-with-period-p
    (x)
    (declare (xargs :guard (stringp x)))
    (let ((xl (length x)))
      (and (> xl 0)
        (eql (char x (- (length x) 1)) #\.)))))

(defsection dumb-string-sublis
  :parents (support)
  :short "Non-recursively applies a list of substring substitutions to a string."
  :long "<p>Earlier key/value pairs take precedence over later ones, and no
substitutions are reapplied to the result of other substitutions.</p>"
  (defun dumb-str-sublis-iter
    (remainder alist
      x
      start
      end
      len)
    (declare (xargs :mode :program))
    (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))))
  (defun dumb-str-sublis
    (alist str)
    (declare (xargs :mode :program))
    (let ((len (length str)))
      (dumb-str-sublis-iter alist
        alist
        str
        0
        len
        len))))

(defsection generic-eval-requirement
  :parents (std/lists/abstract)
  :short "Evaluate a requirement of a generic theorem for deflist/defprojection/defmapappend"
  :long "<p>See @(see acl2::std/lists/abstract).</p>"
  (mutual-recursion (defun generic-eval-requirement
      (req req-alist)
      (declare (xargs :mode :program))
      (if (atom req)
        (let ((look (assoc req req-alist)))
          (if look
            (cdr look)
            (er hard?
              'generic-eval-requirement
              "Unrecognized requirement variable: ~x0~%"
              req)))
        (case (car req)
          ('not (not (generic-eval-requirement (cadr req)
                req-alist)))
          ('and (generic-and-requirements (cdr req)
              req-alist))
          ('or (generic-or-requirements (cdr req) req-alist))
          ('if (if (generic-eval-requirement (cadr req)
                req-alist)
              (generic-eval-requirement (caddr req)
                req-alist)
              (generic-eval-requirement (cadddr req)
                req-alist)))
          (otherwise (er hard?
              'generic-eval-requirement
              "malformed requirement term: ~x0~%"
              req)))))
    (defun generic-and-requirements
      (reqs req-alist)
      (if (atom reqs)
        t
        (and (generic-eval-requirement (car reqs)
            req-alist)
          (generic-and-requirements (cdr reqs)
            req-alist))))
    (defun generic-or-requirements
      (reqs req-alist)
      (if (atom reqs)
        nil
        (or (generic-eval-requirement (car reqs)
            req-alist)
          (generic-or-requirements (cdr reqs)
            req-alist))))))

(mutual-recursion (defun find-calls-of-fns-term
    (x fns acc)
    (declare (xargs :mode :program))
    (cond ((or (atom x) (eq (car x) 'quote)) acc)
      ((member-eq (car x) fns) (find-calls-of-fns-list (cdr x)
          fns
          (cons x acc)))
      (t (find-calls-of-fns-list (cdr x) fns acc))))
  (defun find-calls-of-fns-list
    (x fns acc)
    (if (atom x)
      acc
      (find-calls-of-fns-term (car x)
        fns
        (find-calls-of-fns-list (cdr x) fns acc)))))

(defun expand-calls-computed-hint
  (clause fns)
  (declare (xargs :mode :program))
  (let ((expand-list (find-calls-of-fns-term (car (last clause))
         fns
         nil)))
    `(:expand ,STD::EXPAND-LIST)))

(defmacro expand-calls
  (&rest fns)
  `(expand-calls-computed-hint clause ',STD::FNS))