• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixequiv
      • Deffixtype
      • Defoption
      • Fty-discipline
      • Fold
        • Deffold-reduce
        • Deffold-map
        • Defmake-self
          • Defmake-self-implementation
            • Defmake-self-event-generation
              • Defmake-self-gen-everything
              • Defmake-self-gen-list
              • Defmake-self-gen-omap
              • Defmake-self-gen-clique
              • Defmake-self-gen-table-events
              • Defmake-self-gen-sum-case
              • Defmake-self-gen-sum
              • Defmake-self-gen-prod
              • Defmake-self-gen-option
              • Defmake-self-gen-cliques
              • Defmake-self-gen-prod/sum/option
              • Defmake-self-gen-types
              • Defmake-self-gen-sum-cases
              • Defmake-self-get-make-self-fn
              • Defmake-self-gen-type
              • Defmake-self-gen-table-events-loop
              • Defmake-self-gen-topic-name
              • Defmake-self-gen-name
            • Defmake-self-process-inputs-and-gen-everything
            • Defmake-self-fn
            • Defmake-self-input-processing
            • Defmake-self-macro-definition
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
      • Defomap
      • Defbytelist
      • Fty::basetypes
      • Defvisitors
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Multicase
      • Deffixequiv-mutual
      • Fty::baselists
      • Def-enumcase
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • 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

• Defmake-self-event-generation

Defmake-self-gen-table-events

Generate the table-events for a type clique with the given members.

Signature

(defmake-self-gen-table-events clique-name member-names) 
  → 
events

Arguments

clique-name — Guard (symbolp clique-name).

member-names — Guard (symbol-listp member-names).

Returns

events — Type (acl2::pseudo-event-form-listp events).

Definitions and Theorems

Function: defmake-self-gen-table-events-loop

(defun defmake-self-gen-table-events-loop (member-names)
 (declare (xargs :guard (symbol-listp member-names)))
 (let ((__function__ 'defmake-self-gen-table-events-loop))
  (declare (ignorable __function__))
  (b*
    (((when (endp member-names)) nil)
     (type (first member-names))
     (make-self-name (defmake-self-gen-name (first member-names))))
   (cons
    (cons 'table
          (cons 'make-self
                (cons (cons 'quote (cons type 'nil))
                      (cons (cons 'quote (cons make-self-name 'nil))
                            'nil))))
    (defmake-self-gen-table-events-loop (rest member-names))))))

Theorem: pseudo-event-form-listp-of-defmake-self-gen-table-events-loop

(defthm
      pseudo-event-form-listp-of-defmake-self-gen-table-events-loop
  (b* ((events (defmake-self-gen-table-events-loop member-names)))
    (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: true-listp-of-defmake-self-gen-table-events-loop

(defthm true-listp-of-defmake-self-gen-table-events-loop
  (b* ((events (defmake-self-gen-table-events-loop member-names)))
    (true-listp events))
  :rule-classes :type-prescription)

Function: defmake-self-gen-table-events

(defun defmake-self-gen-table-events (clique-name member-names)
 (declare (xargs :guard (and (symbolp clique-name)
                             (symbol-listp member-names))))
 (let ((__function__ 'defmake-self-gen-table-events))
   (declare (ignorable __function__))
   (b* ((member-table-events
             (defmake-self-gen-table-events-loop member-names)))
     (if (member-eq clique-name member-names)
         member-table-events
       (cons (cons 'table
                   (cons 'make-self
                         (cons (cons 'quote (cons clique-name 'nil))
                               '('nil))))
             member-table-events)))))

Theorem: pseudo-event-form-listp-of-defmake-self-gen-table-events

(defthm pseudo-event-form-listp-of-defmake-self-gen-table-events
  (b*
    ((events
          (defmake-self-gen-table-events clique-name member-names)))
    (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: true-listp-of-defmake-self-gen-table-events

(defthm true-listp-of-defmake-self-gen-table-events
  (b*
    ((events
          (defmake-self-gen-table-events clique-name member-names)))
    (true-listp events))
  :rule-classes :type-prescription)