;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Some useful strategies
;; Cesar A Munoz (munoz@icase.edu)
;; ICASE July 2001

;; Extra-functions

;; Make sure you have manip-strategies in your pvs-strategies file

(setq count 0)

(defun newname (name)
  (progn (setq count (+ 1 count)) (format nil "~A_~A" name count))
)

(defun newnames (name l)
  (cond ((> l 0) (cons (newname name) (newnames name (- l 1))))
	(t NIL))
)

(defun listnames (name l)
  (cond (l (cons (format nil "~A_~A" name (car l))
		 (listnames name (cdr l))))
	(t NIL))
)

(defun expr2str (expr)
  (format nil "~A" expr)
)

(defun fromto (from to) 
  (cond 
   ((< from to) (cons from (fromto (+ from 1) to)))
   ((> from to) (cons from (fromto (- from 1) to)))
   (t (list to))))

(defun minlist (l)
  (eval (cons 'min l)))

(defun maxlist (l)
  (eval (cons 'max l)))

(defun remove-before (from fnums)
  (when fnums
    (if (equal from (car fnums))
	fnums
        (remove-before from (cdr fnums)))))
	       
(defun remove-after (to fnums)
  (when fnums
    (let ((a (car fnums)))
      (if (equal to a)
	  (list a)
          (cons a (remove-after to (cdr fnums)))))))

(defun listeqs (fnums from to)
 (when fnums
   (cond ((AND from to)
	  (remove-before from (remove-after to fnums)))
	 (from (remove-before from fnums))
	 (to   (remove-after to fnums))
	 (t fnums))))

(defun else-rewrite (names)
  (LET ((step (if (NOT names)
                  '(SKIP)
                  (let ((rewcar (if (atom (car names))
				    `(REWRITE ,(car names))
			  	    `(REWRITE ,(caar names)
					      :TARGET-FNUMS ,(cadr names)))))
		       `(ELSE ,rewcar
			      ,(else-rewrite (cdr names)))))))
       step)
)

(defun extra-get-formula (snum)
  (let ((fnum (if (stringp snum)
		  (let ((fnums (extra-map-fnums snum)))
		    (when fnums (car fnums)))
		  snum)))
    (when fnum
      (let ((index (- (abs fnum) 1))
	    (goal (current-goal *ps*)))
	(if (> fnum 0)
	    (formula (nth index (p-sforms goal)))
	  (argument (formula (nth index (n-sforms goal)))))))))

(defun extra-map-fnums (fnums)
  (cond ((numberp fnums) (list fnums))
	((OR (stringp fnums)(symbolp fnums))
	 (gather-fnums (s-forms (current-goal *ps*))
		       fnums nil true-predicate))
	((listp fnums) (when fnums (append (extra-map-fnums (car fnums))
					   (extra-map-fnums (cdr fnums)))))
	(t NIL)))

(defun insert-sorted (l e)
  (cond (l (cond ((equal (car l) e) l)
		 ((< (length (car l)) (length e)) (cons e l))
		 (t (cons (car l) (insert-sorted (cdr l) e)))))
	(t (list e)))
)

(defun is-math-expr (expr)
  (OR (is-term-operator expr '+)
      (is-term-operator expr '-)
      (is-term-operator expr '*)
      (is-term-operator expr '/)))

(defun get-distrib-plus (l expr)
  (cond ((is-term-operator expr '+)
	 (insert-sorted l (expr2str expr)))
	((is-term-operator expr '-)
	 (insert-sorted l (expr2str expr)))
	((is-term-operator expr '/)
	 (get-distrib-expr (get-distrib-expr l (args1 expr))
			   (args2 expr)))
	((is-term-operator expr '*)
	 (get-distrib-plus (get-distrib-plus l (args1 expr))
			   (args2 expr)))
	(t l))
)

(defun get-distrib-expr (l expr)
  (cond ((OR (is-term-operator expr '+)
	     (is-term-operator expr '-)
	     (is-term-operator expr '/)
	     (is-term-operator expr '=)
	     (is-term-operator expr '<)
	     (is-term-operator expr '>)
	     (is-term-operator expr '<=)
	     (is-term-operator expr '>=))
	 (get-distrib-expr (get-distrib-expr l (args1 expr))
			   (args2 expr)))
	((is-term-operator expr '*)
	 (get-distrib-plus (get-distrib-plus l (args1 expr))
			    (args2 expr)))
	(t l))
)

;; Extra-tegies

(defstep REAL-PROPS (&optional (where '*))
  (THEN (auto-rewrite-theory "real_props" :defs NIL)
	(ASSERT where)
	(stop-rewrite-theory "real_props"))
  "Applies real_props and nothing else"
  "~%Applying real_props"
)

(defstep LOOP (n step)
  (IF (<= n 0)
      (SKIP)
      (LET ((m (- n 1)))
	   (THEN step (LOOP m step))))
  "Repeats step n times"
  "~%Repeating ~A times ~A"
)

(defstep LABEL* (tags fnums)
  (LET ((tag     (when tags (car tags)))
	(tagrest (when tags (cdr tags)))
	(fnum    (when fnums (car fnums)))
	(rest    (when fnums (cdr fnums))))
       (IF (AND tag fnum)
	   (IF tagrest
	       (THEN (LABEL tag fnum) (LABEL* tagrest rest))
	       (LABEL tag fnums))
	   (SKIP)))
  "Labels a collection of fomulas using a collection of labels"
  "Labeling with labels ~A formulas ~A"
)
       
(defstep CUT (fnum)
  (LET ((formula (extra-get-formula fnum))
        (step 
           (cond ((AND (> fnum 0) (conjunction? formula))
                  `(THEN (CASE ,(args1 formula)) (BDDSIMP)))
                 ((AND (< fnum 0) (disjunction? formula))
                  `(THEN (CASE ,(format nil "NOT(~A)" (args1 formula)))
			 (BDDSIMP)))
                 (t '(SKIP)))))
       step)
  "Cuts a conjunction in the consequent or a disjunction in the antecedent"
  "~%Cutting a conjunction (consequent) or a disjunciton (antecedent) in ~A"
)

(defstep REPLACE-ASSERT (&optional fnum (where '*) (hide? t) (dir 'LR)
			      (step '(ASSERT)))
  (LET ((fn (if fnum fnum (car (get-equalities)))))
       (TRY (REPLACE fn where :hide? hide? :dir dir)
	    step
	    (SKIP)))
  "Replaces formula FNUM in formulas WHERE (parameters as in REPLACE), then STEP. If FNUM is not provided, then it takes the first equality"
  "~%Replacing and asserting"
)

(defstep REPLACE-LABEL* (&optional flabels
				   (where '*) (hide? t) (dir 'LR)
				   (step '(ASSERT)))
  (IF flabels
      (LET ((fnum   (when flabels (car flabels)))
	    (frest  (when flabels (cdr flabels))))
	   (THEN  (REPLACE-ASSERT fnum :where where :hide? hide?
				  :dir dir :step step)
		  (REPLACE-LABEL* frest :where where :hide? hide?
				  :dir dir :step step)))
      (SKIP))
  "Applies REPLACE-ASSERT repeatedly with labeled equalities"
  "~%Using REPLACE-ASSERT repeatedly"
)

(defstep REPLACE-ASSERT* (&optional (fnums '*) from to
				    (where '*) (hide? t) (dir 'LR)
				    (step '(ASSERT)))
  (LET ((flist (if (equal fnums '*)
		   (get-equalities)
		   (remove-if-not #'(lambda (x) (< x 0))
				  (extra-map-fnums fnums))))
	(feqs  (listeqs flist from to)))
       (IF feqs
	   (LET ((newnames (listnames "EQ" feqs)))
		(THEN (LABEL* newnames feqs)
		      (REPLACE-LABEL* newnames :where where
				      :hide? hide? :dir dir
				      :step step)
		      (UNLABEL newnames)))
	   (SKIP)))
  "Applies REPLACE-ASSERT repeatedly with equalities in FNUMS"
  "~%Using REPLACE-ASSERT repeatedly"
)

(defstep REWRITE-NAMES (names)
  (LET ((step (else-rewrite names)))
       step)
  "Rewrites with a list of NAMES. A NAME can be name-lema OR (name-lema FNUMS)"
  "~%Rewriting with ~A"
)

(defstep REWRITE* (names)
  (REPEAT (REWRITE-NAMES names))
  "Rewrites recursively REWRITE-NAMES. NAMES as in REWRITE-NAMES"
  "~%Rewriting recursively with ~A"
)

(defstep NAME-REPLACE-LABEL (name expr label)
  (BRANCH (NAME-REPLACE name expr :hide? NIL)
	  ((LABEL label -1)
	   (SKIP)))
  "Uses NAME, REPLACE, AND LABEL to abbreviate an expression with a newly chosen name and label"
  "~%REPLACING ~A for ~A with label ~A"
)
  
  
(defstep NAME-REPLACE-LABEL* (name-and-exprs label &optional count)
  (IF name-and-exprs
      (LET ((name (car  name-and-exprs))
	    (expr (cadr name-and-exprs))
	    (rest (cddr name-and-exprs))
	    (nc   (when count (+ count 1)))
	    (tag  (if count
		      (format nil "~A.~A" label count)
		      label)))
	   (THEN (NAME-REPLACE-LABEL name expr tag)
		 (NAME-REPLACE-LABEL* rest label nc)))
      (SKIP))
  "Iterates NAME-REPLACE-LABEL"
  "~%Iterating NAME-REPLACE-LABEL with ~A"
)

(defstep SQ-SIMP ()  
  (REWRITE* ("sq_neg" "sq_times" "sq_plus" "sq_minus" "sq_0"
  	     "sq_div" "sqrt_0" "sqrt_1" "sqrt_def" "sqrt_square"
             "sqrt_sq" "sq_sqrt" "sqrt_times" "sqrt_div"))
  "Simplifies sq and sqrt"
  "~%Simplifying sq and sqrt"
) 

(defstep REPLACE-DIST (fnum &optional (label "RD"))
  (LET ((form    (extra-get-formula fnum))
	(dist    (get-distrib-expr NIL form))
	(l       (length dist))
	(names   (when dist (newnames label l)))
	(eqs     (when dist (fromto -1 (- l))))
	(nameseq (when dist (merge-names-exprs names dist))))
       (NAME-REPLACE-LABEL* nameseq label))
  "Introduces new names to avoid the application of distributive laws"
  "~%Introducing new names in ~A"
)

(defstep REPLACE-DIST* (&optional (fnums '*) (label "RD"))
  (LET ((forms (extra-map-fnums fnums))
	(fnum  (when forms (car forms)))
	(rest  (when forms (cdr forms))))
       (IF forms
	   (THEN (REPLACE-DIST fnum label)
		 (REPLACE-DIST* rest label))
	   (SKIP)))
  "Iterates REPLACE-DIST on several formulas"
  "~%Iterating REPLACE-DIST"
)

(defstep GRIND-REALS ()
  (TRY (REPLACE-DIST* :label "GR")
       (THEN (GRIND :defs NIL :theories "real_props")
	     (REPLACE-ASSERT* "GR" :dir RL))
       (GRIND :defs NIL :theories "real_props"))
   "Applies GRIND with real-props everywhere, avoiding distributive laws"
   "Applying GRIND-REALS"
)