Filtering...

visitor

books/centaur/fty/visitor
other
(in-package "FTY")
other
(include-book "deftypes")
other
(include-book "tools/templates" :dir :system)
other
(program)
other
(define my-intern
  (string sym)
  (intern-in-package-of-symbol string
    (if (equal (symbol-package-name sym) "COMMON-LISP")
      (pkg-witness "ACL2")
      sym)))
other
(def-primitive-aggregate visitorspec
  (name formals
    returns
    accum-vars
    join-vars
    type-fns
    field-fns
    prod-fns
    initial
    join
    xvar
    fnname-template
    renames
    measure
    fixequivs
    prepwork
    reversep
    wrapper
    macrop
    defines-args
    define-args
    order
    binder
    wrld))
other
(define visitor-return-binder-aux
  (returns fldname firstp x)
  (b* (((when (atom returns)) nil) ((visitorspec x))
      ((mv name type) (if (consp (car returns))
          (b* (((list name type) (car returns)))
            (mv name type))
          (mv (car returns) nil)))
      (accum (rassoc-eq name x.accum-vars))
      (name (cond ((or (eq type :update) (eq (car type) :update)) fldname)
          ((or (eq type :ignore) (eq (car type) :ignore)) '&)
          (accum (car accum))
          (firstp name)
          (t (cdr (assoc name x.join-vars))))))
    (cons name
      (visitor-return-binder-aux (cdr returns)
        fldname
        firstp
        x))))
other
(define visitor-return-binder
  (returns fldname firstp x)
  (b* ((returns (if (and (consp returns) (eq (car returns) 'mv))
         (cdr returns)
         (list returns))) (lst (visitor-return-binder-aux returns
          fldname
          firstp
          x))
      (binder (visitorspec->binder x))
      ((when (eql (len returns) 1)) (if binder
          `(,FTY::BINDER ,(CAR FTY::LST))
          (car lst))))
    (cons (or binder 'mv) lst)))
other
(define visitor-macroname
  (x type)
  (b* (((visitorspec x)) (look (assoc type x.renames))
      ((when look) (cadr look))
      ((when x.fnname-template) (tmpl-sym-sublis `(("<TYPE>" . ,(SYMBOL-NAME TYPE)))
          x.fnname-template
          x.name)))
    (tmpl-sym-sublis `(("<TYPE>" . ,(SYMBOL-NAME TYPE)) ("<VISITOR>" . ,(SYMBOL-NAME FTY::X.NAME)))
      '<visitor>-<type>
      x.name)))
other
(define visitor-fnname
  (x type)
  (b* (((visitorspec x)) (macroname (visitor-macroname x type))
      ((when x.macrop) (intern-in-package-of-symbol (concatenate 'string (symbol-name macroname) "-FN")
          macroname)))
    macroname))
other
(define visitor-normalize-fixtype
  (type wrld)
  (b* ((fty (find-fixtype-for-pred type
         (get-fixtypes-alist wrld))) ((when fty) (fixtype->name fty)))
    type))
other
(define visitor-field-fn
  (fldname fldtype prod x)
  (b* (((visitorspec x)) (fldtype (visitor-normalize-fixtype fldtype x.wrld))
      (prod-fns (and prod (cdr (assoc prod x.prod-fns))))
      (prod-fld (and fldname (assoc fldname prod-fns)))
      ((when prod-fld) (if (eq (cdr prod-fld) :skip)
          nil
          (cdr prod-fld)))
      (fld (assoc fldname x.field-fns))
      ((when fld) (if (eq (cdr fld) :skip)
          nil
          (cdr fld)))
      (type (assoc fldtype x.type-fns))
      ((when type) (if (eq (cdr type) :skip)
          nil
          (cdr type))))
    nil))
other
(define strip-cars-of-pairs
  (x)
  (if (atom x)
    nil
    (cons (if (consp (car x))
        (caar x)
        (car x))
      (strip-cars-of-pairs (cdr x)))))
other
(define visitor-formal-names
  (formals)
  (strip-cars-of-pairs (remove-macro-args 'visitor formals nil)))
other
(define visitor-prod-field-joins
  (fields x prodname firstp)
  :returns (mv changes bindings)
  (b* (((visitorspec x) x) ((when (atom fields)) (if firstp
          (mv nil x.initial)
          (mv nil nil)))
      ((flexprod-field fld) (car fields))
      (fnname (visitor-field-fn fld.name
          fld.type
          prodname
          x))
      ((unless fnname) (visitor-prod-field-joins (cdr fields)
          x
          prodname
          firstp))
      ((mv rest-changes rest-bindings) (visitor-prod-field-joins (cdr fields)
          x
          prodname
          nil)))
    (mv `(,(FTY::INTERN$ (SYMBOL-NAME FTY::FLD.NAME) "KEYWORD") ,FTY::FLD.NAME . ,FTY::REST-CHANGES)
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS FTY::FLD.NAME FTY::FIRSTP FTY::X) (,FTY::FNNAME . ,(SUBST
  (FTY::MY-INTERN
   (CONCATENATE 'STRING (SYMBOL-NAME FTY::X.XVAR) "."
                (SYMBOL-NAME FTY::FLD.NAME))
   FTY::X.XVAR)
  FTY::X.XVAR (FTY::VISITOR-FORMAL-NAMES FTY::X.FORMALS)))) ,@(AND (NOT FTY::FIRSTP) FTY::X.JOIN) . ,FTY::REST-BINDINGS))))
other
(define visitor-return-values-aux
  (returns update x typeinfo)
  (b* (((when (atom returns)) nil) ((visitorspec x))
      ((mv name type) (if (consp (car returns))
          (b* (((list name type) (car returns)))
            (mv name type))
          (mv (car returns) nil)))
      (accum (rassoc-eq name x.accum-vars))
      (ret1 (cond ((or (eq type :update) (equal type '(:update))) update)
          ((eq (car type) :update) (template-subst (cadr type)
              :atom-alist (cons (cons :update update) typeinfo)))
          ((eq type :ignore) nil)
          ((eq (car type) :ignore) (cadr (member :return type)))
          (accum (car accum))
          (t name))))
    (cons ret1
      (visitor-return-values-aux (cdr returns)
        update
        x
        typeinfo))))
other
(define visitor-return-values
  (returns update x typeinfo)
  (b* ((returns (if (and (consp returns) (eq (car returns) 'mv))
         (cdr returns)
         (list returns))) (lst (visitor-return-values-aux returns
          update
          x
          typeinfo))
      ((when (eql (len returns) 1)) (car lst)))
    (cons 'mv lst)))
other
(define visitor-return-decls-aux
  (returns type-pred type-fix)
  (b* (((when (atom returns)) nil) ((list* name rettype rest) (car returns))
      (rest-returns (visitor-return-decls-aux (cdr returns)
          type-pred
          type-fix))
      ((when (eq rettype :update)) (cons (list* name type-pred rest)
          rest-returns))
      ((when (eq (car rettype) :update)) (b* ((look (assoc-keyword :type rettype)) ((unless look) (cons (list* name type-pred rest)
                rest-returns)))
          (cons (list* name
              (sublis `((:type . ,FTY::TYPE-PRED) (:fix . ,FTY::TYPE-FIX))
                (cadr look))
              rest)
            rest-returns))))
    (cons (cons name rest) rest-returns)))
other
(define visitor-return-decls
  (returns type-name type-pred type-fix)
  (b* ((returns (if (and (consp returns) (eq (car returns) 'mv))
         (cdr returns)
         (list returns))) (returns (template-subst-top returns
          (make-tmplsubst :strs `(("<TYPE>" ,(SYMBOL-NAME FTY::TYPE-NAME) . ,FTY::TYPE-NAME)))))
      (lst (visitor-return-decls-aux returns
          type-pred
          type-fix)))
    (if (eql (len returns) 1)
      (car lst)
      (cons 'mv lst))))
other
(define visitor-prod-subbody
  (prod x typeinfo)
  (b* (((flexprod prod)) ((visitorspec x))
      ((mv changer-args bindings) (visitor-prod-field-joins (if x.reversep
            (reverse prod.fields)
            prod.fields)
          x
          prod.type-name
          t)))
    `(b* (,@FTY::BINDINGS)
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  `(,(STD::DA-CHANGER-NAME FTY::PROD.CTOR-NAME) ,FTY::X.XVAR
    ,@FTY::CHANGER-ARGS)
  FTY::X FTY::TYPEINFO))))
other
(define visitor-measure
  (x default type-name)
  (b* (((visitorspec x)))
    (if x.measure
      (template-subst x.measure
        :str-alist `(("<TYPE>" ,(SYMBOL-NAME FTY::TYPE-NAME) . ,FTY::TYPE-NAME))
        :atom-alist `((:order . ,FTY::X.ORDER) (:count . ,FTY::DEFAULT)))
      default)))
other
(define visitor-prod-body
  (type x typeinfo)
  (b* (((flexsum type)) ((visitorspec x))
      ((flexprod prod) (car type.prods)))
    `(b* (((,FTY::PROD.CTOR-NAME ,FTY::X.XVAR) (,FTY::TYPE.FIX ,FTY::X.XVAR)))
      ,(FTY::VISITOR-PROD-SUBBODY FTY::PROD FTY::X FTY::TYPEINFO))))
other
(define visitor-prod-bodies
  (prods x typeinfo)
  (b* (((when (atom prods)) nil) ((flexprod prod) (car prods)))
    `(,FTY::PROD.KIND ,(FTY::VISITOR-PROD-SUBBODY FTY::PROD FTY::X FTY::TYPEINFO) . ,(FTY::VISITOR-PROD-BODIES (CDR FTY::PRODS) FTY::X FTY::TYPEINFO))))
other
(define visitor-sum-body
  (type x)
  (b* (((flexsum type)) (typeinfo `((:fix . ,FTY::TYPE.FIX) (:pred . ,FTY::TYPE.PRED)))
      ((when (eql (len type.prods) 1)) (visitor-prod-body type x typeinfo))
      ((visitorspec x)))
    `(,FTY::TYPE.CASE ,FTY::X.XVAR . ,(FTY::VISITOR-PROD-BODIES FTY::TYPE.PRODS FTY::X FTY::TYPEINFO))))
other
(define visitor-sum-measure
  (type x mrec)
  (b* (((flexsum type)) ((visitorspec x)))
    (and (or mrec type.recp)
      `(:measure ,(FTY::VISITOR-MEASURE FTY::X
  (IF FTY::TYPE.COUNT
      `(,FTY::TYPE.COUNT ,FTY::X.XVAR)
      0)
  FTY::TYPE.NAME)))))
other
(define flextranssum-memberlist->typenames
  (members)
  (if (atom members)
    nil
    (cons (flextranssum-member->name (car members))
      (flextranssum-memberlist->typenames (cdr members)))))
other
(define visitor-transsum-updates
  (member x)
  :returns (mv updated-member bindings)
  (b* (((visitorspec x) x) ((flextranssum-member member))
      (typefn-lookup (assoc member.name x.type-fns))
      ((when (or (not typefn-lookup)
           (eq (cdr typefn-lookup) :skip))) (mv x.xvar x.initial))
      (fnname (cdr typefn-lookup))
      (update-name (my-intern (cat (symbol-name x.xvar)
            "."
            (symbol-name member.name))
          x.xvar)))
    (mv update-name
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS FTY::UPDATE-NAME T FTY::X) (,FTY::FNNAME . ,(FTY::VISITOR-FORMAL-NAMES FTY::X.FORMALS)))))))
other
(define visitor-transsum-member-body
  (member x typeinfo)
  (b* (((visitorspec x)) ((mv new-value bindings) (visitor-transsum-updates member x)))
    `(b* (,@FTY::BINDINGS)
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS FTY::NEW-VALUE FTY::X FTY::TYPEINFO))))
other
(define visitor-transsum-member-bodies
  (members x typeinfo)
  (cond ((atom members) nil)
    ((atom (cdr members)) (list (list 'otherwise
          (visitor-transsum-member-body (car members)
            x
            typeinfo))))
    (t (b* (((flextranssum-member member) (car members)))
        (cons `(,FTY::MEMBER.TAGS ,(FTY::VISITOR-TRANSSUM-MEMBER-BODY (CAR FTY::MEMBERS) FTY::X FTY::TYPEINFO))
          (visitor-transsum-member-bodies (cdr members)
            x
            typeinfo))))))
other
(define visitor-transsum-body
  (type x)
  (b* (((flextranssum type)) ((visitorspec x)))
    `(let ((,FTY::X.XVAR (,FTY::TYPE.FIX ,FTY::X.XVAR)))
      (case (tag ,FTY::X.XVAR) . ,(FTY::VISITOR-TRANSSUM-MEMBER-BODIES FTY::TYPE.MEMBERS FTY::X
  `((:FIX . ,FTY::TYPE.FIX) (:PRED . ,FTY::TYPE.PRED)))))))
other
(define visitor-transsum-measure
  (type x mrec)
  (declare (ignorable type mrec))
  (b* ((default 0) (typename (flextranssum->name type)))
    `(:measure ,(FTY::VISITOR-MEASURE FTY::X FTY::DEFAULT FTY::TYPENAME))))
other
(define visitor-list-measure
  (type x mrec)
  (declare (ignorable mrec))
  (b* (((flexlist type)) ((visitorspec x)))
    `(:measure ,(FTY::VISITOR-MEASURE FTY::X
  (IF FTY::TYPE.COUNT
      `(,FTY::TYPE.COUNT ,FTY::X.XVAR)
      `(FTY::LEN ,FTY::X.XVAR))
  FTY::TYPE.NAME))))
other
(define visitor-list-body
  (type x)
  (b* (((flexlist type)) ((visitorspec x))
      (name (visitor-fnname x type.name))
      (elt-fnname (visitor-field-fn :elt type.elt-type
          type.name
          x))
      (formal-names (visitor-formal-names x.formals))
      ((unless elt-fnname) (er hard?
          'defvisitor
          "Nothing to do for list type ~x0 -- use :skip."
          type.name))
      (typeinfo `((:fix . ,FTY::TYPE.FIX) (:pred . ,FTY::TYPE.PRED))))
    `(b* (((when (atom ,FTY::X.XVAR)) (b* (,@FTY::X.INITIAL)
           ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  (IF FTY::TYPE.TRUE-LISTP
      NIL
      FTY::X.XVAR)
  FTY::X FTY::TYPEINFO))) ,@(IF FTY::X.REVERSEP
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR T FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CAR NIL FTY::X)
         (,FTY::ELT-FNNAME
          . ,(SUBST `(CAR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES))))
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CAR T FTY::X)
         (,FTY::ELT-FNNAME
          . ,(SUBST `(CAR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR NIL FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))))
        ,@FTY::X.JOIN)
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  `(FTY::CONS-WITH-HINT CAR CDR ,FTY::X.XVAR) FTY::X FTY::TYPEINFO))))
other
(define visitor-alist-measure
  (type x mrec)
  (declare (ignorable mrec))
  (b* (((flexalist type)) ((visitorspec x)))
    `(:measure ,(FTY::VISITOR-MEASURE FTY::X
  (IF FTY::TYPE.COUNT
      `(,FTY::TYPE.COUNT ,FTY::X.XVAR)
      `(FTY::LEN (,FTY::TYPE.FIX ,FTY::X.XVAR)))
  FTY::TYPE.NAME))))
other
(define visitor-alist-body
  (type x)
  (b* (((flexalist type)) ((visitorspec x))
      (name (visitor-fnname x type.name))
      (key-fnname (visitor-field-fn :key type.key-type
          type.name
          x))
      (val-fnname (visitor-field-fn :val type.val-type
          type.name
          x))
      (formal-names (visitor-formal-names x.formals))
      ((unless (or key-fnname val-fnname)) (er hard?
          'defvisitor
          "Nothing to do for alist type ~x0 -- use :skip."
          type.name))
      (typeinfo `((:fix . ,FTY::TYPE.FIX) (:pred . ,FTY::TYPE.PRED))))
    `(b* ((,FTY::X.XVAR (,FTY::TYPE.FIX ,FTY::X.XVAR)) ((when (atom ,FTY::X.XVAR)) (b* (,@FTY::X.INITIAL)
            ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  (IF FTY::TYPE.TRUE-LISTP
      NIL
      FTY::X.XVAR)
  FTY::X FTY::TYPEINFO)))
        ,@(IF FTY::X.REVERSEP
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR T FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        ,@(AND FTY::VAL-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::VAL NIL
                    FTY::X)
                  (,FTY::VAL-FNNAME
                   . ,(SUBST `(CDAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@FTY::X.JOIN))
        ,@(AND FTY::KEY-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::KEY NIL
                    FTY::X)
                  (,FTY::KEY-FNNAME
                   . ,(SUBST `(CAAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@FTY::X.JOIN)))
      `(,@(AND FTY::KEY-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::KEY T
                    FTY::X)
                  (,FTY::KEY-FNNAME
                   . ,(SUBST `(CAAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))))
        ,@(AND FTY::VAL-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::VAL
                    (NOT FTY::KEY-FNNAME) FTY::X)
                  (,FTY::VAL-FNNAME
                   . ,(SUBST `(CDAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@(AND FTY::KEY-FNNAME FTY::X.JOIN)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR NIL FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        ,@FTY::X.JOIN)))
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  `(FTY::CONS-WITH-HINT
    (FTY::CONS-WITH-HINT
     ,(IF FTY::KEY-FNNAME
          'FTY::KEY
          `(CAAR ,FTY::X.XVAR))
     ,(IF FTY::VAL-FNNAME
          'FTY::VAL
          `(CDAR ,FTY::X.XVAR))
     (CAR ,FTY::X.XVAR))
    CDR ,FTY::X.XVAR)
  FTY::X FTY::TYPEINFO))))
other
(define visitor-set-measure
  (type x mrec)
  (declare (ignorable mrec))
  (b* (((flexset type)) ((visitorspec x)))
    `(:measure ,(FTY::VISITOR-MEASURE FTY::X
  (IF FTY::TYPE.COUNT
      `(,FTY::TYPE.COUNT ,FTY::X.XVAR)
      `(FTY::LEN ,FTY::X.XVAR))
  FTY::TYPE.NAME))))
other
(define visitor-set-body
  (type x)
  (b* (((flexset type)) ((visitorspec x))
      (name (visitor-fnname x type.name))
      (elt-fnname (visitor-field-fn :elt type.elt-type
          type.name
          x))
      (formal-names (visitor-formal-names x.formals))
      ((unless elt-fnname) (er hard?
          'defvisitor
          "Nothing to do for set type ~x0 -- use :skip."
          type.name))
      (typeinfo `((:fix . ,FTY::TYPE.FIX) (:pred . ,FTY::TYPE.PRED))))
    `(b* (((when (atom ,FTY::X.XVAR)) (b* (,@FTY::X.INITIAL)
           ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS NIL FTY::X FTY::TYPEINFO))) ,@(IF FTY::X.REVERSEP
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR T FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CAR NIL FTY::X)
         (,FTY::ELT-FNNAME
          . ,(SUBST `(CAR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES))))
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CAR T FTY::X)
         (,FTY::ELT-FNNAME
          . ,(SUBST `(CAR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR NIL FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))))
        ,@FTY::X.JOIN)
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  `(FTY::CONS-WITH-HINT CAR CDR ,FTY::X.XVAR) FTY::X FTY::TYPEINFO))))
other
(define visitor-omap-measure
  (type x mrec)
  (declare (ignorable mrec))
  (b* (((flexomap type)) ((visitorspec x)))
    `(:measure ,(FTY::VISITOR-MEASURE FTY::X
  (IF FTY::TYPE.COUNT
      `(,FTY::TYPE.COUNT ,FTY::X.XVAR)
      `(FTY::LEN ,FTY::X.XVAR))
  FTY::TYPE.NAME))))
other
(define visitor-omap-body
  (type x)
  (b* (((flexomap type)) ((visitorspec x))
      (name (visitor-fnname x type.name))
      (key-fnname (visitor-field-fn :key type.key-type
          type.name
          x))
      (val-fnname (visitor-field-fn :val type.val-type
          type.name
          x))
      (formal-names (visitor-formal-names x.formals))
      ((unless (or key-fnname val-fnname)) (er hard?
          'defvisitor
          "Nothing to do for omap type ~x0 -- use :skip."
          type.name))
      (typeinfo `((:fix . ,FTY::TYPE.FIX) (:pred . ,FTY::TYPE.PRED))))
    `(b* ((,FTY::X.XVAR (,FTY::TYPE.FIX ,FTY::X.XVAR)) ((when (atom ,FTY::X.XVAR)) (b* (,@FTY::X.INITIAL)
            ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS NIL FTY::X FTY::TYPEINFO)))
        ,@(IF FTY::X.REVERSEP
      `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR T FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        ,@(AND FTY::VAL-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::VAL NIL
                    FTY::X)
                  (,FTY::VAL-FNNAME
                   . ,(SUBST `(CDAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@FTY::X.JOIN))
        ,@(AND FTY::KEY-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::KEY NIL
                    FTY::X)
                  (,FTY::KEY-FNNAME
                   . ,(SUBST `(CAAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@FTY::X.JOIN)))
      `(,@(AND FTY::KEY-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::KEY T
                    FTY::X)
                  (,FTY::KEY-FNNAME
                   . ,(SUBST `(CAAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))))
        ,@(AND FTY::VAL-FNNAME
               `((,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'FTY::VAL
                    (NOT FTY::KEY-FNNAME) FTY::X)
                  (,FTY::VAL-FNNAME
                   . ,(SUBST `(CDAR ,FTY::X.XVAR) FTY::X.XVAR
                             FTY::FORMAL-NAMES)))
                 ,@(AND FTY::KEY-FNNAME FTY::X.JOIN)))
        (,(FTY::VISITOR-RETURN-BINDER FTY::X.RETURNS 'CDR NIL FTY::X)
         (,FTY::NAME
          . ,(SUBST `(CDR ,FTY::X.XVAR) FTY::X.XVAR FTY::FORMAL-NAMES)))
        ,@FTY::X.JOIN)))
      ,(FTY::VISITOR-RETURN-VALUES FTY::X.RETURNS
  `(FTY::CONS-WITH-HINT
    (FTY::CONS-WITH-HINT
     ,(IF FTY::KEY-FNNAME
          'FTY::KEY
          `(CAAR ,FTY::X.XVAR))
     ,(IF FTY::VAL-FNNAME
          'FTY::VAL
          `(CDAR ,FTY::X.XVAR))
     (CAR ,FTY::X.XVAR))
    CDR ,FTY::X.XVAR)
  FTY::X FTY::TYPEINFO))))
other
(define visitor-def
  (type x mrec)
  (b* ((body (with-flextype-bindings type
         (visitor-*-body type x))) (measure-args (with-flextype-bindings type
          (visitor-*-measure type x mrec)))
      ((visitorspec x))
      (type.name (with-flextype-bindings type type.name))
      (type.pred (with-flextype-bindings type type.pred))
      (type.fix (with-flextype-bindings type type.fix))
      (name (visitor-macroname x type.name))
      ((when (eq name :skip)) nil)
      (fnname (visitor-fnname x type.name))
      (formals (template-subst-top x.formals
          (make-tmplsubst :strs `(("<TYPE>" ,(SYMBOL-NAME FTY::TYPE.NAME) . ,FTY::TYPE.NAME))
            :atoms `((:object . ,FTY::TYPE.PRED))))))
    `(define ,FTY::NAME
      ,FTY::FORMALS
      :returns ,(FTY::VISITOR-RETURN-DECLS FTY::X.RETURNS FTY::TYPE.NAME FTY::TYPE.PRED
  FTY::TYPE.FIX)
      :verify-guards nil
      :hooks nil
      ,@FTY::MEASURE-ARGS
      ,@FTY::X.DEFINE-ARGS
      ,(TEMPLATE-SUBST-TOP FTY::X.WRAPPER
  (MAKE-TMPLSUBST :ATOMS
   `((:BODY . ,FTY::BODY) (:FIX . ,FTY::TYPE.FIX) (:PRED . ,FTY::TYPE.PRED))
   :STRS `(("<TYPE>" ,(SYMBOL-NAME FTY::TYPE.NAME) . ,FTY::TYPE.NAME))))
      ///
      ,@(AND (NOT FTY::MREC)
       `(,@(AND FTY::X.FIXEQUIVS `((FTY::DEFFIXEQUIV ,FTY::NAME)))
         (FTY::LOCAL (FTY::IN-THEORY (FTY::DISABLE ,FTY::NAME)))
         (FTY::VERIFY-GUARDS ,FTY::FNNAME))))))
other
(define visitor-omit-bound-types
  (types type-fns)
  (if (atom types)
    nil
    (b* ((name (with-flextype-bindings (x (car types))
           x.name)) (look (assoc name type-fns)))
      (if (cdr look)
        (visitor-omit-bound-types (cdr types)
          type-fns)
        (cons (car types)
          (visitor-omit-bound-types (cdr types)
            type-fns))))))
other
(define visitor-mutual-aux
  (types x)
  (if (atom types)
    nil
    (b* ((def (visitor-def (car types) x t)) (rest (visitor-mutual-aux (cdr types) x)))
      (if def
        (cons def rest)
        rest))))
other
(define visitor-mutual
  (type-name types x other-fns)
  (b* (((visitorspec x)) (defs (visitor-mutual-aux types x))
      ((when (and (not other-fns) (not defs))) nil))
    `(defines ,(FTY::VISITOR-MACRONAME FTY::X FTY::TYPE-NAME)
      ,@FTY::X.DEFINES-ARGS
      ,@FTY::OTHER-FNS
      ,@FTY::DEFS
      ///
      (verify-guards ,(FTY::VISITOR-FNNAME FTY::X
  (FTY::WITH-FLEXTYPE-BINDINGS (TYPE (CAR FTY::TYPES)) FTY::TYPE.NAME)))
      ,@(AND FTY::X.FIXEQUIVS
       `((FTY::DEFFIXEQUIV-MUTUAL
          ,(FTY::VISITOR-MACRONAME FTY::X FTY::TYPE-NAME)))))))
other
(define visitor-multi-aux
  (types-templates)
  (if (atom types-templates)
    nil
    (b* (((cons types template) (car types-templates)))
      (append (visitor-mutual-aux types template)
        (visitor-multi-aux (cdr types-templates))))))
other
(def-primitive-aggregate visitormulti
  (name defines-args other-fns fixequivs))
other
(define visitor-multi
  (multicfg types-templates)
  (b* (((visitormulti multicfg)) (defs (visitor-multi-aux types-templates))
      ((when (and (not multicfg.other-fns) (not defs))) nil))
    `(defines ,FTY::MULTICFG.NAME
      ,@FTY::MULTICFG.DEFINES-ARGS
      ,@FTY::MULTICFG.OTHER-FNS
      ,@FTY::DEFS
      ///
      (verify-guards ,(FTY::VISITOR-FNNAME (CDAR FTY::TYPES-TEMPLATES)
  (FTY::WITH-FLEXTYPE-BINDINGS (TYPE (CAR (CAAR FTY::TYPES-TEMPLATES)))
   FTY::TYPE.NAME)))
      ,@(AND FTY::MULTICFG.FIXEQUIVS `((FTY::DEFFIXEQUIV-MUTUAL ,FTY::MULTICFG.NAME))))))
other
(define visitor-add-type-fns
  (types x)
  (if (atom types)
    nil
    (cons (with-flextype-bindings (type (car types))
        (cons type.name
          (visitor-fnname x type.name)))
      (visitor-add-type-fns (cdr types) x))))
other
(define visitor-parse-return
  (x)
  (b* (((when (or (atom x) (atom (cdr x)))) (er hard?
         'defvisitor-template
         "Bad return entry ~x0"
         x)
       (mv nil nil nil nil)) ((list name retarg) x)
      ((when (eq retarg :update)) (mv nil nil nil nil))
      ((when (atom retarg)) (er hard?
          'defvisitor-template
          "Bad return entry ~x0"
          x)
        (mv nil nil nil nil)))
    (case (car retarg)
      (:join (b* (((mv kwd-alist rest-args) (extract-keywords 'visitor-join-return
               '(:join :tmp-var :initial)
               retarg
               nil)) ((assocs (initial :initial)
               (join :join)
               (tmp-var :tmp-var)) kwd-alist)
            ((when (or rest-args
                 (not tmp-var)
                 (not (symbolp tmp-var)))) (prog2$ (er hard?
                  'defvisitor-template
                  "Bad return entry ~x0"
                  x)
                (mv nil nil nil nil))))
          (mv nil
            (list (list name initial))
            (list (list name join))
            (list (cons name tmp-var)))))
      (:acc (b* (((mv kwd-alist rest-args) (extract-keywords 'visitor-acc-return
               '(:acc :fix)
               retarg
               nil)) (formal (cdr (assoc :acc kwd-alist)))
            (fixp (assoc :fix kwd-alist))
            (fix (cdr fixp))
            ((when rest-args) (prog2$ (er hard?
                  'defvisitor-template
                  "Bad return entry ~x0"
                  x)
                (mv nil nil nil nil))))
          (mv (list (cons formal name))
            (and fixp (list (list formal fix)))
            nil
            nil)))
      (:update (b* (((mv ?kwd-alist rest-args) (extract-keywords 'visitor-acc-return
               '(:update :type)
               retarg
               nil)) ((when rest-args) (prog2$ (er hard?
                  'defvisitor-template
                  "Bad return entry ~x0"
                  x)
                (mv nil nil nil nil))))
          (mv nil nil nil nil)))
      (:ignore (mv nil nil nil nil))
      (otherwise (prog2$ (er hard?
            'defvisitor-template
            "Bad return entry ~x0"
            x)
          (mv nil nil nil nil))))))
other
(define visitor-parse-returns-aux
  (returns)
  (b* (((when (atom returns)) (mv nil nil nil nil nil)) ((mv rest
         accums
         initials
         joins
         joinvars) (visitor-parse-returns-aux (cdr returns)))
      (return1 (car returns))
      ((mv accums1
         initials1
         joins1
         joinvars1) (visitor-parse-return return1)))
    (mv (cons return1 rest)
      (append accums1 accums)
      (append initials1 initials)
      (append joins1 joins)
      (append joinvars1 joinvars))))
other
(define visitor-parse-returns
  (returns)
  (b* ((returns (if (and (consp returns) (eq (car returns) 'mv))
         (cdr returns)
         (list returns))) ((mv rets
         accums
         initials
         joins
         joinvars) (visitor-parse-returns-aux returns)))
    (mv (if (eql (len returns) 1)
        (car rets)
        (cons 'mv rets))
      accums
      initials
      joins
      joinvars)))
other
(define visitor-symbol/fn-doubletonlist-p
  (x)
  (if (atom x)
    (eq x nil)
    (case-match x
      (((name fn) . rest) (and name
          fn
          (symbolp name)
          (or (symbolp fn)
            (and (consp fn) (eq (car fn) 'lambda)))
          (visitor-symbol/fn-doubletonlist-p rest)))
      (& nil))))
other
(define visitor-symbol/fn-doubletonlist-alist-p
  (x)
  (if (atom x)
    (eq x nil)
    (case-match x
      (((name . alist) . rest) (and name
          (symbolp name)
          (visitor-symbol/fn-doubletonlist-p alist)
          (visitor-symbol/fn-doubletonlist-alist-p rest)))
      (& nil))))
other
(define visitor-doubletonlist-to-alist
  (x)
  (if (atom x)
    nil
    (cons (cons (caar x) (cadar x))
      (visitor-doubletonlist-to-alist (cdr x)))))
other
(define visitor-doubletonlist-alist-to-alist
  (x)
  (if (atom x)
    nil
    (cons (cons (caar x)
        (visitor-doubletonlist-to-alist (cdar x)))
      (visitor-doubletonlist-alist-to-alist (cdr x)))))
other
(define visitor-normalize-type-fns
  (type-fns wrld)
  (if (atom type-fns)
    nil
    (cons (cons (visitor-normalize-fixtype (caar type-fns)
          wrld)
        (cdar type-fns))
      (visitor-normalize-type-fns (cdr type-fns)
        wrld))))
other
(defconst *defvisitor-template-keys*
  '(:returns :type-fns :field-fns :prod-fns :parents :short :long :fnname-template :renames :fixequivs :reversep :wrapper :binder :define-args :defines-args))
other
(define visitor-process-fnspecs
  (kwd-alist wrld)
  (b* ((type-fns (cdr (assoc :type-fns kwd-alist))) (- (or (visitor-symbol/fn-doubletonlist-p type-fns)
          (er hard?
            'visitor
            "Bad type-fns -- see ~x0"
            'visitor-symbol/fn-doubletonlist-p)))
      (type-fns (visitor-normalize-type-fns (visitor-doubletonlist-to-alist type-fns)
          wrld))
      (field-fns (cdr (assoc :field-fns kwd-alist)))
      (- (or (visitor-symbol/fn-doubletonlist-p field-fns)
          (er hard?
            'visitor
            "Bad field-fns -- see ~x0"
            'visitor-symbol/fn-doubletonlist-p)))
      (field-fns (visitor-doubletonlist-to-alist field-fns))
      (prod-fns (cdr (assoc :prod-fns kwd-alist)))
      (- (or (visitor-symbol/fn-doubletonlist-alist-p prod-fns)
          (er hard?
            'visitor
            "Bad prod-fns -- see ~x0"
            'visitor-symbol/fn-doubletonlist-alist-p)))
      (prod-fns (visitor-doubletonlist-alist-to-alist prod-fns)))
    (mv type-fns field-fns prod-fns)))
other
(define visitor-check-fnname-template
  (name x)
  (or (not x)
    (and (symbolp x)
      (search "<TYPE>" (symbol-name x)))
    (raise "~x0: fnname-template should be a symbol whose name contains the ~
               substring <TYPE>, but found ~x1."
      name
      x)))
other
(define visitor-xvar-from-formals
  (name formals)
  (cond ((atom formals) (raise "~x0: No input was designated the :object of the visitor."
        name))
    ((and (consp (car formals))
       (eq (cadar formals) :object)) (caar formals))
    (t (visitor-xvar-from-formals name
        (cdr formals)))))
other
(define defvisitor-template-main
  (name args wrld)
  (b* (((mv kwd-alist rest) (extract-keywords name
         *defvisitor-template-keys*
         args
         nil)) ((unless (eql (len rest) 1)) (raise "~x0: the only non-keyword argument after the name should be ~
                the formals."
          name))
      (formals (car rest))
      (returns (cdr (assoc :returns kwd-alist)))
      ((mv type-fns field-fns prod-fns) (visitor-process-fnspecs kwd-alist wrld))
      ((mv stripped-returns
         accums
         initials
         joins
         joinvars) (visitor-parse-returns returns))
      (fnname-template (cdr (assoc :fnname-template kwd-alist)))
      (- (visitor-check-fnname-template name
          fnname-template))
      (macrop (not (equal (remove-macro-args 'defvisitor-template
              formals
              nil)
            formals)))
      (x (make-visitorspec :name name
          :formals formals
          :returns stripped-returns
          :accum-vars accums
          :join-vars joinvars
          :type-fns type-fns
          :field-fns field-fns
          :prod-fns prod-fns
          :initial initials
          :join joins
          :fnname-template fnname-template
          :xvar (visitor-xvar-from-formals name formals)
          :fixequivs (getarg :fixequivs t kwd-alist)
          :prepwork (getarg :prepwork nil kwd-alist)
          :reversep (getarg :reversep nil kwd-alist)
          :wrapper (getarg :wrapper :body kwd-alist)
          :renames (getarg :renames nil kwd-alist)
          :binder (getarg :binder nil kwd-alist)
          :define-args (getarg :define-args nil kwd-alist)
          :defines-args (getarg :defines-args nil kwd-alist)
          :macrop macrop)))
    x))
other
(define defvisitor-template-fn
  (name args)
  `(with-output :off :all :on (error)
    (progn (table visitor-templates
        ',FTY::NAME
        (defvisitor-template-main ',FTY::NAME
          ',FTY::ARGS
          world))
      (with-output :stack :pop (value-triple ',FTY::NAME)))))
defvisitor-templatemacro
(defmacro defvisitor-template
  (name &rest args)
  (defvisitor-template-fn name args))
other
(define visitor-include-types
  (types include-types)
  (cond ((atom types) nil)
    ((with-flextype-bindings (type (car types))
       (member type.name include-types)) (cons (car types)
        (visitor-include-types (cdr types)
          include-types)))
    (t (visitor-include-types (cdr types)
        include-types))))
other
(define visitor-omit-types
  (types omit-types)
  (cond ((atom types) nil)
    ((with-flextype-bindings (type (car types))
       (member type.name omit-types)) (visitor-omit-types (cdr types) omit-types))
    (t (cons (car types)
        (visitor-omit-types (cdr types) omit-types)))))
other
(defconst *defvisitor-keys*
  '(:type :template :type-fns :field-fns :prod-fns :fnname-template :renames :omit-types :include-types :measure :defines-args :define-args :order :parents :short :long))
other
(define visitor-remove-types-from-alist
  (al typenames)
  (if (atom al)
    nil
    (if (member (caar al) typenames)
      (visitor-remove-types-from-alist (cdr al)
        typenames)
      (cons (car al)
        (visitor-remove-types-from-alist (cdr al)
          typenames)))))
other
(define process-defvisitor
  (name kwd-alist wrld)
  (b* ((template (cdr (assoc :template kwd-alist))) (type (cdr (assoc :type kwd-alist)))
      ((unless (and template type)) (er hard?
          'defvisitor
          ":type and :template arguments are mandatory")
        (mv nil nil nil))
      (x1 (cdr (assoc template
            (table-alist 'visitor-templates wrld))))
      ((unless x1) (er hard?
          'defvisitor
          "Template ~x0 wasn't defined"
          template)
        (mv nil nil nil))
      ((mv type-fns field-fns prod-fns) (visitor-process-fnspecs kwd-alist wrld))
      ((visitorspec x1))
      (x1.type-fns (append type-fns x1.type-fns))
      (x1.field-fns (append field-fns x1.field-fns))
      (x1.prod-fns (append prod-fns x1.prod-fns))
      (fty (cdr (assoc type
            (table-alist 'flextypes-table wrld))))
      ((unless fty) (er hard?
          'defvisitor
          "Type ~x0 not found"
          type)
        (mv nil nil nil))
      ((flextypes fty))
      (omit-types (cdr (assoc :omit-types kwd-alist)))
      (include-types (cdr (assoc :include-types kwd-alist)))
      ((when (and omit-types include-types)) (er hard?
          'defvisitor
          ":omit-types and :include-types are mutually exclusive")
        (mv nil nil nil))
      (types (cond (include-types (visitor-include-types fty.types
              include-types))
          (omit-types (visitor-omit-types fty.types omit-types))
          (t fty.types)))
      (fnname-template (or (cdr (assoc :fnname-template kwd-alist))
          x1.fnname-template))
      (- (visitor-check-fnname-template name
          fnname-template))
      (renames (append (cdr (assoc :renames kwd-alist))
          x1.renames))
      (x1-with-renaming (change-visitorspec x1
          :fnname-template fnname-template
          :renames renames))
      (unbound-types (visitor-omit-bound-types types x1.type-fns))
      (added-type-fns (visitor-add-type-fns unbound-types
          x1-with-renaming))
      (new-type-fns (append added-type-fns x1.type-fns))
      (store-template1 (change-visitorspec x1
          :type-fns new-type-fns
          :field-fns x1.field-fns
          :prod-fns x1.prod-fns))
      (local-template (change-visitorspec store-template1
          :wrld wrld
          :fnname-template fnname-template
          :renames renames
          :defines-args (getarg :defines-args x1.defines-args
            kwd-alist)
          :define-args (getarg :define-args x1.define-args
            kwd-alist)
          :measure (cdr (assoc :measure kwd-alist))
          :order (cdr (assoc :order kwd-alist))))
      (store-renames (visitor-remove-types-from-alist x1.renames
          (flextypelist-names types)))
      (store-template (change-visitorspec store-template1
          :renames store-renames)))
    (mv local-template store-template types)))
other
(define defvisitor-fn
  (args wrld)
  (b* (((mv name args) (if (and (symbolp (car args))
           (not (keywordp (car args))))
         (mv (car args) (cdr args))
         (mv nil args))) ((mv pre-/// post-///) (split-/// 'defvisitor args))
      ((mv kwd-alist mrec-fns) (extract-keywords 'defvisitor
          *defvisitor-keys*
          pre-///
          nil))
      ((mv local-x store-x types) (process-defvisitor name kwd-alist wrld))
      (template (cdr (assoc :template kwd-alist)))
      (type (cdr (assoc :type kwd-alist)))
      (event-name (or name (visitor-macroname local-x type)))
      (def (if (and (eql (len types) 1) (atom mrec-fns))
          (visitor-def (car types) local-x nil)
          (visitor-mutual type
            types
            local-x
            mrec-fns))))
    `(defsection-progn ,FTY::EVENT-NAME
      ,(APPEND FTY::DEF FTY::POST-///)
      (with-output :off :all :on (error)
        (table visitor-templates
          ',FTY::TEMPLATE
          ',FTY::STORE-X)))))
defvisitormacro
(defmacro defvisitor
  (&rest args)
  `(with-output :off (event)
    (make-event (defvisitor-fn ',FTY::ARGS (w state)))))
other
(defconst *defvisitors-keys*
  '(:template :types :dep-types :measure :debug :order-base))
other
(define visitor-membertype-collect-member-types
  (type x wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((visitorspec x)) (type (visitor-normalize-fixtype type wrld))
      (type-entry (assoc type x.type-fns))
      ((when (eq (cdr type-entry) :skip)) (mv nil nil))
      (rename-entry (assoc type x.renames))
      (leafp (and (cdr type-entry) t))
      ((when (and leafp
           (or (not rename-entry)
             (not (eq t
                 (getpropc (cadr rename-entry)
                   'formals
                   t
                   wrld)))
             (not (eq t
                 (getpropc (cadr rename-entry)
                   'macro-args
                   t
                   wrld)))))) (mv nil t))
      ((mv fty ?ftype) (search-deftypes-table type
          (table-alist 'flextypes-table wrld)))
      ((when fty) (mv (list type) leafp)))
    (mv nil leafp)))
other
(define visitor-field-collect-member-types
  (field x prod-entry wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((flexprod-field field)) ((visitorspec x))
      (field-entry (or (assoc field.name prod-entry)
          (assoc field.name x.field-fns)))
      ((when field-entry) (b* ((fn (cdr field-entry)))
          (mv nil (and fn (not (eq fn :skip))))))
      ((mv subtypes is-leaf) (visitor-membertype-collect-member-types field.type
          x
          wrld)))
    (mv subtypes is-leaf)))
other
(define visitor-fields-collect-member-types
  (fields x prod-entry wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((when (atom fields)) (mv nil nil)) ((mv subtypes1 is-leaf-type-p1) (visitor-field-collect-member-types (car fields)
          x
          prod-entry
          wrld))
      ((mv subtypes2 is-leaf-type-p2) (visitor-fields-collect-member-types (cdr fields)
          x
          prod-entry
          wrld)))
    (mv (union-eq subtypes1 subtypes2)
      (or is-leaf-type-p1 is-leaf-type-p2))))
other
(define visitor-prods-collect-member-types
  (prods x wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((when (atom prods)) (mv nil nil)) ((visitorspec x))
      ((flexprod prod1) (car prods))
      (prod-entry (cdr (assoc prod1.type-name x.prod-fns)))
      ((mv subtypes1 is-leaf-type1) (visitor-fields-collect-member-types prod1.fields
          x
          prod-entry
          wrld))
      ((mv subtypes2 is-leaf-type2) (visitor-prods-collect-member-types (cdr prods)
          x
          wrld)))
    (mv (union-eq subtypes1 subtypes2)
      (or is-leaf-type1 is-leaf-type2))))
other
(define visitor-sumtype-collect-member-types
  (type x wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((flexsum type)))
    (visitor-prods-collect-member-types type.prods
      x
      wrld)))
other
(define visitor-listtype-collect-member-types
  (type x wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((flexlist type)))
    (visitor-membertype-collect-member-types type.elt-type
      x
      wrld)))
other
(define visitor-alisttype-collect-member-types
  (type x wrld)
  :returns (mv subtypes is-leaf-p)
  (b* (((flexalist type)) ((mv subtypes1 is-leaf1) (visitor-membertype-collect-member-types type.key-type
          x
          wrld))
      ((mv subtypes2 is-leaf2) (visitor-membertype-collect-member-types type.val-type
          x
          wrld)))
    (mv (union-eq subtypes1 subtypes2)
      (or is-leaf1 is-leaf2))))
other
(define visitor-transsum-members-without-actions
  (typenames x)
  (b* (((when (atom typenames)) nil) ((visitorspec x))
      (type-entry (assoc (car typenames) x.type-fns))
      ((when (cdr type-entry)) (visitor-transsum-members-without-actions (cdr typenames)
          x)))
    (cons (car typenames)
      (visitor-transsum-members-without-actions (cdr typenames)
        x))))
other
(define visitor-transsum-is-leaf
  (typenames x)
  (b* (((when (atom typenames)) nil) ((visitorspec x))
      (type (car typenames))
      (type-entry (assoc type x.type-fns))
      ((when (and (cdr type-entry)
           (not (eq (cdr type-entry) :skip)))) t))
    (visitor-transsum-is-leaf (cdr typenames) x)))
other
(define visitor-transsumtype-collect-member-types
  (type x wrld)
  :returns (mv subtypes is-leaf-p)
  (declare (ignorable x wrld))
  (b* (((flextranssum type)) (all-subtypes (flextranssum-memberlist->typenames type.members))
      (new-subtypes (visitor-transsum-members-without-actions all-subtypes
          x))
      (is-leaf-p (visitor-transsum-is-leaf all-subtypes x)))
    (mv new-subtypes is-leaf-p)))
other
(define visitor-type-collect-member-types
  ((typename) (x "The visitorspec object.")
    wrld)
  (b* (((mv ?fty type-obj) (search-deftypes-table typename
         (table-alist 'flextypes-table wrld))) ((unless type-obj) (cw "WARNING: Expected to find deftypes table entry for ~x0 but didn't~%"
          typename)
        (mv nil nil)))
    (case (tag type-obj)
      (:sum (visitor-sumtype-collect-member-types type-obj
          x
          wrld))
      (:list (visitor-listtype-collect-member-types type-obj
          x
          wrld))
      (:alist (visitor-alisttype-collect-member-types type-obj
          x
          wrld))
      (:transsum (visitor-transsumtype-collect-member-types type-obj
          x
          wrld))
      (otherwise (mv nil nil)))))
other
(mutual-recursion (defun visitor-type-make-type-graph
    (typename x
      wrld
      type-graph
      leaf-types)
    (b* (((when (hons-get typename type-graph)) (mv type-graph leaf-types)) ((mv subtypes is-leaf) (visitor-type-collect-member-types typename
            x
            wrld))
        (leaf-types (if is-leaf
            (cons typename leaf-types)
            leaf-types))
        (type-graph (hons-acons typename
            subtypes
            type-graph)))
      (visitor-types-make-type-graph subtypes
        x
        wrld
        type-graph
        leaf-types)))
  (defun visitor-types-make-type-graph
    (types x
      wrld
      type-graph
      leaf-types)
    (b* (((when (atom types)) (mv type-graph leaf-types)) ((mv type-graph leaf-types) (visitor-type-make-type-graph (car types)
            x
            wrld
            type-graph
            leaf-types)))
      (visitor-types-make-type-graph (cdr types)
        x
        wrld
        type-graph
        leaf-types))))
other
(define visitor-types-make-type-graph-top
  (types x wrld)
  (visitor-types-make-type-graph types
    x
    wrld
    nil
    nil))
other
(define visitor-reverse-graph-putlist
  (froms to revgraph)
  (b* (((when (atom froms)) revgraph) (old-val (cdr (hons-get (car froms) revgraph)))
      (new-val (cons to old-val))
      (revgraph (hons-acons (car froms)
          new-val
          revgraph)))
    (visitor-reverse-graph-putlist (cdr froms)
      to
      revgraph)))
other
(define visitor-reverse-graph-aux
  (graph)
  (b* (((when (atom graph)) nil) (revgraph (visitor-reverse-graph-aux (cdr graph))))
    (visitor-reverse-graph-putlist (cdar graph)
      (caar graph)
      revgraph)))
other
(define visitor-reverse-graph
  (graph)
  (fast-alist-clean (visitor-reverse-graph-aux graph)))
other
(mutual-recursion (defun visitor-mark-type-rec
    (type rev-graph marks)
    (b* (((when (hons-get type marks)) marks) (marks (hons-acons type t marks))
        (parents (cdr (hons-get type rev-graph))))
      (visitor-mark-types-rec parents
        rev-graph
        marks)))
  (defun visitor-mark-types-rec
    (types rev-graph marks)
    (if (atom types)
      marks
      (visitor-mark-types-rec (cdr types)
        rev-graph
        (visitor-mark-type-rec (car types)
          rev-graph
          marks)))))
other
(define visitor-check-top-types
  (types marks)
  (cond ((atom types) nil)
    ((cdr (hons-get (car types) marks)) (visitor-check-top-types (cdr types) marks))
    (t (raise "Type ~x0 doesn't have any descendants that need visiting."
        (car types)))))
other
(define visitor-types-filter-marked
  (types marks)
  (cond ((atom types) nil)
    ((cdr (hons-get (car types) marks)) (cons (car types)
        (visitor-types-filter-marked (cdr types)
          marks)))
    (t (visitor-types-filter-marked (cdr types)
        marks))))
other
(define visitor-members-to-ftys
  (memb-types deftypes-table)
  (b* (((when (atom memb-types)) nil) ((mv fty ?ftype) (search-deftypes-table (car memb-types)
          deftypes-table))
      ((unless fty) (cw "Warning: didn't find ~x0 in deftypes table~%"
          (car memb-types)))
      ((flextypes fty)))
    (add-to-set-eq fty.name
      (visitor-members-to-ftys (cdr memb-types)
        deftypes-table))))
other
(define visitor-to-fty-graph
  (type-graph marks
    deftypes-table
    fty-graph)
  (b* (((when (atom type-graph)) (fast-alist-clean fty-graph)) ((cons type memb-types) (car type-graph))
      ((unless (cdr (hons-get type marks))) (visitor-to-fty-graph (cdr type-graph)
          marks
          deftypes-table
          fty-graph))
      ((mv fty ?ftype) (search-deftypes-table type deftypes-table))
      ((unless fty) (cw "Warning: didn't find ~x0 in deftypes table" type)
        (visitor-to-fty-graph (cdr type-graph)
          marks
          deftypes-table
          fty-graph))
      ((flextypes fty))
      (memb-ftys (visitor-members-to-ftys (visitor-types-filter-marked memb-types
            marks)
          deftypes-table))
      (prev-ftys (cdr (hons-get fty.name fty-graph)))
      (fty-graph (hons-acons fty.name
          (union-eq memb-ftys prev-ftys)
          fty-graph)))
    (visitor-to-fty-graph (cdr type-graph)
      marks
      deftypes-table
      fty-graph)))
other
(mutual-recursion (defun visitor-toposort-type
    (type fty-graph seen postorder)
    (b* (((when (hons-get type seen)) (mv seen postorder)) (seen (hons-acons type t seen))
        ((mv seen postorder) (visitor-toposort-types (cdr (hons-get type fty-graph))
            fty-graph
            seen
            postorder)))
      (mv seen (cons type postorder))))
  (defun visitor-toposort-types
    (types fty-graph seen postorder)
    (b* (((when (atom types)) (mv seen postorder)) ((mv seen postorder) (visitor-toposort-type (car types)
            fty-graph
            seen
            postorder)))
      (visitor-toposort-types (cdr types)
        fty-graph
        seen
        postorder))))
other
(define visitor-type-to-fty
  (type deftypes-table)
  (b* (((mv fty ?ftype) (search-deftypes-table type deftypes-table)) ((unless fty) (raise "Didn't find ~x0 in deftypes table" type))
      ((flextypes fty)))
    fty.name))
other
(define visitor-types-to-ftys
  (types deftypes-table)
  (if (atom types)
    nil
    (cons (visitor-type-to-fty (car types)
        deftypes-table)
      (visitor-types-to-ftys (cdr types)
        deftypes-table))))
other
(define visitor-fty-defvisitor-form
  (fty-name order
    marks
    template-name
    deftypes-table
    kwd-alist)
  (b* ((fty (cdr (assoc fty-name deftypes-table))) ((unless fty) (raise "Didn't find ~x0 in the deftypes table~%"
          fty-name))
      (measure-look (assoc :measure kwd-alist)))
    `(defvisitor :template ,FTY::TEMPLATE-NAME
      :type ,FTY::FTY-NAME
      :include-types ,(FTY::VISITOR-TYPES-FILTER-MARKED
  (FTY::FLEXTYPELIST-NAMES (FTY::FLEXTYPES->TYPES FTY::FTY)) FTY::MARKS)
      :order ,FTY::ORDER
      ,@(AND FTY::MEASURE-LOOK `(:MEASURE ,(CDR FTY::MEASURE-LOOK))))))
other
(define visitor-defvisitor-forms
  (toposort order
    marks
    template-name
    deftypes-table
    kwd-alist)
  (if (atom toposort)
    nil
    (cons (visitor-fty-defvisitor-form (car toposort)
        order
        marks
        template-name
        deftypes-table
        kwd-alist)
      (visitor-defvisitor-forms (cdr toposort)
        (+ 1 order)
        marks
        template-name
        deftypes-table
        kwd-alist))))
other
(define process-defvisitors
  (kwd-alist wrld)
  (b* ((template (cdr (assoc :template kwd-alist))) (types (append (cdr (assoc :types kwd-alist))
          (cdr (assoc :dep-types kwd-alist))))
      (types (if (and types (atom types))
          (list types)
          types))
      ((unless (and template
           (symbolp template)
           types
           (symbol-listp types))) (er hard?
          'defvisitors
          ":types and :template arguments are mandatory ~
                               and must be a symbol-list and symbol, ~
                               respectively"))
      (x1 (cdr (assoc template
            (table-alist 'visitor-templates wrld))))
      ((unless x1) (er hard?
          'defvisitors
          "Template ~x0 wasn't defined"
          template))
      (deftypes-table (table-alist 'flextypes-table wrld))
      ((mv type-graph leaf-types) (visitor-types-make-type-graph-top types
          x1
          wrld))
      (rev-graph (visitor-reverse-graph type-graph))
      (marks (visitor-mark-types-rec leaf-types
          rev-graph
          nil))
      (- (visitor-check-top-types types marks))
      (fty-graph (visitor-to-fty-graph type-graph
          marks
          deftypes-table
          nil))
      (dep-ftys (visitor-types-to-ftys (cdr (assoc :dep-types kwd-alist))
          deftypes-table))
      ((mv seen-al rev-toposort) (visitor-toposort-types (set-difference-eq (strip-cars fty-graph)
            dep-ftys)
          fty-graph
          nil
          nil))
      (- (fast-alist-free seen-al))
      (forms (visitor-defvisitor-forms (reverse rev-toposort)
          (or (cdr (assoc :order-base kwd-alist)) 0)
          marks
          template
          deftypes-table
          kwd-alist)))
    (and (cdr (assoc :debug kwd-alist))
      (progn$ (cw "type graph: ~x0~%" type-graph)
        (cw "leaf types: ~x0~%" leaf-types)
        (cw "rev-graph:  ~x0~%" rev-graph)
        (cw "marks:      ~x0~%" marks)
        (cw "fty-graph:  ~x0~%" fty-graph)
        (cw "toposort:  ~x0~%" rev-toposort)))
    forms))
other
(define defvisitors-fn
  (args wrld)
  (b* (((mv name args) (if (and (symbolp (car args))
           (not (keywordp (car args))))
         (mv (car args) (cdr args))
         (mv nil args))) ((mv pre-/// post-///) (split-/// 'defvisitors args))
      ((mv kwd-alist mrec-fns) (extract-keywords 'defvisitors
          *defvisitors-keys*
          pre-///
          nil))
      ((when mrec-fns) (er hard?
          'defvisitors
          "Extra mutually-recursive functions aren't ~
                                allowed in defvisitors unless inside ~
                                defvisitor-multi."))
      (forms (process-defvisitors kwd-alist wrld)))
    `(defsection-progn ,FTY::NAME
      ,@FTY::FORMS . ,FTY::POST-///)))
defvisitorsmacro
(defmacro defvisitors
  (&rest args)
  `(make-event (defvisitors-fn ',FTY::ARGS (w state))))
other
(defconst *defvisitor-multi-keys*
  '(:defines-args :fixequivs))
other
(defconst *defvisitor-inside-multi-keys*
  (set-difference-eq *defvisitor-keys*
    *defvisitor-multi-keys*))
other
(define process-defvisitor-multi
  (args wrld)
  (b* (((when (atom args)) (mv nil nil nil nil)) ((mv args other-fns1 ///-events1) (if (and (consp (car args))
            (eq (caar args) 'defvisitors))
          (b* (((mv pre-/// post-///) (split-/// 'defvisitors (cdar args))) ((mv kwd-alist mrec-fns) (extract-keywords 'defvisitors
                  *defvisitors-keys*
                  pre-///
                  nil))
              (kwd-alist (if (assoc :measure kwd-alist)
                  kwd-alist
                  (cons (cons :measure :count) kwd-alist)))
              (defvisitor-forms (process-defvisitors kwd-alist wrld)))
            (mv (append defvisitor-forms (cdr args))
              mrec-fns
              post-///))
          (mv args nil nil)))
      ((unless (consp (car args))) (er hard?
          'defvisitor-multi
          "Bad arg: ~x0"
          (car args))
        (mv nil nil nil nil))
      ((when (eq (caar args) 'define)) (b* (((mv types-templates
              other-fns
              ///-events
              table-stores) (process-defvisitor-multi (cdr args) wrld)))
          (mv types-templates
            (cons (car args) other-fns)
            ///-events
            table-stores)))
      ((unless (eq (caar args) 'defvisitor)) (er hard?
          'defvisitor-multi
          "Bad arg: ~x0"
          (car args))
        (mv nil nil nil nil))
      ((mv pre-/// post-///) (split-/// 'defvisitor (cdar args)))
      ((mv kwd-alist other-fns2) (extract-keywords 'defvisitor
          *defvisitor-inside-multi-keys*
          pre-///
          nil))
      ((mv local-template store-template types) (process-defvisitor 'bozo-fixme-name-for-process-defvisitor-multi
          kwd-alist
          wrld))
      (wrld (putprop 'visitor-templates
          'table-alist
          (cons (cons (visitorspec->name store-template)
              store-template)
            (table-alist 'visitor-templates wrld))
          wrld))
      ((mv types-templates
         other-fns
         ///-events
         table-stores) (process-defvisitor-multi (cdr args) wrld))
      (types-templates (cons (cons types local-template)
          types-templates))
      (other-fns (append other-fns1 other-fns2 other-fns))
      (///-events (append ///-events1 post-/// ///-events))
      (table-stores (cons `(with-output :off :all :on (error)
            (table visitor-templates
              ',(CDR (ASSOC :TEMPLATE FTY::KWD-ALIST))
              ',FTY::STORE-TEMPLATE))
          table-stores)))
    (mv types-templates
      other-fns
      ///-events
      table-stores)))
other
(define defvisitor-multi-fn
  (args wrld)
  (b* (((cons name args) args) ((unless (and (symbolp name) (not (keywordp name)))) (er hard?
          'defvisitor-multi
          "Defvisitor-multi requires a name for the form as the first argument"))
      ((mv pre-/// post-///) (split-/// 'defvisitor args))
      ((mv kwd-alist args) (extract-keywords 'defvisitor-multi
          *defvisitor-multi-keys*
          pre-///
          nil))
      ((mv types-templates
         other-fns
         ///-events
         table-stores) (process-defvisitor-multi args wrld))
      (multicfg (make-visitormulti :defines-args (cdr (assoc :defines-args kwd-alist))
          :fixequivs (getarg :fixequivs t kwd-alist)
          :name name
          :other-fns other-fns))
      (def (visitor-multi multicfg types-templates)))
    `(defsection-progn ,FTY::NAME
      ,(APPEND FTY::DEF FTY::///-EVENTS FTY::POST-///) . ,FTY::TABLE-STORES)))
defvisitor-multimacro
(defmacro defvisitor-multi
  (&rest args)
  `(with-output :off (event)
    (make-event (defvisitor-multi-fn ',FTY::ARGS (w state)))))
other
(define find-update-index
  (returns idx)
  (if (atom returns)
    nil
    (let ((rettype (cadr (car returns))))
      (if (or (eq rettype :update)
          (and (consp rettype) (eq (car rettype) :update)))
        idx
        (find-update-index (cdr returns) (+ 1 idx))))))
other
(define prod-acc-updater-theorem
  (field prod sum visitor wrld)
  (b* (((flexprod-field field)) ((flexprod prod))
      ((flexsum sum))
      ((visitorspec visitor))
      (sum-fn (cdr (assoc sum.name visitor.type-fns)))
      (field-fn (or (let ((prod-field-fns (cdr (assoc prod.type-name visitor.prod-fns))))
            (cdr (assoc field.name prod-field-fns)))
          (cdr (assoc field.name visitor.field-fns))
          (cdr (assoc (visitor-normalize-fixtype field.type wrld)
              visitor.type-fns))))
      ((unless sum-fn) nil)
      (update-index (and (consp visitor.returns)
          (eq (car visitor.returns) 'mv)
          (find-update-index (cdr visitor.returns) 0)))
      (sum-call1 `(,FTY::SUM-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (sum-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::SUM-CALL1)
          sum-call1))
      (field-call1 `(,FTY::FIELD-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (field-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::FIELD-CALL1)
          field-call1))
      (hyp (if (consp (cdr sum.prods))
          (if sum.kind
            `(equal (,FTY::SUM.KIND ,FTY::VISITOR.XVAR) ,FTY::PROD.KIND)
            (if (eq prod.cond t)
              t
              `(let ((,FTY::SUM.XVAR ,FTY::VISITOR.XVAR))
                ,FTY::PROD.COND)))
          t)))
    (list (template-subst '(defthm <acc>-of-<sum-fn>
          (implies <hyp>
            (equal (<acc> <sum-call>)
              (let ((<xvar> (<acc> <xvar>)))
                <field-call>)))
          :hints (("goal" :expand (<sum-call1>))))
        :atom-alist `((<acc> . ,FTY::FIELD.ACC-NAME) (<sum-call> . ,FTY::SUM-CALL)
          (<sum-call1> . ,FTY::SUM-CALL1)
          (<field-call> . ,(IF FTY::FIELD-FN
     FTY::FIELD-CALL
     FTY::VISITOR.XVAR))
          (<xvar> . ,FTY::VISITOR.XVAR)
          (<hyp> . ,FTY::HYP)
          (<sum-fn> . ,FTY::SUM-FN))
        :str-alist `(("<ACC>" . ,(SYMBOL-NAME FTY::FIELD.ACC-NAME)) ("<SUM-FN>" . ,(SYMBOL-NAME FTY::SUM-FN)))
        :pkg-sym visitor.name))))
other
(define prod-acc-updater-theorems
  (fields prod sum visitor wrld)
  (if (atom fields)
    nil
    (append (prod-acc-updater-theorem (car fields)
        prod
        sum
        visitor
        wrld)
      (prod-acc-updater-theorems (cdr fields)
        prod
        sum
        visitor
        wrld))))
other
(define prod-updater-theorems
  (prods sum visitor wrld)
  (if (atom prods)
    nil
    (append (prod-acc-updater-theorems (flexprod->fields (car prods))
        (car prods)
        sum
        visitor
        wrld)
      (prod-updater-theorems (cdr prods)
        sum
        visitor
        wrld))))
other
(define sum-kind-updater-theorem
  (sum visitor)
  (b* (((flexsum sum)) ((visitorspec visitor))
      (sum-fn (cdr (assoc sum.name visitor.type-fns)))
      ((unless sum-fn) nil)
      ((unless sum.kind) nil)
      (update-index (and (consp visitor.returns)
          (eq (car visitor.returns) 'mv)
          (find-update-index (cdr visitor.returns) 0)))
      (sum-call1 `(,FTY::SUM-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (sum-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::SUM-CALL1)
          sum-call1)))
    (list (template-subst '(defthm <kind>-of-<sum-fn>
          (equal (<kind> <sum-call>)
            (<kind> <xvar>))
          :hints (("goal" :expand (<sum-call1>))))
        :atom-alist `((<kind> . ,FTY::SUM.KIND) (<sum-call> . ,FTY::SUM-CALL)
          (<sum-call1> . ,FTY::SUM-CALL1)
          (<xvar> . ,FTY::VISITOR.XVAR))
        :str-alist `(("<KIND>" . ,(SYMBOL-NAME FTY::SUM.KIND)) ("<SUM-FN>" . ,(SYMBOL-NAME FTY::SUM-FN)))
        :pkg-sym visitor.name))))
other
(define flexsum-updater-theorems
  (x visitor wrld)
  (append (sum-kind-updater-theorem x visitor)
    (prod-updater-theorems (flexsum->prods x)
      x
      visitor
      wrld)))
other
(define flexlist-updater-theorems
  (x visitor wrld)
  (b* (((flexlist x)) ((visitorspec visitor))
      (list-fn (cdr (assoc x.name visitor.type-fns)))
      (elt-fn (cdr (assoc (visitor-normalize-fixtype x.elt-type wrld)
            visitor.type-fns)))
      ((unless list-fn) nil)
      (update-index (and (consp visitor.returns)
          (eq (car visitor.returns) 'mv)
          (find-update-index (cdr visitor.returns) 0)))
      (list-call1 `(,FTY::LIST-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (list-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::LIST-CALL1)
          list-call1))
      (elt-call1 `(,FTY::ELT-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (elt-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::ELT-CALL1)
          elt-call1)))
    (list (template-subst '(progn (defthm car-of-<list-fn>
            (implies (consp <xvar>)
              (equal (car <list-call>)
                (let ((<xvar> (car <xvar>)))
                  <elt-call>)))
            :hints (("goal" :expand (<list-call1>))))
          (defthm cdr-of-<list-fn>
            (implies (consp <xvar>)
              (equal (cdr <list-call>)
                (let ((<xvar> (cdr <xvar>)))
                  <list-call>)))
            :hints (("goal" :expand (<list-call1>))))
          (defthm consp-of-<list-fn>
            (equal (consp <list-call>)
              (consp (<fix> <xvar>)))
            :hints (("goal" :expand (<list-call1>)))))
        :atom-alist `((<list-call> . ,FTY::LIST-CALL) (<list-call1> . ,FTY::LIST-CALL1)
          (<elt-call> . ,(IF FTY::ELT-FN
     FTY::ELT-CALL
     FTY::VISITOR.XVAR))
          (<xvar> . ,FTY::VISITOR.XVAR)
          (<list-fn> . ,FTY::LIST-FN)
          (<fix> . ,FTY::X.FIX))
        :str-alist `(("<LIST-FN>" . ,(SYMBOL-NAME FTY::LIST-FN)))
        :pkg-sym visitor.name))))
other
(define flexalist-updater-theorems
  (x visitor wrld)
  (b* (((flexalist x)) ((visitorspec visitor))
      (alist-fn (cdr (assoc x.name visitor.type-fns)))
      (key-fn (cdr (assoc (visitor-normalize-fixtype x.key-type wrld)
            visitor.type-fns)))
      (val-fn (cdr (assoc (visitor-normalize-fixtype x.val-type wrld)
            visitor.type-fns)))
      ((unless (and alist-fn (or key-fn val-fn))) nil)
      (update-index (and (consp visitor.returns)
          (eq (car visitor.returns) 'mv)
          (find-update-index (cdr visitor.returns) 0)))
      (alist-call1 `(,FTY::ALIST-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (alist-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::ALIST-CALL1)
          alist-call1))
      (key-call1 `(,FTY::KEY-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (key-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::KEY-CALL1)
          key-call1))
      (val-call1 `(,FTY::VAL-FN . ,(FTY::STRIP-CARS FTY::VISITOR.FORMALS)))
      (val-call (if update-index
          `(mv-nth ,FTY::UPDATE-INDEX ,FTY::VAL-CALL1)
          val-call1)))
    (list (template-subst '(progn (:@ :key (defthm caar-of-<alist-fn>
              (implies (consp (<fix> <xvar>))
                (equal (caar <alist-call>)
                  (let ((<xvar> (caar (<fix> <xvar>))))
                    <key-call>)))
              :hints (("goal" :expand (<alist-call1>)))))
          (:@ :val (defthm caar-of-<alist-fn>
              (implies (consp (<fix> <xvar>))
                (equal (cdar <alist-call>)
                  (let ((<xvar> (cdar (<fix> <xvar>))))
                    <val-call>)))
              :hints (("goal" :expand (<alist-call1>)))))
          (defthm cdr-of-<alist-fn>
            (equal (cdr <alist-call>)
              (let ((<xvar> (<fix> <xvar>)))
                (and (consp <xvar>)
                  (let ((<xvar> (cdr <xvar>)))
                    <alist-call>))))
            :hints (("goal" :expand (<alist-call1>))))
          (defthm consp-of-<alist-fn>
            (equal (consp <alist-call>)
              (consp (<fix> <xvar>)))
            :hints (("goal" :expand (<alist-call1>)))))
        :atom-alist `((<alist-call> . ,FTY::ALIST-CALL) (<alist-call1> . ,FTY::ALIST-CALL1)
          (<key-call> . ,FTY::KEY-CALL)
          (<val-call> . ,FTY::VAL-CALL)
          (<xvar> . ,FTY::VISITOR.XVAR)
          (<alist-fn> . ,FTY::ALIST-FN)
          (<fix> . ,FTY::X.FIX))
        :str-alist `(("<ALIST-FN>" . ,(SYMBOL-NAME FTY::ALIST-FN)))
        :features (append (and key-fn '(:key)) (and val-fn '(:val)))
        :pkg-sym visitor.name))))
other
(define type-updater-theorems
  (type visitor wrld)
  (case (tag type)
    (:list (flexlist-updater-theorems type visitor wrld))
    (:sum (flexsum-updater-theorems type visitor wrld))
    (:alist (flexalist-updater-theorems type
        visitor
        wrld))
    (otherwise nil)))
other
(define typename-updater-theorems
  (typename visitor wrld)
  (b* ((deftypes-table (table-alist 'flextypes-table wrld)) ((mv & type) (search-deftypes-table typename
          deftypes-table)))
    (type-updater-theorems type visitor wrld)))
other
(define typenames-updater-theorems
  (typenames visitor wrld)
  (if (atom typenames)
    nil
    (append (typename-updater-theorems (car typenames)
        visitor
        wrld)
      (typenames-updater-theorems (cdr typenames)
        visitor
        wrld))))
other
(define visitor-updater-theorems-fn
  (name wrld)
  (b* (((visitorspec visitor) (cdr (assoc name
           (table-alist 'visitor-templates wrld)))))
    (cons 'progn
      (typenames-updater-theorems (strip-cars visitor.type-fns)
        visitor
        wrld))))
def-visitor-updater-theoremsmacro
(defmacro def-visitor-updater-theorems
  (name)
  `(make-event (visitor-updater-theorems-fn ',FTY::NAME
      (w state))))
other
(defxdoc def-visitor-updater-theorems
  :parents (defvisitors)
  :short "(Beta) Generate theorems relating the result of an updater visitor to the input object"
  :long "<p>If you have a simple visitor that updates some object by a simple transform
such as stripping out some field,this can automatically prove rewrite rules
such as, e.g., an accessor of the transform of some object equals the transform
of the accessor of the object. Not yet tested in more complex cases. It
generates such theorems for all types for which the visitor has been
defined.</p>")