;;; $Id: pvs-status-smiley.el,v 1.3 2011-09-20 12:25:12 tews Exp $
;;;
;;; This package examines a PVS Status buffer and inserts smileys
;;; as comments before the lemmas in the PVS sources to indicate
;;; their proof status.
;;;
;;; Author: Hendrik Tews <hendrik@askra.de>
;;;
;;; Installation:
;;;   Place this file somewhere and add the following lines
;;;   to your .emacs or .pvsemacs:
;;;
;;;       (add-to-list 'load-path
;;;       	     (expand-file-name "~/directory/to/pvs-status-smiley"))
;;;       
;;;       (autoload 'clean-pvs-proof-status "pvs-status-smiley"
;;;         "Clean up PVS proof smileys" t nil)
;;;       (autoload 'pvs-status-annotate-source "pvs-status-smiley"
;;;         "Add PVS proof status smileys" t nil)
;;;
;;;   Edit the config section below to your liking.
;;;
;;; Usage:
;;;
;;;   To annotate your lemmas with proof status smileys:
;;;
;;;     - obtain a PVS Status buffer (prove-pvs-file, *-importchain, status-*)
;;;     - M-x pvs-status-annotate-source
;;;
;;;     You can edit the PVS Status buffer as long as you keep the
;;;     theory headers intact. For instance delete some theories or lemmas.
;;;     You will get an error if some source file is not typechecked.
;;;     Proof status smileys that are found within pvs-status-line-distance
;;;     of the lemma will be replaced. Otherwise a new smiley is inserted.
;;;     Smileys for non-existing proofs (eg. no longer existing TCCS) are
;;;     currently not deleted. See clean-pvs-proof-status.
;;;
;;;   To delete all smileys:     
;;;
;;;     M-x clean-pvs-proof-status
;;;
;;;
;;; Known Bugs:
;;;
;;;   - TCC's for the theory header cause parts of the theory header to
;;;     to be copied before the status smiley comment, thus making the
;;;     file syntactically incorrect.
;;;
;;; License: Copyright (C) 2006-2011 Hendrik Tews
;;;   
;;;   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.


;;; Config Section


;; Regexp matching a proof status smiley line
(setq pvs-status-line "^ *% proof status :-")


;; Format template for a TCC name comment below the smiley line for
;; the TCC. Used as  (format pvs-status-TCC-template tcc-name).
;; Should contain one ``$s'' to be substituted with the TCC name.
;; Insert ``%%'' for a literal ``%''.
(setq pvs-status-TCC-template "%% %s : TCC Obligation")


;; Function mapping the proof status to the text inserted
;; as proof status smiley. Before this function is called a new line
;; is inserted and filled with the current indentation.
(defun pvs-insert-status (status)
  (insert "% proof status ")
  (cond
   ((eq status 'unfinished)
    (insert ":-( unfinished"))
   ((eq status 'unchecked)
    (insert ":-( unchecked"))
   ((eq status 'untried)
    (insert ":-( untried"))   
   ((eq status 'incomplete)
    (insert ":-) incomplete"))
   ((eq status 'complete)
    (insert ":-)"))
   (t (error "Unknown status in pvs-insert-status"))))


;; (defun pvs-insert-status (status)
;;   (insert "% proof status ")
;;   (cond
;;    ((eq status 'unfinished)
;;     (insert ":-( unfinished"))
;;    ((eq status 'unchecked)
;;     (insert ":-( unchecked"))
;;    ((eq status 'untried)
;;     (insert ":-( untried"))   
;;    ((eq status 'incomplete)
;;     (insert ":-) incomplete"))
;;    ((eq status 'complete)
;;     (insert ":-)"))
;;    (t (error "Unknown status in pvs-insert-status"))))


;; Set to t insert smileys for new TCC's. If nil only existing TCC smileys
;; will be updated
(setq pvs-status-insert-TCC-status t)


;; Number of lines to search backward for the smiley. More precisely,
;; starting from the line containing the lemma name
;; (or pvs-status-TCC-template for TCC's), if pvs-status-line-distance
;; lines before that a smiley is found, then this smiley will be updated
;; for this lemma or TCC. If no smiley is found within that distance a
;; new one will be inserted.
(setq pvs-status-line-distance 2)


;;; End of Config Section



;; match a theory start in the PVS Status buffer
(setq pvs-status-theory-regexp
      "Proof summary for theory \\([A-Za-z][A-Za-z0-9_?]*\\)")

;; extract all lemmas with their status from a PVS Status buffer
(defun extract-lemma-status ()
  (let ((theory-start (point-min))
	theory-end theory-name lemma-list)
    (save-excursion
      (while 
	  (progn
	    (goto-char theory-start)
	    (re-search-forward pvs-status-theory-regexp nil t))
	(setq theory-name (match-string 1))
	(when (not (theory-saved-and-typechecked-p theory-name))
	  (error "Theory %s not typechecked" theory-name))
	(unless (re-search-forward pvs-status-theory-regexp nil t)
	  (goto-char (point-max)))
	(beginning-of-line)
	(setq theory-end (point))
	(narrow-to-region theory-start theory-end)
	(goto-char (point-min))
	(while (re-search-forward
		"^    \\([A-Za-z][A-Za-z0-9_?]*\\)\\.+" nil t)
	  (let ((lemma-name (match-string 1))
		lemma-status)
	    (setq lemma-status
		  (cond
		   ((looking-at "unfinished") 'unfinished)
		   ((looking-at "unchecked") 'unchecked)
		   ((looking-at "untried") 'untried)
		   ((looking-at "proved - incomplete") 'incomplete)
		   ((looking-at "proved - complete") 'complete)
		   (t (progn
			(widen)
			(error "Unknown proof status at line %d"
			       (count-lines (point-min) (point)))))))
	    (setq lemma-list
		  (cons (list lemma-name theory-name lemma-status)
			lemma-list))
	    ))
	(widen)
	(setq theory-start theory-end))
      lemma-list)))


;; extract a declaration within theory-name from the declaration list
;; returned from pvs find-declaration
(defun declaration-list-select-theory (decls theory-name)
  (while 
      (and decls
	   (not (equal theory-name
		       (nth 2 (car decls)))))
    (setq decls (cdr decls)))
  (if decls
      (list (nth 3 (car decls))
	    (car (nth 4 (car decls)))
	    (cadr (nth 4 (car decls))))
    nil))
      

;; find lemma-name in theory theory-name, create an emacs marker at the
;; lemma position, determine if it is a TCC or a lemma and return the
;; list (lemma-name theory-name lemma-status TCC-or-lemma marker)
(defun add-lemma-position (lemma-name theory-name lemma-status)
  (let* ((decls
	  (pvs-file-send-and-wait 
	   (format "(find-declaration \"%s\")" lemma-name)
	   nil 'listing 'list))
	 (decl (declaration-list-select-theory decls theory-name))
	 file-pos decl-type)
    (if decl 
	(setq
	 decl-type 'lemma
	 file-pos decl)
      ; lemma-name refers to a TCC ?
      (let* ((parts (split-string lemma-name "_"))
	     (last (nth (- (length parts) 1) parts))
	     oid)
	(if (equal "TCC" (substring last 0 3))
	    (progn
	      ;; yes, seeems to be a TCC
	      (setq oid
		    (substring lemma-name 0
			       (- (length lemma-name) (length last) 1)))
	      (setq decls
		    (pvs-file-send-and-wait 
		     (format "(find-declaration \"%s\")" oid)
		     nil 'listing 'list))
	      (setq decl (declaration-list-select-theory decls theory-name))
	      (if decl
		  (setq 
		   decl-type 'TCC
		   file-pos decl))))))
    (if file-pos
	(save-excursion
	  (set-buffer (get-pvs-file-buffer (car file-pos)))
	  (save-excursion
	    (save-restriction
	      (widen)
	      (goto-line (cadr file-pos))
	      (forward-char (nth 2 file-pos))
	      (list lemma-name theory-name lemma-status
		    decl-type (point-marker)))))
      (error "Cannot find %s in theory %s" lemma-name theory-name))))


;; insert a smiley for the lemma/TCC name at position marker
(defun find-lemma-insert-status (name theory-name status decl-type marker)
  (let ((search-back-for-status t)
	(do-insert-status t)
	indent-string
	start-of-lemma-line)
    (save-excursion
      (set-buffer (marker-buffer marker))
      (save-excursion
	(save-restriction
	  (widen)
	  (goto-char marker)
	  (beginning-of-line)
	  (setq start-of-lemma-line (point))
	  (setq indent-string (buffer-substring start-of-lemma-line marker))
	  (cond
	   ((eq decl-type 'lemma) t)
	   ((eq decl-type 'TCC)
	    (if (search-backward (format pvs-status-TCC-template name) nil t)
		(progn
		  (beginning-of-line)
		  (setq start-of-lemma-line (point)))
	      ;; TCC decl not present yet
	      (if pvs-status-insert-TCC-status
		  (progn
		    (goto-char start-of-lemma-line)
		    (if (re-search-backward "^[[:blank:]]*$" nil t)
			(progn
			  (beginning-of-line)
			  (insert "\n"
				  indent-string
				  (format pvs-status-TCC-template
					  name)
				  "\n")
			  (forward-line -1)
			  (setq start-of-lemma-line (point))
			  (setq search-back-for-status nil))
		      (message "Insert status of %s failed" name)
		      (setq search-back-for-status nil)
		      (setq do-insert-status nil)))
		(setq search-back-for-status nil)
		(setq do-insert-status nil)))))
	  (if (and search-back-for-status
		   (re-search-backward pvs-status-line nil t))
	      (progn
		(beginning-of-line)
		(if (<= (count-lines (point) start-of-lemma-line)
			pvs-status-line-distance)
		    ;; found
		    (delete-region (point)
				   (progn
				     (forward-line 1)
				     (point)))
		  ;; not found - move back
		  (goto-char start-of-lemma-line)))
	    ;; not found - move back
	    (goto-char start-of-lemma-line))
	  (if do-insert-status
	      (progn
		(insert "\n")
		(forward-line -1)
		(insert indent-string)
		(pvs-insert-status status))))))))


;; reset marker to increase emacs performance
(defun clear-marker (name theory-name status decl-type marker)
  (set-marker marker nil))


;; check if theory is saved and typechecked
(defun theory-saved-and-typechecked-p (theory)
  (let* ((fandp
	  (pvs-send-and-wait
	   (format "(and (get-theory \"%s\")
                      (file-and-place (get-theory \"%s\")))" 
		   theory theory)
	   nil nil 'list))
	 (buf (and fandp (find-buffer-visiting (car fandp)))))
    (and
     fandp
     (not (and buf (buffer-modified-p buf)))
     (typechecked-p theory))))


;; add smiley lines in the sources for everything in the PVS Status buffer
(defun pvs-status-annotate-source ()
  "Add proof status comments to all declarations from the `PVS Status' buffer.
The inserted comments contain
a smiley :-) or :-( depending on the proof status of the declaration
in question. For TCC's an additional comment line such as
\"xxx : TCC Obligation\" is inserted"
  (interactive)
  (let (status-list status-pos-list)
    (save-excursion
      (set-buffer "PVS Status")
      (setq status-list (extract-lemma-status)))
    (setq status-pos-list
	  (mapcar (lambda (args)
		    (apply 'add-lemma-position args)) status-list))
    (setq status-pos-list (nreverse status-pos-list))
    (mapc (lambda (args) (apply 'find-lemma-insert-status args))
	  status-pos-list)
    (mapc (lambda (args) (apply 'clear-marker args))
	  status-pos-list)))


;; delete all smiley lines
(defun clean-pvs-proof-status ()
  "Clean all proof status comments that have been inserted by `pvs-status-annotate-source'.
The deletion of those lines is regexp based, so use with care, because it
may also delete other (comment) lines"
  (interactive)
  (save-excursion
    (goto-char (point-min))
    (while (re-search-forward (format pvs-status-TCC-template ".*") nil t)
      (beginning-of-line)
      (delete-region (point) (progn (forward-line 2) (point))))
    (goto-char (point-min))
    (while (re-search-forward pvs-status-line nil t)
      (beginning-of-line)
      (delete-region (point) (progn (forward-line 1) (point))))))


;; delete all smiley lines in a set of files
(defun clean-pvs-proof-status-files (files)
  (let (buf
	(rest files))
    (while rest
      (save-excursion
	(set-buffer (get-pvs-file-buffer (car rest)))
	(clean-pvs-proof-status))
      (setq rest (cdr rest)))))

;; delete all smiley lines in some directory
(defun clean-pvs-proof-status-directory (dir)
  "Clean all proof status comments in directory DIR.
Calls `clean-pvs-proof-status' for all PVS files in directory DIR."
  (interactive "DClean PVS status smilies in directory: ")
  (clean-pvs-proof-status-files
   (directory-files dir t "\\.pvs$" nil)))