• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
      • Updates-to-workshop-material
      • Soft-implementation
        • Soft-implementation-core
        • Gen-macro2-of-macro
        • Defun-inst-implementation
        • Defthm-inst-implementation
        • Defsoft-implementation
        • Defunvar-implementation
          • Defunvar-fn
          • Show-defunvar
          • Defunvar-macro-definition
        • Defund-sk2-implementation
        • Defun-sk2-implementation
        • Define-sk2-implementation
        • Defchoose2-implementation
        • Defund2-implementation
        • Defun2-implementation
        • Define2-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)