• 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
      • Specific-types
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defset
      • Defflatsum
      • Deflist-of-len
        • Deflist-of-len-implementation
          • Deflist-of-len-fn
          • Deflist-of-len-support-lemma
          • Deflist-of-len-macro-definition
      • 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

• Deflist-of-len-implementation

Deflist-of-len-fn

Events generated by deflist-of-len.

Signature

(deflist-of-len-fn type list-type length 
                   pred fix equiv parents short long wrld) 
 
  → 
event

Arguments

wrld — Guard (plist-worldp wrld).

Returns

event — A ACL2::maybe-pseudo-event-formp.

For now we only perform partial validation of the inputs. Future implementations may perform a more thorough validation.

Definitions and Theorems

Function: deflist-of-len-fn

(defun deflist-of-len-fn
       (type list-type length
             pred fix equiv parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'deflist-of-len-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp type))
     (raise
      "The TYPE input must be a symbol, ~
                but it is ~x0 instead."
      type))
    ((unless (symbolp list-type))
     (raise
      "The :LIST-TYPE input must be a symbol, ~
                but it is ~x0 instead."
      list-type))
    (fty-table (get-fixtypes-alist wrld))
    (fty-info (find-fixtype list-type fty-table))
    ((unless fty-info)
     (raise
      "The :LIST-TYPE input ~x0 must name a fixtype, ~
                but it does not."
      list-type))
    (list-pred (fixtype->pred fty-info))
    (list-fix (fixtype->fix fty-info))
    ((unless (natp length))
     (raise
      "The :LENGTH input must be a non-negative integer, ~
                but it is ~x0 instead."
      length))
    ((unless (symbolp pred))
     (raise
      "The :PRED input must be a symbol, ~
                but it is ~x0 instead."
      pred))
    ((unless (symbolp fix))
     (raise
      "The :FIX input must be a symbol, ~
                but it is ~x0 instead."
      fix))
    ((unless (symbolp equiv))
     (raise
      "The :EQUIV input must be a symbol, ~
                but it is ~x0 instead."
      equiv))
    (pkg (symbol-package-name type))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (pred (or pred (add-suffix-to-fn type "-P")))
    (fix (or fix (add-suffix-to-fn type "-FIX")))
    (equiv (or equiv (add-suffix-to-fn type "-EQUIV")))
    (booleanp-of-pred (acl2::packn-pos (list 'booleanp-of- pred)
                                       pkg-witness))
    (list-pred-when-pred-rewrite
         (acl2::packn-pos (list list-pred '-when- pred '-rewrite)
                          pkg-witness))
    (list-pred-when-pred-forward
         (acl2::packn-pos (list list-pred '-when- pred '-forward)
                          pkg-witness))
    (len-when-pred-tau (acl2::packn-pos (list 'len-when- pred '-tau)
                                        pkg-witness))
    (pred-of-fix (acl2::packn-pos (list pred '-of- fix)
                                  pkg-witness))
    (fix-when-pred (acl2::packn-pos (list fix '-when- pred)
                                    pkg-witness))
    (x (intern-in-package-of-symbol "X" pkg-witness))
    (type-ref
      (concatenate
           'string
           "@(tsee "
           (common-lisp::string-downcase (symbol-package-name type))
           "::"
           (common-lisp::string-downcase (symbol-name type))
           ")"))
    (pred-event
     (cons
      'define
      (cons
       pred
       (cons
        (cons x 'nil)
        (cons
         ':parents
         (cons
          (cons type 'nil)
          (cons
           ':short
           (cons
            (concatenate 'string
                         "Recognizer for " type-ref ".")
            (cons
             (cons 'and
                   (cons (cons list-pred (cons x 'nil))
                         (cons (cons 'equal
                                     (cons (cons 'len (cons x 'nil))
                                           (cons length 'nil)))
                               'nil)))
             (cons
              ':no-function
              (cons
               't
               (cons
                '///
                (cons
                 (cons
                  'defrule
                  (cons
                   booleanp-of-pred
                   (cons
                        (cons 'booleanp
                              (cons (cons pred (cons x 'nil)) 'nil))
                        'nil)))
                 (cons
                  (cons
                   'defrule
                   (cons
                    list-pred-when-pred-rewrite
                    (cons
                     (cons
                          'implies
                          (cons (cons pred (cons x 'nil))
                                (cons (cons list-pred (cons x 'nil))
                                      'nil)))
                     'nil)))
                  (cons
                   (cons
                    'defrule
                    (cons
                     list-pred-when-pred-forward
                     (cons
                      (cons
                          'implies
                          (cons (cons pred (cons x 'nil))
                                (cons (cons list-pred (cons x 'nil))
                                      'nil)))
                      '(:rule-classes :forward-chaining))))
                   (cons
                    (cons
                     'defrule
                     (cons
                      len-when-pred-tau
                      (cons
                       (cons
                        'implies
                        (cons
                         (cons pred (cons x 'nil))
                         (cons (cons 'equal
                                     (cons (cons 'len (cons x 'nil))
                                           (cons length 'nil)))
                               'nil)))
                       '(:rule-classes :tau-system))))
                    'nil))))))))))))))))
    (fix-event
     (cons
      'define
      (cons
       fix
       (cons
        (cons (cons x (cons pred 'nil)) 'nil)
        (cons
         ':parents
         (cons
          (cons type 'nil)
          (cons
           ':short
           (cons
            (concatenate 'string
                         "Fixer for " type-ref ".")
            (cons
             (cons
              'mbe
              (cons
               ':logic
               (cons
                (cons
                 'if
                 (cons
                  (cons pred (cons x 'nil))
                  (cons
                   x
                   (cons
                    (cons
                      list-fix
                      (cons (cons 'take (cons length (cons x 'nil)))
                            'nil))
                    'nil))))
                (cons ':exec (cons x 'nil)))))
             (cons
              ':no-function
              (cons
               't
               (cons
                '///
                (cons
                 (cons
                  'defrule
                  (cons
                   pred-of-fix
                   (cons
                    (cons pred
                          (cons (cons fix (cons x 'nil)) 'nil))
                    (cons
                     ':enable
                     (cons
                         (cons pred '(deflist-of-len-support-lemma))
                         '(:disable take))))))
                 (cons
                  (cons
                   'defrule
                   (cons
                    fix-when-pred
                    (cons
                     (cons
                      'implies
                      (cons
                          (cons pred (cons x 'nil))
                          (cons (cons 'equal
                                      (cons (cons fix (cons x 'nil))
                                            (cons x 'nil)))
                                'nil)))
                     'nil)))
                  'nil))))))))))))))
    (type-event
     (cons
      'defsection
      (cons
       type
       (append
        (and parents (list :parents parents))
        (append
         (and short (list :short short))
         (append
          (and long (list :long long))
          (cons
           (cons
            'deffixtype
            (cons
             type
             (cons
              ':pred
              (cons
               pred
               (cons
                ':fix
                (cons
                   fix
                   (cons ':equiv
                         (cons equiv '(:define t :forward t)))))))))
           'nil))))))))
   (cons
    'encapsulate
    (cons 'nil
          (cons '(logic)
                (cons pred-event
                      (cons fix-event (cons type-event 'nil)))))))))