egison-5.0.0: emacs/egison-mode.el
;;; egison-mode.el --- Egison editing mode
;; Copyright (C) 2011-2026 Satoshi Egi
;; Permission is hereby granted, free of charge, to any person obtaining
;; a copy of this software and associated documentation files (the "Software"),
;; to deal in the Software without restriction, including without limitation
;; the rights to use, copy, modify, merge, publish, distribute, sublicense,
;; and/or sell copies of the Software, and to permit persons to whom the Software
;; is furnished to do so, subject to the following conditions:
;; The above copyright notice and this permission notice shall be included
;; in all copies or substantial portions of the Software.
;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED,
;; INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR
;; A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
;; HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF
;; CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE
;; OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
;;; Author: Satoshi Egi <egisatoshi@gmail.com>
;;; URL: https://github.com/egisatoshi/egison/blob/master/emacs/egison-mode.el
;;; Version: 0.3.0
;;; Commentary:
;; Emacs Mode for Egison
;;
;; Please put it in your load-path of Emacs. Then, add the following
;; lines in your .emacs.
;;
;; (autoload 'egison-mode "egison-mode" "Major mode for editing Egison code." t)
;; (setq auto-mode-alist (cons `("\\.egi$" . egison-mode) auto-mode-alist))
;;; Code:
;; ============================================================
;; Face definitions
;; ============================================================
(defface egison-keyword-face
'((t :inherit font-lock-keyword-face))
"Face for Egison keywords."
:group 'egison)
(defface egison-type-keyword-face
'((t :inherit font-lock-type-face))
"Face for Egison type system keywords (class, instance, inductive, etc.)."
:group 'egison)
(defface egison-builtin-type-face
'((t :inherit font-lock-type-face))
"Face for Egison built-in type names."
:group 'egison)
(defface egison-definition-face
'((t :inherit font-lock-keyword-face))
"Face for Egison definition keywords."
:group 'egison)
(defface egison-pattern-variable-face
'((t :inherit font-lock-variable-name-face))
"Face for Egison pattern variables ($x, etc.)."
:group 'egison)
(defface egison-value-pattern-face
'((t :inherit font-lock-constant-face))
"Face for Egison value patterns (#x, etc.)."
:group 'egison)
(defface egison-constructor-face
'((t :inherit font-lock-constant-face))
"Face for Egison data constructors and boolean values."
:group 'egison)
(defface egison-type-constraint-face
'((t :inherit font-lock-type-face))
"Face for Egison type constraints ({Eq a}, etc.)."
:group 'egison)
;; ============================================================
;; Font-lock keywords level 1 (basic)
;; ============================================================
(defconst egison-font-lock-keywords-1
(eval-when-compile
(list
;; ----- Type system keywords (highlighted prominently) -----
(cons (concat "\\<" (regexp-opt
'("class" "instance" "inductive" "extends" "declare") t)
"\\>")
'font-lock-type-face)
;; ----- Definition keywords -----
(cons (concat "\\<" (regexp-opt
'("def" "let" "in" "where") t)
"\\>")
'font-lock-keyword-face)
;; ----- Module and loading -----
(cons (concat "\\<" (regexp-opt
'("load" "loadFile" "execute") t)
"\\>")
'font-lock-builtin-face)
;; ----- Control flow -----
(cons (concat "\\<" (regexp-opt
'("if" "then" "else") t)
"\\>")
'font-lock-keyword-face)
;; ----- Pattern matching -----
(cons (concat "\\<" (regexp-opt
'("match" "matchDFS" "matchAll" "matchAllDFS"
"as" "with" "forall" "loop") t)
"\\>")
'font-lock-keyword-face)
;; ----- Matcher definition -----
(cons (concat "\\<" (regexp-opt
'("matcher" "algebraicDataMatcher") t)
"\\>")
'font-lock-keyword-face)
;; ----- Lambda and special forms -----
(cons (concat "\\<" (regexp-opt
'("memoizedLambda" "cambda" "capply"
"withSymbols" "function") t)
"\\>")
'font-lock-keyword-face)
;; ----- Tensor operations -----
(cons (concat "\\<" (regexp-opt
'("tensor" "generateTensor" "contract"
"tensorMap" "tensorMap2"
"transpose" "flipIndices"
"subrefs" "suprefs" "userRefs") t)
"\\>")
'font-lock-builtin-face)
;; ----- IO and sequencing -----
(cons (concat "\\<" (regexp-opt
'("do" "seq") t)
"\\>")
'font-lock-keyword-face)
;; ----- Infix declarations -----
(cons (concat "\\<" (regexp-opt
'("infixr" "infixl" "infix" "expression" "pattern") t)
"\\>")
'font-lock-keyword-face)
;; ----- Special values -----
(cons (concat "\\<" (regexp-opt
'("undefined" "something") t)
"\\>")
'font-lock-constant-face)
;; ----- Built-in type names -----
(cons (concat "\\<" (regexp-opt
'("Integer" "MathExpr" "Float" "Bool" "Char" "String"
"IO" "Matcher" "Pattern"
"Tensor" "Vector" "Matrix" "DiffForm"
"List") t)
"\\>")
'font-lock-type-face)
;; ----- Boolean literals -----
(cons (concat "\\<" (regexp-opt '("True" "False") t) "\\>")
'font-lock-constant-face)
;; ----- Testing primitives -----
(cons (concat "\\<" (regexp-opt
'("assert" "assertEqual") t)
"\\>")
'font-lock-warning-face)
;; ----- Operators and symbols -----
(cons ":=" 'font-lock-keyword-face)
(cons "::" 'font-lock-keyword-face)
(cons "++" 'font-lock-keyword-face)
(cons "=>" 'font-lock-keyword-face)
(cons "->" 'font-lock-keyword-face)
(cons "\\.\\.\\." 'font-lock-keyword-face)
))
"Subdued expressions to highlight in Egison modes.")
;; ============================================================
;; Font-lock keywords level 2 (gaudy - includes type annotations)
;; ============================================================
(defconst egison-font-lock-keywords-2
(append egison-font-lock-keywords-1
(eval-when-compile
(list
;; Pattern variables ($x, $pat, etc.)
(cons "\\$[a-zA-Z_][a-zA-Z0-9_']*" 'font-lock-variable-name-face)
;; Value patterns (#x, #(expr), etc.)
(cons "#[a-zA-Z_][a-zA-Z0-9_']*" 'font-lock-constant-face)
;; Type class constraints in braces: {Eq a}, {Eq a, Ord b}
(cons "{[A-Z][a-zA-Z0-9_',: ]*}" 'font-lock-type-face)
;; Type annotations in parameter list: (x: Integer), (x: a)
(list "(\\([a-zA-Z_][a-zA-Z0-9_']*\\)\\s-*:" 1 'font-lock-variable-name-face)
;; Type names after colon in type annotations
(list ":\\s-*\\([A-Z][a-zA-Z0-9_]*\\)" 1 'font-lock-type-face)
;; User-defined type names (uppercase identifiers not already matched)
;; in inductive/class/instance declarations
(list "\\<\\(inductive\\|class\\|instance\\)\\s-+\\([A-Z][a-zA-Z0-9_]*\\)"
2 'font-lock-type-face)
;; Data constructors in inductive definitions (after | at start of line)
(list "^\\s-*|\\s-+\\([A-Z][a-zA-Z0-9_]*\\)" 1 'font-lock-constant-face)
;; "declare symbol" combination
(list "\\<\\(declare\\)\\s-+\\(symbol\\)\\>"
(list 1 'font-lock-keyword-face)
(list 2 'font-lock-keyword-face))
;; "inductive pattern" combination
(list "\\<\\(inductive\\)\\s-+\\(pattern\\)\\>"
(list 1 'font-lock-type-face)
(list 2 'font-lock-type-face))
;; "def pattern" combination
(list "\\<\\(def\\)\\s-+\\(pattern\\)\\>"
(list 1 'font-lock-keyword-face)
(list 2 'font-lock-keyword-face))
;; Function name after "def" keyword
(list "\\<def\\s-+\\([a-zA-Z_][a-zA-Z0-9_']*\\)" 1 'font-lock-function-name-face)
;; Index notation: subscripts and superscripts (e.g., v~i, v_j, T~i~j_k)
(cons "[a-zA-Z0-9_'][~_][a-zA-Z0-9_']+" 'font-lock-preprocessor-face)
)))
"Gaudy expressions to highlight in Egison modes.")
(defvar egison-font-lock-keywords egison-font-lock-keywords-1
"Default expressions to highlight in Egison modes.")
;; ============================================================
;; Indentation
;; ============================================================
(defun egison-indent-line ()
"Indent current line as Egison code."
(interactive)
(let ((indent (egison-calculate-indent)))
(when indent
(save-excursion
(beginning-of-line)
(delete-horizontal-space)
(indent-to indent))
(when (< (current-column) indent)
(move-to-column indent)))))
(defun egison-calculate-indent ()
"Calculate the indentation level for the current line."
(save-excursion
(beginning-of-line)
(cond
;; Top-level definitions
((looking-at "^\\(def\\|load\\|class\\|instance\\|inductive\\|declare\\|infixl\\|infixr\\|infix\\)\\>")
0)
;; Match clause continuation (lines starting with |)
((looking-at "^\\s-*|")
(save-excursion
(forward-line -1)
(cond
((looking-at "^\\s-*|")
(current-indentation))
((looking-at ".*\\<with\\>\\s-*$")
(+ (current-indentation) 2))
((looking-at ".*:=\\s-*$")
(+ (current-indentation) 2))
(t (current-indentation)))))
;; Lines after "where"
((save-excursion
(forward-line -1)
(looking-at ".*\\<where\\>\\s-*$"))
(save-excursion
(forward-line -1)
(+ (current-indentation) 2)))
;; Default: match previous line
(t
(save-excursion
(forward-line -1)
(current-indentation))))))
;; ============================================================
;; Keymap
;; ============================================================
(defvar egison-mode-map
(let ((smap (make-sparse-keymap)))
(define-key smap "\C-j" 'newline-and-indent)
smap)
"Keymap for Egison mode.")
;; ============================================================
;; Syntax table
;; ============================================================
(defvar egison-mode-syntax-table
(let ((table (make-syntax-table)))
;; Block comments: {- ... -}
(modify-syntax-entry ?\{ "(}1nb" table)
(modify-syntax-entry ?\} "){4nb" table)
(modify-syntax-entry ?- "_ 123" table)
(modify-syntax-entry ?\n ">" table)
;; String literals
(modify-syntax-entry ?\" "\"" table)
(modify-syntax-entry ?\' "\"" table)
;; Operators that are part of words
(modify-syntax-entry ?_ "w" table)
(modify-syntax-entry ?~ "w" table)
;; Special symbols
(modify-syntax-entry ?$ "'" table)
(modify-syntax-entry ?# "'" table)
(modify-syntax-entry ?& "." table)
(modify-syntax-entry ?| "." table)
(modify-syntax-entry ?! "." table)
(modify-syntax-entry ?? "." table)
(modify-syntax-entry ?@ "." table)
table)
"Syntax table for Egison mode")
;; ============================================================
;; Mode setup
;; ============================================================
(defun egison-mode-set-variables ()
(set-syntax-table egison-mode-syntax-table)
(set (make-local-variable 'font-lock-defaults)
'((egison-font-lock-keywords
egison-font-lock-keywords-1 egison-font-lock-keywords-2)
nil t
;; Include special characters and mathematical symbols as word constituents
(("+*/=!?%:_~.'∂∇αβγδεζηθικλμνξοπρςστυφχψωΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ" . "w"))
))
(set (make-local-variable 'indent-line-function) 'egison-indent-line)
;; Comment settings for -- and {- -}
(set (make-local-variable 'comment-start) "-- ")
(set (make-local-variable 'comment-end) "")
(set (make-local-variable 'comment-start-skip) "{-+ *\\|--+ *")
(set (make-local-variable 'comment-add) 1)
(set (make-local-variable 'comment-end-skip) nil)
;; Block comment delimiters
(set (make-local-variable 'comment-multi-line) t)
)
;;;###autoload
(defun egison-mode ()
"Major mode for editing Egison code.
Features:
- Syntax highlighting for Egison keywords, type annotations,
type class definitions, inductive types, and pattern matching.
- Support for type system keywords: class, instance, inductive,
extends, declare, pattern.
- Highlighting for pattern variables ($x), value patterns (#x),
type constraints ({Eq a}), and type annotations (x: Integer).
- Basic indentation support.
- Comment support for line comments (--) and block comments ({- -}).
Commands:
\\{egison-mode-map}
Entry to this mode calls the value of `egison-mode-hook'
if that value is non-nil."
(interactive)
(kill-all-local-variables)
(setq indent-tabs-mode nil)
(use-local-map egison-mode-map)
(setq major-mode 'egison-mode)
(setq mode-name "Egison")
(egison-mode-set-variables)
(run-mode-hooks 'egison-mode-hook))
(defgroup egison nil
"Editing Egison code."
:link '(custom-group-link :tag "Font Lock Faces group" font-lock-faces)
:group 'lisp)
(defcustom egison-mode-hook nil
"Normal hook run when entering `egison-mode'.
See `run-hooks'."
:type 'hook
:group 'egison)
(provide 'egison-mode)
;;; egison-mode.el ends here