Emacs fixes (#398)

* Minor update

- disable electric indent by default,
- remove unused functions
- some indentation correction:
  + indent by two after a colon that is after a symbol
  + indent queries as the previous line if it begins with a query
- sorted lines alphabetically

* Add test facilities

* Added subscripts and superscripts in quail

editors/emacs/GNUmakefile

@@ -0,0 +1,17 @@
+VERSION = 1.0
+
+.PHONY: build
+build:
+	cask build
+
+.PHONY: dist
+dist:
+	cask package
+
+.PHONY: test
+tests: dist
+	./test.sh $(VERSION)
+
+.PHONY: clean
+clean:
+	cask clean-elc

editors/emacs/lambdapi-input.el

@@ -219,16 +219,21 @@
  ("`fz" ?𝔷) ("`fZ" ?ℨ))
 
 (require 'seq)
+
+;; Quail needs alists with cons cells ‘(COM . CH)’ where COM is a LaTeX command
+;; (e.g. \alpha) and CH a character (e.g. α). We define several lists extracted
+;; from the ‘math-symbol-lists’ package and formatted to suit Quail’s needs.
+;; NOTE we use ‘eval-when-compile’ to avoid traversing all the symbols when the
+;; mode is loaded.
+
 (defconst lambdapi--math-symbol-list-basic
   (eval-when-compile
     (let* ((cat-rx (rx (or "arrow" "greek" "Greek" "bin" "rel" "misc")))
            (pred (lambda (sym) (string-match-p cat-rx (car sym))))
            (filt (seq-filter pred math-symbol-list-basic)))
       (seq-map (lambda (sym) `(,(cadr sym) . ,(cddr sym))) filt)))
-  "Formatted sublist of `math-symbol-list-basic'.
-An element of this list is a dotted pair (COM . CH) where com is the LaTeX
-command (e.g. \alpha) and CH is the character (e.g. α). The list is made up of
-the arrows, greek letters (upper and lowercase), binary relations, relations and
+  "Extracted from ‘math-symbol-list-basic’.
+Arrows, greek letters (upper and lowercase), binary relations, relations and
 miscellaneous.")
 
 (defconst lambdapi--math-symbol-list-extended
@@ -237,16 +242,29 @@ miscellaneous.")
            (pred (lambda (sym) (string-match-p com-rx (cadr sym))))
            (filt (seq-filter pred math-symbol-list-extended)))
       (seq-map (lambda (sym) `(,(cadr sym) . ,(cdddr sym))) filt)))
-  "Formatted sublist of `math-symbol-list-extended'.
-An element of this list is a dotted pair (COM . CH) where com is the LaTeX
-command (e.g. \alpha) and CH is the character (e.g. α). This list is made of the
-double-struck capital letters.")
+  "Extracted from ‘math-symbol-list-extended’. Double struck capital letters.")
+
+(defconst lambdapi--math-symbol-list-subscripts
+  (eval-when-compile
+    (seq-map (lambda (sym)
+               (cons (cl-concatenate 'string "_" (cadr sym)) (cddr sym)))
+             math-symbol-list-subscripts))
+  "Extracted from ‘math-symbol-list-subscripts’.")
+
+(defconst lambdapi--math-symbol-list-superscripts
+  (eval-when-compile
+    (seq-map (lambda (sym)
+               (cons (cl-concatenate 'string "^" (cadr sym)) (cddr sym)))
+             math-symbol-list-superscripts))
+  "Extracted from ‘math-symbol-list-superscripts’.")
 
 (unless lambdapi-unicode-prefer-company
   (seq-do (lambda (com-ltx) (quail-defrule (car com-ltx) (cdr com-ltx)))
           (seq-concatenate 'list
                            lambdapi--math-symbol-list-basic
-                           lambdapi--math-symbol-list-extended)))
+                           lambdapi--math-symbol-list-extended
+                           lambdapi--math-symbol-list-subscripts
+                           lambdapi--math-symbol-list-superscripts)))
 
 (provide 'lambdapi-input)
 ;;; lambdapi-input.el ends here

editors/emacs/lambdapi-mode.el

@@ -109,6 +109,7 @@
    :forward-token #'lambdapi--smie-forward-token
    :backward-token #'lambdapi--smie-backward-token)
   ;; Reindent on colon
+  (electric-indent-mode -1) ; Disable electric indent by default
   (setq-local electric-indent-chars (append '(?↪ ?≔ ?:) electric-indent-chars))
 
   ;; Abbrev mode

editors/emacs/lambdapi-smie.el

@@ -27,34 +27,19 @@
           lambdapi--queries)
   "Commands at top level.")
 
-(defun lambdapi--previous-cmd ()
-  "Return the previous command used in the file."
-  (save-excursion
-    (while
-        (progn
-          (back-to-indentation)
-          (not (looking-at (regexp-opt lambdapi--cmds))))
-      (forward-line -1)))
-  (match-string 0))
-
-(defun lambdapi--colon-indent ()
-  "Indent before colon."
-  (let ((ppss (syntax-ppss)))
-    (when (and (= 0 (nth 0 ppss)) (smie-rule-bolp))
-      '(column 0)))) ; At beginning of line if not inside parentheses
-
 (defun lambdapi--query-indent ()
   "Indent commands that may be in proofs.
 Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
   (save-excursion
     (forward-line -1)
     (back-to-indentation)
     (cond
-     ;; Perhaps `(smie-rule-parent)' would be enough here
      ((looking-at-p (regexp-opt (cons "proof" lambdapi--tactics)))
       `(column . ,lambdapi-indent-basic))
      ((looking-at-p (regexp-opt lambdapi--queries))
-      (smie-rule-parent))
+      ;; If the previous line is a query, indent similarly
+      (back-to-indentation)
+      `(column . ,(current-column)))
      (t '(column . 0)))))
 
 (defconst lambdapi--smie-prec
@@ -81,57 +66,57 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
              ("let" ident ":" sterm "≔" sterm "in" sterm)
              ("let" args ":" sterm "≔" sterm "in" sterm)
              ("let" args "≔" sterm "in" sterm))
-      (tactic ("refine" sterm)
+      (tactic ("apply" sterm)
               ("assume" sterm)
-              ("apply" sterm)
-              ("simpl")
-              ("rewrite" "[" rw-patt "]")
-              ("reflexivity")
+              ("fail")
               ("focus" ident)
               ("print")
               ("proofterm")
-              ("why3")
-              ("fail"))
-      (query ("assert" sterm "≡" sterm)
-             ("assert" sterm ":" sterm)
+              ("refine" sterm)
+              ("reflexivity")
+              ("rewrite" "[" rw-patt "]")
+              ("simpl")
+              ("why3"))
+      (query ("assert" sterm ":" sterm)
+             ("assert" sterm "≡" sterm)
              ("assertnot" sterm ":" sterm)
              ("assertnot" sterm "≡" sterm)
              ("compute" sterm)
-             ("type" sterm)
-             ("set" "prover" ident) ; no stringlit because of conflict
-             ("set" "prover_timeout" ident)
-             ("set" "verbose" ident)
              ("set" "debug" ident)
+             ("set" "flag" ident "off")
              ("set" "flag" ident "on")
-             ("set" "flag" ident "off"))
+             ("set" "prover" ident)
+             ("set" "prover_timeout" ident)
+             ("set" "verbose" ident)
+             ("type" sterm))
       (prfcontent (tactic)
                   (query))
       (unif-rule-rhs (sterm "≡" sterm)
                      (unif-rule-rhs ";" sterm "≡" sterm))
       (symdec ("symbol" args ":" sterm))
-      (command ("injective" symdec)
-               ("constant" symdec)
-               ("private" symdec)
-               ("protected" symdec)
-               (symdec)
-               ("theorem" args ":" sterm)
-               ("proof" prfcontent "qed")
-               ("proof" prfcontent "admit")
-               ("proof" prfcontent "abort")
+      (command ("constant" symdec)
                ("definition" args "≔" sterm)
-               ("rule" sterm "↪" sterm)
-               ("with" sterm "↪" sterm)
-               ("require" ident)
+               ("injective" symdec)
                ("open" ident)
+               ("private" symdec)
+               ("proof" prfcontent "abort")
+               ("proof" prfcontent "admit")
+               ("proof" prfcontent "qed")
+               ("protected" symdec)
                ("require" ident "as" ident)
-               ("set" "unif_rule" sterm "≡" sterm "↪" unif-rule-rhs)
-               ("set" "builtin" ident "≔" ident)
-               ("set" "prefix" ident "≔" ident)
-               ("set" "infix" ident "≔" ident)
-               ("set" "infix" "left" ident "≔" ident)
-               ("set" "infix" "right" ident "≔" ident)
+               ("require" ident)
+               ("rule" sterm "↪" sterm)
+               ("set" "builtin" ident "≔" sterm)
+               ("set" "declared" ident)
+               ("set" "infix" "left" ident "≔" sterm)
+               ("set" "infix" "right" ident "≔" sterm)
+               ("set" "infix" ident "≔" sterm)
+               ("set" "prefix" ident "≔" sterm)
                ("set" "quantifier" ident)
-               ("set" "declared" ident)))
+               ("set" "unif_rule" sterm "≡" sterm "↪" unif-rule-rhs)
+               ("theorem" args ":" sterm)
+               ("with" sterm "↪" sterm)
+               (symdec)))
     '((assoc "≡") (assoc ",") (assoc "in") (assoc "→")))))
 
 (defun lambdapi--smie-forward-token ()
@@ -169,7 +154,10 @@ The default lexer is used because the syntax is primarily made of sexps."
     (`(:before . ,(or "set" "compute" "type" "assert" "assertnot"))
      (lambdapi--query-indent))
 
-    (`(,_ . ,(or "≔" "," "↪" "→" ":" "≡")) (smie-rule-separator kind))
+    (`(,_ . ,(or "," "↪" "→" "≡")) (smie-rule-separator kind))
+
+    (`(,(or :before :list-intro) . ,(or "≔" ":")) (smie-rule-separator kind))
+    (`(:after . ,(or "≔" ":")) lambdapi-indent-basic)
 
     (`(:list-intro . ,(or "with" "rule" "λ" "Π" "proof")) t)
     (`(:after . "proof") lambdapi-indent-basic)
@@ -178,7 +166,7 @@ The default lexer is used because the syntax is primarily made of sexps."
     (`(:after . ,(or "symbol" "definition" "theorem")) lambdapi-indent-basic)
     (`(:after . ,(or "simpl" "rewrite" "assume" "apply" "refine"
                      "why3" "reflexivity" "focus" "print" "fail"))
-      lambdapi-indent-basic)
+     lambdapi-indent-basic)
 
     ;; Toplevel
     (`(:before . "protected") '(column . 0))

editors/emacs/lambdapi-vars.el

@@ -20,8 +20,11 @@
 
 (defconst lambdapi-sig-commands
   '("definition"
+    "as"
     "in"
     "let"
+    "declared"
+    "builtin"
     "open"
     "proof"
     "qed"
@@ -46,7 +49,7 @@
 
 (defconst lambdapi-misc-keywords
   '("TYPE" "left" "right" "infix" "prefix" "quantifier"
-    "protected" "private" "injective" "constant" "as"))
+    "protected" "private" "injective" "constant"))
 
 (defcustom lambdapi-indent-basic 2
   "Basic indentation for lambdapi-mode."

editors/emacs/test.sh

@@ -0,0 +1,17 @@
+#!/bin/sh
+## Test the lambdapi-mode built from '*.el' files.
+## The script  downloads a  fresh and basic  configuration, creates  a temporary
+## directory and launches emacs in it. You  can create a new 'foo.lp' to try the
+## mode.
+##
+## Takes the version of the mode as first argument
+set -eu
+tmp="$(mktemp -d)"
+cp "dist/lambdapi-mode-$1.tar" "${tmp}"
+(cd "${tmp}" || exit 1
+ curl https://sanemacs.com/sanemacs.el > sanemacs.el
+ echo '(use-package eglot)' >> sanemacs.el
+ echo '(use-package math-symbol-lists)' >> sanemacs.el
+ emacs --quick -l sanemacs.el \
+     --eval "(package-install-file \"lambdapi-mode-$1.tar\")")
+rm -rf "${tmp}"