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

Generate the ``make-self'' function for a list type.

Signature

(defmake-self-gen-list list mutrecp fty-table make-self-table) 
  → 
events

Arguments

list — Guard (flexlist-p list).

mutrecp — Guard (booleanp mutrecp).

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

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

Returns

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

Definitions and Theorems

Function: defmake-self-gen-list

(defun defmake-self-gen-list
       (list mutrecp fty-table make-self-table)
 (declare (xargs :guard (and (flexlist-p list)
                             (booleanp mutrecp)
                             (alistp fty-table)
                             (alistp make-self-table))))
 (let ((__function__ 'defmake-self-gen-list))
  (declare (ignorable __function__))
  (b*
   ((type (flexlist->name list))
    ((unless (symbolp type))
     (raise "Internal error: malformed type name ~x0."
            type)
     (list '(_)))
    (type-make-self (defmake-self-gen-name type))
    (type-make-self-loop
         (acl2::packn-pos (list type-make-self '-loop)
                          type-make-self))
    (type-count (flexlist->count list))
    (type-fix (flextype->fix list))
    (recog (flexlist->pred list))
    (elt-recog (flexlist->elt-type list))
    ((unless (symbolp elt-recog))
     (raise "Internal error: malformed recognizer ~x0."
            elt-recog)
     (list '(_)))
    (elt-info (flextype-with-recognizer elt-recog fty-table))
    (elt-type? (if elt-info (flextype->name elt-info)
                 nil))
    (elt-type-make-self?
      (b*
       (((unless elt-type?) nil)
        ((mv erp elt-type-make-self)
         (defmake-self-get-make-self-fn elt-type? make-self-table)))
       (if erp (raise "~@0~%" erp)
         elt-type-make-self)))
    (loop-body
     (cons
      'if
      (cons
       (cons (if (flexlist->true-listp list)
                 'endp
               'atom)
             (cons type 'nil))
       (cons
        'nil
        (cons
         (cons
          'cons
          (cons
              (if elt-type? (cons elt-type-make-self?
                                  (cons (cons 'car (cons type 'nil))
                                        'nil))
                (cons 'car
                      (cons (cons type-fix (cons type 'nil))
                            'nil)))
              (cons (cons type-make-self-loop
                          (cons (cons 'cdr (cons type 'nil))
                                'nil))
                    'nil)))
         'nil)))))
    (body
     (cons
      'let
      (cons
       (cons (cons 'list
                   (cons (cons type-make-self-loop (cons type 'nil))
                         'nil))
             'nil)
       (cons
        (cons
         'if
         (cons
          'list
          (cons
           (cons
             'cons
             (cons ''list
                   (cons (cons type-make-self-loop (cons type 'nil))
                         'nil)))
           '('nil))))
        'nil)))))
   (cons
    (cons
     'define
     (cons
      type-make-self-loop
      (cons
       (cons (cons type (cons recog 'nil))
             'nil)
       (cons
        ':parents
        (cons
         (cons (defmake-self-gen-topic-name type)
               'nil)
         (cons
          loop-body
          (if mutrecp
           (cons
            ':measure
            (cons
             (cons
                'acl2::nat-list-measure
                (cons (cons 'list
                            (cons (cons type-count (cons type 'nil))
                                  '(0)))
                      'nil))
             'nil))
           (cons ':measure
                 (cons (cons (or type-count 'acl2-count)
                             (cons type 'nil))
                       'nil)))))))))
    (cons
     (cons
      'define
      (cons
       type-make-self
       (cons
        (cons (cons type (cons recog 'nil))
              'nil)
        (cons
         ':parents
         (cons
          (cons (defmake-self-gen-topic-name type)
                'nil)
          (cons
           body
           (and
            mutrecp
            (cons
             ':measure
             (cons
              (cons
                'acl2::nat-list-measure
                (cons (cons 'list
                            (cons (cons type-count (cons type 'nil))
                                  '(1)))
                      'nil))
              'nil)))))))))
     'nil)))))

Theorem: pseudo-event-form-listp-of-defmake-self-gen-list

(defthm pseudo-event-form-listp-of-defmake-self-gen-list
  (b*
   ((events
         (defmake-self-gen-list list
                                mutrecp fty-table make-self-table)))
   (acl2::pseudo-event-form-listp events))
  :rule-classes :rewrite)