Filtering...

formals

books/std/util/formals
other
(in-package "STD")
other
(include-book "look-up")
other
(include-book "da-base")
other
(program)
other
(defxdoc extended-formals
  :parents (std/util define)
  :short "Extended syntax for function arguments that allows for built-in
guards, documentation, and macro-like keyword/optional arguments."
  :long "<p>Macros like @(see define) accept an extended formals syntax.  This
syntax properly extends the normal syntax for a function's arguments used by
@(see defun), so you can still use a plain list of variable names if you like.
But there are also some more interesting extensions.</p>

<p>Basic examples of some extended formals in a @('define'):</p>

@({
 (define split-up-string
   ((x stringp "The string to split")
    (separators (and (consp separators)
                     (character-listp separators))
     "Letters to split on -- <b>dropped from the result!</b>")
    &key
    (limit (or (not limit)
               (natp limit))
     "Where to stop, @('nil') means @('(length x)')"))
   ...)
})

<p>The general syntax for extended formals is:</p>

@({
  Formals ::= (Formal*                 ; ordinary formals
               [&optional OptFormal*]  ; optional positional formals
               [&key OptFormal*]       ; optional keyword formals
               )

  OptFormal ::= Formal          ; optional formal w/NIL default
              | (Formal 'val)   ; optional formal w/custom default

  Formal  ::= (varname Item*)

  Item    ::= xdoc       ; documentation string
            | guard      ; guard specifier
            | :key val   ; other additional options
})


<h4>@('&key') and @('&optional') arguments</h4>

<p>You can use @('&key') and @('&optional') as in @(see macro-args).  (Other
lambda-list keywords like @('&rest') aren't supported.)  When macros like
@('define') see these keywords, then instead of just producing a @('defun') we
will generate:</p>

<ul>
<li>A function, @('name-fn'),</li>
<li>A wrapper macro, @('name'),</li>
<li>A <see topic='@(url acl2::macro-aliases-table)'>macro alias</see> associating
@('name-fn') with @('name')</li>
</ul>

<p>The default values for these parameters work just like in ordinary macros.
The explicit quote serves to separate these from Items.</p>


<h4>Inline Documentation</h4>

<p>You can optionally describe your formals with some @(see xdoc)
documentation.  This description will be embedded within some generated
@('<dl>/<dt>/<dd>') tags that describe your function's interface.  You can
freely use @(see xdoc::markup) and @(see xdoc::preprocessor) directives.
Typically your descriptions should be short and should not include
document-structuring tags like @('<p>'), @('<ul>'), @('<h3>'), and so
forth.</p>


<h4>Inline Guards</h4>

<p>As a convenient shorthand, the @('guard') may be a single non-keyword
symbol, e.g., in @('split-up-string') above, the guard for @('x') is
@('(stringp x)').  To be more precise:</p>

<ul>
 <li>@('t') and @('nil') are treated literally, and</li>
 <li>Any other symbol @('g') is treated as short for @('(g var)')</li>
</ul>

<p>For more complex guards, you can also write down arbitrary terms, e.g.,
above @('separators') must be a non-empty character list.  We put a few
sensible restrictions here.  We require that a guard term must be at least a
cons to distinguish it from documentation, symbol guards, and keywords.  We
also require that it is not simply a quoted constant.  This ensures that guards
can be distinguished from default values in macro arguments.  For example,
compare:</p>

@({
     &key (x 'atom)     ;; x has no guard, default value 'atom
 vs. &key (x atom)      ;; x has guard (atom x), default value nil
 vs. &key ((x atom) '3) ;; x has guard (atom x), default value 3
})


<h4>Keyword/Value Options</h4>

<p>To make the formals syntax more flexible, other keyword/value options can be
embedded within the formal.</p>

<p>The valid keywords and their interpretations can vary from macro to macro.
For instance, @(see define) doesn't accept any keyword/value options, but @(see
defaggregate) fields have a @(':rule-classes') option.</p>



<h4>Additional Features</h4>

<p>Some other features of extended formals are not evident in their syntax.</p>

<p>We generally expect macros that take extended formals to automatically
recognize @(see acl2::stobj)s and insert appropriate @('(declare (xargs :stobjs
...))') forms.</p>

<p>Future work (not yet implemented): certain guards like @('stringp') and
@('(unsigned-byte-p 32 x)'), are recognized as @(see acl2::type-spec)s and
result in @(see type) declarations for the Lisp compiler.  This may
occasionally improve efficiency.</p>")
other
(def-primitive-aggregate formal
  (name guard doc opts)
  :tag :formal)
formallist-pfunction
(defun formallist-p
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    t
    (and (formal-p (car x))
      (formallist-p (cdr x)))))
formallist->namesfunction
(defun formallist->names
  (x)
  (declare (xargs :guard (formallist-p x)))
  (if (atom x)
    nil
    (cons (formal->name (car x))
      (formallist->names (cdr x)))))
formallist->guardsfunction
(defun formallist->guards
  (x)
  (declare (xargs :guard (formallist-p x)))
  (if (atom x)
    nil
    (cons (formal->guard (car x))
      (formallist->guards (cdr x)))))
formallist-collect-stobjsfunction
(defun formallist-collect-stobjs
  (x world)
  (declare (xargs :guard (and (formallist-p x)
        (plist-worldp world))))
  (cond ((atom x) nil)
    ((var-is-stobj-p (formal->name (car x))
       world) (cons (car x)
        (formallist-collect-stobjs (cdr x) world)))
    (t (formallist-collect-stobjs (cdr x) world))))
parse-formal-namefunction
(defun parse-formal-name
  (ctx varname)
  (declare (xargs :guard t))
  (b* ((__function__ 'parse-formal-name) ((when (legal-variablep varname)) varname)
      (fake-arglist (list varname))
      ((when (arglistp fake-arglist)) (raise "~x0: formal ~x1: mysterious problem that Jared thinks should ~
                be impossible, please tell him that he is wrong."
          ctx
          varname)
        'default-valid-legal-variablep)
      ((mv & reason) (find-first-bad-arg fake-arglist)))
    (raise (concatenate 'string
        "~x0: formal ~x1 is invalid; it "
        reason)
      ctx
      varname)
    'default-valid-legal-variablep))
check-formal-guardfunction
(defun check-formal-guard
  (ctx varname item world)
  (b* ((__function__ 'check-formal-guard) ((unless world) nil)
      (macro-args (getprop item
          'macro-args
          :bad 'current-acl2-world
          world))
      ((unless (eq macro-args :bad)) nil)
      (formals (getprop item
          'formals
          :bad 'current-acl2-world
          world))
      ((when (eq formals :bad)) (raise "Error in ~x0: the guard for ~x1 is ~x2, but there is no ~
                function or macro named ~x2."
          ctx
          varname
          item))
      ((when (tuplep 1 formals)) nil))
    (raise "Error in ~x0: the guard for ~x1 should take a single argument, ~
            but ~x2 takes ~x3 arguments."
      ctx
      varname
      item
      (len formals))))
parse-formal-itemfunction
(defun parse-formal-item
  (ctx varname
    item
    guards
    docs
    world)
  "Returns (mv guards docs)"
  (declare (xargs :guard (legal-variablep varname)))
  (b* ((__function__ 'parse-formal-item) ((when (booleanp item)) (mv (cons item guards) docs))
      ((when (symbolp item)) (check-formal-guard ctx
          varname
          item
          world)
        (mv (cons `(,STD::ITEM ,STD::VARNAME) guards)
          docs))
      ((when (and (consp item) (not (eq (car item) 'quote)))) (mv (cons item guards) docs))
      ((when (stringp item)) (mv guards (cons item docs))))
    (raise "~x0: formal ~x1: expected guard specifiers or documentation ~
            strings, but found ~x2."
      ctx
      varname
      item)
    (mv guards docs)))
parse-formal-itemsfunction
(defun parse-formal-items
  (ctx varname
    items
    guards
    docs
    world)
  "Returns (mv guards docs)"
  (declare (xargs :guard (legal-variablep varname)))
  (b* ((__function__ 'parse-formal-items) ((when (not items)) (mv guards docs))
      ((when (atom items)) (raise "~x0: formal ~x1: extended formal items should be ~
                nil-terminated; found ~x2 as the final cdr."
          ctx
          varname
          items)
        (mv guards docs))
      ((mv guards docs) (parse-formal-item ctx
          varname
          (car items)
          guards
          docs
          world)))
    (parse-formal-items ctx
      varname
      (cdr items)
      guards
      docs
      world)))
parse-formalfunction
(defun parse-formal
  (ctx formal legal-kwds world)
  "Returns a formal-p"
  (declare (xargs :guard t))
  (b* ((__function__ 'parse-formal) ((when (atom formal)) (b* ((varname (parse-formal-name ctx formal)))
          (make-formal :name varname
            :guard t
            :doc ""
            :opts nil)))
      (varname (parse-formal-name ctx (car formal)))
      (items (cdr formal))
      ((mv opts items) (extract-keywords (cons ctx varname)
          legal-kwds
          items
          nil))
      ((mv guards docs) (parse-formal-items ctx
          varname
          items
          nil
          nil
          world))
      (guard (cond ((atom guards) 't)
          ((atom (cdr guards)) (car guards))
          (t (raise "~x0: formal ~x1: expected a single guard term, ~
                               but found ~&2."
              ctx
              varname
              guards))))
      (doc (cond ((atom docs) "")
          ((atom (cdr docs)) (car docs))
          (t (progn$ (raise "~x0: formal ~x1: expected a single xdoc ~
                                string, but found ~&2."
                ctx
                varname
                docs)
              "")))))
    (make-formal :name varname
      :guard guard
      :doc doc
      :opts opts)))
parse-formalsfunction
(defun parse-formals
  (ctx formals legal-kwds world)
  (declare (xargs :guard t))
  (b* ((__function__ 'parse-formals) ((when (not formals)) nil)
      ((when (atom formals)) (raise "~x0: expected formals to be nil-terminated, but found ~x1 as ~
                the final cdr."
          ctx
          formals)))
    (cons (parse-formal ctx
        (car formals)
        legal-kwds
        world)
      (parse-formals ctx
        (cdr formals)
        legal-kwds
        world))))
has-macro-argsfunction
(defun has-macro-args
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    nil
    (or (lambda-keywordp (car x))
      (has-macro-args (cdr x)))))
remove-macro-argsfunction
(defun remove-macro-args
  (ctx formals seenp)
  (declare (xargs :guard t))
  (b* ((__function__ 'remove-macro-args) ((when (atom formals)) formals)
      ((cons arg1 rest) formals)
      ((when (or (eq arg1 '&key) (eq arg1 '&optional))) (remove-macro-args ctx rest t))
      ((when (lambda-keywordp arg1)) (raise "~x0: only &key and &optional macro-style arguments are ~
                allowed, but found ~x1."
          ctx
          arg1))
      ((unless seenp) (cons arg1
          (remove-macro-args ctx rest seenp)))
      ((when (and (consp arg1)
           (true-listp arg1)
           (equal (len arg1) 2)
           (consp (second arg1))
           (eq (car (second arg1)) 'quote))) (cons (first arg1)
          (remove-macro-args ctx rest seenp))))
    (cons arg1
      (remove-macro-args ctx rest seenp))))
formals-for-macrofunction
(defun formals-for-macro
  (ctx formals seenp)
  (declare (xargs :guard t))
  (b* ((__function__ 'formals-for-macro) ((when (atom formals)) formals)
      ((cons arg1 rest) formals)
      ((when (or (eq arg1 '&key) (eq arg1 '&optional))) (cons arg1 (formals-for-macro ctx rest t)))
      ((when (lambda-keywordp arg1)) (raise "~x0: only &key and &optional macro-style arguments are ~
                allowed, but found ~x1."
          ctx
          arg1))
      ((unless seenp) (cons (if (atom arg1)
            arg1
            (car arg1))
          (formals-for-macro ctx rest seenp)))
      ((when (and (consp arg1)
           (true-listp arg1)
           (equal (len arg1) 2)
           (consp (second arg1))
           (eq (car (second arg1)) 'quote))) (let* ((eformal (first arg1)) (default-val (second arg1))
            (name (if (atom eformal)
                eformal
                (car eformal))))
          (cons (list name default-val)
            (formals-for-macro ctx rest seenp)))))
    (cons (if (atom arg1)
        arg1
        (car arg1))
      (formals-for-macro ctx rest seenp))))
remove-macro-default-valuesfunction
(defun remove-macro-default-values
  (args)
  (declare (xargs :guard t))
  (cond ((atom args) nil)
    ((atom (car args)) (cons (car args)
        (remove-macro-default-values (cdr args))))
    (t (cons (caar args)
        (remove-macro-default-values (cdr args))))))
make-wrapper-macrofunction
(defun make-wrapper-macro
  (fnname fnname-fn formals)
  (declare (xargs :guard (and (symbolp fnname) (symbolp fnname-fn))))
  (b* ((macro-formals (formals-for-macro fnname formals nil)) (fn-arg-names (remove-macro-default-values (set-difference-equal macro-formals
            '(&key &optional)))))
    `(defmacro ,STD::FNNAME
      ,STD::MACRO-FORMALS
      (list ',STD::FNNAME-FN . ,STD::FN-ARG-NAMES))))