Filtering...

defpun

books/misc/defpun

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc defpun
  :parents (events)
  :short "Define a tail-recursive function symbol"
  :long "<p>@('Defpun') is a macro developed by Pete Manolios and J Moore that
 allows tail-recursive definitions, as well as some other ``partial''
 definitions.  Related utilities are discussed at the end of this topic.</p>

 @({
 General Form:

 (defpun g (v1 ... vk)
   dcl ; optional
   body
   :kwd1 val1 :kwd2 val2 ... :kwdn valn)
 })

 <p>where @('dcl') is an optional @(tsee declare) form and the pairs @(':kwdi
 vali') are optional (that is @('n') can be 0).  If the optional arguments are
 omitted, then ACL2 will introduce a constrained function @('g') with this
 exported event:</p>

 @({
 (DEFTHM g-DEF
   (EQUAL (g v1 ... vk)
          body)
   :RULE-CLASSES :DEFINITION)
 })

 <p>First suppose that @('dcl') is not present.  Then the proposed definition
 must have a simple tail-recursive structure (see the discussion of
 @('defp') below for a workaround if this is not the case).</p>

 <p>If @('dcl') is present, then the definition need not be tail-recursive, and
 @('dcl') must have one of the following three forms.</p>

 @({
 (DECLARE (XARGS :witness defpun-fn))
 (DECLARE (XARGS :domain dom-expr :measure m . rest))
 (DECLARE (XARGS :gdomain dom-expr :measure m . rest)).
 })

 <p>You are encouraged to experiment by using @(':')@(tsee trans1) to see the
 expansions of @('defpun') forms that use these @(tsee declare) forms; but here
 is a summary of what is generated.</p>

 <p>The first form specifies a function, @('defpun-fn'), and instructs ACL2 to
 use that function as a witness for the function @('g') to be introduced, as
 follows.</p>

 @({
 (ENCAPSULATE
   ((g (v1 ... vk) t))
   (LOCAL (DEFUN-NONEXEC g (v1 ... vk) (defpun-fn v1 ... vk)))
   (DEFTHM g-DEF
     (EQUAL (g v1 ... vk))
            body)
     :RULE-CLASSES :DEFINITION)
 })

 <p>The remaining two @('declare') forms introduce a function, defined
 recursively, with the given measure and with a modified body:</p>

 @({
 (THE-g v1 ... vk)
 =
 (IF dom-expr body 'UNDEF)
 })

 <p>The following  theorem is exported.</p>

 @({
 (defthm g-DEF
   (IMPLIES domain-expr
            (EQUAL (g v1 ... vk)
                   body))
   :RULE-CLASSES :DEFINITION)
 })

 <p>If @(':gdomain') is used (as opposed to @(':domain')), then the following
 events are also introduced, where @('body\{g:=THE-g}') denotes the result of
 replacing each call of @('g') in @('body') with the corresponding call of
 @('THE-g').</p>

 @({
 (DEFUN THE-g (v1 ... vk)
   (DECLARE (XARGS :MEASURE (IF dom-expr m 0)
                   :GUARD domain-expr
                   :VERIFY-GUARDS NIL))
   (IF dom-expr body 'UNDEF))

 (DEFTHM g-IS-UNIQUE
   (IMPLIES domain-expr
            (EQUAL (g v1 ... vk) (THE-g v1 ... vk))))
 })

 <p>The optional keyword alist @(':kwd1 val1 :kwd2 val2 ... :kwdn valn') is
 attached to the end of the generated @(tsee defthm) event.  If the
 @(':')@(tsee rule-classes) keyword is not specified by the keyword alist,
 @(':')@(tsee definition) is used.</p>

 <p>Details of defpun are provided by Manolios and Moore in the chapter
 ``Partial Functions in ACL2'' published with the <a
 href='http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/'>ACL2 2000
 workshop</a>.  Also see <a
 href='http://www.cs.utexas.edu/users/moore/publications/defpun/index.html'>Partial
 Functions in ACL2</a>.</p>

 <h3>Variants of @('defpun')</h3>

 <p>A variant, @('defp'), allows more general forms of tail recursion.  If
 @('defpun') doesn't work for you, try @('defp') by first executing the
 following event.</p>

 @({
  (include-book "misc/defp" :dir :system)
 })

 <p>Sandip Ray has contributed a variant of @('defpun'), @('defpun-exec'), that
 supports executability.  See community book
 @('books/defexec/defpun-exec/defpun-exec.lisp'):</p>

 @({
  (include-book "defexec/defpun-exec/defpun-exec" :dir :system)
 })

 <p>He has also contributed community book
 @('books/misc/misc2/defpun-exec-domain-example.lisp'), for functions that are
 uniquely defined in a particular domain.</p>

 <p>Finally, it is possible to avoid termination proofs even for functions that
 are not tail-recursive.  See @(see def-partial-measure).</p>")
defun-nonexecmacro
(defmacro defun-nonexec
  (name args &rest rst)
  `(defun-nx ,NAME ,ARGS ,@RST))
other
(defstub defpun-test (x) t)
other
(defstub defpun-base (x) t)
other
(defstub defpun-st (x) t)
defpun-stnfunction
(defun defpun-stn
  (x n)
  (if (zp n)
    x
    (defpun-stn (defpun-st x) (1- n))))
other
(defchoose fch (n) (x) (defpun-test (defpun-stn x n)))
defpun-fnfunction
(defun defpun-fn
  (x n)
  (declare (xargs :measure (nfix n)))
  (if (or (zp n) (defpun-test x))
    (defpun-base x)
    (defpun-fn (defpun-st x) (1- n))))
defpun-ffunction
(defun defpun-f
  (x)
  (if (defpun-test (defpun-stn x (fch x)))
    (defpun-fn x (fch x))
    nil))
generic-tail-recursive-defpun-fencapsulate
(encapsulate nil
  (local (defthm defpun-test-fch
      (implies (defpun-test x)
        (defpun-test (defpun-stn x (fch x))))
      :hints (("goal" :use ((:instance fch (n 0)))))))
  (local (defthm defpun-test-defpun-f-def
      (implies (defpun-test x)
        (equal (defpun-f x) (defpun-base x)))))
  (local (defthm open-defpun-stn
      (implies (and (integerp n) (< 0 n))
        (equal (defpun-stn x n) (defpun-stn (defpun-st x) (1- n))))))
  (local (defthm +1-1 (equal (+ -1 1 x) (fix x))))
  (local (defthm defpun-st-defpun-stn-fch
      (implies (defpun-test (defpun-stn (defpun-st x) (fch (defpun-st x))))
        (defpun-test (defpun-stn x (fch x))))
      :hints (("goal" :use ((:instance fch (n (1+ (nfix (fch (defpun-st x)))))) (:instance fch (n 1)))))
      :rule-classes :forward-chaining))
  (local (defthm defpun-test-nil-fch
      (implies (not (defpun-test x))
        (iff (defpun-test (defpun-stn (defpun-st x) (fch (defpun-st x))))
          (defpun-test (defpun-stn x (fch x)))))
      :hints (("subgoal 2" :expand (defpun-stn x (fch x))
         :use ((:instance fch (x (defpun-st x)) (n (+ -1 (fch x)))))))))
  (local (defthm defpun-fn-defpun-st
      (implies (and (defpun-test (defpun-stn x n))
          (defpun-test (defpun-stn x m)))
        (equal (defpun-fn x n) (defpun-fn x m)))
      :rule-classes nil))
  (defthm generic-tail-recursive-defpun-f
    (equal (defpun-f x)
      (if (defpun-test x)
        (defpun-base x)
        (defpun-f (defpun-st x))))
    :hints (("subgoal 1" :expand (defpun-fn x (fch x))) ("subgoal 1.2'" :use ((:instance defpun-fn-defpun-st
           (x (defpun-st x))
           (n (+ -1 (fch x)))
           (m (fch (defpun-st x)))))))
    :rule-classes nil))
arity-1-tail-recursive-encapfunction
(defun arity-1-tail-recursive-encap
  (defpun-f defpun-test defpun-base defpun-st)
  (declare (xargs :mode :program))
  (let ((defpun-stn (packn-pos (list defpun-f "-defpun-stn") defpun-f)) (fch (packn-pos (list defpun-f "-fch") defpun-f))
      (defpun-fn (packn-pos (list defpun-f "-defpun-fn") defpun-f)))
    `(encapsulate ((,DEFPUN-F (x) t))
      (local (in-theory (disable ,DEFPUN-TEST ,DEFPUN-BASE ,DEFPUN-ST)))
      (local (defun-nonexec ,DEFPUN-STN
          (x n)
          (if (zp n)
            x
            (,DEFPUN-STN (,DEFPUN-ST x) (1- n)))))
      (local (defchoose ,FCH (n) (x) (,DEFPUN-TEST (,DEFPUN-STN x n))))
      (local (defun-nonexec ,DEFPUN-FN
          (x n)
          (declare (xargs :measure (nfix n)))
          (if (or (zp n) (,DEFPUN-TEST x))
            (,DEFPUN-BASE x)
            (,DEFPUN-FN (,DEFPUN-ST x) (1- n)))))
      (local (defun-nonexec ,DEFPUN-F
          (x)
          (if (,DEFPUN-TEST (,DEFPUN-STN x (,FCH x)))
            (,DEFPUN-FN x (,FCH x))
            nil)))
      (local (in-theory '(,DEFPUN-F ,DEFPUN-TEST
            ,DEFPUN-BASE
            ,DEFPUN-ST
            ,DEFPUN-STN
            ,DEFPUN-FN
            (:type-prescription ,DEFPUN-FN))))
      (defthm ,(PACKN-POS (LIST DEFPUN-F "-DEF") DEFPUN-F)
        (equal (,DEFPUN-F x)
          (if (,DEFPUN-TEST x)
            (,DEFPUN-BASE x)
            (,DEFPUN-F (,DEFPUN-ST x))))
        :hints (("Goal" :use (:functional-instance generic-tail-recursive-defpun-f
             (defpun-f ,DEFPUN-F)
             (defpun-test ,DEFPUN-TEST)
             (defpun-base ,DEFPUN-BASE)
             (defpun-st ,DEFPUN-ST)
             (defpun-stn ,DEFPUN-STN)
             (fch ,FCH)
             (defpun-fn ,DEFPUN-FN))) ("Subgoal 2" :use ,FCH))
        :rule-classes nil))))
probably-tail-recursivepfunction
(defun probably-tail-recursivep
  (defpun-f vars body)
  (and (symbolp defpun-f)
    (symbol-listp vars)
    (true-listp body)
    (eq (car body) 'if)
    (or (and (consp (caddr body)) (eq (car (caddr body)) defpun-f))
      (and (consp (cadddr body))
        (eq (car (cadddr body)) defpun-f)))))
destructure-tail-recursion-auxfunction
(defun destructure-tail-recursion-aux
  (vars x)
  (declare (xargs :mode :program))
  (cond ((endp vars) nil)
    (t (cons (list (car vars) (list 'car x))
        (destructure-tail-recursion-aux (cdr vars) (list 'cdr x))))))
destructure-tail-recursionfunction
(defun destructure-tail-recursion
  (defpun-f vars body)
  (declare (xargs :mode :program))
  (cond ((and (consp (caddr body)) (eq (car (caddr body)) defpun-f)) (mv (destructure-tail-recursion-aux vars 'x)
        (list 'not (cadr body))
        (cadddr body)
        (cons 'list (cdr (caddr body)))))
    (t (mv (destructure-tail-recursion-aux vars 'x)
        (cadr body)
        (caddr body)
        (cons 'list (cdr (cadddr body)))))))
arbitrary-tail-recursive-encapfunction
(defun arbitrary-tail-recursive-encap
  (defpun-f vars body keypairs)
  (declare (xargs :mode :program))
  (mv-let (bindings defpun-test-body defpun-base-body step-body)
    (destructure-tail-recursion defpun-f vars body)
    (let ((f1 (packn-pos (list defpun-f "-arity-1") defpun-f)) (defpun-test1 (packn-pos (list defpun-f "-arity-1-defpun-test") defpun-f))
        (defpun-base1 (packn-pos (list defpun-f "-arity-1-defpun-base") defpun-f))
        (step1 (packn-pos (list defpun-f "-arity-1-step") defpun-f)))
      `(encapsulate ((,DEFPUN-F ,VARS t))
        (set-ignore-ok t)
        (set-irrelevant-formals-ok t)
        (local (defun-nonexec ,DEFPUN-TEST1
            (x)
            (let ,BINDINGS
              ,DEFPUN-TEST-BODY)))
        (local (defun-nonexec ,DEFPUN-BASE1
            (x)
            (let ,BINDINGS
              ,DEFPUN-BASE-BODY)))
        (local (defun-nonexec ,STEP1
            (x)
            (let ,BINDINGS
              ,STEP-BODY)))
        (local ,(ARITY-1-TAIL-RECURSIVE-ENCAP F1 DEFPUN-TEST1 DEFPUN-BASE1 STEP1))
        (local (defun-nonexec ,DEFPUN-F ,VARS (,F1 (list ,@VARS))))
        (defthm ,(PACKN-POS (LIST DEFPUN-F "-DEF") DEFPUN-F)
          (equal (,DEFPUN-F ,@VARS) ,BODY)
          :hints (("Goal" :use (:instance ,(PACKN-POS (LIST F1 "-DEF") DEFPUN-F)
               (x (list ,@VARS)))))
          ,@KEYPAIRS)))))
remove-xargs-domain-and-measurefunction
(defun remove-xargs-domain-and-measure
  (dcl)
  (case-match dcl
    (('declare ('xargs ':domain dom-expr ':measure measure-expr . rest)) (mv nil nil dom-expr measure-expr rest))
    (('declare ('xargs ':gdomain dom-expr ':measure measure-expr . rest)) (mv nil t dom-expr measure-expr rest))
    (& (mv t nil nil nil nil))))
subst-defpun-fn-into-pseudo-termmutual-recursion
(mutual-recursion (defun subst-defpun-fn-into-pseudo-term
    (new-defpun-fn old-defpun-fn pterm)
    (declare (xargs :mode :program))
    (cond ((atom pterm) pterm)
      ((eq (car pterm) 'quote) pterm)
      ((or (eq (car pterm) 'let) (eq (car pterm) 'let*)) (list (car pterm)
          (subst-defpun-fn-into-pseudo-bindings new-defpun-fn
            old-defpun-fn
            (cadr pterm))
          (subst-defpun-fn-into-pseudo-term new-defpun-fn
            old-defpun-fn
            (caddr pterm))))
      ((eq (car pterm) 'cond) (cons 'cond
          (subst-defpun-fn-into-pseudo-cond-clauses new-defpun-fn
            old-defpun-fn
            (cdr pterm))))
      (t (cons (if (eq (car pterm) old-defpun-fn)
            new-defpun-fn
            (car pterm))
          (subst-defpun-fn-into-pseudo-term-list new-defpun-fn
            old-defpun-fn
            (cdr pterm))))))
  (defun subst-defpun-fn-into-pseudo-bindings
    (new-defpun-fn old-defpun-fn pbindings)
    (declare (xargs :mode :program))
    (cond ((atom pbindings) pbindings)
      (t (cons (list (car (car pbindings))
            (subst-defpun-fn-into-pseudo-term new-defpun-fn
              old-defpun-fn
              (cadr (car pbindings))))
          (subst-defpun-fn-into-pseudo-bindings new-defpun-fn
            old-defpun-fn
            (cdr pbindings))))))
  (defun subst-defpun-fn-into-pseudo-cond-clauses
    (new-defpun-fn old-defpun-fn pclauses)
    (declare (xargs :mode :program))
    (cond ((atom pclauses) pclauses)
      (t (cons (list (subst-defpun-fn-into-pseudo-term new-defpun-fn
              old-defpun-fn
              (car (car pclauses)))
            (subst-defpun-fn-into-pseudo-term new-defpun-fn
              old-defpun-fn
              (cadr (car pclauses))))
          (subst-defpun-fn-into-pseudo-cond-clauses new-defpun-fn
            old-defpun-fn
            (cdr pclauses))))))
  (defun subst-defpun-fn-into-pseudo-term-list
    (new-defpun-fn old-defpun-fn list)
    (declare (xargs :mode :program))
    (cond ((atom list) list)
      (t (cons (subst-defpun-fn-into-pseudo-term new-defpun-fn
            old-defpun-fn
            (car list))
          (subst-defpun-fn-into-pseudo-term-list new-defpun-fn
            old-defpun-fn
            (cdr list)))))))
default-defpun-rule-classesfunction
(defun default-defpun-rule-classes
  (keyword-alist)
  (cond ((keyword-value-listp keyword-alist) (cond ((assoc-keyword :rule-classes keyword-alist) keyword-alist)
        (t (list* :rule-classes :definition keyword-alist))))
    (t keyword-alist)))
destructure-dcl-body-keypairsfunction
(defun destructure-dcl-body-keypairs
  (lst)
  (cond ((evenp (length lst)) (mv (car lst)
        (cadr lst)
        (default-defpun-rule-classes (cddr lst))))
    (t (mv nil (car lst) (default-defpun-rule-classes (cdr lst))))))
defpun-syntax-er-fnfunction
(defun defpun-syntax-er-fn
  (state)
  (declare (xargs :stobjs state :mode :program))
  (er soft
    'defpun
    "The proper shape of a defpun event is~%~
        (defpun g (v1 ... vn) body).~%~
        A single optional declare form may be present ~
        before the body.  If present, the form must be one of three:~%~
        (DECLARE (XARGS :witness defpun-fn))~%~
        or~%~
        (DECLARE (XARGS :domain dom-expr :measure m . rest))~%~
        or~%~
        (DECLARE (XARGS :gdomain dom-expr :measure m . rest)).~%~
        An optional keyword alist may be ~
        present after the body.  The declare form is used during the ~
        admission of the witness function.  The keyword alist is ~
        attached to the equality axiom constraining the new function ~
        symbol.  If the :rule-classes keyword is not specified by the ~
        keyword alist, :definition is used.  See :DOC defpun."))
defpun-syntax-erfunction
(defun defpun-syntax-er
  nil
  `(make-event (defpun-syntax-er-fn state)))
defpunmacro
(defmacro defpun
  (g vars &rest rest)
  (cond ((and (symbolp g) (symbol-listp vars) (not (endp rest))) (mv-let (dcl body keypairs)
        (destructure-dcl-body-keypairs rest)
        (cond ((not (keyword-value-listp keypairs)) (defpun-syntax-er))
          ((and (not dcl) (probably-tail-recursivep g vars body)) (arbitrary-tail-recursive-encap g vars body keypairs))
          ((and dcl
             (case-match dcl
               (('declare ('xargs ':witness witness)) `(encapsulate ((,G ,VARS t))
                   (local (defun-nonexec ,G ,VARS (,WITNESS ,@VARS)))
                   (defthm ,(PACKN-POS (LIST G "-DEF") G)
                     (equal (,G ,@VARS) ,BODY)
                     ,@KEYPAIRS)))
               (& nil))))
          ((not (and (consp dcl) (eq (car dcl) 'declare))) (defpun-syntax-er))
          (t (mv-let (erp closed-domp dom-expr measure-expr rest-of-xargs)
              (remove-xargs-domain-and-measure dcl)
              (cond (erp (defpun-syntax-er))
                (closed-domp (let ((gwit (packn-pos (list "THE-" g) g)))
                    `(encapsulate nil
                      (defun ,GWIT
                        ,VARS
                        (declare (xargs :measure (if ,DOM-EXPR
                              ,MEASURE-EXPR
                              0)
                            :guard ,DOM-EXPR
                            :verify-guards nil
                            ,@REST-OF-XARGS))
                        (if ,DOM-EXPR
                          ,(SUBST-DEFPUN-FN-INTO-PSEUDO-TERM GWIT G BODY)
                          'undef))
                      (encapsulate ((,G ,VARS t))
                        (local (defun-nonexec ,G ,VARS (,GWIT ,@VARS)))
                        (defthm ,(PACKN-POS (LIST G "-DEF") G)
                          (implies ,DOM-EXPR (equal (,G ,@VARS) ,BODY))
                          ,@KEYPAIRS))
                      (defthm ,(PACKN-POS (LIST G "-IS-UNIQUE") G)
                        (implies ,DOM-EXPR (equal (,G ,@VARS) (,GWIT ,@VARS))))
                      (in-theory (disable ,(PACKN-POS (LIST G "-IS-UNIQUE") G)))
                      (verify-guards ,GWIT))))
                (t `(encapsulate ((,G ,VARS t))
                    (local (defun-nonexec ,G
                        ,VARS
                        (declare (xargs :measure (if ,DOM-EXPR
                              ,MEASURE-EXPR
                              0)
                            ,@REST-OF-XARGS))
                        (if ,DOM-EXPR
                          ,BODY
                          'undef)))
                    (defthm ,(PACKN-POS (LIST G "-DEF") G)
                      (implies ,DOM-EXPR (equal (,G ,@VARS) ,BODY))
                      ,@KEYPAIRS)))))))))
    (t (defpun-syntax-er))))