spthy-mode.el

;;; spthy.el --- SPTHY major mode
;; Author: Katriel Cohn-Gordon

;; PRE-TAMARIN MODE: [UGLY HACK] this mode is only used to be able to highlight comments '//' AND  '/* */'
;;                   since 'modify-syntax-entry' seems unable to deal with both types of comments :(
(require 'generic-x)
(define-generic-mode
  'pre-spthy-mode
  '("//" ("/*" . "*/"))  ;; C-like comments
  '()
  '(((rx "X" (group (any ascii)) "X") . 'font-lock-keyword-face))
  '("\\.spthy$") ;; files for which to activate this mode
  nil            ;; other functions to call
  "A mode for Tamarin files") ;; doc string for this mode

;; TAMARIN-MODE
;; Keybindings
(defvar wpdl-mode-map
  (let ((map (make-sparse-keymap)))
    (define-key map "\C-j" 'newline-and-indent)
    map)
  "Keymap for SPTHY major mode")

;;;###autoload
(add-to-list 'auto-mode-alist '("\\.spthy\\'" . spthy-mode))

(defvar spthy-keywords
  '("axiom" "lemma" "restriction" "protocol" "property" "text" "rule" "let" "in" "Fresh" "fresh" "Public" "public" "All" "Ex" "h" "sk" "pk" "Fr" "In" "Out" "fr" "in" "out" "not" "!"))

(defvar spthy-events
  '("theory" "begin" "end" "subsection" "section" "pb" "lts" "diffie-hellman" "bilinear-pairing" "multiset" "hashing" "symmetric-encryption" "asymmetric-encryption" "exists-trace" "all-traces" "enable" "assertions" "modulo" "default_rules" "anb-proto" "signing"))

(defvar spthy-operators
  '("&" "|" "==>" "=" "<=>" "-->" "^" "[" "]->" "-->" "]" "--["))

(defvar spthy-warnings
  '("@" "functions" "builtins" "equations" "heuristic" "!")) ; we may want to add ! in operators instead

(defvar spthy-quiet
  '("~" "$"))

(defvar spthy-font-lock-defaults
  `((
     ( ,(regexp-opt spthy-keywords          'words) . font-lock-keyword-face)
     ( ,(regexp-opt spthy-events            'words) . font-lock-constant-face)
     ( ,(regexp-opt spthy-warnings                ) . font-lock-warning-face)
     ( ,(regexp-opt spthy-operators               ) . font-lock-constant-face)
     ( ,(regexp-opt spthy-quiet                   ) . font-lock-comment-face)
 )))

(define-derived-mode spthy-mode pre-spthy-mode "SPTHY"
  "Major mode for editing Tamarin's SPTHY files."

  ;; Fontify keywords
  (setq font-lock-defaults spthy-font-lock-defaults)

  ;; Double quotes are for lemmas not strings
  (modify-syntax-entry ?\" "w" spthy-mode-syntax-table)
  (modify-syntax-entry ?' "\"" spthy-mode-syntax-table)

  ;; Use regex to assign syntax classes
  (setq-local syntax-propertize-function
              (syntax-propertize-rules
               ;; Mark '<' as a delimiter if it is preceded by
               ;; '=', '(' or ','.
               ("[=(,]+[[:space:]]*\\(<\\)" (1 "(>"))
               ;; Mark '>' as a delimiter if it is not part of an
               ;; arrow and is succeeded by '=', ')', ',' or by an
               ;; end-of-line.
               ("[^-=]\\(>\\)[[:space:]]*\\([=),]+\\|$\\)" (1 ")<"))
               ;; Treat " as delimiter only when preceded by a line
               ;; ending with ':'.
               (":[[:space:]\n]*\\(\"\\)[^\"]*\\(\"\\)" (1 "(\"") (2 ")\"") )
               ))

  )

(provide 'spthy-mode)