• 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-reduce-implementation
            • Deffold-reduce-event-generation
            • Deffoldred-process-inputs-and-gen-everything
            • Deffoldred-fn
            • Deffold-reduce-input-processing
              • Deffoldred-process-inputs
              • Deffoldred-process-override
              • Deffoldred-process-types
              • *deffoldred-allowed-options*
            • Deffoldred-macro-definition
        • Deffold-map
        • Defmake-self
      • 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

• Deffold-reduce-input-processing

Deffoldred-process-override

Process the :override input.

Signature

(deffoldred-process-override override fty-table) 
  → 
(mv erp overrides)

Arguments

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

Returns

overrides — Type (alistp overrides).

The :override input must be a list. We go through each eleemnt, which must be a 2-tuple or a 3-tuple. In that tuple, the first element must be always a type name, which we must find in the FTY table. Both sum and product types are stored in the table as sum types, but the data structure indicates the type macro, i.e. whether it is a defprod or deftagsum; we use that to distinguish them.

Definitions and Theorems

Function: deffoldred-process-override-loop

(defun deffoldred-process-override-loop (override fty-table)
 (declare (xargs :guard (and (true-listp override)
                             (alistp fty-table))))
 (let ((__function__ 'deffoldred-process-override-loop))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when (endp override)) (retok nil))
    (ovrd (car override))
    ((unless (or (std::tuplep 2 ovrd)
                 (std::tuplep 3 ovrd)))
     (reterr
      (msg
       "Every element of the :OVERRIDE list ~
                         must be a list of 2 or 3 elements, ~
                         but the element ~x0 is not."
       ovrd)))
    (type (car ovrd))
    (term (car (last ovrd)))
    ((unless (symbolp type))
     (reterr
      (msg
       "The first element of ~
                         every element of the :OVERRIDE list ~
                         must be a symbol, ~
                         but ~x0 is not."
       type)))
    (info (flextype-with-name type fty-table))
    ((unless info)
     (reterr
      (msg
       "The first element of ~
                         every element of the :OVERRIDE list ~
                         must be the name of a type, ~
                         but ~x0 is not."
       type)))
    ((unless (flexsum-p info))
     (reterr
      (msg
       "The first element of ~
                         every element of the :OVERRIDE list ~
                         must be the name of a product or sum type, ~
                         but ~x0 is not."
       type)))
    (typemacro (flexsum->typemacro info))
    ((unless (member-eq typemacro (list 'defprod 'deftagsum)))
     (reterr
      (msg
       "The first element of ~
                         every element of the :OVERRIDE list ~
                         must be the name of a product or sum type, ~
                         but ~x0 is not."
       type)))
    ((erp key val)
     (if (= (len ovrd) 2)
         (mv nil type term)
      (b*
       (((reterr) nil nil)
        (kind (cadr ovrd))
        ((unless (keywordp kind))
         (reterr
          (msg
           "The second element of ~
                                 every element of the :OVERRIDE list ~
                                 that is a 3-tuple ~
                                 must be a keyword, ~
                                 but ~x0 is not."
           kind)))
        (prods (flexsum->prods info))
        ((unless (flexprod-listp prods))
         (raise "Internal error: malformed summands ~x0."
                prods)
         (reterr t))
        ((unless (member-eq kind (flexprod-list->kind-list prods)))
         (reterr
          (msg
           "The kind ~x0 that accompanies ~
                                 the type ~x1 in the :OVERRIDE list ~
                                 is not one of the kinds of that sum type."
           kind type))))
       (retok (cons type kind) term))))
    ((erp alist)
     (deffoldred-process-override-loop (cdr override)
                                       fty-table)))
   (retok (acons key val alist)))))

Theorem: alistp-of-deffoldred-process-override-loop.overrides

(defthm alistp-of-deffoldred-process-override-loop.overrides
  (b* (((mv ?erp ?overrides)
        (deffoldred-process-override-loop override fty-table)))
    (alistp overrides))
  :rule-classes :rewrite)

Function: deffoldred-process-override

(defun deffoldred-process-override (override fty-table)
 (declare (xargs :guard (alistp fty-table)))
 (let ((__function__ 'deffoldred-process-override))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((unless (true-listp override))
     (reterr
      (msg
       "The :OVERRIDE input must be a list, ~
                      but it is ~x0 instead."
       override))))
   (deffoldred-process-override-loop override fty-table))))

Theorem: alistp-of-deffoldred-process-override.overrides

(defthm alistp-of-deffoldred-process-override.overrides
  (b* (((mv ?erp ?overrides)
        (deffoldred-process-override override fty-table)))
    (alistp overrides))
  :rule-classes :rewrite)