;; acsl.el, ACSL (ANSI C Specification Language) mode for Emacs.

;; Copyright © 2008 - Pierre ROUX
;;
;; This 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.

;; How to install:
;; copy the following in your .emacs file
;;
;; (setq load-path (cons "/directory/in/which/you/put/the/file/acsl.el" load-path))
;; (autoload 'acsl-mode "acsl" "Major mode for editing ACSL code" t)
;; ;; uncomment this if you want to automatically load ACSL mode with each C file 
;; ;;(setq auto-mode-alist
;; ;;      (append
;; ;;       '(("\\.[ch]" . acsl-mode))
;; ;;       auto-mode-alist))
;;
;; you can then load the mode in emacs with M-x acsl-mode

;; code

(defun acsl-keymap-init ()
  "Init keymap"
  (define-key acsl-mode-map "\C-c\C-j" 'acsl-jessie-gui))

;; font-lock

(defconst acsl-keywords
  '("assert"
    "assigns"
    "assumes"
    "axiom"
    "behavior"
    "ensures"
    "lemma"
    "logic"
    "predicate"
    "reads"
    "requires")
  "List of ACSL keywords to highlight.")

(defun acsl-in-acsl-annot ()
  "If we are in a C comment beginning with @."
  (and (nth 4 (syntax-ppss))
       (eq (char-after (+ (nth 8 (syntax-ppss)) 2)) ?@)))

(defvar acsl-font-lock-keywords
  (let ((pre-match-form (lambda ()
			  (goto-char (match-beginning 0))
			  (match-end 0)))
	(find-annot (lambda (limit)
			;; skip comments
			(if (and (looking-at "//") (acsl-in-acsl-annot))
			    (re-search-forward "\n" limit 'e))
			(while (and (not (acsl-in-acsl-annot)) (< (point) limit))
			  (re-search-forward "/[*/]" limit 'e))
			(if (>= (point) limit)
			    nil
			  (let ((b (save-excursion
				     (re-search-backward "/[*/]" (- (point) 2) t)
				     (point))))
			    (re-search-forward "[*/]/\\|\n" limit 'e)
			    (re-search-backward "//" (- (point) 2) t)  ; don't recolor comments
			    (set-match-data (list b (point) (nth 2 (match-data t))))
			    t)))))
    (list
     `(,find-annot
       (0 font-lock-type-face t)
       (,(concat (regexp-opt acsl-keywords 'words) "\\|<?==>\\|&&\\|||\\|!\\|\\^\\^") (,pre-match-form) nil
	(0 font-lock-keyword-face t))
       ("\\(\\?\\)[^:]*\\(:\\)" (,pre-match-form) nil
	(1 font-lock-keyword-face t)
	(2 font-lock-keyword-face t))
       ("\\<\\(axiom\\|behavior\\|predicate\\|l\\(ogic\\|emma\\)\\)\\>[ \t\n@]*\\([a-zA-Z_][a-zA-Z_0-9]*\\)" (,pre-match-form) nil
	(3 font-lock-function-name-face t))
       ("\\\\\\(e\\(mpty\\|xists\\)\\|f\\(alse\\|orall\\)\\|old\\|result\\|true\\|valid\\(_range\\)?\\)" (,pre-match-form) nil
	(0 font-lock-constant-face t)))))
  "Default highlighting for ACSL mode")

(defun acsl-font-lock-init ()
  "Initialize font-lock for ACSL."
  (add-hook 'c-mode-hook
	    (lambda ()
	      (font-lock-add-keywords nil acsl-font-lock-keywords))))

;; custom variables

(require 'custom)

(defcustom acsl-jessie-gui-prog-name "frama-c -jessie-analysis -jessie-gui"
  "Frama-C/Jessie executable name."
  :group 'acsl
  :type 'string)

(defcustom acsl-jessie-int-model "exact"
  "Jessie int model."
  :group 'acsl
  :type '(choice (const :tag "Exact" "exact")
		 (const :tag "Bounded" "bounded")
		 (const :tag "Modulo" "modulo")))

(defun acsl-jessie-gui ()
  "Generate VCs and show them in a GUI"
  (interactive)
  (compile (concat acsl-jessie-gui-prog-name
		   " -jessie-int-model "
		   acsl-jessie-int-model
		   " "
		   (buffer-file-name))))

;; menu

(require 'easymenu)

(defun acsl-menu-init ()
  (easy-menu-define
   acsl-menu (list acsl-mode-map)
   "ACSL Mode Menu." 
   '("ACSL"
     ["Customize ACSL mode" (customize-group 'acsl) t]
     "---"
     ["Jessie GUI" acsl-jessie-gui t]
     ))
  (easy-menu-add acsl-menu))

;; indent

(defun acsl-indent-command (&optional arg)
  "Indent ACSL code (quite basic yet)."
  (interactive "*")
  (c-indent-line)
  (when (and (acsl-in-acsl-annot)
	     (< (nth 8 (syntax-ppss)) (line-beginning-position)))  ; not the first line of an annot (which don't need to be indented)
    (save-excursion
      (back-to-indentation)
      (if (not (eq (char-after) ?@))
	  (insert "@")
	(goto-char (+ (point) 1)))
      (if (not (looking-at "*/"))  ; to avoid indenting last lines of annotation of the form "@*/" (thanks Yannick)
	  (let ((current (save-excursion
			   (skip-chars-forward " \t@")))
		(expected (save-excursion
			    (let ((cc (current-column)))
			      (forward-line -1)
			      (move-to-column cc))
			    (skip-chars-forward " \t@"))))
	    (if (save-excursion
		  (skip-chars-backward " \t\n@")
		  (memq (char-before) '(?: ?=)))
		(setq expected (+ expected 2)))
	    (if (save-excursion
		  (skip-chars-forward " \t@")
		  (looking-at "\\<\\(axiom\\|behavior\\|predicate\\|l\\(ogic\\|emma\\)\\)\\>"))
		(setq expected (save-excursion
				 (goto-char (+ (nth 8 (syntax-ppss)) 3))
				 (skip-chars-forward " \t@"))))
	    (if (< current expected)
		(insert-char ?  (- expected current)))
	    (if (> current expected)
		(kill-forward-chars (- current expected))))))
    (if (eq (char-after) ?@)
	(skip-chars-forward " \t@"))))

(defun acsl-indent-init ()
  (setq indent-line-function 'acsl-indent-command)
  ;; maybe not the best solution for C code but still works
  (setq indent-region-function nil))

;; main function for the mode

(define-derived-mode acsl-mode c-mode
  "ACSL"
  "Major mode for C annoted with ACSL."
  (acsl-font-lock-init)
  (acsl-keymap-init)
  (acsl-indent-init)
  (acsl-menu-init))

(provide 'acsl-mode)