Filtering...

fty-sum

books/centaur/fty/fty-sum
other
(in-package "FTY")
other
(include-book "fty-parseutils")
other
(include-book "fty-sum-casemacro")
other
(include-book "xdoc/names" :dir :system)
other
(program)
other
(define nice-and
  (x y)
  "Like `(and ,x ,y) but maybe simplify things."
  (cond ((eq x t) y)
    ((eq y t) x)
    ((eq x nil) nil)
    ((eq y nil) nil)
    ((and (consp x) (eq (car x) 'and)) (if (and (consp y) (eq (car y) 'and))
        (append x (cdr y))
        (append x (list y))))
    ((and (consp y) (eq (car y) 'and)) `(and ,FTY::X . ,(CDR FTY::Y)))
    (t `(and ,FTY::X ,FTY::Y))))
other
(define nice-or
  (x y)
  "Like `(or ,x ,y) but maybe simplify things."
  (cond ((eq x t) t)
    ((eq y t) t)
    ((eq x nil) y)
    ((eq y nil) x)
    ((and (consp x) (eq (car x) 'or)) (if (eq (car y) 'or)
        (append x (cdr y))
        (append x (list y))))
    ((and (consp y) (eq (car y) 'or)) `(or ,FTY::X . ,(CDR FTY::Y)))
    (t `(or ,FTY::X ,FTY::Y))))
other
(define nice-implies
  (x y)
  "Like `(implies ,x ,y) but maybe simplify things."
  (cond ((eq x t) y)
    ((eq y t) t)
    ((eq x nil) t)
    ((eq y nil) x)
    (t `(implies ,FTY::X ,FTY::Y))))
other
(define nice-cond
  (x)
  "Like `(cond ...)` but maybe reduce (cond (t foo)) to just foo."
  (cond ((atom x) nil)
    ((eq (caar x) t) (cadar x))
    (t `(cond . ,FTY::X))))
other
(defconst *flexprod-field-keywords*
  '(:type :acc-body :acc-name :default :doc :rule-classes :reqfix :reqfix-vars :shared))
other
(define parse-flexprod-field
  ((x "User-level syntax, a single field they are defining.") (type-name "Product type this field is part of.")
    (our-fixtypes "New fixtypes being defined.")
    (fixtypes "Previous fixtypes."))
  :returns (field "A flexprod-field-p.")
  (b* (((cons name kws) x) ((unless (symbolp name)) (raise "In ~x0: malformed field ~x1: first element should be the name, a symbol."
          type-name
          x))
      ((mv kwd-alist rest) (extract-keywords (list type-name (list name '|[...]|))
          *flexprod-field-keywords*
          kws
          nil))
      ((when rest) (raise "In ~x0: malformed field ~x1: after name should be a keyword/value list."
          type-name
          x))
      (acc-body (getarg :acc-body 0 kwd-alist))
      ((unless (or (symbolp acc-body) (consp acc-body))) (raise "In ~x0: malformed field ~x1: :acc-body should be a term."
          type-name
          x))
      (acc-name (getarg-nonnil! :acc-name (intern-in-package-of-symbol (cat (symbol-name type-name)
              "->"
              (symbol-name name))
            type-name)
          kwd-alist))
      ((mv type fix equiv recp) (get-pred/fix/equiv (getarg :type nil kwd-alist)
          our-fixtypes
          fixtypes))
      (reqfix (getarg :reqfix name kwd-alist)))
    (make-flexprod-field :name name
      :acc-body acc-body
      :acc-name acc-name
      :type type
      :fix fix
      :equiv equiv
      :default (getarg :default nil kwd-alist)
      :doc (getarg :doc "" kwd-alist)
      :reqfix reqfix
      :reqfix-vars (getarg :reqfix-vars :all kwd-alist)
      :rule-classes (let ((look (assoc :rule-classes kwd-alist)))
        (and look `(:rule-classes ,(CDR FTY::LOOK))))
      :recp recp
      :shared (getarg :shared nil kwd-alist))))
other
(define parse-flexprod-fields
  (x type-name our-fixtypes fixtypes)
  (if (atom x)
    nil
    (cons (parse-flexprod-field (car x)
        type-name
        our-fixtypes
        fixtypes)
      (parse-flexprod-fields (cdr x)
        type-name
        our-fixtypes
        fixtypes))))
other
(defconst *flexprod-keywords*
  '(:shape :fields :ctor-body :ctor-name :ctor-macro :remake-name :remake-body :cond :type-name :short :long :inline :require :count-incr :extra-binder-names :no-ctor-macros :verbosep))
other
(define dumb-append-conjunct
  (rev-prev-conds newcond)
  (cond ((or (eq newcond t) (equal newcond ''t)) (reverse rev-prev-conds))
    ((or (eq newcond nil) (equal newcond ''nil)) (list nil))
    (t (revappend rev-prev-conds (list newcond)))))
other
(define parse-flexprod
  ((x "User-level syntax, the whole product type.") (sumname "The name of the superior sum type, e.g., mysum but not mysum-p.")
    (sumkind "The kind function for the superior sum type, if applicable.")
    (sum-kwds "The keyword arguments from the superior sum type.")
    (xvar "The special @('x') variable to use.")
    (rev-not-prevconds "The previous conditions for the sum type, if applicable.")
    (our-fixtypes "New fixtypes being defined.")
    (fixtypes "Previous fixtypes."))
  :returns (prod "A flexprod-p.")
  (b* (((unless (consp x)) (raise "In ~x0: malformed flexprod ~x1: expected (:kind ...)."
         sumname
         x)) ((cons kind kws) x)
      ((unless (keywordp kind)) (raise "In ~x0: malformed flexprod ~x1: kind (~x2) should be a keyword"
          sumname
          x
          kind))
      ((mv kwd-alist rest) (extract-keywords (list kind '|[...]|)
          *flexprod-keywords*
          kws
          nil))
      ((when rest) (raise "In ~x0: malformed flexprod ~x1: after kind keyword ~x1 there ~
                should be only keywords and values."
          sumname
          kind))
      (ctor-body-lookup (assoc :ctor-body kwd-alist))
      ((unless ctor-body-lookup) (raise "In ~x0: malformed product: ~x1: :ctor-body should be a term."
          sumname
          kind))
      (ctor-body (cdr ctor-body-lookup))
      (cond (getarg :cond t kwd-alist))
      (shape (getarg :shape t kwd-alist))
      (type-name (getarg-nonnil! :type-name (intern-in-package-of-symbol (if (getarg :short-names nil sum-kwds)
              (symbol-name kind)
              (cat (symbol-name sumname)
                "-"
                (symbol-name kind)))
            sumname)
          kwd-alist))
      (ctor-name (getarg-nonnil! :ctor-name type-name
          kwd-alist))
      (ctor-macro (getarg-nonnil! :ctor-macro (intern-in-package-of-symbol (cat "MAKE-" (symbol-name ctor-name))
            ctor-name)
          kwd-alist))
      (remake-body (getarg :remake-body nil kwd-alist))
      (remake-name (getarg :remake-name (and remake-body
            (intern-in-package-of-symbol (cat "REMAKE-" (symbol-name ctor-name))
              ctor-name))
          kwd-alist))
      ((when (and remake-name (not remake-body))) (raise "In ~x0: malformed product ~x1: :remake-name is ~x2 but ~
                no :remake-body has been provided."
          sumname
          x
          remake-name))
      (fields (parse-flexprod-fields (getarg :fields nil kwd-alist)
          type-name
          our-fixtypes
          fixtypes))
      (guard (if sumkind
          `(equal (,FTY::SUMKIND ,FTY::XVAR) ,FTY::KIND)
          (let* ((fullcond-terms (dumb-append-conjunct rev-not-prevconds cond)))
            (cond ((atom fullcond-terms) t)
              ((atom (cdr fullcond-terms)) (car fullcond-terms))
              (t `(and . ,FTY::FULLCOND-TERMS))))))
      (inline (get-deftypes-inline-opt (getarg :inline *inline-defaults* sum-kwds)
          kwd-alist))
      (require (getarg :require t kwd-alist))
      (extra-binder-names (getarg :extra-binder-names nil kwd-alist))
      (count-incr (getarg :count-incr nil kwd-alist))
      (no-ctor-macros (getarg :no-ctor-macros nil kwd-alist)))
    (make-flexprod :kind kind
      :cond cond
      :guard guard
      :shape shape
      :require require
      :fields fields
      :type-name type-name
      :ctor-name ctor-name
      :ctor-macro ctor-macro
      :ctor-body ctor-body
      :remake-name remake-name
      :remake-body remake-body
      :extra-binder-names extra-binder-names
      :short (getarg :short nil kwd-alist)
      :long (getarg :long nil kwd-alist)
      :inline inline
      :count-incr count-incr
      :no-ctor-macros no-ctor-macros)))
other
(define dumb-cons-conjunct
  (newcond conds)
  (cond ((or (eq newcond t) (equal newcond ''t)) conds)
    ((or (eq newcond nil) (equal newcond ''nil)) (list nil))
    (t (cons newcond conds))))
other
(define parse-flexprods
  (x sumname
    sumkind
    sum-kwds
    xvar
    rev-not-prevconds
    our-fixtypes
    fixtypes)
  (b* (((when (atom x)) nil) (newprod (parse-flexprod (car x)
          sumname
          sumkind
          sum-kwds
          xvar
          rev-not-prevconds
          our-fixtypes
          fixtypes))
      (rev-not-prevconds (dumb-cons-conjunct (dumb-negate-lit (flexprod->cond newprod))
          rev-not-prevconds)))
    (cons newprod
      (parse-flexprods (cdr x)
        sumname
        sumkind
        sum-kwds
        xvar
        rev-not-prevconds
        our-fixtypes
        fixtypes))))
other
(defconst *flexsum-keywords*
  '(:pred :fix :equiv :kind :count :case :measure :measure-debug :xvar :no-count :shape :kind-body :parents :short :long :short-names :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :inline :enable-rules :verbosep))
other
(define some-flexprod-field-recursivep
  (x)
  (if (atom x)
    nil
    (or (flexprod-field->recp (car x))
      (some-flexprod-field-recursivep (cdr x)))))
other
(define some-flexprod-recursivep
  (x)
  (if (atom x)
    nil
    (or (some-flexprod-field-recursivep (flexprod->fields (car x)))
      (some-flexprod-recursivep (cdr x)))))
other
(define flexsum-infer-xvar
  ((ctx "Context for error messages.") (kwd-alist "Keyword alist that may include :xvar")
    (xvar "The value of :xvar in the superior deftypes call, if applicable.
               When provided, we use this unless the user explicitly overrides
               it in the sum itself.")
    (prods "The products in this sum type, not yet parsed, we're just
               dumbly looking for Xes in these."))
  (b* ((xvar (getarg-nonnil! :xvar xvar kwd-alist)) ((when xvar) xvar)
      (xsyms (find-symbols-named-x prods))
      ((when (atom xsyms)) (raise "In ~x0: no variable named X occurs in the defflexsum form. ~
                Specify another variable with :xvar."
          ctx))
      ((when (consp (cdr xsyms))) (raise "In ~x0: more than one symbol named X occurs in the deftypes ~
                form: ~&1.  Specify the variable denoting the typed object ~
                with :xvar."
          ctx
          xsyms)))
    (car xsyms)))
other
(define flexprod-fields-check-xvar
  (xvar fields prodname)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      ((when (eq x.name xvar)) (raise "Product ~x0 has a field named ~x1, which is not allowed ~
                because it's also the name of the variable representing the ~
                whole product.  You may change the field name or provide an ~
                explicit :xvar argument.~%"
          prodname
          x.name)))
    (flexprod-fields-check-xvar xvar
      (cdr fields)
      prodname)))
other
(define flexprods-check-xvar
  (xvar prods)
  (b* (((when (atom prods)) nil) ((flexprod x) (car prods)))
    (flexprod-fields-check-xvar xvar
      x.fields
      x.kind)
    (flexprods-check-xvar xvar (cdr prods))))
other
(define parse-flexsum
  ((x "User-level syntax, the whole defflexsum form.") (xvar "The special x variable to use.  BOZO but we infer it?")
    (our-fixtypes "New fixtypes being defined.")
    (fixtypes "Previous fixtypes.")
    state)
  :returns (flexsum "A flexsum-p.")
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed flexsum: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist orig-prods) (extract-keywords name
          *flexsum-keywords*
          pre-///
          nil))
      (kwd-alist (append kwd-alist
          (table-alist 'defflexsum-defaults
            (w state))))
      (pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
            name)
          kwd-alist))
      (fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
            name)
          kwd-alist))
      (equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
            name)
          kwd-alist))
      (kind (getarg! :kind (intern-in-package-of-symbol (cat (symbol-name name) "-KIND")
            name)
          kwd-alist))
      (case (getarg! :case (intern-in-package-of-symbol (cat (symbol-name name) "-CASE")
            name)
          kwd-alist))
      (inline (get-deftypes-inline-opt *inline-defaults*
          kwd-alist))
      (shape (getarg :shape t kwd-alist))
      (xvar (flexsum-infer-xvar name
          kwd-alist
          xvar
          orig-prods))
      (measure (getarg! :measure `(acl2-count ,FTY::XVAR)
          kwd-alist))
      (count (flextype-get-count-fn name kwd-alist))
      (prods (parse-flexprods orig-prods
          name
          kind
          kwd-alist
          xvar
          nil
          our-fixtypes
          fixtypes))
      ((when (atom prods)) (raise "Malformed SUM ~x0: Must have at least one product"
          x))
      (- (flexprods-check-xvar xvar prods))
      (recp (some-flexprod-recursivep prods)))
    (make-flexsum :name name
      :pred pred
      :fix fix
      :case case
      :equiv equiv
      :kind kind
      :kind-body (getarg :kind-body nil kwd-alist)
      :count count
      :prods prods
      :xvar xvar
      :inline inline
      :shape shape
      :measure measure
      :kwd-alist (if post-///
        (cons (cons :///-events post-///) kwd-alist)
        kwd-alist)
      :orig-prods orig-prods
      :recp recp
      :typemacro 'defflexsum)))
flexprod-fields-pred-bindingsfunction
(defun flexprod-fields-pred-bindings
  (fields)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      ((unless x.type) (cons (list (intern-in-package-of-symbol (cat "?" (symbol-name x.name))
              x.name)
            x.acc-body)
          (flexprod-fields-pred-bindings (cdr fields)))))
    (cons (list x.name x.acc-body)
      (flexprod-fields-pred-bindings (cdr fields)))))
flexprod-fields-typechecksfunction
(defun flexprod-fields-typechecks
  (fields last)
  (b* (((when (atom fields)) last) ((flexprod-field x) (car fields))
      ((unless x.type) (flexprod-fields-typechecks (cdr fields) last)))
    (nice-and (list x.type x.name)
      (flexprod-fields-typechecks (cdr fields) last))))
flexsum-pred-prod-casefunction
(defun flexsum-pred-prod-case
  (prod)
  (b* (((flexprod prod) prod) (bindings (flexprod-fields-pred-bindings prod.fields))
      (typechecks (flexprod-fields-typechecks prod.fields
          prod.require))
      (typecheckterm `(b* ,FTY::BINDINGS ,FTY::TYPECHECKS)))
    (nice-and prod.shape typecheckterm)))
flexsum-pred-cases-nokindfunction
(defun flexsum-pred-cases-nokind
  (prods)
  (if (atom prods)
    nil
    (cons (list (flexprod->cond (car prods))
        (flexsum-pred-prod-case (car prods)))
      (flexsum-pred-cases-nokind (cdr prods)))))
flexsum-predicate-deffunction
(defun flexsum-predicate-def
  (sum)
  (b* (((flexsum sum) sum) (short (cat "Recognizer for @(see "
          (full-escape-symbol sum.name)
          ") structures."))
      (consp-when-foo-p (intern-in-package-of-symbol (cat "CONSP-WHEN-" (symbol-name sum.pred))
          sum.pred)))
    `(define ,FTY::SUM.PRED
      (,FTY::SUM.XVAR)
      :parents (,FTY::SUM.NAME)
      :short ,FTY::SHORT
      :measure ,FTY::SUM.MEASURE
      ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::SUM.KWD-ALIST) `(:MEASURE-DEBUG T))
      :progn t
      ,(FTY::NICE-AND FTY::SUM.SHAPE
  (FTY::NICE-COND (FTY::FLEXSUM-PRED-CASES-NOKIND FTY::SUM.PRODS)))
      ///
      (make-event '(:or (:do-proofs (with-output :off (error)
              (defthm ,FTY::CONSP-WHEN-FOO-P
                (implies (,FTY::SUM.PRED ,FTY::SUM.XVAR)
                  (consp ,FTY::SUM.XVAR))
                :hints (("goal" :expand ((,FTY::SUM.PRED ,FTY::SUM.XVAR))) (and stable-under-simplificationp '(:error t)))
                :rule-classes :compound-recognizer)))
          (value-triple :skip-compound-recognizer))))))
flextype-sum-kind-conds-basicfunction
(defun flextype-sum-kind-conds-basic
  (prods)
  (if (atom prods)
    nil
    (cons `(,(FTY::FLEXPROD->COND (CAR FTY::PRODS)) ,(FTY::FLEXPROD->KIND (CAR FTY::PRODS)))
      (flextype-sum-kind-conds-basic (cdr prods)))))
match-optimizable-tag-checkfunction
(defun match-optimizable-tag-check
  (prod.cond xvar)
  "Returns (mv matchp possible-tags)"
  (case-match prod.cond
    ((eqsym ('tag var) ('quote foo)) (if (and (member eqsym '(eq eql equal))
          (eq var xvar))
        (mv t (list foo))
        (mv nil nil)))
    (('or ('not ('mbt ('consp var))) tag-cond) (if (eq var xvar)
        (match-optimizable-tag-check tag-cond xvar)
        (mv nil nil)))
    (& (mv nil nil))))
other
(define prod-conds-can-be-optimized-p
  (prods xvar)
  (b* (((when (atom prods)) (raise "never get here")) ((when (atom (cdr prods))) (equal (flexprod->cond (car prods)) t))
      ((mv matchp &) (match-optimizable-tag-check (flexprod->cond (car prods))
          xvar))
      ((unless matchp) nil))
    (prod-conds-can-be-optimized-p (cdr prods)
      xvar)))
other
(define flextype-sum-kind-conds-optimized
  (prods xvar)
  (b* (((when (atom prods)) (raise "should never get here")) (ans1 (flexprod->kind (car prods)))
      ((when (atom (cdr prods))) (list `(otherwise ,FTY::ANS1)))
      ((mv matchp tags1) (match-optimizable-tag-check (flexprod->cond (car prods))
          xvar))
      ((unless matchp) (raise "expected optimizable tags.")))
    (cons `(,FTY::TAGS1 ,FTY::ANS1)
      (flextype-sum-kind-conds-optimized (cdr prods)
        xvar))))
flextype-sum-kind-condsfunction
(defun flextype-sum-kind-conds
  (prods xvar)
  "Returns (mv optimized-p body)"
  (if (prod-conds-can-be-optimized-p prods xvar)
    (mv t
      `(case (tag ,FTY::XVAR) . ,(FTY::FLEXTYPE-SUM-KIND-CONDS-OPTIMIZED FTY::PRODS FTY::XVAR)))
    (mv nil
      (nice-cond (flextype-sum-kind-conds-basic prods)))))
flextype-def-sum-kindfunction
(defun flextype-def-sum-kind
  (sum)
  (b* (((flexsum sum) sum) ((when (not sum.kind)) nil)
      ((mv optimized-p condform) (flextype-sum-kind-conds sum.prods sum.xvar))
      (values (flexprods->kinds sum.prods))
      (possibilities (pairlis$ (make-list (len values) :initial-element 'equal)
          (pairlis$ (make-list (len values)
              :initial-element `(,FTY::SUM.KIND ,FTY::SUM.XVAR))
            (pairlis$ values nil))))
      (short (cat "Get the <i>kind</i> (tag) of a @(see "
          (full-escape-symbol sum.name)
          ") structure."))
      (foo-kind-possibilities (intern-in-package-of-symbol (cat (symbol-name sum.kind) "-POSSIBILITIES")
          sum.kind))
      (foo-kind-tag-preservation-helper (intern-in-package-of-symbol (cat (symbol-name sum.kind)
            "-TAG-PRESERVATION-HELPER")
          sum.kind)))
    `((define ,FTY::SUM.KIND
       ((,FTY::SUM.XVAR ,FTY::SUM.PRED))
       :parents (,FTY::SUM.NAME)
       :short ,FTY::SHORT
       :returns ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL "KIND" FTY::SUM.NAME)
       ,@(AND (MEMBER :KIND FTY::SUM.INLINE) `(:INLINE T))
       :guard-hints (("Goal" :in-theory (disable open-member-equal-on-list-of-tags)) (and stable-under-simplificationp
           '(:expand ((,FTY::SUM.PRED ,FTY::SUM.XVAR)))))
       :progn t
       ,(IF FTY::SUM.KIND-BODY
     `(FTY::MBE :LOGIC ,FTY::CONDFORM :EXEC ,FTY::SUM.KIND-BODY)
     FTY::CONDFORM)
       ///
       (defthm ,FTY::FOO-KIND-POSSIBILITIES
         (or . ,FTY::POSSIBILITIES)
         :rule-classes ((:forward-chaining :trigger-terms ((,FTY::SUM.KIND ,FTY::SUM.XVAR)))))
       (add-to-ruleset tag-reasoning
         '(,FTY::FOO-KIND-POSSIBILITIES))
       ,@(AND FTY::OPTIMIZED-P
       `((FTY::LOCAL
          (FTY::DEFTHMD ,FTY::FOO-KIND-TAG-PRESERVATION-HELPER
           (FTY::IMPLIES (FTY::MEMBER-EQUAL (FTY::TAG FTY::X) ',VALUES)
            (EQUAL (,FTY::SUM.KIND FTY::X) (FTY::TAG FTY::X)))
           :HINTS (("Goal" :IN-THEORY (FTY::ENABLE FTY::CONSP-WHEN-TAG)))))))))))
find-prod-by-kindfunction
(defun find-prod-by-kind
  (kind prods)
  (b* (((when (atom prods)) nil) ((flexprod prod) (car prods))
      ((when (eq prod.kind kind)) prod))
    (find-prod-by-kind kind (cdr prods))))
other
(define flexsum-kind-case-macro-spec-prods
  (prods)
  (if (atom prods)
    nil
    (b* (((flexprod prod) (car prods)))
      (cons (list prod.kind prod.ctor-name)
        (flexsum-kind-case-macro-spec-prods (cdr prods))))))
other
(define flexsum-kind-case-macro-spec
  (sum)
  (b* (((flexsum sum)) (prods (flexsum-kind-case-macro-spec-prods sum.prods)))
    (list* sum.case sum.kind prods)))
other
(define flexsum-cond-case-macro-spec-prods
  (prods)
  (if (atom prods)
    nil
    (b* (((flexprod prod) (car prods)))
      (cons (list prod.kind prod.cond prod.ctor-name)
        (flexsum-cond-case-macro-spec-prods (cdr prods))))))
other
(define flexsum-cond-case-macro-spec
  (sum)
  (b* (((flexsum sum)) (prods (flexsum-cond-case-macro-spec-prods sum.prods)))
    (list* sum.case sum.xvar prods)))
flexsum-def-case-macrofunction
(defun flexsum-def-case-macro
  (sum)
  (b* (((flexsum sum) sum) ((unless sum.case) nil)
      (case-spec (if sum.kind
          (flexsum-kind-case-macro-spec sum)
          (flexsum-cond-case-macro-spec sum)))
      (kind-eq (and sum.kind
          (intern-in-package-of-symbol (concatenate 'string (symbol-name sum.kind) "-EQ")
            sum.kind))))
    `((defmacro ,FTY::SUM.CASE
       (var-or-expr &rest args)
       ,(IF FTY::SUM.KIND
     `(FTY::KIND-CASEMACRO-FN FTY::VAR-OR-EXPR FTY::ARGS ',FTY::CASE-SPEC)
     `(FTY::COND-CASEMACRO-FN FTY::VAR-OR-EXPR FTY::ARGS ',FTY::CASE-SPEC))) ,@(AND FTY::SUM.KIND
       `((DEFMACRO ,FTY::KIND-EQ (FTY::KIND KEYWORD)
           (DECLARE
            (FTY::XARGS :GUARD
             (FTY::MEMBER-EQ KEYWORD
              (QUOTE ,(FTY::FLEXPRODS->KINDS FTY::SUM.PRODS)))))
           `(EQ ,FTY::KIND ,KEYWORD)))))))
flextype-def-sum-kindsfunction
(defun flextype-def-sum-kinds
  (sums)
  (if (atom sums)
    nil
    (append (and (eq (tag (car sums)) :sum)
        (flextype-def-sum-kind (car sums)))
      (and (eq (tag (car sums)) :sum)
        (flexsum-def-case-macro (car sums)))
      (flextype-def-sum-kinds (cdr sums)))))
flexprod-fields-typefix-bindingsfunction
(defun flexprod-fields-typefix-bindings
  (fields names)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields)))
    (if (or (eq names :all)
        (member-eq x.name names))
      (cons `(,FTY::X.NAME ,(IF FTY::X.FIX
     `(,FTY::X.FIX ,FTY::X.ACC-BODY)
     FTY::X.ACC-BODY))
        (flexprod-fields-typefix-bindings (cdr fields)
          names))
      (flexprod-fields-typefix-bindings (cdr fields)
        names))))
flexprod-fields-reqfix-bindingsfunction
(defun flexprod-fields-reqfix-bindings
  (fields)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields)))
    (if (eq x.name x.reqfix)
      (flexprod-fields-reqfix-bindings (cdr fields))
      (cons (list x.name x.reqfix)
        (flexprod-fields-reqfix-bindings (cdr fields))))))
flexsum-fix-prod-casefunction
(defun flexsum-fix-prod-case
  (prod)
  (b* (((flexprod prod) prod) (typefix-bindings (flexprod-fields-typefix-bindings prod.fields
          :all))
      (reqfix-bindings (flexprod-fields-reqfix-bindings prod.fields)))
    (if typefix-bindings
      `(b* ,FTY::TYPEFIX-BINDINGS
        ,(IF FTY::REQFIX-BINDINGS
     `(LET ,FTY::REQFIX-BINDINGS
        ,FTY::PROD.CTOR-BODY)
     FTY::PROD.CTOR-BODY))
      prod.ctor-body)))
flexsum-fix-casesfunction
(defun flexsum-fix-cases
  (prods)
  (if (atom prods)
    nil
    (cons (list (flexprod->kind (car prods))
        (flexsum-fix-prod-case (car prods)))
      (flexsum-fix-cases (cdr prods)))))
flexsum-fix-cases-nokindfunction
(defun flexsum-fix-cases-nokind
  (prods)
  (if (atom prods)
    nil
    (cons (list (flexprod->cond (car prods))
        (flexsum-fix-prod-case (car prods)))
      (flexsum-fix-cases-nokind (cdr prods)))))
flexsum-fix-deffunction
(defun flexsum-fix-def
  (sum flagp)
  (b* (((flexsum sum) sum) (body (if sum.kind
          `(case (,FTY::SUM.KIND ,FTY::SUM.XVAR) . ,(FTY::FLEXSUM-FIX-CASES FTY::SUM.PRODS))
          (nice-cond (flexsum-fix-cases-nokind sum.prods))))
      (short (cat "Fixing function for @(see "
          (full-escape-symbol sum.name)
          ") structures."))
      (newx (intern-in-package-of-symbol "NEW-X" sum.name)))
    `(define ,FTY::SUM.FIX
      ((,FTY::SUM.XVAR ,FTY::SUM.PRED))
      :parents (,FTY::SUM.NAME)
      :short ,FTY::SHORT
      :inline t
      :measure ,FTY::SUM.MEASURE
      :hints ,(AND FTY::SUM.KIND `(("Goal" :EXPAND ((,FTY::SUM.KIND ,FTY::SUM.XVAR)))))
      ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::SUM.KWD-ALIST) `(:MEASURE-DEBUG T))
      ,@(AND FTY::FLAGP `(:FLAG ,FTY::SUM.NAME))
      :returns (,FTY::NEWX ,FTY::SUM.PRED
        :hints ('(:in-theory (disable ,FTY::SUM.FIX
             ,FTY::SUM.PRED . ,(AND FTY::SUM.KIND `(,FTY::SUM.KIND)))
           :expand ((,FTY::SUM.FIX ,FTY::SUM.XVAR))) (and stable-under-simplificationp
            (let ((lit (car (last clause))))
              (and (eq (car lit) ',FTY::SUM.PRED)
                `(:expand (,FTY::LIT)))))))
      :progn t
      :verify-guards nil
      (mbe :logic ,FTY::BODY :exec ,FTY::SUM.XVAR)
      ///
      ,@(AND FTY::SUM.DISABLE-TYPE-PRESCRIPTION
       `((FTY::IN-THEORY (FTY::DISABLE (:T ,FTY::SUM.FIX))))))))
flexsum-fix-posteventsfunction
(defun flexsum-fix-postevents
  (x)
  (b* (((flexsum x) x) (foo-kind-possibilities (intern-in-package-of-symbol (cat (symbol-name x.kind) "-POSSIBILITIES")
          x.kind))
      (foo-kind-tag-preservation-helper (intern-in-package-of-symbol (cat (symbol-name x.kind)
            "-TAG-PRESERVATION-HELPER")
          x.kind)))
    (and x.kind
      `((local (enable-if-theorem ,FTY::FOO-KIND-TAG-PRESERVATION-HELPER)) (local (in-theory (disable ,FTY::FOO-KIND-POSSIBILITIES)))
        (deffixequiv ,FTY::X.KIND
          :args ((,FTY::X.XVAR ,FTY::X.PRED))
          :hints (("Goal" :in-theory (e/d* ((:e member-equal) tag-reasoning)
               ((:rules-of-class :type-prescription :here)))
             :expand ((,FTY::X.FIX ,FTY::X.XVAR) (,FTY::X.KIND ,FTY::X.XVAR))) (and stable-under-simplificationp
              '(:in-theory (enable ,FTY::X.KIND)
                :expand ((,FTY::X.FIX ,FTY::X.XVAR))))))
        (local (disable-if-theorem ,FTY::FOO-KIND-TAG-PRESERVATION-HELPER))
        (make-event (b* ((consp-when-foo-p ',(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT "CONSP-WHEN-" (SYMBOL-NAME FTY::X.PRED)) FTY::X.PRED)) (sum.xvar ',FTY::X.XVAR)
              (sum.fix ',FTY::X.FIX)
              (consp-of-fix ',(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT "CONSP-OF-" (SYMBOL-NAME FTY::X.FIX)) FTY::X.FIX))
              ((unless (fgetprop consp-when-foo-p
                   'theorem
                   nil
                   (w state))) '(value-triple :skip-type-prescription)))
            `(defthm ,FTY::CONSP-OF-FIX
              (consp (,FTY::SUM.FIX ,FTY::SUM.XVAR))
              :hints (("goal" :use ((:instance ,FTY::CONSP-WHEN-FOO-P
                    (,FTY::SUM.XVAR (,FTY::SUM.FIX ,FTY::SUM.XVAR))))
                 :in-theory (disable ,FTY::CONSP-WHEN-FOO-P)))
              :rule-classes :type-prescription)))))))
flexsum-fix-when-pred-thmfunction
(defun flexsum-fix-when-pred-thm
  (x flagp)
  (b* (((flexsum x) x) (foo-fix-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.fix)
            "-WHEN-"
            (symbol-name x.pred))
          x.fix)))
    `(defthm ,FTY::FOO-FIX-WHEN-FOO-P
      (implies (,FTY::X.PRED ,FTY::X.XVAR)
        (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR))
      :hints ('(:expand ((,FTY::X.PRED ,FTY::X.XVAR) (,FTY::X.FIX ,FTY::X.XVAR)
           ,@(AND FTY::X.KIND `((,FTY::X.KIND ,FTY::X.XVAR))))
         :in-theory (disable ,FTY::X.PRED ,FTY::X.FIX))) . ,(AND FTY::FLAGP `(:FLAG ,FTY::X.NAME)))))
flexprod-field-accfunction
(defun flexprod-field-acc
  (x prod sum)
  (b* (((flexsum sum) sum) ((flexprod prod) prod)
      ((flexprod-field x) x)
      (short (b* ((acc nil) (acc (revappend-chars "Get the <tt>@(sym " acc))
            (acc (revappend-chars (full-escape-symbol x.name)
                acc))
            (acc (revappend-chars ")</tt> field from a @(see? "
                acc))
            (acc (revappend-chars (full-escape-symbol prod.type-name)
                acc))
            (acc (revappend-chars ")." acc)))
          (rchars-to-string acc)))
      (long "<p>This is an ordinary field accessor created by @(see fty::defprod).</p>"))
    `((define ,FTY::X.ACC-NAME
       ((,FTY::SUM.XVAR ,FTY::SUM.PRED))
       :parents (,FTY::PROD.TYPE-NAME)
       :short ,FTY::SHORT
       :long ,FTY::LONG
       ,@(AND (MEMBER :ACC FTY::PROD.INLINE) `(:INLINE T))
       ,@(AND (NOT FTY::X.SHARED) `(:GUARD ,FTY::PROD.GUARD))
       :guard-hints (("goal" :expand ((,FTY::SUM.PRED ,FTY::SUM.XVAR) . ,(AND FTY::SUM.KIND `((,FTY::SUM.KIND ,FTY::SUM.XVAR))))))
       :returns ,(IF FTY::X.TYPE
     `(,FTY::X.NAME ,FTY::X.TYPE ,@FTY::X.RULE-CLASSES)
     `(FTY::X.NAME))
       :progn t
       (mbe :logic ,(FTY::B*
  ((FTY::BODY
    (IF (EQ FTY::X.REQFIX FTY::X.NAME)
        (IF FTY::X.FIX
            `(,FTY::X.FIX ,FTY::X.ACC-BODY)
            FTY::X.ACC-BODY)
        FTY::X.REQFIX))
   (FTY::XVAR-BINDING
    (AND (NOT FTY::X.SHARED)
         `((,FTY::SUM.XVAR (AND ,FTY::PROD.GUARD ,FTY::SUM.XVAR)))))
   (FTY::BINDINGS
    (IF (EQ FTY::X.REQFIX FTY::X.NAME)
        FTY::XVAR-BINDING
        (APPEND FTY::XVAR-BINDING
                (FTY::FLEXPROD-FIELDS-TYPEFIX-BINDINGS FTY::PROD.FIELDS
                 FTY::X.REQFIX-VARS)))))
  (IF FTY::BINDINGS
      `(FTY::B* ,FTY::BINDINGS ,FTY::BODY)
      FTY::BODY))
         :exec ,FTY::X.ACC-BODY)
       ///
       (deffixequiv ,FTY::X.ACC-NAME
         :hints (,@(AND FTY::SUM.KIND `(("goal" :IN-THEORY (FTY::DISABLE ,FTY::SUM.KIND)))) (and stable-under-simplificationp
             '(,@(AND FTY::SUM.KIND `(:IN-THEORY (FTY::ENABLE ,FTY::SUM.KIND))) :expand ((,FTY::SUM.FIX ,FTY::SUM.XVAR))))))
       ,@(AND (NOT (EQ FTY::PROD.GUARD T)) (NOT FTY::X.SHARED)
       `((FTY::DEFTHMD
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::X.ACC-NAME) "-WHEN-WRONG-KIND")
            FTY::X.ACC-NAME)
          (FTY::IMPLIES (NOT ,FTY::PROD.GUARD)
           (EQUAL (,FTY::X.ACC-NAME ,FTY::SUM.XVAR)
                  ,(IF (EQ FTY::X.REQFIX FTY::X.NAME)
                       (IF FTY::X.FIX
                           `(,FTY::X.FIX NIL)
                           NIL)
                       `(FTY::B*
                         ((,FTY::SUM.XVAR NIL)
                          . ,(FTY::FLEXPROD-FIELDS-TYPEFIX-BINDINGS
                              FTY::PROD.FIELDS FTY::X.REQFIX-VARS))
                         ,FTY::X.REQFIX))))
          :HINTS
          (("Goal" :IN-THEORY
            (FTY::DISABLE ,@(AND FTY::SUM.KIND `(,FTY::SUM.KIND))))))))) (local (in-theory (enable ,FTY::X.ACC-NAME))))))
flexprod-field-acc-lstfunction
(defun flexprod-field-acc-lst
  (fields prod sum)
  (if (atom fields)
    nil
    (append (flexprod-field-acc (car fields)
        prod
        sum)
      (flexprod-field-acc-lst (cdr fields)
        prod
        sum))))
flexprod-field-accessorsfunction
(defun flexprod-field-accessors
  (prod sum)
  (flexprod-field-acc-lst (flexprod->fields prod)
    prod
    sum))
flexprod-field-names-typesfunction
(defun flexprod-field-names-types
  (fields)
  (if (atom fields)
    nil
    (cons (b* (((flexprod-field x) (car fields)))
        (if x.type
          (list x.name x.type)
          (list x.name)))
      (flexprod-field-names-types (cdr fields)))))
flexprod-fields-mbe-typefix-bindingsfunction
(defun flexprod-fields-mbe-typefix-bindings
  (fields)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      ((unless x.fix) (flexprod-fields-mbe-typefix-bindings (cdr fields))))
    (cons `(,FTY::X.NAME (mbe :logic (,FTY::X.FIX ,FTY::X.NAME)
          :exec ,FTY::X.NAME))
      (flexprod-fields-mbe-typefix-bindings (cdr fields)))))
flexprod-fields-mbe-reqfix-bindingsfunction
(defun flexprod-fields-mbe-reqfix-bindings
  (fields)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      ((when (eq x.reqfix x.name)) (flexprod-fields-mbe-reqfix-bindings (cdr fields))))
    (cons `(,FTY::X.NAME (mbe :logic ,FTY::X.REQFIX :exec ,FTY::X.NAME))
      (flexprod-fields-mbe-reqfix-bindings (cdr fields)))))
flexprod-ctor-callfunction
(defun flexprod-ctor-call
  (prod)
  (b* (((flexprod prod) prod))
    (cons prod.ctor-name
      (flexprod-fields->names prod.fields))))
flexprod-fields-ignorable-typefix-bindingsfunction
(defun flexprod-fields-ignorable-typefix-bindings
  (fields)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      ((unless x.fix) (flexprod-fields-mbe-typefix-bindings (cdr fields))))
    (cons `(,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING "?" (SYMBOL-NAME FTY::X.NAME)) FTY::X.NAME) (,FTY::X.FIX ,FTY::X.NAME))
      (flexprod-fields-ignorable-typefix-bindings (cdr fields)))))
flexprod-acc-of-ctor-thms1function
(defun flexprod-acc-of-ctor-thms1
  (fields all-fields ctor-call)
  (b* (((when (atom fields)) nil) ((flexprod-field x) (car fields))
      (fixterm (if (eq x.reqfix x.name)
          (if x.fix
            `(,FTY::X.FIX ,FTY::X.NAME)
            x.name)
          `(b* ,(FTY::FLEXPROD-FIELDS-IGNORABLE-TYPEFIX-BINDINGS FTY::ALL-FIELDS)
            ,FTY::X.REQFIX)))
      (foo->bar-of-foo (intern-in-package-of-symbol (cat (symbol-name x.acc-name)
            "-OF-"
            (symbol-name (car ctor-call)))
          x.acc-name)))
    (cons `(defthm ,FTY::FOO->BAR-OF-FOO
        (equal (,FTY::X.ACC-NAME ,FTY::CTOR-CALL) ,FTY::FIXTERM)
        :hints (("Goal" :in-theory (e/d (,FTY::X.ACC-NAME) (,(CAR FTY::CTOR-CALL)))) (and stable-under-simplificationp
            '(:in-theory (enable ,(CAR FTY::CTOR-CALL))))))
      (flexprod-acc-of-ctor-thms1 (cdr fields)
        all-fields
        ctor-call))))
flexprod-acc-of-ctor-thmsfunction
(defun flexprod-acc-of-ctor-thms
  (prod)
  (flexprod-acc-of-ctor-thms1 (flexprod->fields prod)
    (flexprod->fields prod)
    (flexprod-ctor-call prod)))
flexprod-fields-acc-callsfunction
(defun flexprod-fields-acc-calls
  (fields xvar)
  (if (atom fields)
    nil
    (cons `(,(FTY::FLEXPROD-FIELD->ACC-NAME (CAR FTY::FIELDS)) ,FTY::XVAR)
      (flexprod-fields-acc-calls (cdr fields) xvar))))
flexprod-equal-of-field-accessorsfunction
(defun flexprod-equal-of-field-accessors
  (fields all-fields xvar)
  (if (atom fields)
    nil
    (cons (b* (((flexprod-field x) (car fields)))
        `(equal (,FTY::X.ACC-NAME ,FTY::XVAR)
          ,(IF (EQ FTY::X.REQFIX FTY::X.NAME)
     (IF FTY::X.FIX
         `(,FTY::X.FIX ,FTY::X.NAME)
         FTY::X.NAME)
     `(FTY::B*
       ,(FTY::FLEXPROD-FIELDS-IGNORABLE-TYPEFIX-BINDINGS FTY::ALL-FIELDS)
       ,FTY::X.REQFIX))))
      (flexprod-equal-of-field-accessors (cdr fields)
        all-fields
        xvar))))
flexprod-fields-macro-argsfunction
(defun flexprod-fields-macro-args
  (x)
  (b* (((when (atom x)) nil) ((flexprod-field f) (car x)))
    (cons `(,FTY::F.NAME ',FTY::F.DEFAULT)
      (flexprod-fields-macro-args (cdr x)))))
flexprod-fields-bind-accessorsfunction
(defun flexprod-fields-bind-accessors
  (x xvar)
  (b* (((when (atom x)) nil) ((flexprod-field f) (car x)))
    (cons (list (intern-in-package-of-symbol (cat "?" (symbol-name f.name))
          f.name)
        `(,FTY::F.ACC-NAME ,FTY::XVAR))
      (flexprod-fields-bind-accessors (cdr x) xvar))))
flexprod-remakerfunction
(defun flexprod-remaker
  (prod sum)
  (b* (((flexsum sum) sum) ((flexprod prod) prod)
      ((unless prod.remake-name) nil)
      (fieldnames (flexprod-fields->names prod.fields))
      (fields/types (flexprod-field-names-types prod.fields)))
    `((define ,FTY::PROD.REMAKE-NAME
       ((,FTY::SUM.XVAR ,FTY::SUM.PRED) . ,FTY::FIELDS/TYPES)
       :guard ,(FTY::NICE-AND FTY::PROD.GUARD FTY::PROD.REQUIRE)
       :parents nil
       ,@(AND (MEMBER :XTOR FTY::PROD.INLINE) `(:INLINE T))
       :hooks nil
       :progn t
       :enabled t
       (mbe :logic (,FTY::PROD.CTOR-NAME . ,FTY::FIELDNAMES)
         :exec ,FTY::PROD.REMAKE-BODY)
       :guard-hints (("Goal" :in-theory (enable ,FTY::SUM.PRED . ,(AND FTY::SUM.KIND `(,FTY::SUM.KIND)))
          :expand ((,FTY::PROD.CTOR-NAME . ,FTY::FIELDNAMES) (,FTY::SUM.PRED ,FTY::SUM.XVAR))))))))
flexprod-constructorfunction
(defun flexprod-constructor
  (prod sum)
  (b* (((flexsum sum) sum) ((flexprod prod) prod)
      (field-calls (flexprod-fields-acc-calls prod.fields
          sum.xvar))
      (fieldnames (flexprod-fields->names prod.fields))
      (field-accs (pairlis$ fieldnames
          (flexprod-fields->acc-names prod.fields)))
      (binder-accs (append field-accs
          (append (extra-binder-names->acc-alist prod.extra-binder-names
              prod.type-name))))
      (foo-of-fields (intern-in-package-of-symbol (cat (symbol-name prod.ctor-name) "-OF-FIELDS")
          prod.ctor-name))
      (foo-fix-when-foo-kind (intern-in-package-of-symbol (cat (symbol-name sum.fix)
            "-WHEN-"
            (symbol-name prod.kind))
          sum.fix))
      (equal-of-foo (intern-in-package-of-symbol (cat "EQUAL-OF-" (symbol-name prod.ctor-name))
          prod.ctor-name))
      (typefixes (flexprod-fields-mbe-typefix-bindings prod.fields))
      (reqfixes (flexprod-fields-mbe-reqfix-bindings prod.fields))
      (reqfix-body (if reqfixes
          `(let ,FTY::REQFIXES
            ,FTY::PROD.CTOR-BODY)
          prod.ctor-body))
      (typefix-body (if typefixes
          `(b* ,FTY::TYPEFIXES ,FTY::REQFIX-BODY)
          reqfix-body)))
    `((define ,FTY::PROD.CTOR-NAME
       ,(FTY::FLEXPROD-FIELD-NAMES-TYPES FTY::PROD.FIELDS)
       :parents nil
       ,@(AND (MEMBER :XTOR FTY::PROD.INLINE) `(:INLINE T))
       :guard ,FTY::PROD.REQUIRE
       :returns (,FTY::SUM.XVAR ,(IF (EQ FTY::PROD.GUARD T)
     FTY::SUM.PRED
     `(AND (,FTY::SUM.PRED ,FTY::SUM.XVAR) ,FTY::PROD.GUARD))
         :hints (("Goal" :in-theory (enable ,FTY::SUM.PRED . ,(AND FTY::SUM.KIND `(,FTY::SUM.KIND))))))
       :progn t
       ,FTY::TYPEFIX-BODY
       ///
       ,@(AND FTY::SUM.DISABLE-TYPE-PRESCRIPTION
       `((FTY::IN-THEORY (FTY::DISABLE (:T ,FTY::PROD.CTOR-NAME)))))
       ,@(FTY::FLEXPROD-ACC-OF-CTOR-THMS FTY::PROD)
       ,@(AND (NOT (EQ FTY::PROD.REQUIRE T))
       (LET ((FTY::FOO-REQUIREMENTS
              (FTY::INTERN-IN-PACKAGE-OF-SYMBOL
               (FTY::CAT (SYMBOL-NAME FTY::PROD.CTOR-NAME) "-REQUIREMENTS")
               FTY::PROD.CTOR-NAME)))
         `((FTY::DEFTHM ,FTY::FOO-REQUIREMENTS
            (FTY::B*
             ,(FTY::FLEXPROD-FIELDS-BIND-ACCESSORS FTY::PROD.FIELDS
               FTY::SUM.XVAR)
             ,FTY::PROD.REQUIRE)))))
       ,@(AND (CONSP FTY::PROD.FIELDS)
       `((FTY::DEFTHM ,FTY::FOO-OF-FIELDS
          ,(FTY::NICE-IMPLIES FTY::PROD.GUARD
            `(EQUAL (,FTY::PROD.CTOR-NAME . ,FTY::FIELD-CALLS)
                    (,FTY::SUM.FIX ,FTY::SUM.XVAR)))
          :HINTS (("Goal" :EXPAND ((,FTY::SUM.FIX ,FTY::SUM.XVAR)))))))
       (,(IF (ATOM FTY::PROD.FIELDS)
     'FTY::DEFTHM
     'FTY::DEFTHMD) ,FTY::FOO-FIX-WHEN-FOO-KIND
         ,(FTY::NICE-IMPLIES FTY::PROD.GUARD
  `(EQUAL (,FTY::SUM.FIX ,FTY::SUM.XVAR)
          (,FTY::PROD.CTOR-NAME . ,FTY::FIELD-CALLS)))
         :hints (("Goal" :expand ((,FTY::SUM.FIX ,FTY::SUM.XVAR)))) . ,(AND (NOT (EQ FTY::PROD.GUARD T))
      '(:RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0)))))
       (defthm ,FTY::EQUAL-OF-FOO
         (equal (equal ,(FTY::FLEXPROD-CTOR-CALL FTY::PROD) ,FTY::SUM.XVAR)
           (and (,FTY::SUM.PRED ,FTY::SUM.XVAR)
             ,@(AND (NOT (EQ FTY::PROD.GUARD T)) (LIST FTY::PROD.GUARD)) . ,(FTY::FLEXPROD-EQUAL-OF-FIELD-ACCESSORS FTY::PROD.FIELDS FTY::PROD.FIELDS
  FTY::SUM.XVAR)))
         :hints (("goal" :in-theory (disable* ,FTY::PROD.CTOR-NAME
              ,@(FTY::FLEXPROD-FIELDS->ACC-NAMES FTY::PROD.FIELDS)
              ,@(AND FTY::SUM.KIND `(,FTY::SUM.KIND))
              ,@(IF (CONSP FTY::PROD.FIELDS)
      `(,FTY::FOO-OF-FIELDS)
      `(,FTY::FOO-FIX-WHEN-FOO-KIND))
              deftypes-temp-thms
              (:rules-of-class :forward-chaining :here)
              (:rules-of-class :type-prescription :here))
            ,@(IF (CONSP FTY::PROD.FIELDS)
      `(:USE ,FTY::FOO-OF-FIELDS)
      `(:USE ,FTY::FOO-FIX-WHEN-FOO-KIND))) (and stable-under-simplificationp
             '(:in-theory (e/d* (,FTY::PROD.CTOR-NAME)
                 (,@(FTY::FLEXPROD-FIELDS->ACC-NAMES FTY::PROD.FIELDS) ,@(AND FTY::SUM.KIND `(,FTY::SUM.KIND))
                   ,@(IF (CONSP FTY::PROD.FIELDS)
      `(,FTY::FOO-OF-FIELDS)
      `(,FTY::FOO-FIX-WHEN-FOO-KIND))
                   deftypes-temp-thms
                   (:rules-of-class :forward-chaining :here)
                   (:rules-of-class :type-prescription :here)))))))
       (deffixequiv ,FTY::PROD.CTOR-NAME)
       (def-b*-binder ,FTY::PROD.CTOR-NAME
         :body (da-patbind-fn ',FTY::PROD.CTOR-NAME
           ',FTY::BINDER-ACCS
           args
           forms
           rest-expr))
       ,@(AND (NOT FTY::PROD.NO-CTOR-MACROS)
       `(,(STD::DA-MAKE-MAKER FTY::PROD.CTOR-NAME FTY::FIELDNAMES
           (FTY::FLEXPROD-FIELDS->DEFAULTS FTY::PROD.FIELDS))
         ,(STD::DA-MAKE-CHANGER FTY::PROD.CTOR-NAME FTY::FIELDNAMES
           FTY::PROD.REMAKE-NAME)))) (local (in-theory (enable ,FTY::PROD.CTOR-NAME))))))
flexprod-fnsfunction
(defun flexprod-fns
  (prod)
  (b* (((flexprod prod) prod))
    (cons prod.ctor-name
      (flexprod-fields->acc-names prod.fields))))
flexsum-prod-fnsfunction
(defun flexsum-prod-fns
  (prods)
  (if (atom prods)
    nil
    (append (flexprod-fns (car prods))
      (flexsum-prod-fns (cdr prods)))))
flexsum-prod-ctorsfunction
(defun flexsum-prod-ctors
  (prods)
  (if (atom prods)
    nil
    (cons (flexprod->ctor-name (car prods))
      (flexsum-prod-ctors (cdr prods)))))
flexsum-fnsfunction
(defun flexsum-fns
  (x)
  (b* (((flexsum x) x) (fns1 (list* x.pred
          x.fix
          (flexsum-prod-fns x.prods))))
    (if x.kind
      (cons x.kind fns1)
      fns1)))
flexprod-accessor/constructorsfunction
(defun flexprod-accessor/constructors
  (prod sum)
  (append (flexprod-field-accessors prod sum)
    (flexprod-constructor prod sum)
    (flexprod-remaker prod sum)))
flexsum-prods-accessor/constructorsfunction
(defun flexsum-prods-accessor/constructors
  (prods sum)
  (if (atom prods)
    nil
    (append (flexprod-accessor/constructors (car prods)
        sum)
      (flexsum-prods-accessor/constructors (cdr prods)
        sum))))
flexprod-x-dot-fieldsfunction
(defun flexprod-x-dot-fields
  (xvar fields)
  (if (atom fields)
    nil
    (cons (let ((name (flexprod-field->name (car fields))))
        (intern-in-package-of-symbol (cat (symbol-name xvar)
            "."
            (symbol-name name))
          name))
      (flexprod-x-dot-fields xvar (cdr fields)))))
flexsum-fix-redef-prod-casesfunction
(defun flexsum-fix-redef-prod-cases
  (prods xvar)
  (if (atom prods)
    nil
    (b* (((flexprod prod) (car prods)))
      (cons `(,FTY::PROD.KIND (,FTY::PROD.CTOR-NAME . ,(FTY::FLEXPROD-FIELDS-ACC-CALLS FTY::PROD.FIELDS FTY::XVAR)))
        (flexsum-fix-redef-prod-cases (cdr prods)
          xvar)))))
flexsum-fix-redef-prod-cases-nokindfunction
(defun flexsum-fix-redef-prod-cases-nokind
  (prods xvar)
  (if (atom prods)
    nil
    (b* (((flexprod prod) (car prods)))
      (cons `(,FTY::PROD.COND (,FTY::PROD.CTOR-NAME . ,(FTY::FLEXPROD-FIELDS-ACC-CALLS FTY::PROD.FIELDS FTY::XVAR)))
        (flexsum-fix-redef-prod-cases-nokind (cdr prods)
          xvar)))))
flextypelist-fixesfunction
(defun flextypelist-fixes
  (types)
  (if (atom types)
    nil
    (cons (with-flextype-bindings (x (car types))
        x.fix)
      (flextypelist-fixes (cdr types)))))
flexsum-acc/ctor-eventsfunction
(defun flexsum-acc/ctor-events
  (sum types)
  (declare (ignorable types))
  (b* (((flexsum sum) sum) (foo-fix-redef (intern-in-package-of-symbol (cat (symbol-name sum.fix) "-REDEF")
          sum.fix)))
    (append (flexsum-prods-accessor/constructors sum.prods
        sum)
      `((defthmd ,FTY::FOO-FIX-REDEF
         (equal (,FTY::SUM.FIX ,FTY::SUM.XVAR)
           ,(IF FTY::SUM.KIND
     `(CASE (,FTY::SUM.KIND ,FTY::SUM.XVAR)
        . ,(FTY::FLEXSUM-FIX-REDEF-PROD-CASES FTY::SUM.PRODS FTY::SUM.XVAR))
     (FTY::NICE-COND
      (FTY::FLEXSUM-FIX-REDEF-PROD-CASES-NOKIND FTY::SUM.PRODS FTY::SUM.XVAR))))
         :hints (("Goal" :in-theory (e/d ,(AND FTY::SUM.KIND
      (LIST
       (FTY::INTERN-IN-PACKAGE-OF-SYMBOL
        (FTY::CAT (SYMBOL-NAME FTY::SUM.KIND) "-POSSIBILITIES") FTY::SUM.KIND)))
              ,(FTY::FLEXSUM-FNS FTY::SUM))) (and stable-under-simplificationp
             '(:expand (,FTY::SUM.FIX ,FTY::SUM.XVAR))))
         :rule-classes :definition)))))
flextypes-sum-accessor/constructorsfunction
(defun flextypes-sum-accessor/constructors
  (types alltypes)
  (if (atom types)
    nil
    (append (and (eq (tag (car types)) :sum)
        (flexsum-acc/ctor-events (car types)
          alltypes))
      (flextypes-sum-accessor/constructors (cdr types)
        alltypes))))
flexprod-field-countfunction
(defun flexprod-field-count
  (x xvar types)
  (b* (((flexprod-field x) x) ((unless x.type) nil)
      (type-count (flextypes-find-count-for-pred x.type types))
      ((unless type-count) nil))
    `((,FTY::TYPE-COUNT (,FTY::X.ACC-NAME ,FTY::XVAR)))))
flexprod-field-countsfunction
(defun flexprod-field-counts
  (fields xvar types)
  (if (atom fields)
    nil
    (append (flexprod-field-count (car fields)
        xvar
        types)
      (flexprod-field-counts (cdr fields)
        xvar
        types))))
flexsum-prod-countsfunction
(defun flexsum-prod-counts
  (prods xvar types)
  (b* (((when (atom prods)) nil) ((flexprod x) (car prods))
      (fieldcounts (flexprod-field-counts x.fields
          xvar
          types))
      (count (if fieldcounts
          `(+ ,(+ 1 (FTY::LEN FTY::X.FIELDS)) . ,FTY::FIELDCOUNTS)
          1))
      (count (if x.count-incr
          `(+ ,(IF (FTY::NATP FTY::X.COUNT-INCR)
     FTY::X.COUNT-INCR
     1)
            ,COUNT)
          count)))
    (cons `(,FTY::X.KIND ,COUNT)
      (flexsum-prod-counts (cdr prods)
        xvar
        types))))
flexsum-prod-counts-nokindfunction
(defun flexsum-prod-counts-nokind
  (prods xvar types)
  (b* (((when (atom prods)) nil) ((flexprod x) (car prods))
      (fieldcounts (flexprod-field-counts x.fields
          xvar
          types))
      (prodcount (if fieldcounts
          `(+ ,(+ 1 (FTY::LEN FTY::X.FIELDS)) . ,FTY::FIELDCOUNTS)
          1))
      (prodcount (if x.count-incr
          `(+ ,(IF (FTY::NATP FTY::X.COUNT-INCR)
     FTY::X.COUNT-INCR
     1)
            ,FTY::PRODCOUNT)
          prodcount)))
    (cons `(,FTY::X.COND ,FTY::PRODCOUNT)
      (flexsum-prod-counts-nokind (cdr prods)
        xvar
        types))))
flexsum-countfunction
(defun flexsum-count
  (x types)
  (b* (((flexsum x) x) ((unless x.count) nil)
      (short (cat "Measure for recurring over @(see "
          (full-escape-symbol x.name)
          ") structures.")))
    `((define ,FTY::X.COUNT
       ((,FTY::X.XVAR ,FTY::X.PRED))
       :parents (,FTY::X.NAME)
       :short ,FTY::SHORT
       :verify-guards nil
       :returns (count natp
         :rule-classes :type-prescription :hints ('(:expand (,FTY::X.COUNT ,FTY::X.XVAR)
            :in-theory (e/d ,(AND FTY::X.KIND
      (LIST
       (FTY::INTERN-IN-PACKAGE-OF-SYMBOL
        (FTY::CAT (SYMBOL-NAME FTY::X.KIND) "-POSSIBILITIES") FTY::X.KIND)))
              (,FTY::X.COUNT . ,(FTY::FLEXSUM-PROD-FNS FTY::X.PRODS))))))
       :measure (let ((,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
         ,FTY::X.MEASURE)
       ,@(AND (FTY::GETARG :MEASURE-DEBUG NIL FTY::X.KWD-ALIST) `(:MEASURE-DEBUG T))
       :progn t
       ,(IF FTY::X.KIND
     `(CASE (,FTY::X.KIND ,FTY::X.XVAR)
        . ,(FTY::FLEXSUM-PROD-COUNTS FTY::X.PRODS FTY::X.XVAR FTY::TYPES))
     (FTY::NICE-COND
      (FTY::FLEXSUM-PROD-COUNTS-NOKIND FTY::X.PRODS FTY::X.XVAR FTY::TYPES)))))))
flexprod-field-count-thmfunction
(defun flexprod-field-count-thm
  (x prod sum types)
  (b* (((flexprod-field x) x) ((unless x.type) nil)
      (type-count (flextypes-find-count-for-pred x.type types))
      ((unless type-count) nil)
      ((flexprod prod) prod)
      ((flexsum sum) sum)
      (bar-count-of-foo->bar (intern-in-package-of-symbol (cat (symbol-name type-count)
            "-OF-"
            (symbol-name x.acc-name))
          x.acc-name)))
    `((defthm ,FTY::BAR-COUNT-OF-FOO->BAR
       ,(FTY::NICE-IMPLIES FTY::PROD.GUARD
  `(< (,FTY::TYPE-COUNT (,FTY::X.ACC-NAME ,FTY::SUM.XVAR))
      (,FTY::SUM.COUNT ,FTY::SUM.XVAR)))
       :hints (("goal" :in-theory (disable ,FTY::TYPE-COUNT
            ,FTY::X.ACC-NAME
            ,FTY::SUM.COUNT . ,(AND FTY::SUM.KIND `(,FTY::SUM.KIND)))
          :expand ((,FTY::SUM.COUNT ,FTY::SUM.XVAR))))
       :rule-classes :linear))))
flexprod-field-count-thmsfunction
(defun flexprod-field-count-thms
  (fields prod sum types)
  (if (atom fields)
    nil
    (append (flexprod-field-count-thm (car fields)
        prod
        sum
        types)
      (flexprod-field-count-thms (cdr fields)
        prod
        sum
        types))))
flexprod-field-count-varfunction
(defun flexprod-field-count-var
  (x types)
  (b* (((flexprod-field x) x) ((unless x.type) nil)
      (type-count (flextypes-find-count-for-pred x.type types))
      ((unless type-count) nil))
    `((,FTY::TYPE-COUNT ,FTY::X.NAME))))
flexprod-field-counts-varsfunction
(defun flexprod-field-counts-vars
  (fields types)
  (if (atom fields)
    nil
    (append (flexprod-field-count-var (car fields) types)
      (flexprod-field-counts-vars (cdr fields)
        types))))
flexprod-ctor-count-thmfunction
(defun flexprod-ctor-count-thm
  (prod sum types)
  (b* (((flexprod x) prod) ((flexsum sum) sum)
      (call (flexprod-ctor-call prod))
      (field-counts (flexprod-field-counts-vars x.fields types))
      ((when (not field-counts)) nil)
      (body `(< (+ . ,FTY::FIELD-COUNTS) (,FTY::SUM.COUNT ,FTY::CALL)))
      (foo-count-of-foo (intern-in-package-of-symbol (cat (symbol-name sum.count)
            "-OF-"
            (symbol-name x.ctor-name))
          sum.count)))
    `((defthm ,FTY::FOO-COUNT-OF-FOO
       ,(IF FTY::X.REQUIRE
     `(FTY::IMPLIES ,FTY::X.REQUIRE ,FTY::BODY)
     FTY::BODY)
       :hints (("goal" :expand ((,FTY::SUM.COUNT ,FTY::CALL))))
       :rule-classes :linear))))
flexsum-prod-count-thmsfunction
(defun flexsum-prod-count-thms
  (prods sum types)
  (if (atom prods)
    nil
    (append (flexprod-ctor-count-thm (car prods)
        sum
        types)
      (flexprod-field-count-thms (flexprod->fields (car prods))
        (car prods)
        sum
        types)
      (flexsum-prod-count-thms (cdr prods)
        sum
        types))))
flexsum-count-post-eventsfunction
(defun flexsum-count-post-events
  (x alltypes)
  (b* (((flexsum x) x) ((unless x.count) nil))
    (flexsum-prod-count-thms x.prods
      x
      alltypes)))
flexprod-fields-collect-fix/pred-pairsfunction
(defun flexprod-fields-collect-fix/pred-pairs
  (fields)
  (if (atom fields)
    nil
    (b* (((flexprod-field x) (car fields)))
      (if (and x.fix x.type)
        (cons (cons x.fix x.type)
          (flexprod-fields-collect-fix/pred-pairs (cdr fields)))
        (flexprod-fields-collect-fix/pred-pairs (cdr fields))))))
flexprods-collect-fix/pred-pairsfunction
(defun flexprods-collect-fix/pred-pairs
  (prods)
  (if (atom prods)
    nil
    (append (flexprod-fields-collect-fix/pred-pairs (flexprod->fields (car prods)))
      (flexprods-collect-fix/pred-pairs (cdr prods)))))
flexsum-collect-fix/pred-pairsfunction
(defun flexsum-collect-fix/pred-pairs
  (sum)
  (flexprods-collect-fix/pred-pairs (flexsum->prods sum)))