Filtering...

defmvtypes

books/std/util/defmvtypes
other
(in-package "STD")
other
(include-book "xdoc/top" :dir :system)
other
(include-book "std/util/bstar" :dir :system)
other
(defxdoc defmvtypes
  :parents (std/util)
  :short "Introduce type-prescription rules for a function that returns
multiple values."
  :long "<p>Defmvtypes is just a shorthand that allows you to quickly introduce
type-prescription rules for a function that returns multiple values.</p>

<p>General form:</p>

@({
 (defmvtypes fn return-types
    [:hyp   hyp]
    [:hints hints])
})

<p>For example,</p>

@({
 (defmvtypes foo
   (true-listp nil booleanp (and (consp x) (true-listp x))))
})

<p>introduces three type-prescription rules:</p>
<ol>
 <li>@('(true-listp (mv-nth 0 (foo ...))')</li>
 <li>@('(booleanp (mv-nth 2 (foo ...))')</li>
 <li>@('(and (consp (mv-nth 3 (foo ...)))
             (true-listp (mv-nth 3 (foo ...))))')</li>
</ol>


<h3>Usage and Arguments</h3>

<p>Each of the @('return-types') should either be a plain symbol like
@('true-listp'), or a term whose only free variable is @('pkg::x'), where
@('pkg') is the package of @('fn').</p>

<p>The theorems introduced will be unconditional unless a @(':hyp') argument is
provided.  For instance,</p>

@({
 (defmvtypes foo
   (nil nil true-listp)
   :hyp (bar a b c))
})

<p>Would result in:</p>

@({
 (implies (bar a b c)
          (true-listp (mv-nth 2 (foo ...))))
})

<p>The @(':hints') argument can be used to specify custom @(see acl2::hints) to
use.  The same hints are given to each theorem.</p>

<h3>Interaction with @(see force)</h3>

<p>Sometimes @(see force) can get in the way of proving nice, hypothesis-free
type-prescription rules.  To try to avoid this, by default @('defmvtypes')
automatically:</p>

<ul>
<li>Disables forcing before submitting its theorems, then</li>
<li>Uses @(see acl2::computed-hints) to re-enable @('force') when goals are
@('stable-under-simplification').</li>
</ul>

<p>The hope is that this will generally prevent @(see force) from screwing up
type-prescription theorems, but will allow it to be used when it would be
useful to do so.  If you do <b>not</b> want this behavior, you can suppress it
by giving any @(':hints').</p>")
inducting-pfunction
(defun inducting-p
  (clause-id)
  (declare (xargs :mode :program))
  (consp (access clause-id clause-id :pool-lst)))
defmvtypes-nonrecursive-hintfunction
(defun defmvtypes-nonrecursive-hint
  (id stable-under-simplificationp)
  (declare (xargs :mode :program))
  (declare (ignore id))
  (and stable-under-simplificationp
    '(:in-theory (enable (:executable-counterpart force)))))
defmvtypes-recursive-hintfunction
(defun defmvtypes-recursive-hint
  (id stable-under-simplificationp)
  (declare (xargs :mode :program))
  (and stable-under-simplificationp
    (inducting-p id)
    '(:in-theory (enable (:executable-counterpart force)))))
defmvtypes-element-to-thmfunction
(defun defmvtypes-element-to-thm
  (spec hyp
    fn
    args
    recp
    place
    hints)
  (declare (xargs :mode :program))
  (b* (((unless spec) nil) (thmname (intern-in-package-of-symbol (concatenate 'string
            (symbol-name fn)
            "-MVTYPES-"
            (coerce (explode-atom place 10) 'string))
          fn))
      (x (intern-in-package-of-symbol "X" fn))
      (rval `(mv-nth ,STD::PLACE (,STD::FN . ,STD::ARGS)))
      (concl (cond ((symbolp spec) (list spec rval))
          ((atom spec) (er hard?
              'defmvtypes-element-to-thm
              "Bad return-value type specifier: ~x0."
              spec))
          (t (let ((new (subst rval x spec)))
              (if (equal new spec)
                (er hard?
                  'defmvtypes-element-to-thm
                  "Bad return-value type specifier: does not ~
                             mention ~x0: ~x1."
                  x
                  spec)
                new))))))
    `((defthm ,STD::THMNAME
       ,(IF STD::HYP
     `(STD::IMPLIES ,STD::HYP ,STD::CONCL)
     STD::CONCL)
       :rule-classes :type-prescription :hints ,(COND (STD::HINTS STD::HINTS)
       (STD::RECP
        '((STD::DEFMVTYPES-RECURSIVE-HINT STD::ID
           STD::STABLE-UNDER-SIMPLIFICATIONP)))
       (T
        '((STD::DEFMVTYPES-NONRECURSIVE-HINT STD::ID
           STD::STABLE-UNDER-SIMPLIFICATIONP))))))))
defmvtypes-elements-to-thmsfunction
(defun defmvtypes-elements-to-thms
  (specs hyp
    fn
    args
    recp
    place
    hints)
  (declare (xargs :mode :program))
  (if (atom specs)
    nil
    (append (defmvtypes-element-to-thm (car specs)
        hyp
        fn
        args
        recp
        place
        hints)
      (defmvtypes-elements-to-thms (cdr specs)
        hyp
        fn
        args
        recp
        (+ 1 place)
        hints))))
defmvtypes-fnfunction
(defun defmvtypes-fn
  (specs fn hyp hints world)
  (declare (xargs :mode :program))
  (b* ((args (getprop fn
         'formals
         :bad 'current-acl2-world
         world)) ((when (eq args :bad)) (er hard?
          'defmvtypes-fn
          "Failed to find formals for ~x0.~%"
          fn))
      (recp (consp (getprop fn
            'induction-machine
            nil
            'current-acl2-world
            world))))
    `(encapsulate nil
      ,(IF STD::HINTS
     `(STD::LOCAL (STD::IN-THEORY (STD::ENABLE ,STD::FN)))
     `(STD::LOCAL
       (STD::IN-THEORY
        (STD::E/D (,STD::FN) ((:EXECUTABLE-COUNTERPART STD::FORCE))))))
      ,@(STD::DEFMVTYPES-ELEMENTS-TO-THMS STD::SPECS STD::HYP STD::FN STD::ARGS
   STD::RECP 0 STD::HINTS))))
defmvtypesmacro
(defmacro defmvtypes
  (fn specs &key hyp hints)
  `(make-event (defmvtypes-fn ',STD::SPECS
      ',STD::FN
      ',STD::HYP
      ',STD::HINTS
      (w state))))
other
(local (encapsulate nil
    (defund foo
      (x y)
      (mv (cons x y)
        0
        1
        (if x
          t
          nil)
        (cons x nil)))
    (defmvtypes foo
      (consp (equal x 0)
        posp
        booleanp
        (and (consp x) (true-listp x))))
    (defun bar (a b) (mv a b))
    (defmvtypes bar
      (consp integerp)
      :hyp (and (force (consp a))
        (force (integerp b))))
    (defun baz (a b) (bar a b))
    (defmvtypes baz
      (atom rationalp)
      :hyp (and (atom a) (rationalp b))
      :hints (("Goal")))
    (defun f
      (x)
      (b* (((when (atom x)) (mv 0 t 0)) ((mv a b c) (f (cdr x))))
        (mv a (not b) (+ 1 c))))
    (defmvtypes f
      ((equal x 0) booleanp natp))))