;; emacs support for rsltc tool ;; Chris George, UNU/IIST, March 1999 ;; Based heavily on compile.el (require 'compile) ;; include directory where rsltc is located if not on path (defvar rsltc-command (if (eq system-type 'windows-nt) "C:\\raise\\rsl\\rsltc" "rsltc") "RSL type checker") ;; set this to vcg command (probably no "x" in Windows, and may need path) ;; like "c:\\raise\\vcg\\bin\\vcg" (defvar vcg-command (if (eq system-type 'windows-nt) "C:\\raise\\vcg\\bin\\vcg" "xvcg") "Command to run vcg") (defvar RSL-entity-regexp "\\<\\(scheme\\|object\\|theory\\|devt_relation\\|hint\\)\\>" "Regular expression for keyword starting an RSL entity.") (defvar RCS-regexp "[ \t]*--[ \t]*\\$Id:" "Regular expression for start of RCS data.") (defvar rsl-line-comment-regexp "[ \t]*--" "Start of line comment") (defvar rsl-block-comment-start-regexp "/\\*" "Start of block comment") (defvar rsl-block-comment-end-regexp "\\*/" "End of block comment") (defvar rsl-context-regexp "[-a-zA-Z0-9_./]+" "Context entry.") (defvar RSL-basename nil "Base name of RSL file") (defvar RSL-process nil "Process created by rsl command, or nil if none exists now. Note that the process may have been \"deleted\" and still be the value of this variable.") (defvar RSL-buffer nil "Buffer containing RSL.") (defvar rsltc-error-regexp "^\\([a-zA-Z][^.]*\\.rsl\\):\\([0-9]+\\):\\([0-9]+\\):" "Regular expression for file, line and column in rsltc error output.") (defun rsltc (params) "Run RSL type checker" (interactive "sCommand line arguments: ") (if (buffer-modified-p) (save-buffer)) (setq RSL-basename (file-name-sans-extension (file-name-nondirectory (buffer-file-name)))) (compile (concat rsltc-command " " params " " RSL-basename))) (defun rslpp (len-str) "Run RSL pretty printer on file in current buffer" (interactive "sLine length (default 60): ") (let ((len (if (string-equal len-str "") 60 (string-to-int len-str)))) (delete-other-windows) ; prevent old error messages still being visible (rsl-do (format "%s -p -pl %d " rsltc-command len) 'end-pp-ok))) (defun end-pp-ok (buff) (save-excursion (set-buffer buff) (copy-to-buffer RSL-buffer (point-min) (point-max)) (message "Pretty printed: C-x u to undo"))) (defun rslgg () "Make dependency graph of file in current buffer and display" (interactive) (rsl-do (concat rsltc-command " -g ") 'end-gg-ok)) (defun end-gg-ok (buff) (call-process shell-file-name nil 0 nil "-c" (concat vcg-command " " RSL-basename ".vcg"))) (defun rsltc-and-sml () "Translate to sml and run sml if no errors" (interactive) (rsl-do (concat rsltc-command " -m ") 'end-sml-ok)) (defun end-sml-ok (buff) (rsl-sml-load)) (defun rsl-do (command post-fun) "Run COMMAND (which must end with a space) on RSL-basename and if successful then run post-fun with shell output buffer name as argument." (if (buffer-modified-p) (save-buffer)) (setq RSL-basename (file-name-sans-extension (file-name-nondirectory (buffer-file-name)))) (setq RSL-buffer (current-buffer)) (if (get-buffer " *rslbuff*") (kill-buffer " *rslbuff*")) (let ((status (call-process shell-file-name nil (get-buffer-create " *rslbuff*") nil "-c" (concat command RSL-basename)))) (if (and (numberp status) (or (zerop status) ;; strange status returned with Cygwin bash (and (string= shell-file-name "bash") (= status 131072)))) (apply post-fun (list " *rslbuff*")) (end-RSL-error " *rslbuff*")))) (defun end-RSL-error (buff) (set-buffer buff) (goto-char (point-min)) (if (re-search-forward rsltc-error-regexp nil t) ;; Extract line and column number from error message. (let ((filename (buffer-substring (match-beginning 1) (match-end 1))) (linenum (string-to-int (buffer-substring (match-beginning 2) (match-end 2)))) (colnum (string-to-int (buffer-substring (match-beginning 3) (match-end 3))))) ;; Go to RSL buffer and find the erring line. (set-buffer RSL-buffer) (if (not (string-equal (buffer-file-name) filename)) (find-file filename)) (goto-char (point-min)) (forward-line (1- linenum)) (forward-char (1- colnum)) (message (format "Error here: %s: line %d, column %d" filename linenum colnum))) ;; something else ;; just show rsltc output (switch-to-buffer-other-window buff))) ;; support error reports in RSL comments (setq compilation-error-regexp-alist (cons '( "[ \t]*(*-- \\([a-zA-Z0-9_/.]+\\):\\([0-9]+\\):\\([0-9]+\\):" 1 2 3) compilation-error-regexp-alist)) ;; additions for emacs-based mkdoc ------------------ (defun mkdoc () "Creates .tex files from \RAISEIN, \RAISEINFRAME, and \RAISEINBOX commands" (interactive) (let ((save-case-fold-search case-fold-search) (save-point (point))) (goto-char (point-min)) (setq case-fold-search nil) (while (re-search-forward "^\\\\\\(RAISEIN\\|RAISEINFRAME{[^}]*}\\|RAISEINBOX\\){\\([^}]*\\)}" nil t) (let ((rslfile (concat (buffer-substring (match-beginning 2) (match-end 2)) ".rsl")) (texfile (concat (buffer-substring (match-beginning 2) (match-end 2)) ".tex"))) (if (file-readable-p rslfile) (if (not (up-to-date texfile rslfile)) (save-excursion ;; uses a special buffer with a leading space in name ;; to avoid font-lock starting and slowing things down (if (get-buffer " *rslbuff*") (kill-buffer " *rslbuff*")) (setq rslfile (expand-file-name rslfile)) (setq texfile (expand-file-name texfile)) (let ((texbuffer (get-buffer-create " *rslbuff*"))) (set-buffer texbuffer) (insert-file rslfile) (goto-char (point-min)) (insert "\\RSLatex\n") (setq case-fold-search nil) (mark-context) (goto-char (point-max)) (backward-char 1) (if (looking-at "\n") (forward-char 1) (progn (forward-char 1) (insert "\n"))) (insert "\\endRSLatex\n") (do-latex) (write-region (point-min) (point-max) texfile) (kill-buffer texbuffer)))) (progn (setq case-fold-search save-case-fold-search) (error "RSL file %s cannot be found" rslfile))))) (setq case-fold-search save-case-fold-search) (goto-char save-point)) (message "mkdoc completed")) (defun up-to-date (texfile rslfile) "Returns t if TEXFILE exists and modified no earlier than RSLFILE." (and (file-readable-p texfile) (let ((tex-mod-time (nth 5 (file-attributes texfile))) (rsl-mod-time (nth 5 (file-attributes rslfile)))) (or (> (car tex-mod-time) (car rsl-mod-time)) (and (= (car tex-mod-time) (car rsl-mod-time)) (>= (car (cdr tex-mod-time)) (car (cdr rsl-mod-time)))))))) (defun mark-context () (re-search-forward (concat rsl-block-comment-start-regexp "\\|" rsl-line-comment-regexp "\\|" rsl-context-regexp) nil t) (if (string-match rsl-block-comment-start-regexp (buffer-substring (match-beginning 0) (match-end 0))) (progn (skip-block-comment 1) (mark-context)) (beginning-of-line) (if (looking-at rsl-line-comment-regexp) (progn (if (looking-at RCS-regexp) ;; do not include RCS data (let ((start (point))) (search-forward "$" nil nil 2) (forward-line 1) (delete-region start (point))) (forward-line 1)) (mark-context)) (if (not (looking-at (concat "[ \t]*" RSL-entity-regexp))) (let ((end-found nil)) (insert "\\CONTTWO{") (re-search-forward "[^ \t]") (while (not end-found) (re-search-forward "[ \t\n]+" nil t) (let ((p1 (match-beginning 0)) (p2 (match-end 0))) (if (looking-at ",") () (goto-char (1- p1)) (setq end-found (not (looking-at ","))) (goto-char p2)))) (backward-char 1) (insert "}")))))) (defun skip-block-comment (count) (while (> count 0) (if (re-search-forward (concat rsl-block-comment-start-regexp "\\|" rsl-block-comment-end-regexp) nil t) (progn (goto-char (match-beginning 0)) (if (looking-at rsl-block-comment-start-regexp) (setq count (1+ count)) (setq count (1- count))) (forward-char 2)) (error "Perhaps opening comment not closed"))) (if (looking-at rsl-line-comment-regexp) (forward-line))) ;; menu functions needed for rsl-mode (defun rsltc-only () "" (interactive) (rsltc "")) (defun rslpp-dflt () "" (interactive) (rslpp "")) (defun rsltc-c () "" (interactive) (rsltc "-c")) (defun rsltc-cc () "" (interactive) (rsltc "-cc")) (defun rsltc-d () "" (interactive) (rsltc "-d")) (defun rsltc-m () "" (interactive) (rsltc "-m")) ;; run sml after translation to sml (defun rsltc-m-and-run () "" (interactive) (rsltc-and-sml)) (defun rsltc-cpp () "" (interactive) (rsltc "-c++")) (defun rsltc-cppv () "" (interactive) (rsltc "-cpp")) (defun rsltc-sql () "" (interactive) (rsltc "-c++ -sql")) (defun rsltc-sqlv () "" (interactive) (rsltc "-cpp -sql")) (defun rsltc-pvs () "" (interactive) (rsltc "-pvs")) (defun rsltc-pc () "" (interactive) (rsltc "-pc")) (defun rsl-has-new-sml-file () (and (fboundp 'sml) (let* ((rslfile (buffer-file-name)) (smlfile (concat (file-name-sans-extension rslfile) ".sml"))) ; considered new enough if rsl file is not newer ; to avoid problems when times not distinguishable (not (file-newer-than-file-p rslfile smlfile))))) (defun rsl-sml-load () ;; based on sml-load-file (interactive) (if (get-buffer "*sml*") (rsl-sml-results)) (if (fboundp 'sml) (let ((file (concat (file-name-sans-extension (buffer-file-name)) ".sml"))) (if (file-readable-p file) (progn (save-excursion (sml)) (setq sml-prev-l/c-dir/file (cons (file-name-directory file) (file-name-nondirectory file))) (sml-update-cursor (sml-proc-buffer)) (comint-send-string (sml-proc) (concat (format sml-use-command file) ";\n")) (switch-to-sml nil)) (error "SML file %s does not exist" file))) (error "You must have SML available"))) (defun rsl-have-sml-buff () (get-buffer "*sml*")) ;; ---------------------------------------------------- ;; support for mutation testing ;; ---------------------------------------------------- (defvar delete-dir-command "rm -rf") (defvar copy-command "cp") (defvar rsl-mutant-base-dir nil "Base directory from which mutants are being created") (defvar rsl-test-case-file nil "Name of last test case file - used as default on next choice.") (defvar coverage-message-string "^\\(Unexecuted expressions in \\|Complete expression coverage of \\)" "Regexp matching strings before RSL file name reporting on coverage in SML output. Must match strings defined in rslml.sml") (defun rsl-sml-results () "Saves test case results from last run of sml and kills *sml* buffer." (interactive) (if (get-buffer "*sml*") (save-excursion (set-buffer "*sml*") (if (file-accessible-directory-p default-directory) (progn (goto-char (point-max)) (if (search-backward "" nil t) (if (search-forward "open ") (let ((beg (point)) (module) (cover-file) (res-file)) (end-of-line) (setq module (buffer-substring beg (point))) (setq res-file (format "%s.sml.results" module)) (forward-line 2) (delete-region (point-min) (point)) (delete-matching-lines "^val it = () : unit" (point-min) (point-max)) (delete-matching-lines "^- *$" (point-min) (point-max)) (goto-char (point-min)) (while (re-search-forward coverage-message-string nil t) (progn (setq beg (point)) (end-of-line) (setq cover-file (concat (buffer-substring beg (point)) ".el")) (rsl-save-coverage cover-file 0))) (delete-matching-lines coverage-message-string (point-min) (point-max)) ; avoid getting backups or previous results (if (file-exists-p res-file) (delete-file res-file)) (write-file res-file nil) (message (format "SML results file %s written." (expand-file-name res-file)))) (message "Has sml finished running?")) (message "Has sml finished running?")))) (kill-buffer nil))) (message "No sml buffer.")) (defun rsl-last-mutant () "Checks for dirs mutant0, ... and returns first n for which mutantn+1 does not extist; or nil if none exist." (rsl-last-mutant1 0)) (defun rsl-last-mutant1 (num) (if rsl-mutant-base-dir (let* ((numstr (int-to-string num)) (dir (concat "mutant" numstr))) (if (file-accessible-directory-p dir) (rsl-last-mutant1 (1+ num)) (if (> num 0) (int-to-string (1- num)) nil))) nil)) (defun make-mutant-dir (num) "Create directory mutantn, choosing n so directory is new." (let* ((numstr (int-to-string num)) (dir (concat "mutant" numstr))) (if (file-accessible-directory-p dir) (make-mutant-dir (1+ num)) (make-directory dir) dir))) (defun has-mutant-dirs () (directory-files default-directory nil "mutant[0-9]+")) (defun is-mutant-dir () (string-match "mutant[0-9]+/$" default-directory)) (defun kill-deleted-file-buffer (buff) (save-excursion (set-buffer buff) (let ((file (buffer-file-name))) (if (and file (string-match "mutant[0-9]+/" (expand-file-name file)) (not (file-exists-p file))) (kill-buffer nil))))) (defun kill-deleted-file-buffers () "Used after deleting mutant directories to kill any buffers visiting deleted files in mutant directories." (let ((bufflist (buffer-list))) (while bufflist (kill-deleted-file-buffer (car bufflist)) (setq bufflist (cdr bufflist))))) (defun kill-deleted-dired-buffers () (let ((alist dired-buffers) elt dir buf) (while alist (setq elt (car alist) dir (car elt) buf (cdr elt)) (if (and (string-match "mutant[0-9]+/" dir) (not (file-directory-p dir))) (kill-buffer buf)) (setq alist (cdr alist))))) (defun rsl-make-mutate () "copy RSL files to directory mutantn, choosing n so directory is new. In copy of current buffer replace string marked by beg end with str." (interactive) (let ((beg (region-beginning)) (end (region-end)) (str (read-string "Replacement string: ")) (mudir (make-mutant-dir 0)) (current (file-name-nondirectory (buffer-file-name))) (testfile)) (shell-command (format "%s *.rsl %s" copy-command mudir)) (save-excursion (find-file (concat mudir "/" current)) (goto-char beg) (delete-region beg end) (insert str) (save-buffer) (kill-buffer nil)) (setq testfile (read-file-name "RSL test case file: " "" (or rsl-test-case-file current) t (or rsl-test-case-file current))) (let ((newfile (concat mudir "/" testfile))) (if (file-exists-p newfile) (progn (setq rsl-test-case-file testfile) (find-file newfile)) (message (format "Cannot open test case file %s" newfile))) mudir))) (defun rsl-mutate () (interactive) (if (get-buffer "*sml*") (rsl-sml-results)) (setq rsl-mutant-base-dir default-directory) (rsl-make-mutate) (rsltc-m-and-run)) (defun rsl-delete-mutant-dirs1 (num) (let* ((numstr (int-to-string num)) (dir (concat "mutant" numstr))) (if (file-accessible-directory-p dir) (progn (shell-command (format "%s %s" delete-dir-command dir)) (rsl-delete-mutant-dirs1 (1+ num)))))) (defun rsl-delete-mutant-dirs () "Deletes directories mutant0, mutant1 etc. Also kills buffers visiting files in deleted mutant directories." (interactive) (rsl-delete-mutant-dirs1 0) (kill-deleted-file-buffers) (kill-deleted-dired-buffers)) (defun rsl-base-results-file () (if (and rsl-test-case-file rsl-mutant-base-dir) (let* ((file-base (file-name-sans-extension rsl-test-case-file)) (res-file (concat rsl-mutant-base-dir file-base ".sml.results"))) (if (file-exists-p res-file) res-file "")) "")) (defun rsl-mutant-results-file (num-string) (if (and rsl-mutant-base-dir rsl-test-case-file) (let* ((file-base (file-name-sans-extension rsl-test-case-file)) (res-file (concat rsl-mutant-base-dir "mutant" num-string "/" file-base ".sml.results"))) (if (file-exists-p res-file) res-file "")) "")) (defun rsl-compare-with-mutant () (interactive) (if (get-buffer "*sml*") (rsl-sml-results)) (let ((filea (rsl-base-results-file)) (fileb "") (numb-string nil) (save-use-dialog-box (if (boundp use-dialog-box) use-dialog-box nil))) (if (string-match "/mutant\\([0-9]+\\)/$" default-directory) (setq numb-string (substring default-directory (match-beginning 1) (match-end 1))) (setq numb-string (rsl-last-mutant))) ;; use minibuffer rather than dialog box to get file names ;; (affects Windows but not Linux) (if (boundp use-dialog-box) (setq use-dialog-box nil)) (setq filea (read-file-name "Base results file: " "" filea t filea)) (if numb-string (setq fileb (rsl-mutant-results-file numb-string))) (setq fileb (read-file-name "Mutant results file: " "" fileb t fileb)) (if (boundp use-dialog-box) (setq use-dialog-box save-use-dialog-box)) (ediff-files filea fileb))) ;; ------------------------------------------------------- ;; support for coverage testing ;; ------------------------------------------------------- (defvar rsl-overlays nil) (defvar rsl-overlay-poss nil) (defun rsl-lc-to-pos (line col) "Convert line and column to point position." (save-excursion (widen) (goto-char (point-min)) (forward-line (1- line)) (forward-char (1- col)) (point))) (defun rsl-clear-overlays () (while rsl-overlays (delete-overlay (car rsl-overlays)) (setq rsl-overlays (cdr rsl-overlays)))) (defun rsl-make-overlays () (rsl-clear-overlays) (rsl-make-overlays1 rsl-overlay-poss) (rsl-show-overlays)) (defun rsl-reduce-finish (position) "Shift left over keyword and then whitespace and/or punctuation" (save-excursion (goto-char position) (while (get-text-property (point) 'face) (backward-char 1)) (skip-syntax-backward " .>b") (rsl-skip-comments-backward) (point))) (defun rsl-skip-comments-backward () (while (equal (get-text-property (1- (point)) 'face) 'font-lock-comment-face) (backward-char 1)) (if (< (skip-syntax-backward " .>b") 0) (rsl-skip-comments-backward))) (defun rsl-make-overlays1 (poss) (if (consp poss) (let* ((pos (car poss)) (beg (car pos)) (fin (car (cdr pos))) (fin1 (rsl-reduce-finish fin)) (overlay (make-overlay beg fin1))) (setq rsl-overlays (cons overlay rsl-overlays)) (rsl-make-overlays1 (cdr poss))))) (defun rsl-show-overlays () (let ((ovs rsl-overlays)) (while ovs (overlay-put (car ovs) 'face 'trailing-whitespace) (setq ovs (cdr ovs))))) (defun rsl-cancel-test-coverage () (interactive) (rsl-clear-overlays)) (defun rsl-has-test-coverage-overlays () (interactive) (consp rsl-overlays)) ; not used (defun rsl-offer-to-delete (file) (interactive) (if (y-or-n-p (format "Coverage file %s out of date. Delete? " file)) (delete-file file))) (defun rsl-save-coverage (file num) (interactive) (if (file-exists-p file) (let* ((next num) (next-file (concat file (int-to-string next)))) (while (file-exists-p next-file) (setq next (1+ next)) (setq next-file (concat file (int-to-string next)))) (rename-file file next-file)))) (defun rsl-has-old () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (rsl-keep-old file (file-name-all-completions base "")))) (consp files))) (defun rsl-delete-coverage () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (file-name-all-completions base ""))) (while files (delete-file (car files)) (setq files (cdr files))))) (defun rsl-delete-old () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (rsl-keep-old file (file-name-all-completions base "")))) (while files (delete-file (car files)) (setq files (cdr files))))) (defun rsl-keep-old (file files) (if (consp files) (let ((next (car files)) (rest (rsl-keep-old file (cdr files)))) (if (up-to-date next file) rest (cons next rest))) nil)) (defun rsl-skip-old (file files) (if (consp files) (let ((next (car files)) (rest (rsl-skip-old file (cdr files)))) (if (not (up-to-date next file)) rest (cons next rest))) nil)) (defun rsl-show-test-coverage () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (rsl-skip-old file (file-name-all-completions base "")))) (if (consp files) (let* ((first-res (car files))) (load-file first-res) (setq files (cdr files)) (while (consp files) (rsl-merge-test-coverage (car files)) (setq files (cdr files))))) (rsl-make-overlays) (if (null rsl-overlays) (message "Coverage is complete")))) (defun rsl-has-current-test-coverage () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (rsl-skip-old file (file-name-all-completions base "")))) (consp files))) (defun rsl-has-test-coverage () (interactive) (let* ((file (buffer-file-name)) (base (file-name-nondirectory (concat file ".el"))) (files (file-name-all-completions base ""))) (consp files))) (defun rsl-intersect-region (r1 r2) "Intersection of two regions, each a list of beginning and end." (let* ((beg1 (car r1)) (beg2 (car r2)) (beg (max beg1 beg2)) (fin1 (car (cdr r1))) (fin2 (car (cdr r2))) (fin (min fin1 fin2))) (if (< beg fin) (list beg fin) nil))) (defun rsl-intersect-coverage (pos poss) "Calculate intersections of region and list of regions" (if (consp poss) (let ((pos1 (rsl-intersect-region pos (car poss))) (rest (rsl-intersect-coverage pos (cdr poss)))) (if (consp pos1) (cons pos1 rest) rest)) nil)) (defun rsl-merge-coverages (poss0 poss1) "Calculate intersections of regions of two lists" (if (consp poss0) (let ((poss (rsl-intersect-coverage (car poss0) poss1)) (rest (rsl-merge-coverages (cdr poss0) poss1))) (append poss rest)) nil)) (defun rsl-merge-test-coverage (file) "File has the form (setq rsl-overlay-poss list). Merge list with existing contents of rsl-overlay-poss. Will give nil if rsl-overlay-poss is nil, so do not use for initial load of coverage file." (interactive) (if (file-exists-p file) (let ((poss rsl-overlay-poss)) (load-file file) (setq rsl-overlay-poss (rsl-merge-coverages poss rsl-overlay-poss))))) (provide 'rsltc)