#|

   Fully Ordered Finite Sets, Version 0.91
   Copyright (C) 2003-2006 by Jared Davis <jared@cs.utexas.edu>

   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 Lic-
   ense along with this program; if not, write to the Free Soft-
   ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
   02111-1307, USA.
 


  instance.lisp

    This is a system for dynamically instantiating ACL2 "theories"
    (which are represented as constants) to create new, concrete
    "theories".  

|#

(in-package "INSTANCE")


; Everything in this file is in program mode.  We do not intend to 
; reason about these functions -- instead, we intend to use these
; functions to create new functions, which the user will reason 
; about.

(program)


; Introduction
;
;
; The following work has been motivated by my work with quantification
; over sets.  When I started on this file, I had roughly 2000 lines of
; complicted macros in order to be able to instantiate generic and
; concrete theories for this work, and it was just becoming
; unmanageable.  My hope was that rewriting the definitions and
; theorems into concrete forms would provide a more concise way of
; instantiating the theory, and make it easier to keep everything
; consistent.
;
; Originally, I wanted to extract the definitions for generic
; functions from ACL2's state (well, actually from the current world).
; But, to do so becomes very complicated, because of the restrictions
; on macros that they cannot take state as a parameter.  So, the best
; that I could ever accomplish that way would be to display a list of
; events, which a user could copy into a file.  But, that is wholly
; unsatisfying, because it would mean that the resulting theories
; could never be "automagically" updated when new theorems are added
; to the generic theory.
;
; So, instead of doing things that way, I now simply store events in 
; constants.  These constants can then be rewritten to create new but
; related theories.
;
; A first step towards this is to introduce a simple rewriter.
; Originally I had based my rewriter on the built in one-way-unify
; function in ACL2, but it operates only on pseudo-terms, and
; pseudo-terms cannot contain atoms other than symbols.  This gave me
; serious trouble when trying to rewrite theorems involving constants,
; e.g., to say that something was an integerp and greater than zero.
; So, instead of using one-way-unify, I introduce a simple unification
; algorithm which has been adapted from Warren Hunt's work.  

; The system treats all symbols beginning with a ? as variables, and
; all other atoms as literals.

(defun instance-variablep (x)
  (and (symbolp x)
       (equal (car (explode-atom x 10)) #\?)))



; We return two values: a boolean flag which indicates if we are
; successful in finding a match, and a list of substitutions of the
; form (variable . value).  This is all be fairly standard stuff.
; 
; For example:
;
;    (instance-unify-term '(predicate ?x) '(predicate (car a)) nil)
;    ==>
;    (t ((?x . (car a))))

(mutual-recursion 

  (defun instance-unify-term (pattern term sublist)
    (if (atom pattern)
	(if (instance-variablep pattern)
	    (let ((value (assoc pattern sublist)))
	      (if (consp value)
		  (if (equal term (cdr value))
		      (mv t sublist)
		    (mv nil nil))
		(mv t (acons pattern term sublist))))
	  (if (equal term pattern)
	      (mv t sublist)
	    (mv nil nil)))
      (if (or (atom term)
	      (not (eq (car term) (car pattern))))
	  (mv nil nil)
	(if (or (eq (car term) 'quote)
		(eq (car pattern) 'quote))
	    (if (equal term pattern)
		(mv t sublist)
	      (mv nil nil))
	  (instance-unify-list (cdr pattern) (cdr term) sublist)))))
      
  (defun instance-unify-list (pattern-list term-list sublist)
    (if (or (atom term-list)
	    (atom pattern-list))
	(if (and (atom term-list)
		 (atom pattern-list))
	    (mv t sublist)
	  (mv nil nil))
      (mv-let (successp new-sublist)
	      (instance-unify-term (car pattern-list) 
				   (car term-list) 
				   sublist)
	      (if successp
		  (instance-unify-list (cdr pattern-list) 
				       (cdr term-list) 
				       new-sublist)
		(mv nil nil)))))
)


; After a list of substitutions has been generated, we typically want
; to apply them to a term.  We recur over the list of substitutions, 
; simply calling subst to do our work throughout a term.
;
; For example:
; 
;   (instance-substitute '((?x . (car a))) '(not (predicate ?x)))
;   ==>
;   (not (predicate (car a)))

(defun instance-substitute (sublist term)
  (if (endp sublist)
      term
    (let* ((old (car (car sublist)))
           (new (cdr (car sublist)))
	   (result (subst new old term)))
      (instance-substitute (cdr sublist) result))))



; We now introduce our actual rewriter.  We take three arguments: pat
; is the pattern to look for throughout the term, e.g., (predicate
; ?x), repl is the replacement to use, e.g., (not (predicate ?x)), and
; term is the term to match the pattern against in order to get the
; substitutions.
;
; For Example:
;  
;   (instance-rewrite1 '(predicate ?x) 
;                      '(not (predicate ?x))
;                      '(if (predicate (car x)) t nil))
;   =>
;   (if (not (predicate (car x))) t nil)

(mutual-recursion 

  (defun instance-rewrite1 (pat repl term)
    (mv-let (successful sublist)
            (instance-unify-term pat term nil)
	    (if successful 
		(instance-substitute sublist repl)
	      (if (atom term)
		  term
		(cons (instance-rewrite1 pat repl (car term))
		      (instance-rewrite-lst1 pat repl (cdr term)))))))

  (defun instance-rewrite-lst1 (pat repl lst)
    (if (endp lst)
        nil
      (cons (instance-rewrite1 pat repl (car lst))
            (instance-rewrite-lst1 pat repl (cdr lst)))))
)



; Finally, given that we can apply a rewrite a term with a single
; replacement, we go ahead and extend this notion to multiple
; replacements.  In other words, we walk through a list of
; substitutions, sequentially rewriting the term using each
; substitution.

(defun instance-rewrite (term subs)
  (if (endp subs)
      term
    (let ((first-sub (car subs)))
      (instance-rewrite (instance-rewrite1 (first first-sub)
					   (second first-sub)
					   term)
			(cdr subs)))))




; Instantiating Defuns
;
;
; Theories consist mainly of definitions and theorems.  Given generic
; theorems, we will want to rewrite them so that they perform
; different functions.  For example, a generic "all" function might
; need to be rewritten so that its calls to (predicate x) are replaced
; with calls to (not (predicate x)) for all x.  
; 
; To begin, we instantiate the function's declarations (e.g., comment
; strings, xargs, ignores, and so forth).  We simply duplicate comment
; strings, but for declare forms we allow rewriting to occur.

(defun instance-decls (decls subs)
  (if (endp decls)
      nil
    (if (pseudo-termp (car decls))
	(cons (instance-rewrite (car decls) subs)
	      (instance-decls (cdr decls) subs))
      (cons (car decls)
	    (instance-decls (cdr decls) subs)))))


; For the defun itself, we retain the same defun symbol (e.g., defun
; or defund), but we change the name and args of the function by first
; creating the list '(oldname oldarg1 oldarg2 ...) then applying our
; substitutions to the new function.
;
; As a trivial example, 
;  (instance-defun '(defun f (x) (+ x 1)) '(((f x) (g x))))
;    =>
;  (defun g (x) (+ x 1))

(defun instance-defun (defun subs)
  (let* ((defun-symbol  (first defun))
 	 (defun-name    (second defun))
	 (defun-args    (third defun))
         (defun-decls   (butlast (cdddr defun) 1))
	 (defun-body    (car (last defun)))
	 (name/args     (cons defun-name defun-args))
	 (new-body      (instance-rewrite defun-body subs))
	 (new-name/args (instance-rewrite name/args subs))
	 (new-decls     (instance-decls defun-decls subs))
	 (new-name      (car new-name/args))
	 (new-args      (cdr new-name/args)))
    `(,defun-symbol 
       ,new-name ,new-args 
       ,@new-decls
       ,new-body)))

; We also provide a convenience function that allows you to instance
; a list of defuns.

(defun instance-defuns (defun-list subs)
  (if (endp defun-list)
      nil
    (cons (instance-defun (car defun-list) subs)
	  (instance-defuns (cdr defun-list) subs))))



; Renaming theorems

(defun defthm-names (event-list)
  (if (endp event-list)
      nil
    (let* ((first-event (car event-list))
	   (event-type  (first first-event)))
      (cond ((or (eq event-type 'defthm)
		 (eq event-type 'defthmd))
	     (cons (second first-event)
		   (defthm-names (cdr event-list))))
	    ((eq event-type 'encapsulate)
	     (append (defthm-names (cddr first-event))
		     (defthm-names (cdr event-list))))
	    (t (defthm-names (cdr event-list)))))))

(defun create-new-names (name-list suffix)
  (if (endp name-list)
      nil
    (acons (car name-list)
	   (intern-in-package-of-symbol (string-append (symbol-name (car name-list))
						       (symbol-name suffix))
					suffix)
	   (create-new-names (cdr name-list) suffix))))
	
(defun rename-defthms (event-list suffix)
  (sublis (create-new-names (defthm-names event-list) suffix)
	  event-list))



; Instantiating Theorems
;
;
; To instantiate defthms, we will want to be able to provide
; functional instantiations of the generic theory.  This is much
; more complicated than instancing definitions, and involves:
;
;   a) determining what functional substitutions to make
;   b) determining the theory in which to conduct the proofs 
;   c) handling rule classes and other optional components
;   d) generating the actual defthm event
;
; My idea is essentially that if a substitution list can be used for
; functionally instantiating theorems, then it can also be used for 
; creating the new theorem.
;
; (a) Determining what functional substitutions to make.
;
; I pass in a list of substitutions of the following form.
;
;   (((predicate ?x)  (not (in ?x y)))
;    ((all ?x)        (all-not-in ?x y))
;    ((exists ?x)     (exists-not-in ?x y)))
; 
; From this list we can generate the functional instantiation hints.
; So, for example, we simply convert ((predicate ?x) (not (in ?x y)))
; into the substitution:
;
;   (predicate (lambda (?x) (not (in ?x y))))
;
; This is easy to do with the following functions:

(defun sub-to-lambda (sub)
  (let ((term (first sub))
	(repl (second sub)))
    (let ((function-symbol (car term))
	  (lambda-args (cdr term)))
      `(,function-symbol (lambda ,lambda-args ,repl)))))

(defun subs-to-lambdas (subs)
  (if (endp subs)
      nil
    (cons (sub-to-lambda (car subs))
	  (subs-to-lambdas (cdr subs)))))


; (b) Determining the theory in which to conduct the proofs.
;
; When we prove the functional instantiation constraints, ideally we
; should work in an environment where the only definitions that are
; enabled are the definitions used in the functional instantiation 
; hints.  
;
; Well, the definitions we need are (almost) simply all of the
; function symbols in the right-hand side of the substitution list.
; In other words, for the above substitutions, I would want to have
; the definitions of not, in, all-not-in, and exists-not-in available.
;
; Now, the problem with this approach is, what if those symbols don't
; have definitions?  This can occur if, for example, we are using a
; constrained function in the substitution list.  This is actually
; useful, e.g., for substituting (predicate ?x) -> (not (predicate
; ?x)).  
;
; My solution is a stupid hack.  We simply pass in the names of the 
; generic functions for which we do not want to generate definitions
; along with the substitutinos.
;
; To begin, the following function will extract all function symbols
; that occur within a term.

(mutual-recursion 

  (defun term-functions (term)
    (if (atom term)
        nil
      (cons (car term) 
	    (term-list-functions (cdr term)))))

  (defun term-list-functions (list)
    (if (endp list)
	nil
      (append (term-functions (car list))
	      (term-list-functions (cdr list)))))
)

; Next, I wrote the following function, which walks over the
; substitution list and extracts the function symbols from each right
; hand side, using term-functions.  The net result is the list of all
; functions that were used in replacements.
  
(defun subs-repl-functions (subs)
  (if (endp subs)
      nil
    (let* ((sub1 (car subs))
	   (repl (second sub1)))
      (append (term-functions repl)
	      (subs-repl-functions (cdr subs))))))

; Given the above, we could then convert the list of function symbols 
; into a list of (:definition f)'s with the following function.
   
(defun function-list-to-definitions (funcs)
  (if (endp funcs)
      nil
    (cons `(:definition ,(car funcs))
	  (function-list-to-definitions (cdr funcs)))))

; And finally, here is a function that does "all of the work", calling
; function-list-to-definitions for all of the functions found in the
; substitution list, minus all of the generic functions that we don't
; want to generate :definition hints for.

(defun subs-to-defs (subs generics)
  (let* ((all-fns (subs-repl-functions subs))
	 (real-fns (set-difference-eq all-fns generics)))
    (function-list-to-definitions real-fns)))


; (c) Handling rule classes and other optional components.
;
; We are interested in several parts of a defthm.  In addition to the
; conjecture itself, we need to consider the rule-classes used by the
; theorem, and the other optional attributes such as the :hints, :doc,
; :otf-flg, etc.  We parse these attributes into a five-tuple of pairs
; of the form (present . value), where present is a boolean that says
; whether or not the flag has been seen, value is its value, and the
; order of the elements is rule-classes, instructions, hints, otf-flg,
; and finally doc.  We parse these options with the following code:

(defconst *default-parse-values* 
  '((nil . nil) (nil . nil) (nil . nil) (nil . nil) (nil . nil)))

(defun parse-defthm-option (option return-value)
  (cond ((equal (first option) :rule-classes)
         (update-nth 0 (list t (second option)) return-value))
	((equal (first option) :instructions)
	 (update-nth 1 (list t (second option)) return-value))
	((equal (first option) :hints)
	 (update-nth 2 (list t (second option)) return-value))
	((equal (first option) :otf-flg)
	 (update-nth 3 (list t (second option)) return-value))
	((equal (first option) :doc)
	 (update-nth 4 (list t (second option)) return-value))
	(t (er hard "Unknown flag in defthm options ~x0." (first option)))))

(defun parse-defthm-options (options return-value)
  (if (endp options)
      return-value
    (parse-defthm-options (cddr options)
			  (parse-defthm-option options return-value))))


; (d) Generating the actual defthm event.
;
; When we are ready to instance a defthm event, we combine the above
; work with a few new things.  First of all, we need the original
; theorem event, a new name to use, the substitutions to use, and the
; list of generic function symbols in use so that we do not create
; (:definition f) entries for them.
;
; We begin by making our substitutions in the body of the theorem.  We
; then parse the optional components of the defthm, but we only are
; interested in the rule-classes.  (Hints, instructions, and otf-flg
; will not be needed, because we will be proving this via functional
; instantiation.  Doc we ignore for no good reason.)  We construct a
; new theorem that has our new name and body, replicating the rule
; classes if necessary.  We also provide a functional instantiation
; hint of the generic theorem's name, along with a list of lambda
; substitutions to make.

(defun instance-defthm (event new-name subs generics extra-defs)
  (let* ((defthm-symbol (first event)) 
	 (defthm-name   (second event))
	 (defthm-body   (third event))
	 (new-body      (instance-rewrite defthm-body subs))
	 (options       (parse-defthm-options (cdddr event) 
					      *default-parse-values*))
	 (rc-opt        (first options)))
    `(,defthm-symbol ,new-name 
       ,new-body
       :hints(("Goal"
	       :use (:functional-instance ,defthm-name
					  ,@(subs-to-lambdas subs))
	       :in-theory (union-theories (theory 'minimal-theory)
			   (union-theories ',extra-defs
					   ',(subs-to-defs subs generics)))))
       ,@(if (car rc-opt) `(:rule-classes ,(cdr rc-opt)) nil))))



; Instantiating Encapsulates
;
;
; There are two reasons that I typically use encapsulation.  The first
; is as a purely structural/organizational purpose, where I am trying
; to prove some theorem is true, but I need some lemmas to do so.  In
; this case I use an (encapsulate nil ...) and wrap my lemmas in local
; forms.  The other reason is to actually go ahead and introduce
; constrained functions.
;
; Two strategies will be necessary for handling these situations.  In
; particular, if we are in an encapsulate which has no constrained
; function symbols, we will want to skip all local events and only add
; the non-local events (using functional instantiation to create the
; theorems).  On the other hand, for the case when we are introducing
; constrained functions, we will want to introduce new constrained 
; functions based on the encapsulate.
;
; So, encapsulates are handled separately based on whether or not any
; functions are constrained.
;
; Within an (encapsulate nil ...), local events will be skipped and
; defthm events will be proven using the functional instantiation of
; their generic counterparts.
;
; Within an (encapsulate (...) ...), local events will not be skipped
; but will instead be reintroduced with new names.  Further, defthm
; events will be copied using new names and will not be proven using
; functional instantiation.
;
; The only "extra" thing we really need for handling encapsulates is a
; system to make the substitutions within the signatures.  We do that
; here by simple rewriting.  Note that we do not allow the number of
; return values to change.  I don't really think of this as a major
; limitation, since almost always my constrained functions return a 
; single value.  If you have an example of where this would be useful,
; it would be interesting to see it.

(defun instance-signature (signature subs)
  (let ((name (first signature))
	(rest (rest signature)))
    (cons (instance-rewrite subs name) rest)))

(defun instance-signatures (signatures subs)
  (if (endp signatures)
      nil
    (cons (instance-signature (car signatures) subs)
	  (instance-signatures (cdr signatures) subs))))

; Because encapsulates can contain many events within them, it is
; natural to make them mutually recursive with the main event list
; handler, which we are now ready to introduce.





; Instantiating Entire Theories
;
; 
; We are now ready to introduce the functions which will walk through
; a theory and call the appropriate instancing functions on each of 
; the forms we encounter.  To support encapsulation, our functions 
; here are all mutually recursive.
;
; The arguments that we pass around are the following:
;
;   - The event or event list to instantiate 
;
;   - The global list of substitutions used to derive the instance
;
;   - A suffix which will be appended to generate new names
;
;   - A list of generic functions which have no definitions
;
;   - A mode, which is either 'constrained to indicate that the
;     nearest encapsulate event has constrained functions, or is nil
;     to indicate that the nearest encapsulate is merely a structural
;     wrapper for local lemmas.
;
; Finally, we overload our behavior based on suffix, so that if no 
; suffix is given, we simply replicate the generic theory instead 
; of instantiating a concrete instance of it.


(mutual-recursion

  (defun instance-event (event subs suffix generics mode extra-defs)
    (if (null suffix)
	event
      (cond ((or (eq (car event) 'defun)
		 (eq (car event) 'defund))
	     (instance-defun event subs))
	    ((or (eq (car event) 'defthm)
		 (eq (car event) 'defthmd))
	     (let* ((name (second event))
		    (new-name (intern-in-package-of-symbol
			       (string-upcase 
				(concatenate 'string 
					     (symbol-name name)
					     (symbol-name suffix)))
			       suffix)))
	       (instance-defthm event new-name subs generics extra-defs)))
	    ((equal (car event) 'local)
	     (if (eq mode 'constrained)
		 (instance-event (second event) subs suffix generics mode extra-defs)
	       nil))
	    ((equal (car event) 'encapsulate)
	     (instance-encapsulate event subs suffix generics mode extra-defs))
	    (t (er hard "Don't know how to handle ~x0" (car event))))))

  (defun instance-event-list (events subs suffix generics mode extra-defs)
    (if (endp events)
	nil
      (let ((first (instance-event (car events) subs suffix generics mode extra-defs))
	    (rest  (instance-event-list (cdr events) subs suffix generics mode extra-defs)))
	(if first 
	    (cons first rest)
	  rest))))

  (defun instance-encapsulate (event subs suffix generics mode extra-defs)
    (declare (ignore mode))
    (let* ((signatures (second event))
	   (new-sigs   (if signatures 
			   (instance-signatures subs signatures)
			 nil))
	   (new-events (instance-event-list (cddr event) subs suffix generics
					    (if signatures 
						'constrained
					      nil)
					    extra-defs)))
      `(encapsulate ,new-sigs ,@new-events)))

)


; To be able to actually introduce the events, we need to emit a macro that
; can be used to actually perform substitutions.

(defmacro instance (theory)
  (let ((macro-name (intern-in-package-of-symbol
		     (string-upcase (concatenate 'string 
						 "instance-" (string theory)))
		     theory)))
    `(defmacro ,macro-name (&key subs suffix generics extra-defs)
       (list* 'encapsulate 
	      nil
	      (instance-event-list ,theory subs suffix generics nil extra-defs)))))




; Some thoughts
;
; A fundamental issue seems to be that a function and its arguments
; are not always used in a consistent manner.  For example, say we
; want to rewrite (all ?x) to (all-foo ?x y) and we want to rewrite
; (predicate ?x) to (not (foo ?x y)).  How can we accurately say just
; what it is that we want to rewrite in each case?
;
; Right now our substitutions are based on 
;  ( (predicate ?x)  (not (foo ?x y)) )
;  ( (all ?x)        (all-foo ?x y) )
;
; We can easily pick out and say "all" is replaced by "all-foo", 
; but if we try to just use the car of the term as its symbol
; replacement, then "predicate" would be "not".  
;
; OK, so we could do some kind of preprocessing step where we fill
; in argument guards.  The "generics" list right now is a big huge
; hack that allows us to ignore the fact that :predicate doens't
; have a definition.  Really the issue that this is trying to solve
; is to tell us how to build our :in-theory event.  Right now the 
; :in-theory event is just a hack that we don't really understand.