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

Generate all the events.

Signature

(defmake-self-gen-everything type/clique-name 
                             parents-presentp parents 
                             short-presentp short long-presentp 
                             long print fty-table make-self-table) 
 
  → 
(mv er? event)

Arguments

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

parents-presentp — Guard (booleanp parents-presentp).

short-presentp — Guard (booleanp short-presentp).

long-presentp — Guard (booleanp long-presentp).

print — Guard (acl2::evmac-input-print-p print).

fty-table — Guard (alistp fty-table).

make-self-table — Guard (alistp make-self-table).

Returns

er? — Type (acl2::maybe-msgp er?).

event — Type (acl2::pseudo-event-formp event).

Definitions and Theorems

Function: defmake-self-gen-everything

(defun defmake-self-gen-everything
       (type/clique-name parents-presentp parents
                         short-presentp short long-presentp
                         long print fty-table make-self-table)
 (declare (xargs :guard (and (symbolp type/clique-name)
                             (booleanp parents-presentp)
                             (booleanp short-presentp)
                             (booleanp long-presentp)
                             (acl2::evmac-input-print-p print)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((reterr) '(_))
    (main-clique
     (or
        (flextypes-with-name type/clique-name fty-table)
        (flextypes-containing-flextype type/clique-name fty-table)))
    ((unless main-clique)
     (retmsg$ "No type (clique) with name ~x0."
              type/clique-name))
    ((unless (flextypes-p main-clique))
     (retmsg$ "Internal error: malformed type clique ~x0."
              main-clique))
    (clique-name (flextypes->name main-clique))
    ((unless (symbolp clique-name))
     (retmsg$ "Internal error: malformed clique name ~x0."
              clique-name))
    (clique-names (topo-dependencies clique-name fty-table))
    ((erp make-self-events)
     (defmake-self-gen-cliques
          clique-names fty-table make-self-table))
    (xdoc-name (defmake-self-gen-topic-name clique-name))
    (xdoc-event
     (cons
      'acl2::defxdoc+
      (cons
        xdoc-name
        (append (and parents-presentp
                     (cons ':parents (cons parents 'nil)))
                (append (and short-presentp
                             (cons ':short (cons short 'nil)))
                        (append (and long-presentp
                                     (cons ':long (cons long 'nil)))
                                '(:order-subtopics t)))))))
    (encapsulate (cons 'encapsulate
                       (cons 'nil
                             (cons xdoc-event make-self-events)))
)
    (encapsulate (acl2::restore-output? (eq print :all)
                                        encapsulate)
)
    (print-result
      (if
       (member-eq print '(:result :info))
       (cons (cons 'acl2::cw-event
                   (cons '"~x0~|"
                         (cons (cons 'quote (cons encapsulate 'nil))
                               'nil)))
             'nil)
       nil)))
   (retok (cons 'progn
                (append print-result
                        (cons encapsulate
                              '((value-triple :invisible)))))))))

Theorem: maybe-msgp-of-defmake-self-gen-everything.er?

(defthm maybe-msgp-of-defmake-self-gen-everything.er?
  (b* (((mv ?er? acl2::?event)
        (defmake-self-gen-everything
             type/clique-name
             parents-presentp parents
             short-presentp short long-presentp
             long print fty-table make-self-table)))
    (acl2::maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-defmake-self-gen-everything.event

(defthm pseudo-event-formp-of-defmake-self-gen-everything.event
  (b* (((mv ?er? acl2::?event)
        (defmake-self-gen-everything
             type/clique-name
             parents-presentp parents
             short-presentp short long-presentp
             long print fty-table make-self-table)))
    (acl2::pseudo-event-formp event))
  :rule-classes :rewrite)