		Search-engine friendly clone of the ACL2 documentation.

Defunvar-implementation

Defunvar-fn

Validate the inputs to defunvar and generate the event form to submit.

Signature
(defunvar-fn inputs call ctx state) → (mv erp event state)
Arguments: inputs — Guard (true-listp inputs).; call — Call to defunvar.
Guard (pseudo-event-formp call).; ctx — Context for errors.
Returns: erp — booleanp flag of the error triple.; event — Type (maybe-pseudo-event-formp event).

Similary to *-listp, any * and => symbol (i.e. in any package) is allowed.

Definitions and Theorems

Function: defunvar-fn

(defun defunvar-fn (inputs call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp inputs)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defunvar-fn))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (>= (len inputs) 4))
     (er-soft+ ctx t nil
               "At least four inputs must be supplied, not ~n0."
               (len inputs)))
    (funvar (first inputs))
    (arguments (second inputs))
    (arrow (third inputs))
    (result (fourth inputs))
    (options (nthcdr 4 inputs))
    ((unless (symbolp funvar))
     (er-soft+ ctx t nil
               "The first input must be a symbol, but ~x0 is not."
               funvar))
    ((unless (*-listp arguments))
     (er-soft+
        ctx t nil
        "The second input must be a list (* ... *), but ~x0 is not."
        arguments))
    ((unless (and (symbolp arrow)
                  (equal (symbol-name arrow) "=>")))
     (er-soft+ ctx t nil
               "The third input must be =>, but ~x0 is not."
               arrow))
    ((unless (and (symbolp result)
                  (equal (symbol-name result) "*")))
     (er-soft+ ctx t nil
               "The fourth input must be *, but ~x0 is not."
               result))
    ((unless (or (null options)
                 (and (= (len options) 2)
                      (eq (car options) :print))))
     (er-soft+
      ctx t nil
      "After the * input there may be at most one :PRINT option, ~
                   but instead ~x0 was supplied."
      options))
    (print (if options (cadr options) nil))
    ((unless (member-eq print '(nil :all)))
     (er-soft+
          ctx t nil
          "The :PRINT input must be NIL or :ALL, but ~x0 is not."
          print))
    ((when (funvarp funvar wrld))
     (b* ((arity (arity funvar wrld)))
      (if (= arity (len arguments))
          (prog2$ (cw "~%The call ~x0 is redundant.~%" call)
                  (value '(value-triple :invisible)))
       (er-soft+
        ctx t nil
        "A function variable ~x0 with arity ~x1 ~
                                 already exists.~%"
        funvar arity))))
    (event
     (cons
      'progn
      (cons (cons 'defstub
                  (cons funvar
                        (cons arguments
                              (cons arrow (cons result 'nil)))))
            (cons (cons 'table
                        (cons 'function-variables
                              (cons (cons 'quote (cons funvar 'nil))
                                    '(nil))))
                  (cons (cons 'value-triple
                              (cons (cons 'quote (cons funvar 'nil))
                                    'nil))
                        'nil)))))
    (event (restore-output? (eq print :all)
                            event)))
   (value event))))

Theorem: maybe-pseudo-event-formp-of-defunvar-fn.event

(defthm maybe-pseudo-event-formp-of-defunvar-fn.event
  (b* (((mv ?erp acl2::?event acl2::?state)
        (defunvar-fn inputs call ctx state)))
    (maybe-pseudo-event-formp event))
  :rule-classes :rewrite)