		Search-engine friendly clone of the ACL2 documentation.

Vls-commands

Define-vls-command-fn

Signature
(define-vls-command-fn name args type rest) → *

Definitions and Theorems

Function: define-vls-command-fn

(defun define-vls-command-fn (name args type rest)
 (declare (xargs :guard t))
 (let ((__function__ 'define-vls-command-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise "Name must be a symbol, but got ~x0."
            name))
    ((unless (and (symbol-listp args)
                  (uniquep args)))
     (raise "Arguments to ~x0 must be unique symbols."
            name))
    ((unless
         (uniquep
              (str::downcase-string-list (symbol-list-names args))))
     (raise "Arguments to ~x0 do not have unique symbol names."
            name))
    ((unless (member 'data args))
     (raise "Arguments to ~x0 do not include data."
            name))
    (reserved-names
         (intersection-equal '("BASE" "MODEL")
                             (str::symbol-list-names args)))
    ((when reserved-names)
     (raise "Arguments to ~x0 use reserved names ~&1."
            reserved-names))
    ((unless (vls-commandtype-p type))
     (raise "Unrecognized command type for ~x0."
            name))
    (info (make-vls-commandinfo :fn name
                                :args args
                                :type type))
    (eargs (vls-command-args-to-eformals args)))
   (cons
    'progn
    (cons
     (cons
      'define
      (cons
           name
           (cons eargs
                 (cons ':returns
                       (cons '(ans stringp
                                   :rule-classes :type-prescription)
                             rest)))))
     (cons
      (cons
        'table
        (cons 'vl-server
              (cons ''commands
                    (cons (cons 'cons
                                (cons (cons 'quote (cons info 'nil))
                                      '((get-vls-commands world))))
                          'nil))))
      'nil))))))