;  Copyright (C) 2000 Panagiotis Manolios and J Strother Moore

;  This program is free software; you can redistribute it and/or modify
;  it under the terms of the GNU General Public License as published by
;  the Free Software Foundation; either version 2 of the License, or
;  (at your option) any later version.

;  This program is distributed in the hope that it will be useful,
;  but WITHOUT ANY WARRANTY; without even the implied warranty of
;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;  GNU General Public License for more details.

;  You should have received a copy of the GNU General Public License
;  along with this program; if not, write to the Free Software
;  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

;  Written by Panagiotis Manolios and J Strother Moore who can be
;  reached as follows.

;  Email: pete@cs.utexas.edu, moore@cs.utexas.edu

;  Postal Mail:
;  Department of Computer Sciences
;  Taylor Hall 2.124 [C0500]
;  The University of Texas at Austin
;  Austin, TX 78712-1188 USA

; To introduce an arbitrary tail-recursive function we proceed in
; three steps.  First is the proof that we can admit the generic one
; argument tail recursive function.  This ``generic theorem'' is
; proved once; the proof is not redone for each new function.  Second,
; the generic theorem is used to introduce the arity one version of
; the desired function.  Third, we prove that the arity one version is
; a witness for the desired equation.

; Here is an example.  Suppose we wish to admit the tail recursive
; factorial.

; (defun trfact (n a)
;   (if (equal n 0)
;       a
;     (trfact (- n 1) (* n a))))

; We first recognize that this is probably tail recursive (without
; checking that trfact is new, that the vars are distinct, etc.).
; Successful recognition produces

; (mv '((n (car x))
;       (a (cadr x)))
;     '(equal n 0)
;     'a
;     '(list (- n 1) (* n a)))

; Using the output of this check, we introduce three defuns

; (defun test1 (x)
;   (let ((n (car x))
;         (a (cadr x)))
;     (equal n 0)))

; (defun base1 (x)
;   (let ((n (car x))
;         (a (cadr x)))
;     a))

; (defun step1 (x)
;   (let ((n (car x))
;         (a (cadr x)))
;     (list (- n 1) (* n a))))

; We then use the generic theorem to introduce

; (defun trfact1 (x)
;   (if (test1 x)
;       (base1 x)
;     (trfact1 (step1 x))))

; We then define

; (defun trfact (n a)
;   (trfact1 (list n a)))

; and we prove that it satisfies the constraint

; (equal (trfact n a)
;        (if (equal n 0)
;            a
;          (trfact (- n 1) (* n a))))

; Now we write the code to do all this.

; First, we prove the generic theorem.  We use the proof Pete
; developed in his prototype implementation of defpartial but for the
; generic case.

(in-package "ACL2")

(defstub test (x) t)
(defstub base (x) t)
(defstub st (x) t)

(defun stn (x n)
  (if (zp n) x (stn (st x) (1- n))))

(defchoose fch (n)
  (x)
  (test (stn x n)))

(defun fn (x n)
  (declare (xargs :measure (nfix n)))
  (if (or (zp n) (test x))
      (base x)
      (fn (st x) (1- n))))

(defun f (x)
  (if (test (stn x (fch x)))
      (fn x (fch x))
      nil))

; The following encapsulate exports one constrained function, namely,
; f, with the constraint

; (DEFTHM GENERIC-TAIL-RECURSIVE-F
;   (EQUAL (F X)
;          (IF (TEST X) (BASE X) (F (ST X))))
;   :RULE-CLASSES NIL)

; Nothing else is exported.

(encapsulate nil
 (local (defthm test-fch
          (implies (test x)
                   (test (stn x (fch x))))
          :hints
          (("goal" :use ((:instance fch (n 0)))))))
 (local (defthm test-f-def
          (implies (test x)
                   (equal (f x) (base x)))))
 (local (defthm open-stn
          (implies (and (integerp n) (< 0 n))
                   (equal (stn x n) (stn (st x) (1- n))))))

 (local (defthm +1-1 (equal (+ -1 +1 x) (fix x))))

 (local (defthm st-stn-fch
          (implies (test (stn (st x) (fch (st x))))
                   (test (stn x (fch x))))
          :hints
          (("goal" :use
            ((:instance fch (n (1+ (nfix (fch (st x))))))
             (:instance fch (n 1)))))
          :rule-classes :forward-chaining))
 (local (defthm test-nil-fch
          (implies (not (test x))
                   (iff (test (stn (st x) (fch (st x))))
                        (test (stn x (fch x)))))
          :hints
          (("subgoal 2" :expand (stn x (fch x))
            :use
            ((:instance fch (x (st x))
                        (n (+ -1 (fch x)))))))))
 (local (defthm fn-st
          (implies (and (test (stn x n)) (test (stn x m)))
                   (equal (fn x n) (fn x m)))
          :rule-classes nil))
 (defthm generic-tail-recursive-f
   (equal (f x)
          (if (test x) (base x) (f (st x))))
   :hints
   (("subgoal 1" :expand (fn x (fch x)))
    ("subgoal 1.2'" :use
     ((:instance fn-st (x (st x))
                 (n (+ -1 (fch x)))
                 (m (fch (st x)))))))
   :rule-classes nil))

(defun arity-1-tail-recursive-encap (f test base st)

; Execution of this function produces an encapsulation that introduces
; a constrained tail recursive f with the constraint
; (equal (f x) (if (test x) (base x) (f (st x)))),
; where test, base and st are previously defined functions of arity 1.

  (declare (xargs :mode :program))

  (let ((stn (packn-pos (list f "-stn") f))
        (fch (packn-pos (list f "-fch") f))
        (fn  (packn-pos (list f "-fn") f)))

    `(encapsulate
      ((,f (x) t))

      (local (in-theory (disable ,test ,base ,st)))

      (local (defun ,stn (x n)
               (if (zp n)
                   x
                 (,stn (,st x) (1- n)))))

      (local (defchoose ,fch (n) (x)
               (,test (,stn x n))))

      (local (defun ,fn (x n)
               (declare (xargs :measure (nfix n)))
               (if (or (zp n)
                       (,test x))
                   (,base x) 
                 (,fn (,st x) (1- n)))))

      (local (defun ,f (x)
               (if (,test (,stn x (,fch x)))
                   (,fn x (,fch x))
                 nil)))

      (local (in-theory '(,f ,test ,base ,st ,stn ,fn

; This last entry is needed when fn is a constant function returning T, NIL,
; or 0 (one of the singleton type sets)

                             (:type-prescription ,fn))))
      (defthm ,(packn-pos (list f "-DEF") f)
        (equal (,f x)
               (if (,test x) 
                   (,base x) 
                 (,f (,st x))))
        :hints (("Goal"
                 :use
                 (:functional-instance GENERIC-TAIL-RECURSIVE-F
                                       (f ,f)
                                       (test ,test)
                                       (base ,base)
                                       (st ,st)
                                       (stn ,stn)
                                       (fch ,fch)
                                       (fn ,fn)
                                       ))
                ("Subgoal 2" :use ,fch))

        :rule-classes nil)
      )
    ))

; Second, we recognize probably tail-recursive definitions and introduce
; the appropriate functions of arity 1.

; Note that probably-tail-recursivep and destructure-tail-recursion should be
; kept in sync.

(defun probably-tail-recursivep (f vars body)
  (and (symbolp f)
       (symbol-listp vars)
       (true-listp body)
       (eq (car body) 'IF)
       (or (and (consp (caddr body))
                (eq (car (caddr body)) f))
           (and (consp (cadddr body))
                (eq (car (cadddr body)) f)))))

(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))))))

(defun destructure-tail-recursion (f vars body)
  (declare (xargs :mode :program))
  (cond
   ((and (consp (caddr body))
         (eq (car (caddr body)) 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)))))))

(defun arbitrary-tail-recursive-encap (f vars body)
  (declare (xargs :mode :program))
  (mv-let
   (bindings test-body base-body step-body)
   (destructure-tail-recursion f vars body)
   (let ((f1 (packn-pos (list f "-arity-1") f))
         (test1 (packn-pos (list f "-arity-1-test") f))
         (base1 (packn-pos (list f "-arity-1-base") f))
         (step1 (packn-pos (list f "-arity-1-step") f)))
     `(encapsulate
       ((,f ,vars t))
       (set-ignore-ok t)
       (set-irrelevant-formals-ok t)
       (local (defun ,test1 (x) (let ,bindings ,test-body)))
       (local (defun ,base1 (x) (let ,bindings ,base-body)))
       (local (defun ,step1 (x) (let ,bindings ,step-body)))
       (local ,(arity-1-tail-recursive-encap f1 test1 base1 step1))
       (local (defun ,f ,vars (,f1 (list ,@vars))))
       (defthm ,(packn-pos (list f "-DEF") f)
         (equal (,f ,@vars) ,body)
         :hints (("Goal" :use (:instance ,(packn-pos (list f1 "-DEF") f)
                                         (x (list ,@vars)))))
         :rule-classes :definition)))))

(defun remove-xargs-domain-and-measure (dcl)
  (case-match dcl
              (('declare ('xargs ':domain dom-expr
                                 ':measure measure-expr
                                 . rest))
               (mv nil dom-expr measure-expr rest))
              (('declare ('xargs ':gdomain dom-expr
                                 ':measure measure-expr
                                 . rest))
               (mv t dom-expr measure-expr rest))
              (& (mv nil nil 0 nil))))

(mutual-recursion
 (defun subst-fn-into-pseudo-term (new-fn old-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-fn-into-pseudo-bindings new-fn old-fn (cadr pterm))
           (subst-fn-into-pseudo-term new-fn old-fn (caddr pterm))))
    ((eq (car pterm) 'cond)
     (cons 'cond
           (subst-fn-into-pseudo-cond-clauses new-fn old-fn (cdr pterm))))
    (t
     (cons (if (eq (car pterm) old-fn)
               new-fn
             (car pterm))
           (subst-fn-into-pseudo-term-list new-fn old-fn (cdr pterm))))))

 (defun subst-fn-into-pseudo-bindings (new-fn old-fn pbindings)
   (declare (xargs :mode :program))
   (cond
    ((atom pbindings) pbindings)
    (t (cons (list (car (car pbindings))
                   (subst-fn-into-pseudo-term new-fn old-fn
                                              (cadr (car pbindings))))
             (subst-fn-into-pseudo-bindings new-fn old-fn (cdr pbindings))))))

 (defun subst-fn-into-pseudo-cond-clauses (new-fn old-fn pclauses)
   (declare (xargs :mode :program))
   (cond
    ((atom pclauses) pclauses)
    (t (cons (list (subst-fn-into-pseudo-term new-fn old-fn
                                              (car (car pclauses)))
                   (subst-fn-into-pseudo-term new-fn old-fn
                                              (cadr (car pclauses))))
             (subst-fn-into-pseudo-cond-clauses new-fn old-fn
                                                (cdr pclauses))))))

 (defun subst-fn-into-pseudo-term-list (new-fn old-fn list)
   (declare (xargs :mode :program))
   (cond
    ((atom list) list)
    (t (cons (subst-fn-into-pseudo-term new-fn old-fn (car list))
             (subst-fn-into-pseudo-term-list new-fn old-fn (cdr list)))))))

(defun default-defpun-rule-classes (keyword-alist)

; We add :rule-classes :definition to keyword-alist if :rule-classes is
; not mentioned in it.

  (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)))

(defun destructure-dcl-body-keypairs (lst)

; Lst is the tail of some defpun.  It optionally contains a DECLARE
; form, a body, and some keyword binding pairs, in that order.  We
; return the three components.  Body must be present, and if keyword
; binding pairs are present, the length of that part of the list must
; be even.  So the parity of the length of the list determines which
; optional components are present.

; 0. illegal - never allowed to happen
; 1. body
; 2. dcl body
; 3. body :rule-classes classes
; 4. dcl body :rule-classes classes
; 5. body :rule-classes classes :hints hints
; 6. dcl body :rule-classes classes :hints hints
; etc.
; If rule-classes is unspecified it defaults to :definition.

  (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))))))

(defun defpun-syntax-er nil
  '(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 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."))

(defmacro defpun (g vars &rest rest)
  (cond
   ((and (symbolp g)
         (symbol-listp vars)
         (not (endp rest)))

; This form may be legal, so we will destructure it and proceed.  Otherwise,
; we will cause an error.

    (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))
      ((and dcl
            (match dcl
                   ('declare ('xargs ':witness &))))
       `(encapsulate
         ((,g ,vars t))
         (local (defun ,g ,vars (,(caddr (cadr dcl))
                                 ,@vars)))
         (defthm ,(packn-pos (list g "-DEF") g)
           (equal (,g ,@vars)
                  ,body)
           ,@keypairs)))
      ((not (and (consp dcl)
                 (eq (car dcl) 'declare)))
       (defpun-syntax-er))
      (t
       (mv-let
        (closed-domp dom-expr measure-expr rest-of-xargs)
        (remove-xargs-domain-and-measure dcl)
        (cond
         (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-fn-into-pseudo-term gwit g body)
                  'undef))
              (encapsulate
               ((,g ,vars t))
               (local (defun ,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 ,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))))