;; Copyright (C) 2019  Christian Barthel <bch@online.de>

 ;; Author: Christian Barthel
 ;; Keywords: TLA+

 ;; This file 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, or (at your option)
 ;; any later version.

 ;; This file 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 License
 ;; along with GNU Emacs; see the file COPYING.  If not, write to
 ;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330,
 ;; Boston, MA 02111-1307, USA.

 ;;; Commentary:

;; This package defines TLA+ Major Mode to manipulate TLA+
;; specifications.


;;; Code:

(defcustom tla+-mode-hook '()
  "Normal hook run when entering TLA+ mode."
  :type 'hook
  :options '()
  :group 'tla+)

(defcustom tla+-java-path "java"
  "Path to the `java' program"
  :type 'file
  :group 'tla+)

(defcustom tla+-tlatools-path
  "/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools.jar"
  "Path to the TLA+ `tlatools.jar' file"
  :type 'file
  :group 'tla+)

(defcustom tla+-dvipdf-path
  "dvipdf"
  "Path to the `dvipdf' program"
  :type 'file
  :group 'tla+)

(defcustom tla+-dvips-path
  "dvips"
  "Path to the `dvips' program"
  :type 'file
  :group 'tla+)

(defvar tla+-mode-map
  (let
      ((map (make-sparse-keymap))
       (menu-map (make-sparse-keymap "TLA+"))
       (operator-map (make-sparse-keymap))
       (action-operator-map (make-sparse-keymap))              
       (temporal-operator-map (make-sparse-keymap))       
       (export-map (make-sparse-keymap)))
    (set-keymap-parent map lisp-mode-shared-map)
    (define-key map "\e\t" 'ispell-complete-word)

    ;; Main TLA+ Menu:
    (bindings--define-key map [menu-bar tla+]
      (cons "TLA+" menu-map))

    ;; Operators
    (bindings--define-key menu-map [operator]
      (cons "Insert Operator.." operator-map))

    ;; Action Operators
    (bindings--define-key operator-map [action-operator]
      (cons "Action Operator" action-operator-map))

    (bindings--define-key
	action-operator-map [primed-operator]
      '(menu-item "e'" tla+-operator-primed
                  :help "Value of e in final state of a step"))
    
    (bindings--define-key
	action-operator-map [stutter-operator]
      '(menu-item "[A]_e" tla+-operator-stutter
                  :help "A \\/ (e' = e)"))

    (bindings--define-key
	action-operator-map [nonstutter-operator]
      '(menu-item "<<A>>_e" tla+-operator-nonstutter
                  :help "A /\ (e' \\= e)"))

    (bindings--define-key
	action-operator-map [enabled-operator]
      '(menu-item "ENABLED A" tla+-operator-enabled
                  :help "An A step is possible"))

    (bindings--define-key
	action-operator-map [unchanged-operator]
      '(menu-item "UNCHANGED e" tla+-operator-unchanged
                  :help "e = e'"))

    (bindings--define-key
	action-operator-map [composition-operator]
      '(menu-item "A \\cdot B" tla+-operator-composition
                  :help "Composition of actions"))    
    
    ;; Temporal operators:
    (bindings--define-key operator-map [temporal-operator]
      (cons "Temporal Operator" temporal-operator-map))

    (bindings--define-key
	temporal-operator-map [always-temporal-operator]
      '(menu-item "[]F" tla+-operator-alwaystrue
                  :help "F is always true"))

    (bindings--define-key
	temporal-operator-map [eventually-temporal-operator]
      '(menu-item "<>F" tla+-operator-eventually
                  :help "F is eventually true"))

    (bindings--define-key
	temporal-operator-map [wf-temporal-operator]
      '(menu-item "WF_e(A)" tla+-operator-weakfairness
                  :help "Weak fairness for action A"))

    (bindings--define-key
	temporal-operator-map [sf-temporal-operator]
      '(menu-item "SF_e(A)" tla+-operator-strongfairness
                  :help "Strong fairness for action A"))

    (bindings--define-key
	temporal-operator-map [leadsto-temporal-operator]
      '(menu-item "F ~> G" tla+-operator-leadsto
                  :help "F leads to G"))
    
    ;; Export Menu:
    (bindings--define-key menu-map [export] (cons "Export.." export-map))
    
    (bindings--define-key export-map [export-pdf]
      '(menu-item "Run TLatex and create PDF" tla+-run-tlatex-pdf
                  :help "Typeset TLaTex and create PDF Document"))

    (bindings--define-key export-map [export-dvi]
      '(menu-item "Run TLatex and create DVI" tla+-run-tlatex-dvi
                  :help "Typeset TLaTex and create DVI Document"))

    (bindings--define-key export-map [export-ps]
      '(menu-item "Run TLatex and create PS" tla+-run-tlatex-ps
                  :help "Typeset TLaTex and create PS Document"))
    
    (bindings--define-key export-map [export-open]
      '(menu-item "Open DVI Viewer" tla+-open-dvi
                  :help "Open DVI Viewer"))

    ;; Main Menu
    (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)

    (bindings--define-key map [menu-bar tla+ tla+-run-sany]
      '(menu-item "Run Syntax Checker" tla+-run-sany
		  :help
		  "Run SANY2 "
		  "(parser/syntax checker for TLA+ specifications.) "))
     
    (bindings--define-key map [menu-bar tla+ tla+-create-module]
      '(menu-item "Create new Module" tla+-create-module
		  :help "Create a new TLA+ Module"))
    (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)    
    map)
  "Keymap for `tla+-mode'.")


(defconst tla+-font-lock-keywords
  (list
   '("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|INSTANCE\\|LOCAL\\|ASUME\\|EXCEPT\\|EXTENDS?\\)\\>"
     . font-lock-builtin-face)
   '("\\<\\(TRUE\\|FALSE\\|OTHER\\|BOOLEAN\\)\\>" . font-lock-type-face)   
   '("\\<\\(CONSTANT\\|SUBSET\\|ENABLED\\|UNCHANGED\\|UNION\\|DOMAIN\\|EXCEPT\\|IF\\|THEN\\|ELSE\\|CHOOSE\\)\\>" . font-lock-keyword-face)
   '("\\\\\\*.*$" . font-lock-comment-face)
   '("(\\*.*\\*)" . font-lock-comment-face)
   '("\\('\\w*'\\)" . font-lock-variable-name-face)
  "Highlighting for TLA+ Operators, Keywords etc."))


;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode))
;;;###autoload
(define-derived-mode tla+-mode nil "TLA+"
  "Major mode for editing TLA+ specifications. 
In this mode, syntax highlighting is activated for TLA+ specification
files.  Various operators can be inserted by `tla+-operator-NAME'.
\\{text-mode-map}
Turning on Text mode runs the normal hook `text-mode-hook'."
  (setq-local font-lock-defaults
	      '(tla+-font-lock-keywords))
  (setq-local text-mode-variant t)
  (setq-local comment-start "\\* ")
  (setq-local require-final-newline mode-require-final-newline))

(defun tla+-create-module ()
  (interactive)
  (insert
   (concat
   "------------------- MODULE ......... -----------------------\n"
   "EXTENDS Naturals, ...\n"
   "VARIABLE ..\n"
   "------------------------------------------------------------\n"
   "============================================================\n"
   "\\* Modification History\n"
   "\\* Created "
   (current-time-string) " by " user-full-name "\n")))
    
    
(defun tla+-run-sany ()
  "TODO: jump to line.."
  (interactive)
  (let* ((filename (buffer-file-name))
	 (sanybuffer (get-buffer-create "*tla2sany.SANY*"))
	 (output   (shell-command-to-string (concat
				   tla+-java-path
				   " -cp "
				   tla+-tlatools-path
				   " tla2sany.SANY "
				   filename))))
    (save-excursion
      (split-window-below)
      (other-window 1)
      (switch-to-buffer sanybuffer)
      (erase-buffer)
      (insert output))))

(defun tla+-open-dvi (buffername)
  (interactive "b")
  (save-excursion
    (switch-to-buffer buffername)
    (let* ((filename (buffer-file-name))
	   (dviname (replace-regexp-in-string
		     ".tla$" ".dvi" filename)))
      (shell-command (concat "xdvi " dviname " &")))))

(defun tla+-operator-alwaystrue ()
  (interactive) (insert " []F"))

(defun tla+-operator-eventually ()
  (interactive) (insert " <>F"))

(defun tla+-operator-weakfairness ()
  (interactive) (insert " WF_e(A)"))

(defun tla+-operator-strongfairness ()
  (interactive) (insert " SF_e(A)"))

(defun tla+-operator-leadsto ()
  (interactive) (insert " F~>G "))

(defun tla+-operator-stutter ()
  (interactive) (insert " [A]_e"))

(defun tla+-operator-primed ()
  (interactive) (insert " e'"))


(defun tla+-operator-nonstutter ()
  (interactive) (insert " <<A>>_e"))

(defun tla+-operator-enabled ()
  (interactive) (insert " ENABLED A"))

(defun tla+-operator-unchanged ()
  (interactive) (insert " UNCHANGED e"))

(defun tla+-operator-unchanged ()
  (interactive) (insert " A \\cdot B"))

(defun tla+-run-tlatex (type)
  "TODO: jump to line.."
  (interactive
   (list
    (completing-read
     "Format: "
           '(("pdf" 1) ("dvi" 2) ("ps" 3)) nil t "")))
  (let* ((filename (buffer-file-name))
	 (output   (shell-command (concat
				   tla+-java-path
				   " -cp "
				   tla+-tlatools-path
				   " tla2tex.TLA "
				   filename)))
	 (dvipath (replace-regexp-in-string
		   ".tla$" ".dvi" filename))
	 (convert2pdf (concat
		       tla+-dvipdf-path " " dvipath))
	 (convert2ps (concat
		      tla+-dvips-path " " dvipath)))
    (progn
      (cond
       ((eq type 'pdf)
	(shell-command convert2pdf))
       ((eq type 'ps)
	(shell-command convert2ps)))
      type)))
;;    (save-excursion
;;      (split-window-below)
;;      (other-window 1)
;;      (switch-to-buffer sanybuffer)
;;       (insert output))))

(defun tla+-run-tlatex-pdf ()
  (interactive) (tla+-run-tlatex 'pdf))
(defun tla+-run-tlatex-dvi ()
  (interactive) (tla+-run-tlatex 'dvi))
(defun tla+-run-tlatex-ps ()
  (interactive) (tla+-run-tlatex 'ps))

(provide 'tla+-mode)