Filtering...

defsum

books/std/util/defsum
other
(in-package "STD")
other
(include-book "defaggregate")
other
(include-book "deflist")
other
(set-state-ok t)
other
(program)
other
(defxdoc defsum
  :parents (std/util)
  :short "(Beta) Introduce a tagged union data type, also commonly called a
variant or sum type."
  :long "<box><p>Note: Defsum is currently under development.  You are welcome
to use it, but please be advised that we may drastically change its interface
and implementation.</p></box>

<h3>Introduction</h3>

<p><b>Defsum</b> is a macro that automates introducing a recognizer,
pattern-binding macro, and certain supporting theorems for new <a
href='https://en.wikipedia.org/wiki/Tagged_union'>tagged union</a> data
types.</p>

<p>Defsum is currently restricted to unions of tagged aggregates, which must be
introduced ahead of time using @(see defaggregate), and does not currently
support mutual recursive data types.  (In the future we may work to lift these
restrictions).</p>")
other
(defconst *defsum-valid-keywords*
  '(:mode :parents :short :long))
ds-find-aggregatesfunction
(defun ds-find-aggregates
  (names agginfo-alist)
  (b* (((when (atom names)) nil) ((cons name rest) names)
      (look (assoc name agginfo-alist))
      ((unless look) (er hard?
          'ds-find-aggregates
          "Aggregate ~x0 not found; has it been defined with defaggregate?"
          name)))
    (cons (cdr look)
      (ds-find-aggregates rest agginfo-alist))))
ds-xfunction
(defun ds-x
  (basename)
  (intern-in-package-of-symbol "X" basename))
ds-recognizer-namefunction
(defun ds-recognizer-name
  (basename)
  (intern-in-package-of-symbol (concatenate 'string (symbol-name basename) "-P")
    basename))
ds-recognizer-logic-def-auxfunction
(defun ds-recognizer-logic-def-aux
  (agginfos xvar)
  (if (atom agginfos)
    nil
    (cons `(,(STD::DA-RECOGNIZER-NAME (STD::AGGINFO->NAME (CAR STD::AGGINFOS))
  (STD::AGGINFO->PRED (CAR STD::AGGINFOS))) ,STD::XVAR)
      (ds-recognizer-logic-def-aux (cdr agginfos)
        xvar))))
ds-recognizer-logic-deffunction
(defun ds-recognizer-logic-def
  (name agginfos)
  (cons 'or
    (ds-recognizer-logic-def-aux agginfos
      (ds-x name))))
ds-recognizer-exec-def-auxfunction
(defun ds-recognizer-exec-def-aux
  (agginfos xvar)
  (cond ((atom agginfos) nil)
    ((atom (cdr agginfos)) `((otherwise (,(STD::DA-RECOGNIZER-NAME (STD::AGGINFO->NAME (CAR STD::AGGINFOS))
  (STD::AGGINFO->PRED (CAR STD::AGGINFOS))) ,STD::XVAR))))
    (t (cons `(,(STD::AGGINFO->TAG (CAR STD::AGGINFOS)) (,(STD::DA-RECOGNIZER-NAME (STD::AGGINFO->NAME (CAR STD::AGGINFOS))
  (STD::AGGINFO->PRED (CAR STD::AGGINFOS))) ,STD::XVAR))
        (ds-recognizer-exec-def-aux (cdr agginfos)
          xvar)))))
ds-recognizer-exec-deffunction
(defun ds-recognizer-exec-def
  (name agginfos)
  (let ((xvar (ds-x name)))
    `(case (tag ,STD::XVAR) . ,(STD::DS-RECOGNIZER-EXEC-DEF-AUX STD::AGGINFOS STD::XVAR))))
ds-recognizer-deffunction
(defun ds-recognizer-def
  (name agginfos)
  (let ((xvar (ds-x name)))
    `(defund ,(STD::DS-RECOGNIZER-NAME STD::NAME)
      (,STD::XVAR)
      (declare (xargs :guard t))
      (mbe :logic ,(STD::DS-RECOGNIZER-LOGIC-DEF STD::NAME STD::AGGINFOS)
        :exec ,(STD::DS-RECOGNIZER-EXEC-DEF STD::NAME STD::AGGINFOS)))))
ds-member-implies-sum-thmfunction
(defun ds-member-implies-sum-thm
  (name agginfo)
  (b* ((xvar (ds-x name)) (sum-name (ds-recognizer-name name))
      ((agginfo agginfo) agginfo)
      (mem-name (da-recognizer-name agginfo.name
          agginfo.pred))
      (thm-name (intern-in-package-of-symbol (concatenate 'string
            (symbol-name sum-name)
            "-WHEN-"
            (symbol-name mem-name))
          name)))
    `(defthm ,STD::THM-NAME
      (implies (,STD::MEM-NAME ,STD::XVAR)
        (,STD::SUM-NAME ,STD::XVAR)))))
ds-member-implies-sum-thmsfunction
(defun ds-member-implies-sum-thms
  (name agginfos)
  (if (atom agginfos)
    nil
    (cons (ds-member-implies-sum-thm name
        (car agginfos))
      (ds-member-implies-sum-thms name
        (cdr agginfos)))))
ds-by-tag-thmfunction
(defun ds-by-tag-thm
  (name agginfo)
  (b* ((xvar (ds-x name)) (sum-name (ds-recognizer-name name))
      ((agginfo agginfo) agginfo)
      (mem-name (da-recognizer-name agginfo.name
          agginfo.pred))
      (thm-name (intern-in-package-of-symbol (concatenate 'string
            (symbol-name mem-name)
            "-BY-TAG-WHEN-"
            (symbol-name sum-name))
          name)))
    `(defthm ,STD::THM-NAME
      (implies (and (equal (tag ,STD::XVAR) ,STD::AGGINFO.TAG)
          (,STD::SUM-NAME ,STD::XVAR))
        (,STD::MEM-NAME ,STD::XVAR)))))
ds-by-tag-thmsfunction
(defun ds-by-tag-thms
  (name agginfos)
  (if (atom agginfos)
    nil
    (cons (ds-by-tag-thm name (car agginfos))
      (ds-by-tag-thms name (cdr agginfos)))))
ds-when-invalid-tag-hypsfunction
(defun ds-when-invalid-tag-hyps
  (name agginfos)
  (b* (((when (atom agginfos)) nil) (xvar (ds-x name))
      ((agginfo agginfo) (car agginfos)))
    (cons `(not (equal (tag ,STD::XVAR) ,STD::AGGINFO.TAG))
      (ds-when-invalid-tag-hyps name
        (cdr agginfos)))))
ds-when-invalid-tag-thmfunction
(defun ds-when-invalid-tag-thm
  (name agginfos)
  (b* ((xvar (ds-x name)) (sum-name (ds-recognizer-name name))
      (thm-name (intern-in-package-of-symbol (concatenate 'string
            (symbol-name sum-name)
            "-WHEN-INVALID-TAG")
          name)))
    `(defthm ,STD::THM-NAME
      (implies (and . ,(STD::DS-WHEN-INVALID-TAG-HYPS STD::NAME STD::AGGINFOS))
        (not (,STD::SUM-NAME ,STD::XVAR)))
      :rule-classes ((:rewrite :backchain-limit-lst 0)))))
defsum-fnfunction
(defun defsum-fn
  (name other-args
    kwd-alist
    other-events
    state)
  (b* ((__function__ 'deflist) (?mksym-package-symbol name)
      (short (getarg :short nil kwd-alist))
      (long (getarg :long nil kwd-alist))
      (mode (getarg :mode (default-defun-mode (w state))
          kwd-alist))
      (parents-p (assoc :parents kwd-alist))
      (parents (cdr parents-p))
      (parents (if parents-p
          parents
          (or (get-default-parents (w state))
            '(undocumented))))
      ((unless (or (eq mode :logic) (eq mode :program))) (raise ":mode must be one of :logic or :program, but is ~x0."
          mode))
      ((unless (or (not short) (stringp short))) (raise ":short must be a string or nil, but is ~x0."
          short))
      ((unless (or (not long) (stringp long))) (raise ":long must be a string or nil, but is ~x0."
          long))
      (long (or long
          (and parents
            "<p>This is an ordinary @(see std::defsum) of aggregates.</p>")))
      ((unless (tuplep 1 other-args)) (raise "defsum should be given exactly one non-keyword argument, but got ~x0"
          other-args))
      (aggnames (first other-args))
      (agginfos (ds-find-aggregates aggnames
          (get-aggregates (w state))))
      (def (ds-recognizer-def name agginfos))
      (name-p (ds-recognizer-name name))
      (x (ds-x name))
      ((when (eq mode :program)) `(defsection ,STD::NAME
          ,@(AND STD::PARENTS `(:PARENTS ,STD::PARENTS))
          ,@(AND STD::SHORT `(:SHORT ,STD::SHORT))
          ,@(AND STD::LONG `(:LONG ,STD::LONG))
          (program)
          ,STD::DEF . ,STD::OTHER-EVENTS))
      (events `((logic) ,STD::DEF
          (local (in-theory (enable ,STD::NAME-P)))
          (defthm ,(STD::MKSYM 'STD::CONSP-WHEN- STD::NAME-P)
            (implies (,STD::NAME-P ,STD::X) (consp ,STD::X))
            :rule-classes :compound-recognizer)
          ,@(STD::DS-MEMBER-IMPLIES-SUM-THMS STD::NAME STD::AGGINFOS)
          ,@(STD::DS-BY-TAG-THMS STD::NAME STD::AGGINFOS)
          ,(STD::DS-WHEN-INVALID-TAG-THM STD::NAME STD::AGGINFOS))))
    `(defsection ,STD::NAME
      ,@(AND STD::PARENTS `(:PARENTS ,STD::PARENTS))
      ,@(AND STD::SHORT `(:SHORT ,STD::SHORT))
      ,@(AND STD::LONG `(:LONG ,STD::LONG))
      (encapsulate nil . ,STD::EVENTS) . ,STD::OTHER-EVENTS)))
defsummacro
(defmacro defsum
  (name &rest args)
  (b* ((__function__ 'defsum) ((unless (symbolp name)) (raise "Name must be a symbol."))
      (ctx (list 'defsum name))
      ((mv main-stuff other-events) (split-/// ctx args))
      ((mv kwd-alist other-args) (extract-keywords ctx
          *defsum-valid-keywords*
          main-stuff
          nil)))
    `(make-event `(progn ,(STD::DEFSUM-FN ',STD::NAME ',STD::OTHER-ARGS ',STD::KWD-ALIST
  ',STD::OTHER-EVENTS STD::STATE)
        (value-triple '(defsum ,',STD::NAME))))))