Filtering...

da-base

books/std/util/da-base
other
(in-package "STD")
other
(include-book "support")
other
(include-book "tools/rulesets" :dir :system)
other
(include-book "cons")
other
(defsection tag
  :parents (defaggregate)
  :short "Get the tag from a tagged object."
  :long "<p>The @('tag') function is simply an alias for @('car') that is
especially meant to be used for accessing the <i>tag</i> of a <i>tagged
object</i>.</p>

<p>When new types are introduced by macros such as @(see defaggregate), @(see
fty::defprod), @(see fty::deftagsum), etc., they may be tagged.  When a type is
tagged, its objects have the form @('(tag . data)'), where the @('tag') says
what kind of object is being represented (e.g., ``employee'', ``student'',
etc.) and @('data') contains the actual information for this kind of
structure (e.g., name, age, ...).  Tagging objects has some runtime/memory
cost (an extra cons for each object), but makes it easy to tell different kinds
of objects apart by inspecting their tags.</p>

<p>We could (of course) just get the tag with @(see car), but @('car') is a
widely used function and we do not want to slow down reasoning about it.
Instead, we introduce @('tag') as an alias for @('car') and keep it disabled so
that reasoning about the tags of objects does not slow down reasoning about
@('car') in general.</p>

<p>Even so, tag reasoning can occasionally get expensive.  Macros like
@('defaggregate'), @(see fty::defprod), etc., generally add their tag-related
rules to the @('tag-reasoning') ruleset; see @(see acl2::rulesets).  You may
generally want to keep this ruleset disabled, and only enable it when you
really want to use tags to distinguish between objects.</p>

<p>Note: if you are using the @(see fty::fty) framework, it is generally best
to avoid using @('tag') to distinguish between members of the same sum of
products type.  Instead, consider using the custom @('-kind') macros that are
introduced by macros such as @(see fty::deftagsum) and @(see
fty::deftranssum).</p>"
  (defund-inline tag
    (x)
    (declare (xargs :guard t))
    (mbe :logic (car x)
      :exec (if (consp x)
        (car x)
        nil)))
  (defthm tag-forward-to-consp
    (implies (tag x) (consp x))
    :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable tag))))
  (def-ruleset! tag-reasoning nil))
other
(deftheory defaggregate-basic-theory
  (union-theories '(tag car-cons
      cdr-cons
      alistp
      assoc-equal
      hons
      booleanp
      booleanp-compound-recognizer
      prod-car
      prod-cdr
      prod-hons
      prod-cons-with-hint
      cons-with-hint
      booleanp-of-prod-consp
      prod-consp-compound-recognizer
      prod-consp-of-prod-cons
      car-of-prod-cons
      cdr-of-prod-cons
      prod-cons-of-car/cdr
      prod-cons-when-either)
    (theory 'minimal-theory)))
other
(program)
da-xfunction
(defun da-x
  (basename)
  (intern-in-package-of-symbol "X" basename))
da-constructor-namefunction
(defun da-constructor-name
  (basename)
  basename)
da-honsed-constructor-namefunction
(defun da-honsed-constructor-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string "HONSED-" (symbol-name basename))
    basename))
da-accessor-namefunction
(defun da-accessor-name
  (basename field)
  (intern-in-package-of-symbol (concatenate 'string
      (symbol-name basename)
      "->"
      (symbol-name field))
    basename))
da-accessor-namesfunction
(defun da-accessor-names
  (basename fields)
  (if (consp fields)
    (cons (da-accessor-name basename (car fields))
      (da-accessor-names basename (cdr fields)))
    nil))
da-recognizer-namefunction
(defun da-recognizer-name
  (basename pred)
  (or pred
    (intern-in-package-of-symbol (concatenate 'string (symbol-name basename) "-P")
      basename)))
da-changer-namefunction
(defun da-changer-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string "CHANGE-" (symbol-name basename))
    basename))
da-changer-fn-namefunction
(defun da-changer-fn-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string
      "CHANGE-"
      (symbol-name basename)
      "-FN")
    basename))
da-remake-namefunction
(defun da-remake-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string "REMAKE-" (symbol-name basename))
    basename))
da-maker-namefunction
(defun da-maker-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string "MAKE-" (symbol-name basename))
    basename))
da-honsed-maker-namefunction
(defun da-honsed-maker-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string
      "MAKE-HONSED-"
      (symbol-name basename))
    basename))
da-bodyfunction
(defun da-body
  (basename tag)
  (if tag
    `(cdr ,(STD::DA-X STD::BASENAME))
    (da-x basename)))
da-illegible-split-fieldsfunction
(defun da-illegible-split-fields
  (fields)
  (let ((length (len fields)))
    (cond ((equal length 1) (first fields))
      ((equal length 2) (cons (first fields) (second fields)))
      (t (let* ((halfway (floor length 2)) (firsthalf (take halfway fields))
            (lasthalf (nthcdr halfway fields)))
          (cons (da-illegible-split-fields firsthalf)
            (da-illegible-split-fields lasthalf)))))))
da-illegible-fields-map-auxfunction
(defun da-illegible-fields-map-aux
  (split-fields path car cdr)
  (if (consp split-fields)
    (append (da-illegible-fields-map-aux (car split-fields)
        `(,CAR ,STD::PATH)
        car
        cdr)
      (da-illegible-fields-map-aux (cdr split-fields)
        `(,CDR ,STD::PATH)
        car
        cdr))
    (list (cons split-fields path))))
da-illegible-fields-mapfunction
(defun da-illegible-fields-map
  (basename tag fields car cdr)
  (da-illegible-fields-map-aux (da-illegible-split-fields fields)
    (da-body basename tag)
    car
    cdr))
da-illegible-structure-checks-auxfunction
(defun da-illegible-structure-checks-aux
  (split-fields path consp car cdr)
  (if (consp split-fields)
    (cons `(,CONSP ,STD::PATH)
      (append (da-illegible-structure-checks-aux (car split-fields)
          `(,CAR ,STD::PATH)
          consp
          car
          cdr)
        (da-illegible-structure-checks-aux (cdr split-fields)
          `(,CDR ,STD::PATH)
          consp
          car
          cdr)))
    nil))
da-illegible-structure-checksfunction
(defun da-illegible-structure-checks
  (basename tag fields consp car cdr)
  (da-illegible-structure-checks-aux (da-illegible-split-fields fields)
    (da-body basename tag)
    consp
    car
    cdr))
da-illegible-pack-auxfunction
(defun da-illegible-pack-aux
  (cons split-fields)
  (if (consp split-fields)
    `(,CONS ,(STD::DA-ILLEGIBLE-PACK-AUX CONS (CAR STD::SPLIT-FIELDS))
      ,(STD::DA-ILLEGIBLE-PACK-AUX CONS (CDR STD::SPLIT-FIELDS)))
    split-fields))
da-illegible-pack-fieldsfunction
(defun da-illegible-pack-fields
  (layout honsp tag fields)
  (b* ((cons (cond ((eq layout :fulltree) (if honsp
             'hons
             'cons))
         ((eq layout :tree) (if honsp
             'prod-hons
             'prod-cons))
         (t (er hard?
             'da-illegible-pack-fields
             "Bad layout ~x0"
             layout)))) (body (da-illegible-pack-aux cons
          (da-illegible-split-fields fields))))
    (if tag
      `(,(IF STD::HONSP
     'STD::HONS
     'CONS) ,STD::TAG
        ,STD::BODY)
      body)))
da-illegible-remake-auxfunction
(defun da-illegible-remake-aux
  (split-fields path cons-with-hint car cdr)
  (if (consp split-fields)
    `(,STD::CONS-WITH-HINT ,(STD::DA-ILLEGIBLE-REMAKE-AUX (CAR STD::SPLIT-FIELDS) `(,CAR ,STD::PATH)
  STD::CONS-WITH-HINT CAR CDR)
      ,(STD::DA-ILLEGIBLE-REMAKE-AUX (CDR STD::SPLIT-FIELDS) `(,CDR ,STD::PATH)
  STD::CONS-WITH-HINT CAR CDR)
      ,STD::PATH)
    split-fields))
da-illegible-remake-fieldsfunction
(defun da-illegible-remake-fields
  (basename layout tag fields)
  (b* (((mv cons-with-hint car cdr) (cond ((eq layout :fulltree) (mv 'cons-with-hint 'car 'cdr))
         ((eq layout :tree) (mv 'prod-cons-with-hint
             'prod-car
             'prod-cdr))
         (t (mv (er hard?
               'da-illegible-remake-fields
               "Bad layout ~x0"
               layout)
             nil
             nil)))) (x (da-x basename))
      (body (da-body basename tag))
      (split-fields (da-illegible-split-fields fields))
      (new-body (da-illegible-remake-aux split-fields
          body
          cons-with-hint
          car
          cdr)))
    (if tag
      `(cons-with-hint ,STD::TAG ,STD::NEW-BODY ,STD::X)
      new-body)))
da-legible-fields-mapfunction
(defun da-legible-fields-map
  (basename tag fields)
  (if (consp fields)
    (cons (cons (car fields)
        `(cdr (assoc ',(CAR STD::FIELDS)
            ,(STD::DA-BODY STD::BASENAME STD::TAG))))
      (da-legible-fields-map basename
        tag
        (cdr fields)))
    nil))
da-legible-pack-fields-auxfunction
(defun da-legible-pack-fields-aux
  (honsp fields)
  (if (consp fields)
    `(,(IF STD::HONSP
     'STD::HONS
     'CONS) (,(IF STD::HONSP
     'STD::HONS
     'CONS) ',(CAR STD::FIELDS)
        ,(CAR STD::FIELDS))
      ,(STD::DA-LEGIBLE-PACK-FIELDS-AUX STD::HONSP (CDR STD::FIELDS)))
    nil))
da-legible-pack-fieldsfunction
(defun da-legible-pack-fields
  (honsp tag fields)
  (let ((body (da-legible-pack-fields-aux honsp fields)))
    (if tag
      `(,(IF STD::HONSP
     'STD::HONS
     'CONS) ,STD::TAG
        ,STD::BODY)
      body)))
da-nthcdr-fnfunction
(defun da-nthcdr-fn
  (n x)
  (if (zp n)
    x
    `(cdr ,(STD::DA-NTHCDR-FN (- STD::N 1) STD::X))))
da-nthmacro
(defmacro da-nth
  (n x)
  `(car ,(STD::DA-NTHCDR-FN STD::N STD::X)))
da-ordered-fields-mapfunction
(defun da-ordered-fields-map
  (n basename tag fields)
  (if (consp fields)
    (cons (cons (car fields)
        `(cdr (da-nth ,STD::N ,(STD::DA-BODY STD::BASENAME STD::TAG))))
      (da-ordered-fields-map (+ 1 n)
        basename
        tag
        (cdr fields)))
    nil))
da-ordered-pack-fields-auxfunction
(defun da-ordered-pack-fields-aux
  (honsp fields)
  (if (consp fields)
    `(,(IF STD::HONSP
     'STD::HONS
     'CONS) (,(IF STD::HONSP
     'STD::HONS
     'CONS) ',(CAR STD::FIELDS)
        ,(CAR STD::FIELDS))
      ,(STD::DA-ORDERED-PACK-FIELDS-AUX STD::HONSP (CDR STD::FIELDS)))
    nil))
da-ordered-pack-fieldsfunction
(defun da-ordered-pack-fields
  (honsp tag fields)
  (let ((body (da-ordered-pack-fields-aux honsp fields)))
    (if tag
      `(,(IF STD::HONSP
     'STD::HONS
     'CONS) ,STD::TAG
        ,STD::BODY)
      body)))
da-ordered-structure-checks-auxfunction
(defun da-ordered-structure-checks-aux
  (fields path)
  (if (consp fields)
    (list* `(consp ,STD::PATH)
      `(consp (car ,STD::PATH))
      `(eq (caar ,STD::PATH) ',(CAR STD::FIELDS))
      (da-ordered-structure-checks-aux (cdr fields)
        `(cdr ,STD::PATH)))
    (list `(not ,STD::PATH))))
da-ordered-structure-checksfunction
(defun da-ordered-structure-checks
  (basename tag fields)
  (da-ordered-structure-checks-aux fields
    (da-body basename tag)))
da-fields-mapfunction
(defun da-fields-map
  (basename tag layout fields)
  (case layout
    (:alist (da-legible-fields-map basename
        tag
        fields))
    (:list (da-ordered-fields-map 0
        basename
        tag
        fields))
    (:tree (da-illegible-fields-map basename
        tag
        fields
        'prod-car
        'prod-cdr))
    (:fulltree (da-illegible-fields-map basename
        tag
        fields
        'car
        'cdr))
    (otherwise (er hard?
        'da-fields-map
        "Bad layout ~x0"
        layout))))
da-pack-fieldsfunction
(defun da-pack-fields
  (honsp layout tag fields)
  (case layout
    (:alist (da-legible-pack-fields honsp
        tag
        fields))
    (:list (da-ordered-pack-fields honsp
        tag
        fields))
    ((:tree :fulltree) (da-illegible-pack-fields layout
        honsp
        tag
        fields))
    (otherwise (er hard?
        'da-pack-fields
        "Bad layout ~x0"
        layout))))
da-structure-checksfunction
(defun da-structure-checks
  (basename tag layout fields)
  (case layout
    (:alist `((alistp ,(STD::DA-BODY STD::BASENAME STD::TAG)) (consp ,(STD::DA-BODY STD::BASENAME STD::TAG))))
    (:list (da-ordered-structure-checks basename
        tag
        fields))
    (:tree (da-illegible-structure-checks basename
        tag
        fields
        'prod-consp
        'prod-car
        'prod-cdr))
    (:fulltree (da-illegible-structure-checks basename
        tag
        fields
        'consp
        'car
        'cdr))
    (otherwise (er hard?
        'da-structure-checks
        "Bad layout ~x0"
        layout))))
da-fields-map-let-bindingsfunction
(defun da-fields-map-let-bindings
  (map)
  (if (consp map)
    (let* ((entry (car map)) (field (car entry))
        (path (cdr entry)))
      (cons (list field path)
        (da-fields-map-let-bindings (cdr map))))
    nil))
da-make-constructor-rawfunction
(defun da-make-constructor-raw
  (basename tag
    fields
    guard
    honsp
    layout)
  (let ((foo (da-constructor-name basename)))
    `(defund ,STD::FOO
      ,STD::FIELDS
      (declare (xargs :guard ,STD::GUARD
          :guard-hints (("Goal" :in-theory (theory 'minimal-theory)) (and stable-under-simplificationp
              '(:in-theory (enable))))))
      ,(STD::DA-PACK-FIELDS STD::HONSP STD::LAYOUT STD::TAG STD::FIELDS))))
da-make-honsed-constructor-rawfunction
(defun da-make-honsed-constructor-raw
  (basename tag fields guard layout)
  (let ((foo (da-constructor-name basename)) (honsed-foo (da-honsed-constructor-name basename)))
    `(defun ,STD::HONSED-FOO
      ,STD::FIELDS
      (declare (xargs :guard ,STD::GUARD
          :guard-hints (("Goal" :in-theory (union-theories '(,STD::FOO hons)
               (theory 'minimal-theory))) (and stable-under-simplificationp
              '(:in-theory (enable))))))
      (mbe :logic (,STD::FOO . ,STD::FIELDS)
        :exec ,(STD::DA-PACK-FIELDS T STD::LAYOUT STD::TAG STD::FIELDS)))))
da-make-recognizer-rawfunction
(defun da-make-recognizer-raw
  (basename tag
    fields
    guard
    layout
    pred)
  (let* ((foo-p (da-recognizer-name basename pred)) (x (da-x basename))
      (fields-map (da-fields-map basename
          tag
          layout
          fields))
      (let-binds (da-fields-map-let-bindings fields-map)))
    `(defund ,STD::FOO-P
      (,STD::X)
      (declare (xargs :guard t
          :guard-hints (("Goal" :in-theory (union-theories '((:executable-counterpart eqlablep) consp-assoc-equal
                 assoc-eql-exec-is-assoc-equal)
               (theory 'defaggregate-basic-theory))) (and stable-under-simplificationp
              '(:in-theory (enable))))))
      (and ,@(IF STD::TAG
      `((CONSP ,STD::X) (EQ (CAR ,STD::X) ,STD::TAG))
      NIL)
        ,@(STD::DA-STRUCTURE-CHECKS STD::BASENAME STD::TAG STD::LAYOUT STD::FIELDS)
        (let ,STD::LET-BINDS
          (declare (ignorable ,@STD::FIELDS))
          ,STD::GUARD)))))
da-make-accessorfunction
(defun da-make-accessor
  (basename field map pred)
  (let ((foo-p (da-recognizer-name basename pred)) (foo->bar (da-accessor-name basename field))
      (x (da-x basename))
      (body (cdr (assoc field map))))
    `(defund-inline ,STD::FOO->BAR
      (,STD::X)
      (declare (xargs :guard (,STD::FOO-P ,STD::X)
          :guard-hints (("Goal" :expand (,STD::FOO-P ,STD::X)
             :in-theory (union-theories '(,STD::FOO-P (:executable-counterpart eqlablep)
                 consp-assoc-equal
                 assoc-eql-exec-is-assoc-equal)
               (theory 'defaggregate-basic-theory))))))
      ,STD::BODY)))
da-make-accessors-auxfunction
(defun da-make-accessors-aux
  (basename fields map pred)
  (if (consp fields)
    (cons (da-make-accessor basename
        (car fields)
        map
        pred)
      (da-make-accessors-aux basename
        (cdr fields)
        map
        pred))
    nil))
da-make-accessorsfunction
(defun da-make-accessors
  (basename tag fields layout pred)
  (da-make-accessors-aux basename
    fields
    (da-fields-map basename
      tag
      layout
      fields)
    pred))
da-make-accessor-of-constructorfunction
(defun da-make-accessor-of-constructor
  (basename field all-fields)
  (let ((foo->bar (da-accessor-name basename field)) (foo (da-constructor-name basename)))
    `(defthm ,(STD::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME STD::FOO->BAR) "-OF-"
               (SYMBOL-NAME STD::FOO))
  STD::BASENAME)
      (equal (,STD::FOO->BAR (,STD::FOO . ,STD::ALL-FIELDS))
        ,STD::FIELD)
      :hints (("Goal" :in-theory (union-theories '(,STD::FOO->BAR ,STD::FOO)
           (theory 'defaggregate-basic-theory)))))))
da-make-accessors-of-constructor-auxfunction
(defun da-make-accessors-of-constructor-aux
  (basename fields all-fields)
  (if (consp fields)
    (cons (da-make-accessor-of-constructor basename
        (car fields)
        all-fields)
      (da-make-accessors-of-constructor-aux basename
        (cdr fields)
        all-fields))
    nil))
da-make-accessors-of-constructorfunction
(defun da-make-accessors-of-constructor
  (basename fields)
  (da-make-accessors-of-constructor-aux basename
    fields
    fields))
da-layout-supports-remake-pfunction
(defun da-layout-supports-remake-p
  (honsp layout)
  (and (member layout '(:tree :fulltree))
    (not honsp)))
da-maybe-remake-namefunction
(defun da-maybe-remake-name
  (basename honsp layout)
  (and (da-layout-supports-remake-p honsp layout)
    (da-remake-name basename)))
da-make-remaker-rawfunction
(defun da-make-remaker-raw
  (basename tag
    fields
    guard
    honsp
    layout
    pred)
  (b* (((unless (da-layout-supports-remake-p honsp layout)) nil) (x (da-x basename))
      (foo (da-constructor-name basename))
      (foo-p (da-recognizer-name basename pred))
      (remake-foo (da-remake-name basename)))
    `((defun ,STD::REMAKE-FOO
       (,STD::X . ,STD::FIELDS)
       (declare (xargs :guard (and (,STD::FOO-P ,STD::X) ,STD::GUARD)
           :guard-hints (("Goal" :expand ((,STD::FOO-P ,STD::X) (,STD::FOO . ,STD::FIELDS))
              :in-theory (union-theories '(,STD::FOO ,STD::FOO-P)
                (theory 'defaggregate-basic-theory))))))
       (mbe :logic (,STD::FOO . ,STD::FIELDS)
         :exec ,(STD::DA-ILLEGIBLE-REMAKE-FIELDS STD::BASENAME STD::LAYOUT STD::TAG
  STD::FIELDS))))))
da-make-valid-fields-for-changerfunction
(defun da-make-valid-fields-for-changer
  (fields)
  (if (consp fields)
    (cons (intern-in-package-of-symbol (symbol-name (car fields))
        :keyword)
      (da-make-valid-fields-for-changer (cdr fields)))
    nil))
da-changer-args-to-alistfunction
(defun da-changer-args-to-alist
  (macroname args kwd-fields)
  (b* (((when (null args)) nil) ((when (atom args)) (er hard?
          macroname
          "Expected a true-list, but instead it ends with ~x0."
          args))
      ((when (atom (cdr args))) (er hard?
          macroname
          "Expected :field val pairs, but found ~x0."
          args))
      (field (first args))
      (value (second args))
      ((unless (member-equal field kwd-fields)) (er hard?
          macroname
          "~x0 is not among the allowed fields, ~&1."
          field
          kwd-fields))
      (rest (da-changer-args-to-alist macroname
          (cddr args)
          kwd-fields))
      ((when (assoc field rest)) (er hard?
          macroname
          "Multiple occurrences of ~x0 in change/make macro."
          field)))
    (cons (cons field value) rest)))
da-changer-let-bindings-and-argsfunction
(defun da-changer-let-bindings-and-args
  (change-name acc-map alist)
  "Returns (mv let-bindings constructor-args)"
  (b* (((when (atom acc-map)) (mv nil nil)) ((mv rest-bindings rest-args) (da-changer-let-bindings-and-args change-name
          (cdr acc-map)
          alist))
      ((cons field1 accessor1) (car acc-map))
      (look1 (assoc field1 alist))
      ((when look1) (mv (cons (list accessor1 (cdr look1))
            rest-bindings)
          (cons accessor1 rest-args))))
    (mv rest-bindings
      (cons `(,STD::ACCESSOR1 ,STD::CHANGE-NAME) rest-args))))
change-aggregatefunction
(defun change-aggregate
  (basename obj
    args
    acc-map
    macroname
    remake-name)
  (b* ((kwd-fields (strip-cars acc-map)) (alist (da-changer-args-to-alist macroname
          args
          kwd-fields))
      (all-setp (subsetp kwd-fields (strip-cars alist)))
      (remake-name (and (not all-setp) remake-name))
      ((mv arg-bindings ctor-args) (da-changer-let-bindings-and-args macroname
          acc-map
          alist))
      (ctor-name (da-constructor-name basename)))
    (if (not remake-name)
      (if all-setp
        `(let ,STD::ARG-BINDINGS
          (,STD::CTOR-NAME . ,STD::CTOR-ARGS))
        `(let ((,STD::MACRONAME ,STD::OBJ) . ,STD::ARG-BINDINGS)
          (,STD::CTOR-NAME . ,STD::CTOR-ARGS)))
      `(let ((,STD::MACRONAME ,STD::OBJ) . ,STD::ARG-BINDINGS)
        (mbe :logic (,STD::CTOR-NAME . ,STD::CTOR-ARGS)
          :exec (,STD::REMAKE-NAME ,STD::MACRONAME . ,STD::CTOR-ARGS))))))
da-make-changerfunction
(defun da-make-changer
  (basename fields remake-name)
  (b* ((x (da-x basename)) (change-foo (da-changer-name basename))
      (acc-names (da-accessor-names basename fields))
      (kwd-fields (da-make-valid-fields-for-changer fields))
      (acc-map (pairlis$ kwd-fields acc-names)))
    `(defmacro ,STD::CHANGE-FOO
      (,STD::X &rest args)
      (change-aggregate ',STD::BASENAME
        ,STD::X
        args
        ',STD::ACC-MAP
        ',STD::CHANGE-FOO
        ',STD::REMAKE-NAME))))
da-maker-fill-in-fieldsfunction
(defun da-maker-fill-in-fields
  (dflt-map alist)
  (b* (((when (atom dflt-map)) nil) (rest (da-maker-fill-in-fields (cdr dflt-map)
          alist))
      ((cons field1 default1) (car dflt-map))
      (look1 (assoc field1 alist))
      ((when look1) (cons (cdr look1) rest)))
    (cons default1 rest)))
make-aggregatefunction
(defun make-aggregate
  (basename args
    dflt-map
    macroname
    honsp)
  (b* ((ctor-name (if honsp
         (da-honsed-constructor-name basename)
         (da-constructor-name basename))) (kwd-fields (strip-cars dflt-map))
      (alist (da-changer-args-to-alist macroname
          args
          kwd-fields)))
    (cons ctor-name
      (da-maker-fill-in-fields dflt-map alist))))
da-make-makerfunction
(defun da-make-maker
  (basename fields defaults)
  (let* ((make-foo (da-maker-name basename)) (kwd-fields (da-make-valid-fields-for-changer fields))
      (dflt-map (pairlis$ kwd-fields defaults)))
    `(defmacro ,STD::MAKE-FOO
      (&rest args)
      (make-aggregate ',STD::BASENAME
        args
        ',STD::DFLT-MAP
        ',STD::MAKE-FOO
        nil))))
da-make-honsed-makerfunction
(defun da-make-honsed-maker
  (basename fields defaults)
  (let* ((make-foo (da-honsed-maker-name basename)) (kwd-fields (da-make-valid-fields-for-changer fields))
      (dflt-map (pairlis$ kwd-fields defaults)))
    `(defmacro ,STD::MAKE-FOO
      (&rest args)
      (make-aggregate ',STD::BASENAME
        args
        ',STD::DFLT-MAP
        ',STD::MAKE-FOO
        t))))
da-patbind-make-field-acc-alistfunction
(defun da-patbind-make-field-acc-alist
  (var fields-accs)
  (if (atom fields-accs)
    nil
    (acons (concatenate 'string
        (symbol-name var)
        "."
        (symbol-name (caar fields-accs)))
      (cdar fields-accs)
      (da-patbind-make-field-acc-alist var
        (cdr fields-accs)))))
da-patbind-find-used-varsfunction
(defun da-patbind-find-used-vars
  (form varstrs acc)
  (if (atom form)
    (if (and (symbolp form)
        (not (keywordp form))
        (member-equal (symbol-name form) varstrs)
        (not (member-eq form acc)))
      (cons form acc)
      acc)
    (da-patbind-find-used-vars (car form)
      varstrs
      (da-patbind-find-used-vars (cdr form)
        varstrs
        acc))))
da-patbind-alist-to-bindingsfunction
(defun da-patbind-alist-to-bindings
  (vars valist target extra-args)
  (if (atom vars)
    nil
    (let* ((accessor (cdr (assoc-equal (symbol-name (car vars)) valist))) (call (list* accessor target extra-args))
        (binding (list (car vars) call)))
      (cons binding
        (da-patbind-alist-to-bindings (cdr vars)
          valist
          target
          extra-args)))))
da-patbind-fnfunction
(defun da-patbind-fn
  (name fields-accs
    args
    forms
    rest-expr)
  (b* (((mv kwd-alist args) (extract-keywords `(da-patbind-fn ',STD::NAME)
         '(:quietp :extra-args)
         args
         nil)) (forms (if (and (not forms)
            (tuplep 1 args)
            (symbolp (car args)))
          args
          forms))
      (- (or (and (tuplep 1 args)
            (tuplep 1 forms)
            (symbolp (car args))
            (not (booleanp (car args))))
          (er hard?
            'da-patbind-fn
            "B* bindings for ~x0 aggregates must have the form ((~x0 ~
                   <name>) <expr>), where <name> is a symbol and <expr> is a ~
                   single term.  The attempted binding of~|~% ~p1~%~%is not ~
                   of this form.~%(Exception:  ((~x0 <name>)) is allowed as ~
                   an abbreviation for ((~x0 <name>) <name>).)"
            name
            (cons (cons name args) forms))))
      (var (car args))
      (full-vars-alist (da-patbind-make-field-acc-alist var
          fields-accs))
      (field-vars (strip-cars full-vars-alist))
      (used-vars (da-patbind-find-used-vars rest-expr
          field-vars
          nil))
      (- (or used-vars
          (cdr (assoc :quietp kwd-alist))
          (cw "Note: not introducing any ~x0 field bindings for ~x1, ~
                   since none of its fields appear to be used.~%"
            name
            var)))
      (bindings (da-patbind-alist-to-bindings used-vars
          full-vars-alist
          var
          (cdr (assoc :extra-args kwd-alist)))))
    (if (eq var (car forms))
      `(b* ,STD::BINDINGS ,STD::REST-EXPR)
      `(let ((,STD::VAR ,(CAR STD::FORMS)))
        (declare (ignorable ,STD::VAR))
        (b* ,STD::BINDINGS ,STD::REST-EXPR)))))
da-make-binder-genfunction
(defun da-make-binder-gen
  (name field-alist)
  `(defmacro ,(STD::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING "PATBIND-" (SYMBOL-NAME STD::NAME)) STD::NAME)
    (args forms rest-expr)
    (da-patbind-fn ',STD::NAME
      ',STD::FIELD-ALIST
      args
      forms
      rest-expr)))
da-make-binderfunction
(defun da-make-binder
  (name fields)
  (da-make-binder-gen name
    (pairlis$ fields
      (da-accessor-names name fields))))
def-primitive-aggregate-fnfunction
(defun def-primitive-aggregate-fn
  (basename fields tag)
  (let ((honsp nil) (layout :alist) (guard t))
    `(progn ,(STD::DA-MAKE-RECOGNIZER-RAW STD::BASENAME STD::TAG STD::FIELDS STD::GUARD
  STD::LAYOUT NIL)
      ,(STD::DA-MAKE-CONSTRUCTOR-RAW STD::BASENAME STD::TAG STD::FIELDS STD::GUARD
  STD::HONSP STD::LAYOUT)
      ,@(STD::DA-MAKE-ACCESSORS STD::BASENAME STD::TAG STD::FIELDS STD::LAYOUT NIL)
      ,@(STD::DA-MAKE-ACCESSORS-OF-CONSTRUCTOR STD::BASENAME STD::FIELDS)
      ,@(STD::DA-MAKE-REMAKER-RAW STD::BASENAME STD::TAG STD::FIELDS STD::GUARD
   STD::HONSP STD::LAYOUT NIL)
      ,(STD::DA-MAKE-BINDER STD::BASENAME STD::FIELDS)
      ,(STD::DA-MAKE-CHANGER STD::BASENAME STD::FIELDS
  (STD::DA-MAYBE-REMAKE-NAME STD::BASENAME STD::HONSP STD::LAYOUT))
      ,(STD::DA-MAKE-MAKER STD::BASENAME STD::FIELDS NIL))))
def-primitive-aggregatemacro
(defmacro def-primitive-aggregate
  (name fields &key tag)
  `(make-event (def-primitive-aggregate-fn ',STD::NAME
      ',STD::FIELDS
      ',STD::TAG)))